P. 8 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 8 of 11)	< Previous Next >
		Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List

**Theorem List for brismu bridi -** 701-800 *Has distinct variable group(s)
Type	Label	Description
Statement

6.2.2 Square roots: {fe'a}

Syntax	pf 701	Syntax for square roots.
PA fe'a ku'i'a

Definition	df-feha 702
⊢ go li fe'a ku'i'a du ko'a gi li ku'i'a li ku'i'a sumji ko'a

Theorem	feha2irr 703	The square root of two is not rational. Theorem 1 of [Freek].
⊢ naku li fe'a re frinyna'u ko'a ko'e

6.3 Complex numbers

6.3.1 Complex number predicate: {lujna'u}

Syntax	sblujnahu 704
selbri lujna'u

Syntax	pc 705*	Syntax for complex numbers. (Contributed by la korvo, 3-Jan-2025.)
PA ku'i'a ka'o ku'i'e

Axiom	ax-comp-pa 706	One is a complex number. One of Megill's axioms.
⊢ li pa ka'o no lujna'u

Axiom	ax-comp-kaho 707	The imaginary unit is a complex number. One of Megill's axioms.
⊢ li no ka'o pa lujna'u

Axiom	ax-comp-suhi 708*	Complex numbers are closed under addition. One of Megill's axioms.
⊢ ganai li ku'i'a .e li ku'i'e lujna'u gi li su'i ku'i'a ku'i'e lujna'u

Axiom	ax-comp-pihi 709*	Complex numbers are closed under multiplication. One of Megill's axioms.
⊢ ganai li ku'i'a .e li ku'i'e lujna'u gi li pi'i ku'i'a ku'i'e lujna'u

Axiom	ax-comp-i2m1 710	The imaginary unit is a square root of negative one. One of Megill's axioms.
⊢ li su'i pi'i no ka'o pa no ka'o pa pa du li no

Axiom	ax-comp-1ne0 711	One is not zero. One of Megill's axioms.
⊢ naku li pa du li no

6.3.2 Norm: {cu'a}

Syntax	pcn 712
PA cu'a ku'i'a

Definition	df-cuha 713	The norm or absolute value of a number. This generic definition operates over any multiplicative structure.
⊢ li cu'a ku'i'a du li fe'a pi'i ku'i'a ku'i'a

Theorem	cuhatri 714*	Norms in the complex plane have a triangle inequality. Theorem 91 of [Freek].
⊢ ganai li ku'i'a .e li ku'i'e lujna'u gi li cu'a su'i ku'i'a ku'i'e kacnalmau li su'i cu'a ku'i'a cu'a ku'i'e

6.3.3 Real number predicate: {mrena'u}

Syntax	sbmrenahu 715
selbri mrena'u

Axiom	ax-real-suhi 716*	Real numbers are closed under addition. One of Megill's axioms.
⊢ ganai li ku'i'a .e li ku'i'e mrena'u gi li su'i ku'i'a ku'i'e mrena'u

Axiom	ax-real-pihi 717*	Real numbers are closed under multiplication. One of Megill's axioms.
⊢ ganai li ku'i'a .e li ku'i'e mrena'u gi li pi'i ku'i'a ku'i'e mrena'u

6.4 Functions I

6.4.1 {fancu}

Syntax	sbfancu 718
selbri fancu

Definition	df-fancu 719*	Definition of {fancu}. Note that the name of the function is neither unique nor concrete.
⊢ go ko'a fancu ko'e ko'i ko'o gi ro da poi ke'a cmima ko'e ku'o zo'u pa de zo'u ge de cmima ko'i gi da ckini de ko'o

Theorem	fancui 720*	Inference form of df-fancu 719 (Contributed by la korvo, 12-Aug-2024.)
⊢ ko'a fancu ko'e ko'i ko'o ⊢ ro da poi ke'a cmima ko'e ku'o zo'u pa de zo'u ge de cmima ko'i gi da ckini de ko'o

Theorem	fancuii 721*	Inference form of df-fancu 719 (Contributed by la korvo, 12-Aug-2024.)
⊢ ko'a fancu ko'e ko'i ko'o ⊢ de cmima ko'e ⊢ pa da zo'u ge da cmima ko'i gi de ckini da ko'o

6.4.2 {pagyfancu}

Syntax	sbpagyfancu 722
selbri pagyfancu

Definition	df-pagyfancu 723*	Definition of {pagyfancu} in terms of {ki'irni'i}.
⊢ go su'o da zo'u su'o de zo'u su'o di zo'u da pagyfancu de di pa ka ce'u bu'a ce'u ku gi pa ka su'o da zo'u ce'u .e ce'u bu'a da ku ki'irni'i pa ka ce'u du ce'u ku

6.5 Assorted claims

6.5.1 {mapti}

Syntax	sbmapti 724
selbri mapti

Definition	df-mapti 725	Proposed definition of {mapti} as a witness to an inhabited bijection.
⊢ go ko'a mapti ko'e ko'i gi ge ko'a ckini ko'e ko'i gi ge ro da zo'u ganai da ckini ko'e ko'i gi da du ko'a gi ro da zo'u ganai ko'a ckini da ko'i gi da du ko'e

Theorem	mapti-ckini 726	Under postulated definitions of la xorxes and la korvo, {mapti} is a subrelation of {ckini}. (Contributed by la korvo, 22-Aug-2024.)
⊢ ganai ko'a mapti ko'e ko'i gi ko'a ckini ko'e ko'i

6.5.2 {drata}

Syntax	sbdrata 727
selbri drata

Axiom	ax-drata-irrefl 728	{drata} is irreflexive.
⊢ naku ko'a drata ko'a ko'e

6.5.3 {frica}

Syntax	sbfrica 729
selbri frica

Axiom	ax-frica-irrefl 730	{frica} is irreflexive.
⊢ naku ko'a frica ko'a ko'e

6.5.4 {nenri}

Syntax	sbnenri 731
selbri nenri

Axiom	ax-nenri-trans 732	{nenri} is transitive.
⊢ ganai ge ko'a nenri ko'e gi ko'e nenri ko'i gi ko'a nenri ko'i

6.5.5 {fatne}

Syntax	sbfatne 733
selbri fatne

Axiom	ax-fatne-sym 734	{fatne} is symmetric.
⊢ go ko'a fatne ko'e gi ko'e fatne ko'a

6.5.6 {rinka}

Syntax	sbrinka 735
selbri rinka

Axiom	ax-rinka-balvi 736	Physical causation implies spatiotemporal causation.
⊢ ganai ko'a rinka ko'e ko'i gi ko'a balvi ko'e

6.6 Ontological classes

6.6.1 Colors: {skari} The schema for colors classifies one type, the colors ({skaselbri}).

Syntax	sbskari 737
selbri skari

Axiom	ax-skari-ckaji 738	Colors are extensionally defined in terms of {skari}.
⊢ ganai ko'a skari ko'e ko'i ko'o gi ko'a ckaji ko'e

Syntax	sbska 739	All {skaselbri} are {selbri}.
skaselbri bu'a selbri bu'a

Definition	df-skaselbri 740*	To be colored is to appear colored in a certain context.
skaselbri bu'a ⊢ go ko'a bu'a gi su'o da zo'u su'o de zo'u ko'a skari pa ka ce'u bu'a ku da de

Axiom	ax-xinmo2-skari2 741*	Definitionally, xinmo2 is drawn from skari2.
⊢ ganai ko'a se xinmo ko'e gi su'o da zo'u su'o de zo'u su'o di zo'u ko'a se skari da de di

6.6.2 Families: {lanzu}

Syntax	sblanzu 742
selbri lanzu

Syntax	sblazmihu 743
selbri lazmi'u

Axiom	ax-lanzu-cmima 744	{lanzu} is a subrelation of {cmima} as implied by df-lazmihu 745 and baseline notes.
⊢ ganai ko'a lanzu ko'e ko'i gi ko'e cmima ko'a

Definition	df-lazmihu 745	Definition of {lazmi'u} in terms of {lanzu} and {cmima} from the baseline notes.
⊢ go ko'a lazmi'u ko'e gi su'o da poi ke'a lanzu ku'o zo'u ko'a mintu ko'e pa ka ce'u cmima da ku

6.7 Generated baseline ontology

Syntax	sbbakni 746	### Generated baseline ontology ###
selbri bakni

Syntax	sbbambu 747
selbri bambu

Syntax	sbbanfi 748
selbri banfi

Syntax	sbbifce 749
selbri bifce

Syntax	sbcindu 750
selbri cindu

Syntax	sbcinfo 751
selbri cinfo

Syntax	sbcinki 752
selbri cinki

Syntax	sbcipni 753
selbri cipni

Syntax	sbcivla 754
selbri civla

Syntax	sbckunu 755
selbri ckunu

Syntax	sbcribe 756
selbri cribe

Syntax	sbcurnu 757
selbri curnu

Syntax	sbdanlu 758
selbri danlu

Syntax	sbdatka 759
selbri datka

Syntax	sbfinpe 760
selbri finpe

Syntax	sbgerku 761
selbri gerku

Syntax	sbgumri 762
selbri gumri

Syntax	sbgunse 763
selbri gunse

Syntax	sbjalra 764
selbri jalra

Syntax	sbjipci 765
selbri jipci

Syntax	sbjukni 766
selbri jukni

Syntax	sbkanba 767
selbri kanba

Syntax	sbkuhurkupresu 768
selbri ku'urkupresu

Syntax	sbkumte 769
selbri kumte

Syntax	sblabno 770
selbri labno

Syntax	sblanme 771
selbri lanme

Syntax	sblelxe 772
selbri lelxe

Syntax	sblorxu 773
selbri lorxu

Syntax	sbmabru 774
selbri mabru

Syntax	sbmanti 775
selbri manti

Syntax	sbmarna 776
selbri marna

Syntax	sbmirli 777
selbri mirli

Syntax	sbmlatu 778
selbri mlatu

Syntax	sbmledi 779
selbri mledi

Syntax	sbnimre 780
selbri nimre

Syntax	sbpoplu 781
selbri poplu

Syntax	sbractu 782
selbri ractu

Syntax	sbratcu 783
selbri ratcu

Syntax	sbremna 784
selbri remna

Syntax	sbrespa 785
selbri respa

Syntax	sbrozgu 786
selbri rozgu

Syntax	sbsfani 787
selbri sfani

Syntax	sbsince 788
selbri since

Syntax	sbsluni 789
selbri sluni

Syntax	sbsmacu 790
selbri smacu

Syntax	sbsmani 791
selbri smani

Syntax	sbspati 792
selbri spati

Syntax	sbsrasu 793
selbri srasu

Syntax	sbtirxu 794
selbri tirxu

Syntax	sbtoldi 795
selbri toldi

Syntax	sbtujli 796
selbri tujli

Syntax	sbxanto 797
selbri xanto

Syntax	sbxarju 798
selbri xarju

Syntax	sbxasli 799
selbri xasli

Syntax	sbxirma 800
selbri xirma

< Previous Next >

Page List Jump to page: Contents 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1070

< Previous Next >