P. 7 of Theorem List - brismu bridi

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

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

Axiom	ax-plus-succ 601*	Addition with successor. A standard axiom of second-order arithmetic.
⊢ li su'i ku'i'a bai'ei ku'i'e du li bai'ei su'i ku'i'a ku'i'e

Theorem	1p0e1 602	1 + 0 = 1 (Contributed by la korvo, 30-Aug-2024.)
⊢ li su'i pa no du li pa

3.1.6 Addition II: {sumji}

Syntax	bsumji 603
selbri sumji

Definition	df-sumji 604*	Definition of {sumji} in terms of {su'i}.
⊢ go li ku'i'a sumji li ku'i'e ko'a gi li su'i ku'i'a ku'i'e du ko'a

Theorem	sumji-no 605	Every natural number is equal to zero plus itself. (Contributed by la korvo, 30-Aug-2024.)
⊢ li ku'i'a sumji li no li ku'i'a

Axiom	ax-sumji-succ 606	Addition on natural numbers is well-founded and proceeds by successors. This is Robinson axiom 5.
⊢ su'o da zo'u ge ko'i sumji ko'a da gi ko'e kacli'e da ⊢ su'o da zo'u ge da sumji ko'a ko'e gi da kacli'e ko'i

3.1.7 Multiplication I: {pi'i}

Syntax	mpihi 607*
PA pi'i ku'i'a ku'i'e

Axiom	ax-mul-zero 608	Multiplication with zero. A standard axiom of second-order arithmetic. Robinson's sixth axiom.
⊢ li pi'i ku'i'a no du li no

Axiom	ax-mul-succ 609*	Multiplication with successor. A standard axiom of second-order arithmetic.
⊢ li pi'i ku'i'a bai'ei ku'i'e du li su'i pi'i ku'i'a ku'i'e ku'i'a

3.1.8 Multiplication II: {pilji}

Syntax	bpilji 610
selbri pilji

Definition	df-pilji 611*	Definition of {pilji} in terms of {pi'i}.
⊢ go li ku'i'a pilji li ku'i'e ko'a gi li pi'i ku'i'a ku'i'e du ko'a

Theorem	pilji-no 612	Every natural number times zero is zero. (Contributed by la korvo, 30-Aug-2024.)
⊢ li ku'i'a pilji li no li no

Axiom	ax-pilji-succ 613	Multiplication on natural numbers is well-founded. This is Robinson axiom 7.
⊢ su'o da zo'u ge ko'i pilji ko'a da gi ko'e kacli'e da ⊢ su'o da zo'u ge ko'i sumji da ko'a gi da pilji ko'a ko'e

3.1.9 Comparison I: {kacme'a}

Syntax	bkacmeha 614
selbri kacme'a

Axiom	ax-gt-zero 615	Zero is not greater than any natural number. This is Robinson axiom 8.
⊢ naku ko'a kacme'a li no

Theorem	gt-zero-ref 616	Refutation of any natural number less than zero. (Contributed by la korvo, 21-Jun-2024.)
⊢ ko'a kacme'a li no ⊢ gai'o

Definition	df-kacmeha 617	Recursive definition of {kacme'a}. This is Robinson axiom 11.
⊢ go ko'a kacme'a ko'e gi su'o da poi ke'a kacli'e ko'a zo'u ga da kacme'a ko'e gi da du ko'e

3.2 Exponents I: {tenfa}

Syntax	sbtenfa 618
selbri tenfa

3.3 Logarithms: {dugri}

Syntax	sbdugri 619
selbri dugri

Definition	df-dugri 620	{dugri} is a permutation of {tenfa}.
⊢ go ko'a dugri ko'e ko'i gi ko'a te se tenfa ko'e ko'i

Theorem	dugrii 621	Inference form of df-dugri 620 (Contributed by la korvo, 9-Aug-2023.)
⊢ ko'a dugri ko'e ko'i ⊢ ko'a te se tenfa ko'e ko'i

Theorem	dugriri 622	Inference form of df-dugri 620 (Contributed by la korvo, 9-Aug-2023.)
⊢ ko'a te se tenfa ko'e ko'i ⊢ ko'a dugri ko'e ko'i

3.4 Cardinality

3.4.1 {ka'au}

Syntax	mkahau 623	Syntax for cardinality over arbitrary sumti.
PA ka'au ko'a

3.4.2 {kazmi}

Syntax	sbkazmi 624
selbri kazmi

Definition	df-kazmi 625	Definition of {kazmi} in terms of {ka'au}.
⊢ go ko'a kazmi ko'e gi ko'a du li ka'au ko'e

Axiom	ax-card-fun 626	Cardinality is a function on sets. An axiom of Fregean cardinality.
⊢ ganai ko'a .e ko'e kazmi ko'i gi ko'a du ko'e

Theorem	kazmi-funii 627	Inference form of ax-card-fun 626 (Contributed by la korvo, 31-Jul-2024.)
⊢ ko'a kazmi ko'i ⊢ ko'e kazmi ko'i ⊢ ko'a du ko'e

Axiom	ax-card-ex 628	A unary relation describes the empty set when it never holds. An axiom of Fregean cardinality.
⊢ go li no kazmi pa ka ce'u bo'a kei gi naku su'o da zo'u da bo'a

PART 4 MEREOLOGY Mereology is an alternative to set theory. Where set theory focuses on elementhood, using {cmima}, mereology focuses on parthood, using {pagbu}.

4.1 Parthood

4.1.1 {pagbu}

Syntax	sbpagbu 629
selbri pagbu

Axiom	ax-pagbu-refl 630	Parthood is reflexive.
⊢ ko'a pagbu ko'a

Theorem	pagbu-kinra 631	{pagbu} is reflexive over any domain. (Contributed by la korvo, 31-Aug-2024.)
⊢ pa ka ce'u pagbu ce'u kei kinra ko'e

Axiom	ax-pagbu-antisym 632	Parthood is antisymmetric.
⊢ ganai ge ko'a pagbu ko'e gi ko'e pagbu ko'a gi ko'a du ko'e

Theorem	pagbu-antisym 633	Inference form of ax-pagbu-antisym 632 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a pagbu ko'e ⊢ ko'e pagbu ko'a ⊢ ko'a du ko'e

Axiom	ax-pagbu-trans 634	Parthood is transitive.
⊢ ganai ge ko'a pagbu ko'e gi ko'e pagbu ko'i gi ko'a pagbu ko'i

Theorem	pagbu-trans 635	Inference form of ax-pagbu-trans 634 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a pagbu ko'e ⊢ ko'e pagbu ko'i ⊢ ko'a pagbu ko'i

Axiom	ax-pagbu-top 636	The universe exists.
⊢ su'o da zo'u ko'a pagbu da

Axiom	ax-pagbu-bot 637	The empty part exists.
⊢ su'o da zo'u da pagbu ko'a

4.1.2 {jompau}

Syntax	sbjompau 638
selbri jompau

Definition	df-jompau 639	Definition of {jompau} in terms of {pagbu}.
⊢ go ko'a jompau ko'e gi su'o da zo'u da pagbu ko'a .e ko'e

Theorem	jompaui 640	Inference form of df-jompau 639 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a jompau ko'e ⊢ su'o da zo'u da pagbu ko'a .e ko'e

Theorem	jompauri 641	Reverse inference form of df-jompau 639 (Contributed by la korvo, 4-Sep-2023.)
⊢ su'o da zo'u da pagbu ko'a .e ko'e ⊢ ko'a jompau ko'e

4.1.3 {kuzypau}

Syntax	sbkuzypau 642
selbri kuzypau

Definition	df-kuzypau 643	Definition of {kuzypau} in terms of {pagbu}.
⊢ go ko'a kuzypau ko'e gi su'o da zo'u ko'a .e ko'e pagbu da

Theorem	kuzypaui 644	Inference form of df-kuzypau 643 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a kuzypau ko'e ⊢ su'o da zo'u ko'a .e ko'e pagbu da

Theorem	kuzypauri 645	Reverse inference form of df-kuzypau 643 (Contributed by la korvo, 4-Sep-2023.)
⊢ su'o da zo'u ko'a .e ko'e pagbu da ⊢ ko'a kuzypau ko'e

PART 5 SPACE & SPACETIME

5.1 Two-dimensional Euclidean space

5.1.1 Compass directions

Syntax	sbberti 646
selbri berti

Syntax	sbsnanu 647
selbri snanu

Syntax	sbstici 648
selbri stici

Syntax	sbstuna 649
selbri stuna

Axiom	ax-berti-snanu 650	Northward and southward are opposite.
⊢ go ko'a berti ko'e ko'i gi ko'e snanu ko'a ko'i

Axiom	ax-stici-stuna 651	Westward and eastward are opposite.
⊢ go ko'a stici ko'e ko'i gi ko'e stuna ko'a ko'i

5.2 Three-dimensional Euclidean space

5.2.1 Spatial directions

Syntax	sbcrane 652
selbri crane

Syntax	sbtrixe 653
selbri trixe

Syntax	sbzunle 654
selbri zunle

Syntax	sbpritu 655
selbri pritu

Syntax	sbgapru 656
selbri gapru

Syntax	sbcnita 657
selbri cnita

Axiom	ax-crane-trixe 658	Forward and backward are opposite.
⊢ go ko'a crane ko'e ko'i gi ko'e trixe ko'a ko'i

Axiom	ax-zunle-pritu 659	Leftward and rightward are opposite.
⊢ go ko'a zunle ko'e ko'i gi ko'e pritu ko'a ko'i

Axiom	ax-gapru-cnita 660	Upward and downward are opposite.
⊢ go ko'a gapru ko'e ko'i gi ko'e cnita ko'a ko'i

5.3 Minkowski spacetime

5.3.1 Events: {cfabalvi}, {mulpru}

Syntax	sbcfabalvi 661
selbri cfabalvi

Syntax	sbmulpru 662
selbri mulpru

Definition	df-mulpru 663	Definition of {mulpru} as the dagger of {cfabalvi}.
⊢ go ko'a mulpru ko'e gi ko'e cfabalvi ko'a

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

5.3.2 Simultaneity: {cabna}

Syntax	sbcabna 665
selbri cabna

Syntax	sbmokca 666
selbri mokca

Definition	df-cabna 667	Definition of {cabna} in terms of {mokca}: two events are simultaneous when they have a moment in common.
⊢ go ko'a cabna ko'e gi su'o da zo'u da mokca ko'a .e ko'e

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

5.3.3 Non-aorist events: {balvi}, {purci}

Syntax	sbbalvi 669
selbri balvi

Syntax	sbpurci 670
selbri purci

Definition	df-balvi 671	Definition of non-aorist {balvi} in terms of aorist {cfabalvi} and {cabna}.
⊢ go ko'a balvi ko'e gi ko'a cfabalvi ja cabna ko'e

Definition	df-purci 672	Definition of non-aorist {purci} in terms of aorist {mulpru} and {cabna}.
⊢ go ko'a purci ko'e gi ko'a mulpru ja cabna ko'e

Axiom	ax-balvi-purci 673	{balvi} and {purci} are each other's daggers.
⊢ go ko'a balvi ko'e gi ko'e purci ko'a

5.3.4 Elsewhen: {xlane}

Syntax	sbxlane 674
selbri xlane

Definition	df-xlane 675	Proposed definition of {xlane} in terms of {balvi} and {purci}: two events are separated when they are neither in each other's past nor future.
⊢ go ko'a xlane ko'e gi naku zo'u ko'a balvi ja purci ko'e

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

PART 6 RELATIONAL LOGIC

6.1 Lattice of relations

6.1.1 {ki'irni'i}

Syntax	sbkihirnihi 677
selbri ki'irni'i

Definition	df-kihirnihi 678*	Definition of {ki'irni'i} in terms of {ckini} and {na.a}. Unlike prior definitions, this one does not require any terbri inspection.
⊢ go ko'a ki'irni'i ko'e gi ro da zo'u ro de zo'u da ckini de ko'a na.a ko'e

Theorem	kihirnihi-refl 679	{ki'irni'i} is reflexive. (Contributed by la korvo, 13-Aug-2024.)
⊢ ko'a ki'irni'i ko'a

Theorem	kihirnihi-kinra 680	{ki'irni'i} is reflexive over any domain. (Contributed by la korvo, 13-Aug-2024.)
⊢ pa ka ce'u ki'irni'i ce'u kei kinra ko'e

Axiom	ax-kihirnihi-trans 681	{ki'irni'i} is transitive.
⊢ ganai ge ko'a ki'irni'i ko'e gi ko'e ki'irni'i ko'i gi ko'a ki'irni'i ko'i

6.1.2 {ki'irdu'i}

Syntax	sbkihirduhi 682
selbri ki'irdu'i

Definition	df-kihirduhi 683*	Definition of {ki'irdu'i} in terms of {ckini} and {.o}.
⊢ go ko'a ki'irdu'i ko'e gi ro da zo'u ro de zo'u da ckini de ko'a .o ko'e

Theorem	kihirduhi-refl 684	{ki'irdu'i} is reflexive. (Contributed by la korvo, 15-Jul-2025.)
⊢ ko'a ki'irdu'i ko'a

Theorem	kihirnihi-antisym 685	{ki'irni'i} is antisymmetric, reducing to {ki'irdu'i}. (Contributed by la korvo, 15-Jul-2025.)
⊢ ko'a ki'irni'i ko'e ⊢ ko'e ki'irni'i ko'a ⊢ ko'a ki'irdu'i ko'e

6.1.3 {ki'irkanxe}

Syntax	sbkihirkanxe 686
selbri ki'irkanxe

Definition	df-kihirkanxe 687*	Definition of {ki'irkanxe}
⊢ pa ka ce'u bu'a je bu'e ce'u kei ki'irkanxe pa ka ce'u bu'a ce'u kei pa ka ce'u bu'e ce'u kei

6.1.4 {ki'irvlina}

Syntax	sbkihirvlina 688
selbri ki'irvlina

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

6.2 Complex numbers

6.2.1 Complex number predicate: {lujna'u}

Syntax	sblujnahu 690
selbri lujna'u

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

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

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

Axiom	ax-comp-suhi 694*	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 695*	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 696	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 697	One is not zero. One of Megill's axioms.
⊢ naku li pa du li no

6.2.2 Real number predicate: {mrena'u}

Syntax	sbmrenahu 698
selbri mrena'u

Axiom	ax-real-suhi 699*	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 700*	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

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

< Previous Next >