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

Theorem	nat-indi 601*	Inference form of ax-nat-ind 600 (Contributed by la korvo, 10-Aug-2023.)
⊢ ge li no bo'a gi ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a ⊢ ro da poi ke'a kacna'u ku'o zo'u da bo'a

Theorem	nat-indii 602*	Inference form of ax-nat-ind 600 (Contributed by la korvo, 10-Aug-2023.)
⊢ li no bo'a ⊢ ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a ⊢ ro da poi ke'a kacna'u ku'o zo'u da bo'a

Theorem	nat-ind-cur 603*	Curried form of ax-nat-ind 600 (Contributed by la korvo, 20-Aug-2023.)
⊢ ganai li no bo'a gi ganai ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a gi ro da poi ke'a kacna'u ku'o zo'u da bo'a

Axiom	ax-succ-std 604*	There are no non-standard natural numbers. This axiom upgrades our arithmetic from BA, "baby arithmetic", to Robinson's Q. This is Robinson axiom 3.
⊢ ro da poi ke'a kacna'u ku'o zo'u ga da du li no gi su'o de zo'u de kacli'e da

3.1.5 Addition I: {su'i}

Syntax	msuhi 605*
PA su'i ku'i'a ku'i'e

Axiom	ax-plus-zero 606	Addition with zero. A standard axiom of second-order arithmetic. Robinson's fourth axiom.
⊢ li su'i ku'i'a no du li ku'i'a

Axiom	ax-plus-succ 607*	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 608	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 609
selbri sumji

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

Theorem	sumji-no 611	Every natural number is equal to itself plus zero. This theorem is usually stated on the left, but we state it on the right to align with ax-plus-zero 606 (Contributed by la korvo, 30-Aug-2024.)
⊢ li ku'i'a sumji li ku'i'a li no

Axiom	ax-sumji-succ 612	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 613*
PA pi'i ku'i'a ku'i'e

Axiom	ax-mul-zero 614	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 615*	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 616
selbri pilji

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

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

Axiom	ax-pilji-succ 619	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 620
selbri kacme'a

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

Theorem	gt-zero-ref 622	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 623	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

Syntax	sbkacnalmau 624
selbri kacnalmau

Definition	df-kacnalmau 625	A less-than-or-equal relation.
⊢ go ko'a kacnalmau ko'e gi ga ko'a du ko'e gi ko'a kacme'a ko'e

3.2 Exponents I: {tenfa}

Syntax	sbtenfa 626
selbri tenfa

3.3 Logarithms: {dugri}

Syntax	sbdugri 627
selbri dugri

Definition	df-dugri 628	{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 629	Inference form of df-dugri 628 (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 630	Inference form of df-dugri 628 (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 631	Syntax for cardinality over arbitrary sumti.
PA ka'au ko'a

3.4.2 {kazmi}

Syntax	sbkazmi 632
selbri kazmi

Definition	df-kazmi 633	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 634	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 635	Inference form of ax-card-fun 634 (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 636	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 ku gi naku su'o da zo'u da bo'a

3.4.3 Primes: {dilcysle}, {dilcymu'o}

Syntax	sbdilcysle 637
selbri dilcysle

Syntax	sbdilcymuho 638
selbri dilcymu'o

Definition	df-dilcymuho 639	A relation between multiples and divisors.
⊢ go ko'a dilcymu'o ko'e gi ko'a pilji ko'e ko'i

Definition	df-dilcysle 640	The set of prime numbers.
⊢ go ko'a dilcysle gi go ko'a dilcymu'o ko'e gi ko'e du ko'a .a li pa

Theorem	bpos 641	Bertand's postulate. Chebyshev said it and we'll say it again. Theorem 98 of [Freek].
⊢ ganai li ku'i'a kacna'u gi su'o da poi ce'u dilcysle ku'o zo'u ge li ku'i'a kacme'a da gi da kacnalmau li pi'i re ku'i'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 642
selbri pagbu

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

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

Axiom	ax-pagbu-antisym 645	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 646	Inference form of ax-pagbu-antisym 645 (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 647	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 648	Inference form of ax-pagbu-trans 647 (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 649	The universe exists.
⊢ su'o da zo'u ko'a pagbu da

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

4.1.2 {jompau}

Syntax	sbjompau 651
selbri jompau

Definition	df-jompau 652	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 653	Inference form of df-jompau 652 (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 654	Reverse inference form of df-jompau 652 (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 655
selbri kuzypau

Definition	df-kuzypau 656	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 657	Inference form of df-kuzypau 656 (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 658	Reverse inference form of df-kuzypau 656 (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 659
selbri berti

Syntax	sbsnanu 660
selbri snanu

Syntax	sbstici 661
selbri stici

Syntax	sbstuna 662
selbri stuna

Axiom	ax-berti-snanu 663	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 664	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 665
selbri crane

Syntax	sbtrixe 666
selbri trixe

Syntax	sbzunle 667
selbri zunle

Syntax	sbpritu 668
selbri pritu

Syntax	sbgapru 669
selbri gapru

Syntax	sbcnita 670
selbri cnita

Axiom	ax-crane-trixe 671	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 672	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 673	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 674
selbri cfabalvi

Syntax	sbmulpru 675
selbri mulpru

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

Axiom	ax-cfabalvi-trans 677	{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 678
selbri cabna

Syntax	sbmokca 679
selbri mokca

Definition	df-cabna 680	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 681	{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 682
selbri balvi

Syntax	sbpurci 683
selbri purci

Definition	df-balvi 684	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 685	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 686	{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 687
selbri xlane

Definition	df-xlane 688	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 689	{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 690
selbri ki'irni'i

Definition	df-kihirnihi 691*	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 692	{ki'irni'i} is reflexive. (Contributed by la korvo, 13-Aug-2024.)
⊢ ko'a ki'irni'i ko'a

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

Axiom	ax-kihirnihi-trans 694	{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 695
selbri ki'irdu'i

Definition	df-kihirduhi 696*	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 697	{ki'irdu'i} is reflexive. (Contributed by la korvo, 15-Jul-2025.)
⊢ ko'a ki'irdu'i ko'a

Theorem	kihirnihi-antisym 698	{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 699
selbri ki'irkanxe

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

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