![]() |
Metamath
Proof Explorer Theorem List (p. 416 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | decpmulnc 41501 | Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11669. (Contributed by Steven Nguyen, 9-Dec-2022.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ π· β β0 & β’ (π΄ Β· πΆ) = πΈ & β’ ((π΄ Β· π·) + (π΅ Β· πΆ)) = πΉ & β’ (π΅ Β· π·) = πΊ β β’ (;π΄π΅ Β· ;πΆπ·) = ;;πΈπΉπΊ | ||
Theorem | decpmul 41502 | Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ π· β β0 & β’ (π΄ Β· πΆ) = πΈ & β’ ((π΄ Β· π·) + (π΅ Β· πΆ)) = πΉ & β’ (π΅ Β· π·) = ;πΊπ» & β’ (;πΈπΊ + πΉ) = πΌ & β’ πΊ β β0 & β’ π» β β0 β β’ (;π΄π΅ Β· ;πΆπ·) = ;πΌπ» | ||
Theorem | sqdeccom12 41503 | The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.) |
β’ π΄ β β0 & β’ π΅ β β0 β β’ ((;π΄π΅ Β· ;π΄π΅) β (;π΅π΄ Β· ;π΅π΄)) = (;99 Β· ((π΄ Β· π΄) β (π΅ Β· π΅))) | ||
Theorem | sq3deccom12 41504 | Variant of sqdeccom12 41503 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ (π΄ + πΆ) = π· β β’ ((;;π΄π΅πΆ Β· ;;π΄π΅πΆ) β (;π·π΅ Β· ;π·π΅)) = (;99 Β· ((;π΄π΅ Β· ;π΄π΅) β (πΆ Β· πΆ))) | ||
Theorem | 4t5e20 41505 | 4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.) |
β’ (4 Β· 5) = ;20 | ||
Theorem | sq9 41506 | The square of 9 is 81. (Contributed by SN, 30-Mar-2025.) |
β’ (9β2) = ;81 | ||
Theorem | 235t711 41507 |
Calculate a product by long multiplication as a base comparison with other
multiplication algorithms.
Conveniently, 711 has two ones which greatly simplifies calculations like 235 Β· 1. There isn't a higher level mulcomli 11227 saving the lower level uses of mulcomli 11227 within 235 Β· 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12790 are added then this proof would benefit more than ex-decpmul 41508. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 12351 or 8t7e56 12801. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) |
β’ (;;235 Β· ;;711) = ;;;;;167085 | ||
Theorem | ex-decpmul 41508 | Example usage of decpmul 41502. This proof is significantly longer than 235t711 41507. There is more unnecessary carrying compared to 235t711 41507. Although saving 5 visual steps, using mulcomli 11227 early on increases the compressed proof length. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (;;235 Β· ;;711) = ;;;;;167085 | ||
Theorem | fz1sumconst 41509* | The sum of π constant terms (π is not free in πΆ). (Contributed by SN, 21-Mar-2025.) |
β’ (π β π β β0) & β’ (π β πΆ β β) β β’ (π β Ξ£π β (1...π)πΆ = (π Β· πΆ)) | ||
Theorem | fz1sump1 41510* | Add one more term to a sum. Special case of fsump1 15706 generalized to π β β0. (Contributed by SN, 22-Mar-2025.) |
β’ (π β π β β0) & β’ ((π β§ π β (1...(π + 1))) β π΄ β β) & β’ (π = (π + 1) β π΄ = π΅) β β’ (π β Ξ£π β (1...(π + 1))π΄ = (Ξ£π β (1...π)π΄ + π΅)) | ||
Theorem | oddnumth 41511* | The Odd Number Theorem. The sum of the first π odd numbers is πβ2. A corollary of arisum 15810. (Contributed by SN, 21-Mar-2025.) |
β’ (π β β0 β Ξ£π β (1...π)((2 Β· π) β 1) = (πβ2)) | ||
Theorem | nicomachus 41512* | Nicomachus's Theorem. The sum of the odd numbers from πβ2 β π + 1 to πβ2 + π β 1 is πβ3. Proof 2 from https://proofwiki.org/wiki/Nicomachus%27s_Theorem. (Contributed by SN, 21-Mar-2025.) |
β’ (π β β0 β Ξ£π β (1...π)(((πβ2) β π) + ((2 Β· π) β 1)) = (πβ3)) | ||
Theorem | sumcubes 41513* | The sum of the first π perfect cubes is the sum of the first π nonnegative integers, squared. This is the Proof by Nicomachus from https://proofwiki.org/wiki/Sum_of_Sequence_of_Cubes using induction and index shifting to collect all the odd numbers. (Contributed by SN, 22-Mar-2025.) |
β’ (π β β0 β Ξ£π β (1...π)(πβ3) = (Ξ£π β (1...π)πβ2)) | ||
Theorem | oexpreposd 41514 | Lemma for dffltz 41678. TODO-SN?: This can be used to show exp11d 41518 holds for all integers when the exponent is odd. The more standard Β¬ 2 β₯ π should be used. (Contributed by SN, 4-Mar-2023.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β Β¬ (π / 2) β β) β β’ (π β (0 < π β 0 < (πβπ))) | ||
Theorem | ltexp1d 41515 | ltmul1d 13061 for exponentiation of positive reals. (Contributed by Steven Nguyen, 22-Aug-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β) β β’ (π β (π΄ < π΅ β (π΄βπ) < (π΅βπ))) | ||
Theorem | ltexp1dd 41516 | Raising both sides of 'less than' to the same positive integer preserves ordering. (Contributed by Steven Nguyen, 24-Aug-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β) & β’ (π β π΄ < π΅) β β’ (π β (π΄βπ) < (π΅βπ)) | ||
Theorem | exp11nnd 41517 | sq11d 14225 for positive real bases and positive integer exponents. The base cannot be generalized much further, since if π is even then we have π΄βπ = -π΄βπ. (Contributed by SN, 14-Sep-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β) & β’ (π β (π΄βπ) = (π΅βπ)) β β’ (π β π΄ = π΅) | ||
Theorem | exp11d 41518 | exp11nnd 41517 for nonzero integer exponents. (Contributed by SN, 14-Sep-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β€) & β’ (π β π β 0) & β’ (π β (π΄βπ) = (π΅βπ)) β β’ (π β π΄ = π΅) | ||
Theorem | 0dvds0 41519 | 0 divides 0. (Contributed by SN, 15-Sep-2024.) |
β’ 0 β₯ 0 | ||
Theorem | absdvdsabsb 41520 | Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (absβπ) β₯ (absβπ))) | ||
Theorem | dvdsexpim 41521 | dvdssqim 16500 generalized to nonnegative exponents. (Contributed by Steven Nguyen, 2-Apr-2023.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β0) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | gcdnn0id 41522 | The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.) |
β’ (π β β0 β (π gcd π) = π) | ||
Theorem | gcdle1d 41523 | The greatest common divisor of a positive integer and another integer is less than or equal to the positive integer. (Contributed by SN, 25-Aug-2024.) |
β’ (π β π β β) & β’ (π β π β β€) β β’ (π β (π gcd π) β€ π) | ||
Theorem | gcdle2d 41524 | The greatest common divisor of a positive integer and another integer is less than or equal to the positive integer. (Contributed by SN, 25-Aug-2024.) |
β’ (π β π β β€) & β’ (π β π β β) β β’ (π β (π gcd π) β€ π) | ||
Theorem | dvdsexpad 41525 | Deduction associated with dvdsexpim 41521. (Contributed by SN, 21-Aug-2024.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β π β β0) & β’ (π β π΄ β₯ π΅) β β’ (π β (π΄βπ) β₯ (π΅βπ)) | ||
Theorem | nn0rppwr 41526 | If π΄ and π΅ are relatively prime, then so are π΄βπ and π΅βπ. rppwr 16505 extended to nonnegative integers. Less general than rpexp12i 16665. (Contributed by Steven Nguyen, 4-Apr-2023.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ π β β0) β ((π΄ gcd π΅) = 1 β ((π΄βπ) gcd (π΅βπ)) = 1)) | ||
Theorem | expgcd 41527 | Exponentiation distributes over GCD. sqgcd 16506 extended to nonnegative exponents. (Contributed by Steven Nguyen, 4-Apr-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β ((π΄ gcd π΅)βπ) = ((π΄βπ) gcd (π΅βπ))) | ||
Theorem | nn0expgcd 41528 | Exponentiation distributes over GCD. nn0gcdsq 16692 extended to nonnegative exponents. expgcd 41527 extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ π β β0) β ((π΄ gcd π΅)βπ) = ((π΄βπ) gcd (π΅βπ))) | ||
Theorem | zexpgcd 41529 | Exponentiation distributes over GCD. zgcdsq 16693 extended to nonnegative exponents. nn0expgcd 41528 extended to integer bases by symmetry. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β0) β ((π΄ gcd π΅)βπ) = ((π΄βπ) gcd (π΅βπ))) | ||
Theorem | numdenexp 41530 | numdensq 16694 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β β§ π β β0) β ((numerβ(π΄βπ)) = ((numerβπ΄)βπ) β§ (denomβ(π΄βπ)) = ((denomβπ΄)βπ))) | ||
Theorem | numexp 41531 | numsq 16695 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β β§ π β β0) β (numerβ(π΄βπ)) = ((numerβπ΄)βπ)) | ||
Theorem | denexp 41532 | densq 16696 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β β§ π β β0) β (denomβ(π΄βπ)) = ((denomβπ΄)βπ)) | ||
Theorem | dvdsexpnn 41533 | dvdssqlem 16507 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | dvdsexpnn0 41534 | dvdsexpnn 41533 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ π β β) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | dvdsexpb 41535 | dvdssq 16508 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | posqsqznn 41536 | When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16698 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.) |
β’ (π β (π΄β2) β β€) & β’ (π β π΄ β β) & β’ (π β 0 < π΄) β β’ (π β π΄ β β) | ||
Theorem | zrtelqelz 41537 | zsqrtelqelz 16698 generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023.) |
β’ ((π΄ β β€ β§ π β β β§ (π΄βπ(1 / π)) β β) β (π΄βπ(1 / π)) β β€) | ||
Theorem | zrtdvds 41538 | A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023.) |
β’ ((π΄ β β€ β§ π β β β§ (π΄βπ(1 / π)) β β) β (π΄βπ(1 / π)) β₯ π΄) | ||
Theorem | rtprmirr 41539 | The root of a prime number is irrational. (Contributed by Steven Nguyen, 6-Apr-2023.) |
β’ ((π β β β§ π β (β€β₯β2)) β (πβπ(1 / π)) β (β β β)) | ||
Syntax | cresub 41540 | Real number subtraction. |
class ββ | ||
Definition | df-resub 41541* | Define subtraction between real numbers. This operator saves a few axioms over df-sub 11450 in certain situations. Theorem resubval 41542 shows its value, resubadd 41554 relates it to addition, and rersubcl 41553 proves its closure. It is the restriction of df-sub 11450 to the reals: subresre 41605. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ββ = (π₯ β β, π¦ β β β¦ (β©π§ β β (π¦ + π§) = π₯)) | ||
Theorem | resubval 41542* | Value of real subtraction, which is the (unique) real π₯ such that π΅ + π₯ = π΄. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) = (β©π₯ β β (π΅ + π₯) = π΄)) | ||
Theorem | renegeulemv 41543* | Lemma for renegeu 41545 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ (π β π΅ β β) & β’ (π β βπ¦ β β (π΅ + π¦) = π΄) β β’ (π β β!π₯ β β (π΅ + π₯) = π΄) | ||
Theorem | renegeulem 41544* | Lemma for renegeu 41545 and similar. Remove a change in bound variables from renegeulemv 41543. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ (π β π΅ β β) & β’ (π β βπ¦ β β (π΅ + π¦) = π΄) β β’ (π β β!π¦ β β (π΅ + π¦) = π΄) | ||
Theorem | renegeu 41545* | Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β β!π₯ β β (π΄ + π₯) = 0) | ||
Theorem | rernegcl 41546 | Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β (0 ββ π΄) β β) | ||
Theorem | renegadd 41547 | Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((0 ββ π΄) = π΅ β (π΄ + π΅) = 0)) | ||
Theorem | renegid 41548 | Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β (π΄ + (0 ββ π΄)) = 0) | ||
Theorem | reneg0addlid 41549 | Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β ((0 ββ 0) + π΄) = π΄) | ||
Theorem | resubeulem1 41550 | Lemma for resubeu 41552. A value which when added to zero, results in negative zero. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β (0 + (0 ββ (0 + 0))) = (0 ββ 0)) | ||
Theorem | resubeulem2 41551 | Lemma for resubeu 41552. A value which when added to π΄, results in π΅. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + ((0 ββ π΄) + ((0 ββ (0 + 0)) + π΅))) = π΅) | ||
Theorem | resubeu 41552* | Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β β!π₯ β β (π΄ + π₯) = π΅) | ||
Theorem | rersubcl 41553 | Closure for real subtraction. Based on subcl 11463. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) β β) | ||
Theorem | resubadd 41554 | Relation between real subtraction and addition. Based on subadd 11467. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) = πΆ β (π΅ + πΆ) = π΄)) | ||
Theorem | resubaddd 41555 | Relationship between subtraction and addition. Based on subaddd 11593. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ ββ π΅) = πΆ β (π΅ + πΆ) = π΄)) | ||
Theorem | resubf 41556 | Real subtraction is an operation on the real numbers. Based on subf 11466. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ββ :(β Γ β)βΆβ | ||
Theorem | repncan2 41557 | Addition and subtraction of equals. Compare pncan2 11471. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ + π΅) ββ π΄) = π΅) | ||
Theorem | repncan3 41558 | Addition and subtraction of equals. Based on pncan3 11472. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + (π΅ ββ π΄)) = π΅) | ||
Theorem | readdsub 41559 | Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) ββ πΆ) = ((π΄ ββ πΆ) + π΅)) | ||
Theorem | reladdrsub 41560 | Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11629 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄ + π΅) = πΆ) β β’ (π β π΅ = (πΆ ββ π΄)) | ||
Theorem | reltsub1 41561 | Subtraction from both sides of 'less than'. Compare ltsub1 11714. (Contributed by SN, 13-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ < π΅ β (π΄ ββ πΆ) < (π΅ ββ πΆ))) | ||
Theorem | reltsubadd2 41562 | 'Less than' relationship between addition and subtraction. Compare ltsubadd2 11689. (Contributed by SN, 13-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) < πΆ β π΄ < (π΅ + πΆ))) | ||
Theorem | resubcan2 41563 | Cancellation law for real subtraction. Compare subcan2 11489. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ πΆ) = (π΅ ββ πΆ) β π΄ = π΅)) | ||
Theorem | resubsub4 41564 | Law for double subtraction. Compare subsub4 11497. (Contributed by Steven Nguyen, 14-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = (π΄ ββ (π΅ + πΆ))) | ||
Theorem | rennncan2 41565 | Cancellation law for real subtraction. Compare nnncan2 11501. (Contributed by Steven Nguyen, 14-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ πΆ) ββ (π΅ ββ πΆ)) = (π΄ ββ π΅)) | ||
Theorem | renpncan3 41566 | Cancellation law for real subtraction. Compare npncan3 11502. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) + (πΆ ββ π΄)) = (πΆ ββ π΅)) | ||
Theorem | repnpcan 41567 | Cancellation law for addition and real subtraction. Compare pnpcan 11503. (Contributed by Steven Nguyen, 19-May-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) ββ (π΄ + πΆ)) = (π΅ ββ πΆ)) | ||
Theorem | reppncan 41568 | Cancellation law for mixed addition and real subtraction. Compare ppncan 11506. (Contributed by SN, 3-Sep-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ) + (π΅ ββ πΆ)) = (π΄ + π΅)) | ||
Theorem | resubidaddlidlem 41569 | Lemma for resubidaddlid 41570. A special case of npncan 11485. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β (π΄ ββ π΅) = (π΅ ββ πΆ)) β β’ (π β ((π΄ ββ π΅) + (π΅ ββ πΆ)) = (π΄ ββ πΆ)) | ||
Theorem | resubidaddlid 41570 | Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ ββ π΄) + π΅) = π΅) | ||
Theorem | resubdi 41571 | Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β· (π΅ ββ πΆ)) = ((π΄ Β· π΅) ββ (π΄ Β· πΆ))) | ||
Theorem | re1m1e0m0 41572 | Equality of two left-additive identities. See resubidaddlid 41570. Uses ax-i2m1 11180. (Contributed by SN, 25-Dec-2023.) |
β’ (1 ββ 1) = (0 ββ 0) | ||
Theorem | sn-00idlem1 41573 | Lemma for sn-00id 41576. (Contributed by SN, 25-Dec-2023.) |
β’ (π΄ β β β (π΄ Β· (0 ββ 0)) = (π΄ ββ π΄)) | ||
Theorem | sn-00idlem2 41574 | Lemma for sn-00id 41576. (Contributed by SN, 25-Dec-2023.) |
β’ ((0 ββ 0) β 0 β (0 ββ 0) = 1) | ||
Theorem | sn-00idlem3 41575 | Lemma for sn-00id 41576. (Contributed by SN, 25-Dec-2023.) |
β’ ((0 ββ 0) = 1 β (0 + 0) = 0) | ||
Theorem | sn-00id 41576 | 00id 11393 proven without ax-mulcom 11176 but using ax-1ne0 11181. (Though note that the current version of 00id 11393 can be changed to avoid ax-icn 11171, ax-addcl 11172, ax-mulcl 11174, ax-i2m1 11180, ax-cnre 11185. Most of this is by using 0cnALT3 41476 instead of 0cn 11210). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.) |
β’ (0 + 0) = 0 | ||
Theorem | re0m0e0 41577 | Real number version of 0m0e0 12336 proven without ax-mulcom 11176. (Contributed by SN, 23-Jan-2024.) |
β’ (0 ββ 0) = 0 | ||
Theorem | readdlid 41578 | Real number version of addlid 11401. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (0 + π΄) = π΄) | ||
Theorem | sn-addlid 41579 | addlid 11401 without ax-mulcom 11176. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (0 + π΄) = π΄) | ||
Theorem | remul02 41580 | Real number version of mul02 11396 proven without ax-mulcom 11176. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (0 Β· π΄) = 0) | ||
Theorem | sn-0ne2 41581 | 0ne2 12423 without ax-mulcom 11176. (Contributed by SN, 23-Jan-2024.) |
β’ 0 β 2 | ||
Theorem | remul01 41582 | Real number version of mul01 11397 proven without ax-mulcom 11176. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ Β· 0) = 0) | ||
Theorem | resubid 41583 | Subtraction of a real number from itself (compare subid 11483). (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ ββ π΄) = 0) | ||
Theorem | readdrid 41584 | Real number version of addrid 11398 without ax-mulcom 11176. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ + 0) = π΄) | ||
Theorem | resubid1 41585 | Real number version of subid1 11484 without ax-mulcom 11176. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ ββ 0) = π΄) | ||
Theorem | renegneg 41586 | A real number is equal to the negative of its negative. Compare negneg 11514. (Contributed by SN, 13-Feb-2024.) |
β’ (π΄ β β β (0 ββ (0 ββ π΄)) = π΄) | ||
Theorem | readdcan2 41587 | Commuted version of readdcan 11392 without ax-mulcom 11176. (Contributed by SN, 21-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ) = (π΅ + πΆ) β π΄ = π΅)) | ||
Theorem | renegid2 41588 | Commuted version of renegid 41548. (Contributed by SN, 4-May-2024.) |
β’ (π΄ β β β ((0 ββ π΄) + π΄) = 0) | ||
Theorem | remulneg2d 41589 | Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ Β· (0 ββ π΅)) = (0 ββ (π΄ Β· π΅))) | ||
Theorem | sn-it0e0 41590 | Proof of it0e0 12438 without ax-mulcom 11176. Informally, a real number times 0 is 0, and βπ β βπ = i Β· π by ax-cnre 11185 and renegid2 41588. (Contributed by SN, 30-Apr-2024.) |
β’ (i Β· 0) = 0 | ||
Theorem | sn-negex12 41591* | A combination of cnegex 11399 and cnegex2 11400, this proof takes cnre 11215 π΄ = π + i Β· π and shows that i Β· -π + -π is both a left and right inverse. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β βπ β β ((π΄ + π) = 0 β§ (π + π΄) = 0)) | ||
Theorem | sn-negex 41592* | Proof of cnegex 11399 without ax-mulcom 11176. (Contributed by SN, 30-Apr-2024.) |
β’ (π΄ β β β βπ β β (π΄ + π) = 0) | ||
Theorem | sn-negex2 41593* | Proof of cnegex2 11400 without ax-mulcom 11176. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β βπ β β (π + π΄) = 0) | ||
Theorem | sn-addcand 41594 | addcand 11421 without ax-mulcom 11176. Note how the proof is almost identical to addcan 11402. (Contributed by SN, 5-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ + π΅) = (π΄ + πΆ) β π΅ = πΆ)) | ||
Theorem | sn-addrid 41595 | addrid 11398 without ax-mulcom 11176. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β (π΄ + 0) = π΄) | ||
Theorem | sn-addcan2d 41596 | addcan2d 11422 without ax-mulcom 11176. (Contributed by SN, 5-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ + πΆ) = (π΅ + πΆ) β π΄ = π΅)) | ||
Theorem | reixi 41597 | ixi 11847 without ax-mulcom 11176. (Contributed by SN, 5-May-2024.) |
β’ (i Β· i) = (0 ββ 1) | ||
Theorem | rei4 41598 | i4 14172 without ax-mulcom 11176. (Contributed by SN, 27-May-2024.) |
β’ ((i Β· i) Β· (i Β· i)) = 1 | ||
Theorem | sn-addid0 41599 | A number that sums to itself is zero. Compare addid0 11637, readdridaddlidd 41480. (Contributed by SN, 5-May-2024.) |
β’ (π β π΄ β β) & β’ (π β (π΄ + π΄) = π΄) β β’ (π β π΄ = 0) | ||
Theorem | sn-mul01 41600 | mul01 11397 without ax-mulcom 11176. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β (π΄ Β· 0) = 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |