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

Syntax	sbkacnalmau 618
selbri kacnalmau

Definition	df-kacnalmau 619	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 620
selbri tenfa

3.3 Logarithms: {dugri}

Syntax	sbdugri 621
selbri dugri

Definition	df-dugri 622	{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 623	Inference form of df-dugri 622 (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 624	Inference form of df-dugri 622 (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 625	Syntax for cardinality over arbitrary sumti.
PA ka'au ko'a

3.4.2 {kazmi}

Syntax	sbkazmi 626
selbri kazmi

Definition	df-kazmi 627	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 628	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 629	Inference form of ax-card-fun 628 (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 630	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 631
selbri dilcysle

Syntax	sbdilcymuho 632
selbri dilcymu'o

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

Definition	df-dilcysle 634	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 635	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 636
selbri pagbu

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

Theorem	pagbu-kinra 638	{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 639	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 640	Inference form of ax-pagbu-antisym 639 (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 641	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 642	Inference form of ax-pagbu-trans 641 (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 643	The universe exists.
⊢ su'o da zo'u ko'a pagbu da

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

4.1.2 {jompau}

Syntax	sbjompau 645
selbri jompau

Definition	df-jompau 646	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 647	Inference form of df-jompau 646 (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 648	Reverse inference form of df-jompau 646 (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 649
selbri kuzypau

Definition	df-kuzypau 650	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 651	Inference form of df-kuzypau 650 (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 652	Reverse inference form of df-kuzypau 650 (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 653
selbri berti

Syntax	sbsnanu 654
selbri snanu

Syntax	sbstici 655
selbri stici

Syntax	sbstuna 656
selbri stuna

Axiom	ax-berti-snanu 657	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 658	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 659
selbri crane

Syntax	sbtrixe 660
selbri trixe

Syntax	sbzunle 661
selbri zunle

Syntax	sbpritu 662
selbri pritu

Syntax	sbgapru 663
selbri gapru

Syntax	sbcnita 664
selbri cnita

Axiom	ax-crane-trixe 665	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 666	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 667	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 668
selbri cfabalvi

Syntax	sbmulpru 669
selbri mulpru

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

Axiom	ax-cfabalvi-trans 671	{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 672
selbri cabna

Syntax	sbmokca 673
selbri mokca

Definition	df-cabna 674	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 675	{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 676
selbri balvi

Syntax	sbpurci 677
selbri purci

Definition	df-balvi 678	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 679	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 680	{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 681
selbri xlane

Definition	df-xlane 682	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 683	{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 684
selbri ki'irni'i

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

Theorem	kihirnihi-kinra 687	{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 688	{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 689
selbri ki'irdu'i

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

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

Definition	df-kihirkanxe 694*	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

6.1.4 {ki'irvlina}

Syntax	sbkihirvlina 695
selbri ki'irvlina

Definition	df-kihirvlina 696*	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	sbfrinynahu 697
selbri frinyna'u

Syntax	sbfrinyduhi 698
selbri frinydu'i

Definition	df-frinynahu 699*	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

Definition	df-frinyduhi 700	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 ge fo'a pilji fo'o fo'u gi fo'e pilji fo'i fo'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-1070

< Previous Next >