![]() |
Metamath
Proof Explorer Theorem List (p. 396 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | zrtdvds 39501 | A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℕ) → (𝐴↑𝑐(1 / 𝑁)) ∥ 𝐴) | ||
Theorem | rtprmirr 39502 | The root of a prime number is irrational. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑃↑𝑐(1 / 𝑁)) ∈ (ℝ ∖ ℚ)) | ||
Syntax | cresub 39503 | Real number subtraction. |
class −ℝ | ||
Definition | df-resub 39504* | Define subtraction between real numbers. This operator saves a few axioms over df-sub 10861 in certain situations. Theorem resubval 39505 shows its value, resubadd 39517 relates it to addition, and rersubcl 39516 proves its closure. It is the restriction of df-sub 10861 to the reals: subresre 39567. (Contributed by Steven Nguyen, 7-Jan-2022.) |
⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥)) | ||
Theorem | resubval 39505* | Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2022.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)) | ||
Theorem | renegeulemv 39506* | Lemma for renegeu 39508 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴) | ||
Theorem | renegeulem 39507* | Lemma for renegeu 39508 and similar. Remove a change in bound variables from renegeulemv 39506. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) | ||
Theorem | renegeu 39508* | Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Theorem | rernegcl 39509 | Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (0 −ℝ 𝐴) ∈ ℝ) | ||
Theorem | renegadd 39510 | Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 −ℝ 𝐴) = 𝐵 ↔ (𝐴 + 𝐵) = 0)) | ||
Theorem | renegid 39511 | Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (𝐴 + (0 −ℝ 𝐴)) = 0) | ||
Theorem | reneg0addid2 39512 | Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 0) + 𝐴) = 𝐴) | ||
Theorem | resubeulem1 39513 | Lemma for resubeu 39515. 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 39514 | Lemma for resubeu 39515. A value which when added to 𝐴, results in 𝐵. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + ((0 −ℝ 𝐴) + ((0 −ℝ (0 + 0)) + 𝐵))) = 𝐵) | ||
Theorem | resubeu 39515* | Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 𝐵) | ||
Theorem | rersubcl 39516 | Closure for real subtraction. Based on subcl 10874. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) ∈ ℝ) | ||
Theorem | resubadd 39517 | Relation between real subtraction and addition. Based on subadd 10878. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | resubaddd 39518 | Relationship between subtraction and addition. Based on subaddd 11004. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | resubf 39519 | Real subtraction is an operation on the real numbers. Based on subf 10877. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ −ℝ :(ℝ × ℝ)⟶ℝ | ||
Theorem | repncan2 39520 | Addition and subtraction of equals. Compare pncan2 10882. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵) | ||
Theorem | repncan3 39521 | Addition and subtraction of equals. Based on pncan3 10883. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵) | ||
Theorem | readdsub 39522 | Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵)) | ||
Theorem | reladdrsub 39523 | Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11040 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴)) | ||
Theorem | reltsub1 39524 | Subtraction from both sides of 'less than'. Compare ltsub1 11125. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶))) | ||
Theorem | reltsubadd2 39525 | 'Less than' relationship between addition and subtraction. Compare ltsubadd2 11100. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) | ||
Theorem | resubcan2 39526 | Cancellation law for real subtraction. Compare subcan2 10900. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | resubsub4 39527 | Law for double subtraction. Compare subsub4 10908. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶))) | ||
Theorem | rennncan2 39528 | Cancellation law for real subtraction. Compare nnncan2 10912. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵)) | ||
Theorem | renpncan3 39529 | Cancellation law for real subtraction. Compare npncan3 10913. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵)) | ||
Theorem | repnpcan 39530 | Cancellation law for addition and real subtraction. Compare pnpcan 10914. (Contributed by Steven Nguyen, 19-May-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶)) | ||
Theorem | reppncan 39531 | Cancellation law for mixed addition and real subtraction. Compare ppncan 10917. (Contributed by SN, 3-Sep-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵)) | ||
Theorem | resubidaddid1lem 39532 | Lemma for resubidaddid1 39533. A special case of npncan 10896. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶)) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶)) | ||
Theorem | resubidaddid1 39533 | Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵) | ||
Theorem | resubdi 39534 | Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶))) | ||
Theorem | re1m1e0m0 39535 | Equality of two left-additive identities. See resubidaddid1 39533. Uses ax-i2m1 10594. (Contributed by SN, 25-Dec-2023.) |
⊢ (1 −ℝ 1) = (0 −ℝ 0) | ||
Theorem | sn-00idlem1 39536 | Lemma for sn-00id 39539. (Contributed by SN, 25-Dec-2023.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴)) | ||
Theorem | sn-00idlem2 39537 | Lemma for sn-00id 39539. (Contributed by SN, 25-Dec-2023.) |
⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1) | ||
Theorem | sn-00idlem3 39538 | Lemma for sn-00id 39539. (Contributed by SN, 25-Dec-2023.) |
⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0) | ||
Theorem | sn-00id 39539 | 00id 10804 proven without ax-mulcom 10590 but using ax-1ne0 10595. (Though note that the current version of 00id 10804 can be changed to avoid ax-icn 10585, ax-addcl 10586, ax-mulcl 10588, ax-i2m1 10594, ax-cnre 10599. Most of this is by using 0cnALT3 39461 instead of 0cn 10622). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.) |
⊢ (0 + 0) = 0 | ||
Theorem | re0m0e0 39540 | Real number version of 0m0e0 11745 proven without ax-mulcom 10590. (Contributed by SN, 23-Jan-2024.) |
⊢ (0 −ℝ 0) = 0 | ||
Theorem | readdid2 39541 | Real number version of addid2 10812. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴) | ||
Theorem | sn-addid2 39542 | addid2 10812 without ax-mulcom 10590. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) | ||
Theorem | remul02 39543 | Real number version of mul02 10807 proven without ax-mulcom 10590. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0) | ||
Theorem | sn-0ne2 39544 | 0ne2 11832 without ax-mulcom 10590. (Contributed by SN, 23-Jan-2024.) |
⊢ 0 ≠ 2 | ||
Theorem | remul01 39545 | Real number version of mul01 10808 proven without ax-mulcom 10590. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0) | ||
Theorem | resubid 39546 | Subtraction of a real number from itself (compare subid 10894). (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 𝐴) = 0) | ||
Theorem | readdid1 39547 | Real number version of addid1 10809, without ax-mulcom 10590. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴) | ||
Theorem | resubid1 39548 | Real number version of subid1 10895, without ax-mulcom 10590. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 0) = 𝐴) | ||
Theorem | renegneg 39549 | A real number is equal to the negative of its negative. Compare negneg 10925. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (0 −ℝ (0 −ℝ 𝐴)) = 𝐴) | ||
Theorem | readdcan2 39550 | Commuted version of readdcan 10803 without ax-mulcom 10590. (Contributed by SN, 21-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | renegid2 39551 | Commuted version of renegid 39511. (Contributed by SN, 4-May-2024.) |
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 𝐴) + 𝐴) = 0) | ||
Theorem | sn-it0e0 39552 | Proof of it0e0 11847 without ax-mulcom 10590. Informally, a real number times 0 is 0, and ∃𝑟 ∈ ℝ𝑟 = i · 𝑠 by ax-cnre 10599 and renegid2 39551. (Contributed by SN, 30-Apr-2024.) |
⊢ (i · 0) = 0 | ||
Theorem | sn-negex12 39553* | A combination of cnegex 10810 and cnegex2 10811, this proof takes cnre 10627 𝐴 = 𝑟 + i · 𝑠 and shows that i · -𝑠 + -𝑟 is both a left and right inverse. (Contributed by SN, 5-May-2024.) |
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ ((𝐴 + 𝑏) = 0 ∧ (𝑏 + 𝐴) = 0)) | ||
Theorem | sn-negex 39554* | Proof of cnegex 10810 without ax-mulcom 10590. (Contributed by SN, 30-Apr-2024.) |
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝐴 + 𝑏) = 0) | ||
Theorem | sn-negex2 39555* | Proof of cnegex2 10811 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.) |
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝑏 + 𝐴) = 0) | ||
Theorem | sn-addcand 39556 | addcand 10832 without ax-mulcom 10590. Note how the proof is almost identical to addcan 10813. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | sn-addid1 39557 | addid1 10809 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | ||
Theorem | sn-addcan2d 39558 | addcan2d 10833 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | reixi 39559 | ixi 11258 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.) |
⊢ (i · i) = (0 −ℝ 1) | ||
Theorem | rei4 39560 | i4 13563 without ax-mulcom 10590. (Contributed by SN, 27-May-2024.) |
⊢ ((i · i) · (i · i)) = 1 | ||
Theorem | sn-addid0 39561 | A number that sums to itself is zero. Compare addid0 11048, readdid1addid2d 39465. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐴) = 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
Theorem | sn-mul01 39562 | mul01 10808 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0) | ||
Theorem | sn-subeu 39563* | negeu 10865 without ax-mulcom 10590 and complex number version of resubeu 39515. (Contributed by SN, 5-May-2024.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵) | ||
Theorem | sn-subcl 39564 | subcl 10874 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) | ||
Theorem | sn-subf 39565 | subf 10877 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.) |
⊢ − :(ℂ × ℂ)⟶ℂ | ||
Theorem | resubeqsub 39566 | Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (𝐴 − 𝐵)) | ||
Theorem | subresre 39567 | Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.) |
⊢ −ℝ = ( − ↾ (ℝ × ℝ)) | ||
Theorem | addinvcom 39568 | A number commutes with its additive inverse. Compare remulinvcom 39569. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 0) ⇒ ⊢ (𝜑 → (𝐵 + 𝐴) = 0) | ||
Theorem | remulinvcom 39569 | A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 10590. (Contributed by SN, 5-Feb-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) = 1) | ||
Theorem | remulid2 39570 | Commuted version of ax-1rid 10596 without ax-mulcom 10590. (Contributed by SN, 5-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴) | ||
Theorem | sn-1ticom 39571 | Lemma for sn-mulid2 39572 and it1ei 39573. (Contributed by SN, 27-May-2024.) |
⊢ (1 · i) = (i · 1) | ||
Theorem | sn-mulid2 39572 | mulid2 10629 without ax-mulcom 10590. (Contributed by SN, 27-May-2024.) |
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | ||
Theorem | it1ei 39573 | 1 is a multiplicative identity for i (see sn-mulid2 39572 for commuted version). (Contributed by SN, 1-Jun-2024.) |
⊢ (i · 1) = i | ||
Theorem | ipiiie0 39574 | The multiplicative inverse of i (per i4 13563) is also its additive inverse. (Contributed by SN, 30-Jun-2024.) |
⊢ (i + (i · (i · i))) = 0 | ||
Theorem | remulcand 39575 | Commuted version of remulcan2d 39464 without ax-mulcom 10590. (Contributed by SN, 21-Feb-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | sn-0tie0 39576 | Lemma for sn-mul02 39577. Commuted version of sn-it0e0 39552. (Contributed by SN, 30-Jun-2024.) |
⊢ (0 · i) = 0 | ||
Theorem | sn-mul02 39577 | mul02 10807 without ax-mulcom 10590. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 10590 for an outline. (Contributed by SN, 30-Jun-2024.) |
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) | ||
Theorem | sn-ltaddpos 39578 | ltaddpos 11119 without ax-mulcom 10590. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))) | ||
Theorem | reposdif 39579 | Comparison of two numbers whose difference is positive. Compare posdif 11122. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 −ℝ 𝐴))) | ||
Theorem | relt0neg1 39580 | Comparison of a real and its negative to zero. Compare lt0neg1 11135. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < (0 −ℝ 𝐴))) | ||
Theorem | relt0neg2 39581 | Comparison of a real and its negative to zero. Compare lt0neg2 11136. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (0 −ℝ 𝐴) < 0)) | ||
Theorem | mulgt0con1dlem 39582 | Lemma for mulgt0con1d 39583. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (0 < 𝐴 → 0 < 𝐵)) & ⊢ (𝜑 → (𝐴 = 0 → 𝐵 = 0)) ⇒ ⊢ (𝜑 → (𝐵 < 0 → 𝐴 < 0)) | ||
Theorem | mulgt0con1d 39583 | Counterpart to mulgt0con2d 39584, though not a lemma of anything. This is the first use of ax-pre-mulgt0 10603. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐵) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ (𝜑 → 𝐴 < 0) | ||
Theorem | mulgt0con2d 39584 | Lemma for mulgt0b2d 39585 and contrapositive of mulgt0 10707. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ (𝜑 → 𝐵 < 0) | ||
Theorem | mulgt0b2d 39585 | Biconditional, deductive form of mulgt0 10707. The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi 39534 does not have a commuted form. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵))) | ||
Theorem | sn-ltmul2d 39586 | ltmul2d 12461 without ax-mulcom 10590. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐶) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) < (𝐶 · 𝐵) ↔ 𝐴 < 𝐵)) | ||
Theorem | sn-0lt1 39587 | 0lt1 11151 without ax-mulcom 10590. (Contributed by SN, 13-Feb-2024.) |
⊢ 0 < 1 | ||
Theorem | sn-ltp1 39588 | ltp1 11469 without ax-mulcom 10590. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1)) | ||
Theorem | reneg1lt0 39589 | Lemma for sn-inelr 39590. (Contributed by SN, 1-Jun-2024.) |
⊢ (0 −ℝ 1) < 0 | ||
Theorem | sn-inelr 39590 | inelr 11615 without ax-mulcom 10590. (Contributed by SN, 1-Jun-2024.) |
⊢ ¬ i ∈ ℝ | ||
Theorem | itrere 39591 | i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024.) |
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0)) | ||
Theorem | retire 39592 | Commuted version of itrere 39591. (Contributed by SN, 27-Jun-2024.) |
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0)) | ||
Theorem | cnreeu 39593 | The reals in the expression given by cnre 10627 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.) |
⊢ (𝜑 → 𝑟 ∈ ℝ) & ⊢ (𝜑 → 𝑠 ∈ ℝ) & ⊢ (𝜑 → 𝑡 ∈ ℝ) & ⊢ (𝜑 → 𝑢 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) ↔ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))) | ||
Theorem | sn-sup2 39594* | sup2 11584 with exactly the same proof except for using sn-ltp1 39588 instead of ltp1 11469, saving ax-mulcom 10590. (Contributed by SN, 26-Jun-2024.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Looking at a corner in 3D space, one can see three right angles. It is impossible to draw three lines in 2D space such that any two of these lines are perpendicular, but a good enough representation is made by casting lines from the 2D surface. Points along the same cast line are collapsed into one point on the 2D surface. In many cases, the 2D surface is smaller than whatever needs to be represented. If the lines cast were perpendicular to the 2D surface, then only areas as small as the 2D surface could be represented. To fix this, the lines need to get further apart as they go farther from the 2D surface. On the other side of the 2D surface the lines will get closer together and intersect at a point. (Because it's defined that way). From this perspective, two parallel lines in 3D space will be represented by two lines that seem to intersect at a point "at infinity". Considering all maximal classes of parallel lines on a 2D plane in 3D space, these classes will all appear to intersect at different points at infinity, forming a line at infinity. Therefore the real projective plane can be thought of as the real affine plane together with the line at infinity. The projective plane takes care of some exceptions that may be found in the affine plane. For example, consider the curve that is the zeroes of 𝑦 = 𝑥↑2. Any line connecting the point (0, 1) to the x-axis intersects with the curve twice, except for the vertical line between (0, 1) and (0, 0). In the projective plane, the curve becomes an ellipse and there is no exception. While it may not seem like it, points at infinity and points corresponding to the affine plane are the same type of point. Consider a line going through the origin in 3D (affine) space. Either it intersects the plane 𝑧 = 1 once, or it is entirely within the plane 𝑧 = 0. If it is entirely within the plane 𝑧 = 0, then it corresponds to the point at infinity intersecting all lines on the plane 𝑧 = 1 with the same slope. Else it corresponds to the point in the 2D plane 𝑧 = 1 that it intersects. So there is a bijection between 3D lines through the origin and points on the real projective plane. The concept of projective spaces generalizes the projective plane to any dimension. | ||
Syntax | cprjsp 39595 | Extend class notation with the projective space function. |
class ℙ𝕣𝕠𝕛 | ||
Definition | df-prjsp 39596* | Define the projective space function. In the bijection between 3D lines through the origin and points in the projective plane (see section comment), this is equivalent to making any two 3D points (excluding the origin) equivalent iff one is a multiple of another. This definition does not quite give all the properties needed, since the scalars of a left vector space can be "less dense" than the vectors (for example, equivocating rational multiples of real numbers). (Contributed by BJ and Steven Nguyen, 29-Apr-2023.) |
⊢ ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})) | ||
Theorem | prjspval 39597* | Value of the projective space function, which is also known as the projectivization of 𝑉. (Contributed by Steven Nguyen, 29-Apr-2023.) |
⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑉 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑉) = (𝐵 / {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))})) | ||
Theorem | prjsprel 39598* | Utility theorem regarding the relation used in ℙ𝕣𝕠𝕛. (Contributed by Steven Nguyen, 29-Apr-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} ⇒ ⊢ (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌))) | ||
Theorem | prjspertr 39599* | The relation in ℙ𝕣𝕠𝕛 is transitive. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ ((𝑉 ∈ LMod ∧ (𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍)) → 𝑋 ∼ 𝑍) | ||
Theorem | prjsperref 39600* | The relation in ℙ𝕣𝕠𝕛 is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑉 ∈ LMod → (𝑋 ∈ 𝐵 ↔ 𝑋 ∼ 𝑋)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |