![]() |
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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sqn5ii 41501 | The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.) |
β’ π΄ β β0 & β’ (π΄ + 1) = π΅ & β’ (π΄ Β· π΅) = πΆ β β’ (;π΄5 Β· ;π΄5) = ;;πΆ25 | ||
Theorem | decpmulnc 41502 | Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11670. (Contributed by Steven Nguyen, 9-Dec-2022.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ π· β β0 & β’ (π΄ Β· πΆ) = πΈ & β’ ((π΄ Β· π·) + (π΅ Β· πΆ)) = πΉ & β’ (π΅ Β· π·) = πΊ β β’ (;π΄π΅ Β· ;πΆπ·) = ;;πΈπΉπΊ | ||
Theorem | decpmul 41503 | Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ π· β β0 & β’ (π΄ Β· πΆ) = πΈ & β’ ((π΄ Β· π·) + (π΅ Β· πΆ)) = πΉ & β’ (π΅ Β· π·) = ;πΊπ» & β’ (;πΈπΊ + πΉ) = πΌ & β’ πΊ β β0 & β’ π» β β0 β β’ (;π΄π΅ Β· ;πΆπ·) = ;πΌπ» | ||
Theorem | sqdeccom12 41504 | The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.) |
β’ π΄ β β0 & β’ π΅ β β0 β β’ ((;π΄π΅ Β· ;π΄π΅) β (;π΅π΄ Β· ;π΅π΄)) = (;99 Β· ((π΄ Β· π΄) β (π΅ Β· π΅))) | ||
Theorem | sq3deccom12 41505 | Variant of sqdeccom12 41504 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ (π΄ + πΆ) = π· β β’ ((;;π΄π΅πΆ Β· ;;π΄π΅πΆ) β (;π·π΅ Β· ;π·π΅)) = (;99 Β· ((;π΄π΅ Β· ;π΄π΅) β (πΆ Β· πΆ))) | ||
Theorem | 4t5e20 41506 | 4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.) |
β’ (4 Β· 5) = ;20 | ||
Theorem | sq9 41507 | The square of 9 is 81. (Contributed by SN, 30-Mar-2025.) |
β’ (9β2) = ;81 | ||
Theorem | 235t711 41508 |
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 11228 saving the lower level uses of mulcomli 11228 within 235 Β· 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12791 are added then this proof would benefit more than ex-decpmul 41509. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 12352 or 8t7e56 12802. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) |
β’ (;;235 Β· ;;711) = ;;;;;167085 | ||
Theorem | ex-decpmul 41509 | Example usage of decpmul 41503. This proof is significantly longer than 235t711 41508. There is more unnecessary carrying compared to 235t711 41508. Although saving 5 visual steps, using mulcomli 11228 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 41510* | The sum of π constant terms (π is not free in πΆ). (Contributed by SN, 21-Mar-2025.) |
β’ (π β π β β0) & β’ (π β πΆ β β) β β’ (π β Ξ£π β (1...π)πΆ = (π Β· πΆ)) | ||
Theorem | fz1sump1 41511* | Add one more term to a sum. Special case of fsump1 15707 generalized to π β β0. (Contributed by SN, 22-Mar-2025.) |
β’ (π β π β β0) & β’ ((π β§ π β (1...(π + 1))) β π΄ β β) & β’ (π = (π + 1) β π΄ = π΅) β β’ (π β Ξ£π β (1...(π + 1))π΄ = (Ξ£π β (1...π)π΄ + π΅)) | ||
Theorem | oddnumth 41512* | The Odd Number Theorem. The sum of the first π odd numbers is πβ2. A corollary of arisum 15811. (Contributed by SN, 21-Mar-2025.) |
β’ (π β β0 β Ξ£π β (1...π)((2 Β· π) β 1) = (πβ2)) | ||
Theorem | nicomachus 41513* | 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 41514* | 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 41515 | Lemma for dffltz 41679. TODO-SN?: This can be used to show exp11d 41519 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 41516 | ltmul1d 13062 for exponentiation of positive reals. (Contributed by Steven Nguyen, 22-Aug-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β) β β’ (π β (π΄ < π΅ β (π΄βπ) < (π΅βπ))) | ||
Theorem | ltexp1dd 41517 | Raising both sides of 'less than' to the same positive integer preserves ordering. (Contributed by Steven Nguyen, 24-Aug-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β) & β’ (π β π΄ < π΅) β β’ (π β (π΄βπ) < (π΅βπ)) | ||
Theorem | exp11nnd 41518 | sq11d 14226 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 41519 | exp11nnd 41518 for nonzero integer exponents. (Contributed by SN, 14-Sep-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β€) & β’ (π β π β 0) & β’ (π β (π΄βπ) = (π΅βπ)) β β’ (π β π΄ = π΅) | ||
Theorem | 0dvds0 41520 | 0 divides 0. (Contributed by SN, 15-Sep-2024.) |
β’ 0 β₯ 0 | ||
Theorem | absdvdsabsb 41521 | Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (absβπ) β₯ (absβπ))) | ||
Theorem | dvdsexpim 41522 | dvdssqim 16501 generalized to nonnegative exponents. (Contributed by Steven Nguyen, 2-Apr-2023.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β0) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | gcdnn0id 41523 | The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.) |
β’ (π β β0 β (π gcd π) = π) | ||
Theorem | gcdle1d 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 | gcdle2d 41525 | 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 41526 | Deduction associated with dvdsexpim 41522. (Contributed by SN, 21-Aug-2024.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β π β β0) & β’ (π β π΄ β₯ π΅) β β’ (π β (π΄βπ) β₯ (π΅βπ)) | ||
Theorem | nn0rppwr 41527 | If π΄ and π΅ are relatively prime, then so are π΄βπ and π΅βπ. rppwr 16506 extended to nonnegative integers. Less general than rpexp12i 16666. (Contributed by Steven Nguyen, 4-Apr-2023.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ π β β0) β ((π΄ gcd π΅) = 1 β ((π΄βπ) gcd (π΅βπ)) = 1)) | ||
Theorem | expgcd 41528 | Exponentiation distributes over GCD. sqgcd 16507 extended to nonnegative exponents. (Contributed by Steven Nguyen, 4-Apr-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β ((π΄ gcd π΅)βπ) = ((π΄βπ) gcd (π΅βπ))) | ||
Theorem | nn0expgcd 41529 | Exponentiation distributes over GCD. nn0gcdsq 16693 extended to nonnegative exponents. expgcd 41528 extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ π β β0) β ((π΄ gcd π΅)βπ) = ((π΄βπ) gcd (π΅βπ))) | ||
Theorem | zexpgcd 41530 | Exponentiation distributes over GCD. zgcdsq 16694 extended to nonnegative exponents. nn0expgcd 41529 extended to integer bases by symmetry. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β0) β ((π΄ gcd π΅)βπ) = ((π΄βπ) gcd (π΅βπ))) | ||
Theorem | numdenexp 41531 | numdensq 16695 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β β§ π β β0) β ((numerβ(π΄βπ)) = ((numerβπ΄)βπ) β§ (denomβ(π΄βπ)) = ((denomβπ΄)βπ))) | ||
Theorem | numexp 41532 | numsq 16696 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β β§ π β β0) β (numerβ(π΄βπ)) = ((numerβπ΄)βπ)) | ||
Theorem | denexp 41533 | densq 16697 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β β§ π β β0) β (denomβ(π΄βπ)) = ((denomβπ΄)βπ)) | ||
Theorem | dvdsexpnn 41534 | dvdssqlem 16508 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | dvdsexpnn0 41535 | dvdsexpnn 41534 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ π β β) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | dvdsexpb 41536 | dvdssq 16509 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | posqsqznn 41537 | When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16699 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.) |
β’ (π β (π΄β2) β β€) & β’ (π β π΄ β β) & β’ (π β 0 < π΄) β β’ (π β π΄ β β) | ||
Theorem | zrtelqelz 41538 | zsqrtelqelz 16699 generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023.) |
β’ ((π΄ β β€ β§ π β β β§ (π΄βπ(1 / π)) β β) β (π΄βπ(1 / π)) β β€) | ||
Theorem | zrtdvds 41539 | A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023.) |
β’ ((π΄ β β€ β§ π β β β§ (π΄βπ(1 / π)) β β) β (π΄βπ(1 / π)) β₯ π΄) | ||
Theorem | rtprmirr 41540 | The root of a prime number is irrational. (Contributed by Steven Nguyen, 6-Apr-2023.) |
β’ ((π β β β§ π β (β€β₯β2)) β (πβπ(1 / π)) β (β β β)) | ||
Syntax | cresub 41541 | Real number subtraction. |
class ββ | ||
Definition | df-resub 41542* | Define subtraction between real numbers. This operator saves a few axioms over df-sub 11451 in certain situations. Theorem resubval 41543 shows its value, resubadd 41555 relates it to addition, and rersubcl 41554 proves its closure. It is the restriction of df-sub 11451 to the reals: subresre 41606. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ββ = (π₯ β β, π¦ β β β¦ (β©π§ β β (π¦ + π§) = π₯)) | ||
Theorem | resubval 41543* | Value of real subtraction, which is the (unique) real π₯ such that π΅ + π₯ = π΄. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) = (β©π₯ β β (π΅ + π₯) = π΄)) | ||
Theorem | renegeulemv 41544* | Lemma for renegeu 41546 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ (π β π΅ β β) & β’ (π β βπ¦ β β (π΅ + π¦) = π΄) β β’ (π β β!π₯ β β (π΅ + π₯) = π΄) | ||
Theorem | renegeulem 41545* | Lemma for renegeu 41546 and similar. Remove a change in bound variables from renegeulemv 41544. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ (π β π΅ β β) & β’ (π β βπ¦ β β (π΅ + π¦) = π΄) β β’ (π β β!π¦ β β (π΅ + π¦) = π΄) | ||
Theorem | renegeu 41546* | Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β β!π₯ β β (π΄ + π₯) = 0) | ||
Theorem | rernegcl 41547 | Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β (0 ββ π΄) β β) | ||
Theorem | renegadd 41548 | Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((0 ββ π΄) = π΅ β (π΄ + π΅) = 0)) | ||
Theorem | renegid 41549 | Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β (π΄ + (0 ββ π΄)) = 0) | ||
Theorem | reneg0addlid 41550 | Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β ((0 ββ 0) + π΄) = π΄) | ||
Theorem | resubeulem1 41551 | Lemma for resubeu 41553. 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 41552 | Lemma for resubeu 41553. A value which when added to π΄, results in π΅. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + ((0 ββ π΄) + ((0 ββ (0 + 0)) + π΅))) = π΅) | ||
Theorem | resubeu 41553* | Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β β!π₯ β β (π΄ + π₯) = π΅) | ||
Theorem | rersubcl 41554 | Closure for real subtraction. Based on subcl 11464. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) β β) | ||
Theorem | resubadd 41555 | Relation between real subtraction and addition. Based on subadd 11468. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) = πΆ β (π΅ + πΆ) = π΄)) | ||
Theorem | resubaddd 41556 | Relationship between subtraction and addition. Based on subaddd 11594. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ ββ π΅) = πΆ β (π΅ + πΆ) = π΄)) | ||
Theorem | resubf 41557 | Real subtraction is an operation on the real numbers. Based on subf 11467. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ββ :(β Γ β)βΆβ | ||
Theorem | repncan2 41558 | Addition and subtraction of equals. Compare pncan2 11472. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ + π΅) ββ π΄) = π΅) | ||
Theorem | repncan3 41559 | Addition and subtraction of equals. Based on pncan3 11473. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + (π΅ ββ π΄)) = π΅) | ||
Theorem | readdsub 41560 | Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) ββ πΆ) = ((π΄ ββ πΆ) + π΅)) | ||
Theorem | reladdrsub 41561 | Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11630 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄ + π΅) = πΆ) β β’ (π β π΅ = (πΆ ββ π΄)) | ||
Theorem | reltsub1 41562 | Subtraction from both sides of 'less than'. Compare ltsub1 11715. (Contributed by SN, 13-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ < π΅ β (π΄ ββ πΆ) < (π΅ ββ πΆ))) | ||
Theorem | reltsubadd2 41563 | 'Less than' relationship between addition and subtraction. Compare ltsubadd2 11690. (Contributed by SN, 13-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) < πΆ β π΄ < (π΅ + πΆ))) | ||
Theorem | resubcan2 41564 | Cancellation law for real subtraction. Compare subcan2 11490. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ πΆ) = (π΅ ββ πΆ) β π΄ = π΅)) | ||
Theorem | resubsub4 41565 | Law for double subtraction. Compare subsub4 11498. (Contributed by Steven Nguyen, 14-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = (π΄ ββ (π΅ + πΆ))) | ||
Theorem | rennncan2 41566 | Cancellation law for real subtraction. Compare nnncan2 11502. (Contributed by Steven Nguyen, 14-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ πΆ) ββ (π΅ ββ πΆ)) = (π΄ ββ π΅)) | ||
Theorem | renpncan3 41567 | Cancellation law for real subtraction. Compare npncan3 11503. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) + (πΆ ββ π΄)) = (πΆ ββ π΅)) | ||
Theorem | repnpcan 41568 | Cancellation law for addition and real subtraction. Compare pnpcan 11504. (Contributed by Steven Nguyen, 19-May-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) ββ (π΄ + πΆ)) = (π΅ ββ πΆ)) | ||
Theorem | reppncan 41569 | Cancellation law for mixed addition and real subtraction. Compare ppncan 11507. (Contributed by SN, 3-Sep-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ) + (π΅ ββ πΆ)) = (π΄ + π΅)) | ||
Theorem | resubidaddlidlem 41570 | Lemma for resubidaddlid 41571. A special case of npncan 11486. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β (π΄ ββ π΅) = (π΅ ββ πΆ)) β β’ (π β ((π΄ ββ π΅) + (π΅ ββ πΆ)) = (π΄ ββ πΆ)) | ||
Theorem | resubidaddlid 41571 | Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ ββ π΄) + π΅) = π΅) | ||
Theorem | resubdi 41572 | Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β· (π΅ ββ πΆ)) = ((π΄ Β· π΅) ββ (π΄ Β· πΆ))) | ||
Theorem | re1m1e0m0 41573 | Equality of two left-additive identities. See resubidaddlid 41571. Uses ax-i2m1 11181. (Contributed by SN, 25-Dec-2023.) |
β’ (1 ββ 1) = (0 ββ 0) | ||
Theorem | sn-00idlem1 41574 | Lemma for sn-00id 41577. (Contributed by SN, 25-Dec-2023.) |
β’ (π΄ β β β (π΄ Β· (0 ββ 0)) = (π΄ ββ π΄)) | ||
Theorem | sn-00idlem2 41575 | Lemma for sn-00id 41577. (Contributed by SN, 25-Dec-2023.) |
β’ ((0 ββ 0) β 0 β (0 ββ 0) = 1) | ||
Theorem | sn-00idlem3 41576 | Lemma for sn-00id 41577. (Contributed by SN, 25-Dec-2023.) |
β’ ((0 ββ 0) = 1 β (0 + 0) = 0) | ||
Theorem | sn-00id 41577 | 00id 11394 proven without ax-mulcom 11177 but using ax-1ne0 11182. (Though note that the current version of 00id 11394 can be changed to avoid ax-icn 11172, ax-addcl 11173, ax-mulcl 11175, ax-i2m1 11181, ax-cnre 11186. Most of this is by using 0cnALT3 41477 instead of 0cn 11211). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.) |
β’ (0 + 0) = 0 | ||
Theorem | re0m0e0 41578 | Real number version of 0m0e0 12337 proven without ax-mulcom 11177. (Contributed by SN, 23-Jan-2024.) |
β’ (0 ββ 0) = 0 | ||
Theorem | readdlid 41579 | Real number version of addlid 11402. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (0 + π΄) = π΄) | ||
Theorem | sn-addlid 41580 | addlid 11402 without ax-mulcom 11177. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (0 + π΄) = π΄) | ||
Theorem | remul02 41581 | Real number version of mul02 11397 proven without ax-mulcom 11177. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (0 Β· π΄) = 0) | ||
Theorem | sn-0ne2 41582 | 0ne2 12424 without ax-mulcom 11177. (Contributed by SN, 23-Jan-2024.) |
β’ 0 β 2 | ||
Theorem | remul01 41583 | Real number version of mul01 11398 proven without ax-mulcom 11177. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ Β· 0) = 0) | ||
Theorem | resubid 41584 | Subtraction of a real number from itself (compare subid 11484). (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ ββ π΄) = 0) | ||
Theorem | readdrid 41585 | Real number version of addrid 11399 without ax-mulcom 11177. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ + 0) = π΄) | ||
Theorem | resubid1 41586 | Real number version of subid1 11485 without ax-mulcom 11177. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ ββ 0) = π΄) | ||
Theorem | renegneg 41587 | A real number is equal to the negative of its negative. Compare negneg 11515. (Contributed by SN, 13-Feb-2024.) |
β’ (π΄ β β β (0 ββ (0 ββ π΄)) = π΄) | ||
Theorem | readdcan2 41588 | Commuted version of readdcan 11393 without ax-mulcom 11177. (Contributed by SN, 21-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ) = (π΅ + πΆ) β π΄ = π΅)) | ||
Theorem | renegid2 41589 | Commuted version of renegid 41549. (Contributed by SN, 4-May-2024.) |
β’ (π΄ β β β ((0 ββ π΄) + π΄) = 0) | ||
Theorem | remulneg2d 41590 | Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ Β· (0 ββ π΅)) = (0 ββ (π΄ Β· π΅))) | ||
Theorem | sn-it0e0 41591 | Proof of it0e0 12439 without ax-mulcom 11177. Informally, a real number times 0 is 0, and βπ β βπ = i Β· π by ax-cnre 11186 and renegid2 41589. (Contributed by SN, 30-Apr-2024.) |
β’ (i Β· 0) = 0 | ||
Theorem | sn-negex12 41592* | A combination of cnegex 11400 and cnegex2 11401, this proof takes cnre 11216 π΄ = π + i Β· π and shows that i Β· -π + -π is both a left and right inverse. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β βπ β β ((π΄ + π) = 0 β§ (π + π΄) = 0)) | ||
Theorem | sn-negex 41593* | Proof of cnegex 11400 without ax-mulcom 11177. (Contributed by SN, 30-Apr-2024.) |
β’ (π΄ β β β βπ β β (π΄ + π) = 0) | ||
Theorem | sn-negex2 41594* | Proof of cnegex2 11401 without ax-mulcom 11177. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β βπ β β (π + π΄) = 0) | ||
Theorem | sn-addcand 41595 | addcand 11422 without ax-mulcom 11177. Note how the proof is almost identical to addcan 11403. (Contributed by SN, 5-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ + π΅) = (π΄ + πΆ) β π΅ = πΆ)) | ||
Theorem | sn-addrid 41596 | addrid 11399 without ax-mulcom 11177. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β (π΄ + 0) = π΄) | ||
Theorem | sn-addcan2d 41597 | addcan2d 11423 without ax-mulcom 11177. (Contributed by SN, 5-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ + πΆ) = (π΅ + πΆ) β π΄ = π΅)) | ||
Theorem | reixi 41598 | ixi 11848 without ax-mulcom 11177. (Contributed by SN, 5-May-2024.) |
β’ (i Β· i) = (0 ββ 1) | ||
Theorem | rei4 41599 | i4 14173 without ax-mulcom 11177. (Contributed by SN, 27-May-2024.) |
β’ ((i Β· i) Β· (i Β· i)) = 1 | ||
Theorem | sn-addid0 41600 | A number that sums to itself is zero. Compare addid0 11638, readdridaddlidd 41481. (Contributed by SN, 5-May-2024.) |
β’ (π β π΄ β β) & β’ (π β (π΄ + π΄) = π΄) β β’ (π β π΄ = 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |