| Metamath
Proof Explorer Theorem List (p. 425 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | rernegcl 42401 | Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ (𝐴 ∈ ℝ → (0 −ℝ 𝐴) ∈ ℝ) | ||
| Theorem | renegadd 42402 | Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 −ℝ 𝐴) = 𝐵 ↔ (𝐴 + 𝐵) = 0)) | ||
| Theorem | renegid 42403 | Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴 + (0 −ℝ 𝐴)) = 0) | ||
| Theorem | reneg0addlid 42404 | Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ (𝐴 ∈ ℝ → ((0 −ℝ 0) + 𝐴) = 𝐴) | ||
| Theorem | resubeulem1 42405 | Lemma for resubeu 42407. 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 42406 | Lemma for resubeu 42407. A value which when added to 𝐴, results in 𝐵. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + ((0 −ℝ 𝐴) + ((0 −ℝ (0 + 0)) + 𝐵))) = 𝐵) | ||
| Theorem | resubeu 42407* | Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 𝐵) | ||
| Theorem | rersubcl 42408 | Closure for real subtraction. Based on subcl 11507. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) ∈ ℝ) | ||
| Theorem | resubadd 42409 | Relation between real subtraction and addition. Based on subadd 11511. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
| Theorem | resubaddd 42410 | Relationship between subtraction and addition. Based on subaddd 11638. (Contributed by Steven Nguyen, 8-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
| Theorem | resubf 42411 | Real subtraction is an operation on the real numbers. Based on subf 11510. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ −ℝ :(ℝ × ℝ)⟶ℝ | ||
| Theorem | repncan2 42412 | Addition and subtraction of equals. Compare pncan2 11515. (Contributed by Steven Nguyen, 8-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵) | ||
| Theorem | repncan3 42413 | Addition and subtraction of equals. Based on pncan3 11516. (Contributed by Steven Nguyen, 8-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵) | ||
| Theorem | readdsub 42414 | Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵)) | ||
| Theorem | reladdrsub 42415 | Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11674 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴)) | ||
| Theorem | reltsub1 42416 | Subtraction from both sides of 'less than'. Compare ltsub1 11759. (Contributed by SN, 13-Feb-2024.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶))) | ||
| Theorem | reltsubadd2 42417 | 'Less than' relationship between addition and subtraction. Compare ltsubadd2 11734. (Contributed by SN, 13-Feb-2024.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) | ||
| Theorem | resubcan2 42418 | Cancellation law for real subtraction. Compare subcan2 11534. (Contributed by Steven Nguyen, 8-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | resubsub4 42419 | Law for double subtraction. Compare subsub4 11542. (Contributed by Steven Nguyen, 14-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶))) | ||
| Theorem | rennncan2 42420 | Cancellation law for real subtraction. Compare nnncan2 11546. (Contributed by Steven Nguyen, 14-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵)) | ||
| Theorem | renpncan3 42421 | Cancellation law for real subtraction. Compare npncan3 11547. (Contributed by Steven Nguyen, 28-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵)) | ||
| Theorem | repnpcan 42422 | Cancellation law for addition and real subtraction. Compare pnpcan 11548. (Contributed by Steven Nguyen, 19-May-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶)) | ||
| Theorem | reppncan 42423 | Cancellation law for mixed addition and real subtraction. Compare ppncan 11551. (Contributed by SN, 3-Sep-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵)) | ||
| Theorem | resubidaddlidlem 42424 | Lemma for resubidaddlid 42425. A special case of npncan 11530. (Contributed by Steven Nguyen, 8-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶)) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶)) | ||
| Theorem | resubidaddlid 42425 | Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵) | ||
| Theorem | resubdi 42426 | Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶))) | ||
| Theorem | re1m1e0m0 42427 | Equality of two left-additive identities. See resubidaddlid 42425. Uses ax-i2m1 11223. (Contributed by SN, 25-Dec-2023.) |
| ⊢ (1 −ℝ 1) = (0 −ℝ 0) | ||
| Theorem | sn-00idlem1 42428 | Lemma for sn-00id 42431. (Contributed by SN, 25-Dec-2023.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴)) | ||
| Theorem | sn-00idlem2 42429 | Lemma for sn-00id 42431. (Contributed by SN, 25-Dec-2023.) |
| ⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1) | ||
| Theorem | sn-00idlem3 42430 | Lemma for sn-00id 42431. (Contributed by SN, 25-Dec-2023.) |
| ⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0) | ||
| Theorem | sn-00id 42431 | 00id 11436 proven without ax-mulcom 11219 but using ax-1ne0 11224. (Though note that the current version of 00id 11436 can be changed to avoid ax-icn 11214, ax-addcl 11215, ax-mulcl 11217, ax-i2m1 11223, ax-cnre 11228. Most of this is by using 0cnALT3 42294 instead of 0cn 11253). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.) |
| ⊢ (0 + 0) = 0 | ||
| Theorem | re0m0e0 42432 | Real number version of 0m0e0 12386 proven without ax-mulcom 11219. (Contributed by SN, 23-Jan-2024.) |
| ⊢ (0 −ℝ 0) = 0 | ||
| Theorem | readdlid 42433 | Real number version of addlid 11444. (Contributed by SN, 23-Jan-2024.) |
| ⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴) | ||
| Theorem | sn-addlid 42434 | addlid 11444 without ax-mulcom 11219. (Contributed by SN, 23-Jan-2024.) |
| ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) | ||
| Theorem | remul02 42435 | Real number version of mul02 11439 proven without ax-mulcom 11219. (Contributed by SN, 23-Jan-2024.) |
| ⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0) | ||
| Theorem | sn-0ne2 42436 | 0ne2 12473 without ax-mulcom 11219. (Contributed by SN, 23-Jan-2024.) |
| ⊢ 0 ≠ 2 | ||
| Theorem | remul01 42437 | Real number version of mul01 11440 proven without ax-mulcom 11219. (Contributed by SN, 23-Jan-2024.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0) | ||
| Theorem | resubid 42438 | Subtraction of a real number from itself (compare subid 11528). (Contributed by SN, 23-Jan-2024.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 𝐴) = 0) | ||
| Theorem | readdrid 42439 | Real number version of addrid 11441 without ax-mulcom 11219. (Contributed by SN, 23-Jan-2024.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴) | ||
| Theorem | resubid1 42440 | Real number version of subid1 11529 without ax-mulcom 11219. (Contributed by SN, 23-Jan-2024.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 0) = 𝐴) | ||
| Theorem | renegneg 42441 | A real number is equal to the negative of its negative. Compare negneg 11559. (Contributed by SN, 13-Feb-2024.) |
| ⊢ (𝐴 ∈ ℝ → (0 −ℝ (0 −ℝ 𝐴)) = 𝐴) | ||
| Theorem | readdcan2 42442 | Commuted version of readdcan 11435 without ax-mulcom 11219. (Contributed by SN, 21-Feb-2024.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | renegid2 42443 | Commuted version of renegid 42403. (Contributed by SN, 4-May-2024.) |
| ⊢ (𝐴 ∈ ℝ → ((0 −ℝ 𝐴) + 𝐴) = 0) | ||
| Theorem | remulneg2d 42444 | Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 · (0 −ℝ 𝐵)) = (0 −ℝ (𝐴 · 𝐵))) | ||
| Theorem | sn-it0e0 42445 | Proof of it0e0 12488 without ax-mulcom 11219. Informally, a real number times 0 is 0, and ∃𝑟 ∈ ℝ𝑟 = i · 𝑠 by ax-cnre 11228 and renegid2 42443. (Contributed by SN, 30-Apr-2024.) |
| ⊢ (i · 0) = 0 | ||
| Theorem | sn-negex12 42446* | A combination of cnegex 11442 and cnegex2 11443, this proof takes cnre 11258 𝐴 = 𝑟 + i · 𝑠 and shows that i · -𝑠 + -𝑟 is both a left and right inverse. (Contributed by SN, 5-May-2024.) (Proof shortened by SN, 4-Jul-2025.) |
| ⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ ((𝐴 + 𝑏) = 0 ∧ (𝑏 + 𝐴) = 0)) | ||
| Theorem | sn-negex 42447* | Proof of cnegex 11442 without ax-mulcom 11219. (Contributed by SN, 30-Apr-2024.) |
| ⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝐴 + 𝑏) = 0) | ||
| Theorem | sn-negex2 42448* | Proof of cnegex2 11443 without ax-mulcom 11219. (Contributed by SN, 5-May-2024.) |
| ⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝑏 + 𝐴) = 0) | ||
| Theorem | sn-addcand 42449 | addcand 11464 without ax-mulcom 11219. Note how the proof is almost identical to addcan 11445. (Contributed by SN, 5-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) | ||
| Theorem | sn-addrid 42450 | addrid 11441 without ax-mulcom 11219. (Contributed by SN, 5-May-2024.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | ||
| Theorem | sn-addcan2d 42451 | addcan2d 11465 without ax-mulcom 11219. (Contributed by SN, 5-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | reixi 42452 | ixi 11892 without ax-mulcom 11219. (Contributed by SN, 5-May-2024.) |
| ⊢ (i · i) = (0 −ℝ 1) | ||
| Theorem | rei4 42453 | i4 14243 without ax-mulcom 11219. (Contributed by SN, 27-May-2024.) |
| ⊢ ((i · i) · (i · i)) = 1 | ||
| Theorem | sn-addid0 42454 | A number that sums to itself is zero. Compare addid0 11682, readdridaddlidd 42299. (Contributed by SN, 5-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐴) = 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
| Theorem | sn-mul01 42455 | mul01 11440 without ax-mulcom 11219. (Contributed by SN, 5-May-2024.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0) | ||
| Theorem | sn-subeu 42456* | negeu 11498 without ax-mulcom 11219 and complex number version of resubeu 42407. (Contributed by SN, 5-May-2024.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵) | ||
| Theorem | sn-subcl 42457 | subcl 11507 without ax-mulcom 11219. (Contributed by SN, 5-May-2024.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) | ||
| Theorem | sn-subf 42458 | subf 11510 without ax-mulcom 11219. (Contributed by SN, 5-May-2024.) |
| ⊢ − :(ℂ × ℂ)⟶ℂ | ||
| Theorem | resubeqsub 42459 | Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (𝐴 − 𝐵)) | ||
| Theorem | subresre 42460 | Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.) |
| ⊢ −ℝ = ( − ↾ (ℝ × ℝ)) | ||
| Theorem | addinvcom 42461 | A number commutes with its additive inverse. Compare remulinvcom 42462. (Contributed by SN, 5-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 0) ⇒ ⊢ (𝜑 → (𝐵 + 𝐴) = 0) | ||
| Theorem | remulinvcom 42462 | A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 11219. (Contributed by SN, 5-Feb-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) = 1) | ||
| Theorem | remullid 42463 | Commuted version of ax-1rid 11225 without ax-mulcom 11219. (Contributed by SN, 5-Feb-2024.) |
| ⊢ (𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴) | ||
| Theorem | sn-1ticom 42464 | Lemma for sn-mullid 42465 and sn-it1ei 42466. (Contributed by SN, 27-May-2024.) |
| ⊢ (1 · i) = (i · 1) | ||
| Theorem | sn-mullid 42465 | mullid 11260 without ax-mulcom 11219. (Contributed by SN, 27-May-2024.) |
| ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | ||
| Theorem | sn-it1ei 42466 | it1ei 42351 without ax-mulcom 11219. (See sn-mullid 42465 for commuted version). (Contributed by SN, 1-Jun-2024.) |
| ⊢ (i · 1) = i | ||
| Theorem | ipiiie0 42467 | The multiplicative inverse of i (per i4 14243) is also its additive inverse. (Contributed by SN, 30-Jun-2024.) |
| ⊢ (i + (i · (i · i))) = 0 | ||
| Theorem | remulcand 42468 | Commuted version of remulcan2d 42298 without ax-mulcom 11219. (Contributed by SN, 21-Feb-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | sn-0tie0 42469 | Lemma for sn-mul02 42470. Commuted version of sn-it0e0 42445. (Contributed by SN, 30-Jun-2024.) |
| ⊢ (0 · i) = 0 | ||
| Theorem | sn-mul02 42470 | mul02 11439 without ax-mulcom 11219. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 11219 for an outline. (Contributed by SN, 30-Jun-2024.) |
| ⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) | ||
| Theorem | sn-ltaddpos 42471 | ltaddpos 11753 without ax-mulcom 11219. (Contributed by SN, 13-Feb-2024.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))) | ||
| Theorem | sn-ltaddneg 42472 | ltaddneg 11477 without ax-mulcom 11219. (Contributed by SN, 25-Jan-2025.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵)) | ||
| Theorem | reposdif 42473 | Comparison of two numbers whose difference is positive. Compare posdif 11756. (Contributed by SN, 13-Feb-2024.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 −ℝ 𝐴))) | ||
| Theorem | relt0neg1 42474 | Comparison of a real and its negative to zero. Compare lt0neg1 11769. (Contributed by SN, 13-Feb-2024.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < (0 −ℝ 𝐴))) | ||
| Theorem | relt0neg2 42475 | Comparison of a real and its negative to zero. Compare lt0neg2 11770. (Contributed by SN, 13-Feb-2024.) |
| ⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (0 −ℝ 𝐴) < 0)) | ||
| Theorem | sn-addlt0d 42476 | The sum of negative numbers is negative. (Contributed by SN, 25-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) & ⊢ (𝜑 → 𝐵 < 0) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < 0) | ||
| Theorem | sn-addgt0d 42477 | The sum of positive numbers is positive. Proof of addgt0d 11838 without ax-mulcom 11219. (Contributed by SN, 25-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 + 𝐵)) | ||
| Theorem | sn-nnne0 42478 | nnne0 12300 without ax-mulcom 11219. (Contributed by SN, 25-Jan-2025.) |
| ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) | ||
| Theorem | reelznn0nn 42479 | elznn0nn 12627 restated using df-resub 42396. (Contributed by SN, 25-Jan-2025.) |
| ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ (0 −ℝ 𝑁) ∈ ℕ))) | ||
| Theorem | nn0addcom 42480 | Addition is commutative for nonnegative integers. Proven without ax-mulcom 11219. (Contributed by SN, 1-Feb-2025.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
| Theorem | zaddcomlem 42481 | Lemma for zaddcom 42482. (Contributed by SN, 1-Feb-2025.) |
| ⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
| Theorem | zaddcom 42482 | Addition is commutative for integers. Proven without ax-mulcom 11219. (Contributed by SN, 25-Jan-2025.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
| Theorem | renegmulnnass 42483 | Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((0 −ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁))) | ||
| Theorem | nn0mulcom 42484 | Multiplication is commutative for nonnegative integers. Proven without ax-mulcom 11219. (Contributed by SN, 25-Jan-2025.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
| Theorem | zmulcomlem 42485 | Lemma for zmulcom 42486. (Contributed by SN, 25-Jan-2025.) |
| ⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
| Theorem | zmulcom 42486 | Multiplication is commutative for integers. Proven without ax-mulcom 11219. From this result and grpcominv1 42518, we can show that rationals commute under multiplication without using ax-mulcom 11219. (Contributed by SN, 25-Jan-2025.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
| Theorem | mulgt0con1dlem 42487 | Lemma for mulgt0con1d 42488. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (0 < 𝐴 → 0 < 𝐵)) & ⊢ (𝜑 → (𝐴 = 0 → 𝐵 = 0)) ⇒ ⊢ (𝜑 → (𝐵 < 0 → 𝐴 < 0)) | ||
| Theorem | mulgt0con1d 42488 | Counterpart to mulgt0con2d 42489, though not a lemma of anything. This is the first use of ax-pre-mulgt0 11232. (Contributed by SN, 26-Jun-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐵) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ (𝜑 → 𝐴 < 0) | ||
| Theorem | mulgt0con2d 42489 | Lemma for mulgt0b2d 42490 and contrapositive of mulgt0 11338. (Contributed by SN, 26-Jun-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ (𝜑 → 𝐵 < 0) | ||
| Theorem | mulgt0b2d 42490 | Biconditional, deductive form of mulgt0 11338. The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi 42426 does not have a commuted form. (Contributed by SN, 26-Jun-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵))) | ||
| Theorem | sn-ltmul2d 42491 | ltmul2d 13119 without ax-mulcom 11219. (Contributed by SN, 26-Jun-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐶) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) < (𝐶 · 𝐵) ↔ 𝐴 < 𝐵)) | ||
| Theorem | sn-ltmulgt11d 42492 | ltmulgt11d 13112 without ax-mulcom 11219. (Contributed by SN, 26-Jun-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴))) | ||
| Theorem | sn-0lt1 42493 | 0lt1 11785 without ax-mulcom 11219. (Contributed by SN, 13-Feb-2024.) |
| ⊢ 0 < 1 | ||
| Theorem | sn-ltp1 42494 | ltp1 12107 without ax-mulcom 11219. (Contributed by SN, 13-Feb-2024.) |
| ⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1)) | ||
| Theorem | sn-mulgt1d 42495 | mulgt1d 12204 without ax-mulcom 11219. (Contributed by SN, 26-Jun-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 1 < 𝐵) ⇒ ⊢ (𝜑 → 1 < (𝐴 · 𝐵)) | ||
| Theorem | reneg1lt0 42496 | Lemma for sn-inelr 42497. (Contributed by SN, 1-Jun-2024.) |
| ⊢ (0 −ℝ 1) < 0 | ||
| Theorem | sn-inelr 42497 | inelr 12256 without ax-mulcom 11219. (Contributed by SN, 1-Jun-2024.) |
| ⊢ ¬ i ∈ ℝ | ||
| Theorem | sn-itrere 42498 | i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024.) |
| ⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0)) | ||
| Theorem | sn-retire 42499 | Commuted version of sn-itrere 42498. (Contributed by SN, 27-Jun-2024.) |
| ⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0)) | ||
| Theorem | cnreeu 42500 | The reals in the expression given by cnre 11258 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.) |
| ⊢ (𝜑 → 𝑟 ∈ ℝ) & ⊢ (𝜑 → 𝑠 ∈ ℝ) & ⊢ (𝜑 → 𝑡 ∈ ℝ) & ⊢ (𝜑 → 𝑢 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) ↔ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |