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.1.4 {ki'irvlina}

Syntax	sbkihirvlina 701
selbri ki'irvlina

Definition	df-kihirvlina 702*	Definition of {ki'irvlina}
⊢ pa ka ce'u bu'a ja bu'e ce'u ku ki'irvlina pa ka ce'u bu'a ce'u ku pa ka ce'u bu'e ce'u ku

6.2 Fractions

6.2.1 Rational number predicate: {frinyna'u}

Syntax	pfr 703*	Syntax for fractions.
PA ku'i'a fi'u ku'i'e

Syntax	sbfrinynahu 704
selbri frinyna'u

Syntax	sbfrinyduhi 705
selbri frinydu'i

Definition	df-frinynahu 706*	Definition of equivalence classes of the field of fractions of natural numbers.
⊢ go li ku'i'a fi'u ku'i'e frinyna'u li ku'i'a li ku'i'e gi ge ge li ku'i'a kacna'u gi li ku'i'e kacna'u gi naku li ku'i'e du li no

Theorem	frinynahu-kacnahul 707*	Numerators of fractions are natural numbers. (Contributed by la korvo, 11-Aug-2026.)
⊢ li ku'i'a fi'u ku'i'e frinyna'u li ku'i'a li ku'i'e ⊢ li ku'i'a kacna'u

Theorem	frinynahu-kacnahur 708*	Denominators of fractions are natural numbers. (Contributed by la korvo, 11-Aug-2026.)
⊢ li ku'i'a fi'u ku'i'e frinyna'u li ku'i'a li ku'i'e ⊢ li ku'i'e kacna'u

Definition	df-frinyduhi 709	Definition of equivalence of fractions.
⊢ go ko'a frinydu'i ko'e gi ge ge ko'a frinyna'u fo'a fo'e gi ko'e frinyna'u fo'i fo'o gi su'o da zo'u da pilji fo'a fo'o gi'e pilji fo'e fo'i

Theorem	frinyduhi-refl 710	Fractions are equivalent to themselves.
⊢ ko'a frinyna'u ko'e ko'i ⊢ ko'a frinydu'i ko'a

6.2.2 Square roots: {fe'a}

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

Definition	df-feha 712
⊢ go ko'a du li fe'a ku'i'a gi ko'a pilji li ku'i'a li ku'i'a

Theorem	feha2irr 713	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 714
selbri lujna'u

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

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

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

Axiom	ax-comp-suhi 718*	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 719*	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 720	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 721	One is not zero. One of Megill's axioms.
⊢ naku li pa du li no

6.3.2 Norm: {cu'a}

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

Definition	df-cuha 723	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 724*	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 725
selbri mrena'u

Axiom	ax-real-suhi 726*	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 727*	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 728
selbri fancu

Definition	df-fancu 729*	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 730*	Inference form of df-fancu 729 (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 731*	Inference form of df-fancu 729 (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 732
selbri pagyfancu

Definition	df-pagyfancu 733*	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 734
selbri mapti

Definition	df-mapti 735	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 736	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 737
selbri drata

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

6.5.3 {frica}

Syntax	sbfrica 739
selbri frica

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

6.5.4 {nenri}

Syntax	sbnenri 741
selbri nenri

Axiom	ax-nenri-trans 742	{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 743
selbri fatne

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

6.5.6 {rinka}

Syntax	sbrinka 745
selbri rinka

Axiom	ax-rinka-balvi 746	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 747
selbri skari

Axiom	ax-skari-ckaji 748	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 749	All {skaselbri} are {selbri}.
skaselbri bu'a selbri bu'a

Definition	df-skaselbri 750*	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 751*	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 752
selbri lanzu

Syntax	sblazmihu 753
selbri lazmi'u

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

Definition	df-lazmihu 755	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 756	### Generated baseline ontology ###
selbri bakni

Syntax	sbbambu 757
selbri bambu

Syntax	sbbanfi 758
selbri banfi

Syntax	sbbifce 759
selbri bifce

Syntax	sbcindu 760
selbri cindu

Syntax	sbcinfo 761
selbri cinfo

Syntax	sbcinki 762
selbri cinki

Syntax	sbcipni 763
selbri cipni

Syntax	sbcivla 764
selbri civla

Syntax	sbckunu 765
selbri ckunu

Syntax	sbcribe 766
selbri cribe

Syntax	sbcurnu 767
selbri curnu

Syntax	sbdanlu 768
selbri danlu

Syntax	sbdatka 769
selbri datka

Syntax	sbfinpe 770
selbri finpe

Syntax	sbgerku 771
selbri gerku

Syntax	sbgumri 772
selbri gumri

Syntax	sbgunse 773
selbri gunse

Syntax	sbjalra 774
selbri jalra

Syntax	sbjipci 775
selbri jipci

Syntax	sbjukni 776
selbri jukni

Syntax	sbkanba 777
selbri kanba

Syntax	sbkuhurkupresu 778
selbri ku'urkupresu

Syntax	sbkumte 779
selbri kumte

Syntax	sblabno 780
selbri labno

Syntax	sblanme 781
selbri lanme

Syntax	sblelxe 782
selbri lelxe

Syntax	sblorxu 783
selbri lorxu

Syntax	sbmabru 784
selbri mabru

Syntax	sbmanti 785
selbri manti

Syntax	sbmarna 786
selbri marna

Syntax	sbmirli 787
selbri mirli

Syntax	sbmlatu 788
selbri mlatu

Syntax	sbmledi 789
selbri mledi

Syntax	sbnimre 790
selbri nimre

Syntax	sbpoplu 791
selbri poplu

Syntax	sbractu 792
selbri ractu

Syntax	sbratcu 793
selbri ratcu

Syntax	sbremna 794
selbri remna

Syntax	sbrespa 795
selbri respa

Syntax	sbrozgu 796
selbri rozgu

Syntax	sbsfani 797
selbri sfani

Syntax	sbsince 798
selbri since

Syntax	sbsluni 799
selbri sluni

Syntax	sbsmacu 800
selbri smacu

< 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-1080

< Previous Next >