Home | Metamath
Proof Explorer Theorem List (p. 393 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Towards the start of this section are several proofs regarding the different complex number axioms that could be used to prove some results. For example, ax-1rid 10607 is used in mulid1 10639 related theorems, so one could trade off the extra axioms in mulid1 10639 for the axioms needed to prove that something is a real number. Another example is avoiding complex number closure laws by using real number closure laws and then using ax-resscn 10594; in the other direction, real number closure laws can be avoided by using ax-resscn 10594 and then the complex number closure laws. (This only works if the result of (𝐴 + 𝐵) only needs to be a complex number). The natural numbers are especially amenable to axiom reductions, as the set ℕ is the recursive set {1, (1 + 1), ((1 + 1) + 1)}, etc., i.e. the set of numbers formed by only additions of 1. The digits 2 through 9 are defined so that they expand into additions of 1. This makes adding natural numbers conveniently only require the rearrangement of parentheses, as shown with the following: (4 + 3) = 7 ((3 + 1) + (2 + 1)) = (6 + 1) ((((1 + 1) + 1) + 1) + ((1 + 1) + 1)) = ((((((1 + 1) + 1) + 1) + 1) + 1) + 1) This only requires ax-addass 10602, ax-1cn 10595, and ax-addcl 10597. (And in practice, the expression isn't completely expanded into ones.) Multiplication by 1 requires either mulid2i 10646 or (ax-1rid 10607 and 1re 10641) as seen in 1t1e1 11800 and 1t1e1ALT 39204. Multiplying with greater natural numbers uses ax-distr 10604. Still, this takes fewer axioms than adding zero. When zero is involved in the decimal constructor, there's an implicit addition operation which causes such theorems (e.g. (9 + 1) = ;10) to use almost every complex number axiom. | ||
Theorem | c0exALT 39201 | Alternate proof of c0ex 10635 using more set theory axioms but fewer complex number axioms (add ax-10 2145, ax-11 2161, ax-13 2390, ax-nul 5210, and remove ax-1cn 10595, ax-icn 10596, ax-addcl 10597, and ax-mulcl 10599). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ V | ||
Theorem | 0cnALT3 39202 | Alternate proof of 0cn 10633 using ax-resscn 10594, ax-addrcl 10598, ax-rnegex 10608, ax-cnre 10610 instead of ax-icn 10596, ax-addcl 10597, ax-mulcl 10599, ax-i2m1 10605. Version of 0cnALT 10874 using ax-1cn 10595 instead of ax-icn 10596. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℂ | ||
Theorem | elre0re 39203 | Specialized version of 0red 10644 without using ax-1cn 10595 and ax-cnre 10610. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ) | ||
Theorem | 1t1e1ALT 39204 | Alternate proof of 1t1e1 11800 using a different set of axioms (add ax-mulrcl 10600, ax-i2m1 10605, ax-1ne0 10606, ax-rrecex 10609 and remove ax-resscn 10594, ax-mulcom 10601, ax-mulass 10603, ax-distr 10604). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (1 · 1) = 1 | ||
Theorem | remulcan2d 39205 | mulcan2d 11274 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | readdid1addid2d 39206 | Given some real number 𝐵 where 𝐴 acts like a right additive identity, derive that 𝐴 is a left additive identity. Note that the hypothesis is weaker than proving that 𝐴 is a right additive identity (for all numbers). Although, if there is a right additive identity, then by readdcan 10814, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶) | ||
Theorem | sn-1ne2 39207 | A proof of 1ne2 11846 without using ax-mulcom 10601, ax-mulass 10603, ax-pre-mulgt0 10614. Based on mul02lem2 10817. (Contributed by SN, 13-Dec-2023.) |
⊢ 1 ≠ 2 | ||
Theorem | nnn1suc 39208* | A positive integer that is not 1 is a successor of some other positive integer. (Contributed by Steven Nguyen, 19-Aug-2023.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ≠ 1) → ∃𝑥 ∈ ℕ (𝑥 + 1) = 𝐴) | ||
Theorem | nnadd1com 39209 | Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴)) | ||
Theorem | nnaddcom 39210 | Addition is commutative for natural numbers. Uses fewer axioms than addcom 10826. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | nnaddcomli 39211 | Version of addcomli 10832 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 | ||
Theorem | nnadddir 39212 | Right-distributivity for natural numbers without ax-mulcom 10601. (Contributed by SN, 5-Feb-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | nnmul1com 39213 | Multiplication with 1 is commutative for natural numbers, without ax-mulcom 10601. Since (𝐴 · 1) is 𝐴 by ax-1rid 10607, this is equivalent to remulid2 39298 for natural numbers, but using fewer axioms (avoiding ax-resscn 10594, ax-addass 10602, ax-mulass 10603, ax-rnegex 10608, ax-pre-lttri 10611, ax-pre-lttrn 10612, ax-pre-ltadd 10613). (Contributed by SN, 5-Feb-2024.) |
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1)) | ||
Theorem | nnmulcom 39214 | Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | addsubeq4com 39215 | Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵))) | ||
Theorem | sqsumi 39216 | A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵))) | ||
Theorem | negn0nposznnd 39217 | Lemma for dffltz 39320. (Contributed by Steven Nguyen, 27-Feb-2023.) |
⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → ¬ 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℕ) | ||
Theorem | sqmid3api 39218 | Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝑁 ∈ ℂ & ⊢ (𝐴 + 𝑁) = 𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁)) | ||
Theorem | decaddcom 39219 | Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵) | ||
Theorem | sqn5i 39220 | 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 ⇒ ⊢ (;𝐴5 · ;𝐴5) = ;;(𝐴 · (𝐴 + 1))25 | ||
Theorem | sqn5ii 39221 | 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 39222 | Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11091. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = 𝐺 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺 | ||
Theorem | decpmul 39223 | Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = ;𝐺𝐻 & ⊢ (;𝐸𝐺 + 𝐹) = 𝐼 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻 | ||
Theorem | sqdeccom12 39224 | The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) | ||
Theorem | sq3deccom12 39225 | Variant of sqdeccom12 39224 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐴 + 𝐶) = 𝐷 ⇒ ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶))) | ||
Theorem | 235t711 39226 |
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 10650 saving the lower level uses of mulcomli 10650 within 235 · 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12208 are added then this proof would benefit more than ex-decpmul 39227. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 11773 or 8t7e56 12219. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) |
⊢ (;;235 · ;;711) = ;;;;;167085 | ||
Theorem | ex-decpmul 39227 | Example usage of decpmul 39223. This proof is significantly longer than 235t711 39226. There is more unnecessary carrying compared to 235t711 39226. Although saving 5 visual steps, using mulcomli 10650 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 | oexpreposd 39228 | Lemma for dffltz 39320. (Contributed by Steven Nguyen, 4-Mar-2023.) |
⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℕ) ⇒ ⊢ (𝜑 → (0 < 𝑁 ↔ 0 < (𝑁↑𝑀))) | ||
Theorem | cxpgt0d 39229 | Exponentiation with a positive mantissa is positive. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 < (𝐴↑𝑐𝑁)) | ||
Theorem | dvdsexpim 39230 | dvdssqim 15904 generalized to nonnegative exponents. (Contributed by Steven Nguyen, 2-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ 𝐵 → (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
Theorem | nn0rppwr 39231 | If 𝐴 and 𝐵 are relatively prime, then so are 𝐴↑𝑁 and 𝐵↑𝑁. rppwr 15908 extended to nonnegative integers. (Contributed by Steven Nguyen, 4-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd (𝐵↑𝑁)) = 1)) | ||
Theorem | expgcd 39232 | Exponentiation distributes over GCD. sqgcd 15909 extended to nonnegative exponents. (Contributed by Steven Nguyen, 4-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | nn0expgcd 39233 | Exponentiation distributes over GCD. nn0gcdsq 16092 extended to nonnegative exponents. expgcd 39232 extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | zexpgcd 39234 | Exponentiation distributes over GCD. zgcdsq 16093 extended to nonnegative exponents. nn0expgcd 39233 extended to integer bases by symmetry. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | numdenexp 39235 | numdensq 16094 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → ((numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁) ∧ (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁))) | ||
Theorem | numexp 39236 | numsq 16095 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁)) | ||
Theorem | denexp 39237 | densq 16096 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁)) | ||
Theorem | exp11d 39238 | sq11d 13622 for positive real bases and nonzero exponents. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ≠ 0) & ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | ltexp1d 39239 | ltmul1d 12473 for exponentiation of positive reals. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑𝑁) < (𝐵↑𝑁))) | ||
Theorem | ltexp1dd 39240 | Raising both sides of 'less than' to the same positive integer preserves ordering. (Contributed by Steven Nguyen, 24-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) < (𝐵↑𝑁)) | ||
Theorem | zrtelqelz 39241 | zsqrtelqelz 16098 generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℚ) → (𝐴↑𝑐(1 / 𝑁)) ∈ ℤ) | ||
Theorem | zrtdvds 39242 | A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℕ) → (𝐴↑𝑐(1 / 𝑁)) ∥ 𝐴) | ||
Theorem | rtprmirr 39243 | The root of a prime number is irrational. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑃↑𝑐(1 / 𝑁)) ∈ (ℝ ∖ ℚ)) | ||
Syntax | cresub 39244 | Real number subtraction. |
class −ℝ | ||
Definition | df-resub 39245* | Define subtraction between real numbers. This operator saves a few axioms over df-sub 10872 in certain situations. Theorem resubval 39246 shows its value, resubadd 39258 relates it to addition, and rersubcl 39257 proves its closure. Based on df-sub 10872. (Contributed by Steven Nguyen, 7-Jan-2022.) |
⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥)) | ||
Theorem | resubval 39246* | Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2022.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)) | ||
Theorem | renegeulemv 39247* | Lemma for renegeu 39249 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴) | ||
Theorem | renegeulem 39248* | Lemma for renegeu 39249 and similar. Remove a change in bound variables from renegeulemv 39247. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) | ||
Theorem | renegeu 39249* | Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Theorem | rernegcl 39250 | Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (0 −ℝ 𝐴) ∈ ℝ) | ||
Theorem | renegadd 39251 | Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 −ℝ 𝐴) = 𝐵 ↔ (𝐴 + 𝐵) = 0)) | ||
Theorem | renegid 39252 | Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (𝐴 + (0 −ℝ 𝐴)) = 0) | ||
Theorem | reneg0addid2 39253 | Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 0) + 𝐴) = 𝐴) | ||
Theorem | resubeulem1 39254 | Lemma for resubeu 39256. 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 39255 | Lemma for resubeu 39256. A value which when added to 𝐴, results in 𝐵. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + ((0 −ℝ 𝐴) + ((0 −ℝ (0 + 0)) + 𝐵))) = 𝐵) | ||
Theorem | resubeu 39256* | Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 𝐵) | ||
Theorem | rersubcl 39257 | Closure for real subtraction. Based on subcl 10885. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) ∈ ℝ) | ||
Theorem | resubadd 39258 | Relation between real subtraction and addition. Based on subadd 10889. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | resubaddd 39259 | Relationship between subtraction and addition. Based on subaddd 11015. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | resubf 39260 | Real subtraction is an operation on the real numbers. Based on subf 10888. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ −ℝ :(ℝ × ℝ)⟶ℝ | ||
Theorem | repncan2 39261 | Addition and subtraction of equals. Compare pncan2 10893. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵) | ||
Theorem | repncan3 39262 | Addition and subtraction of equals. Based on pncan3 10894. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵) | ||
Theorem | readdsub 39263 | Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵)) | ||
Theorem | reladdrsub 39264 | Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11051 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴)) | ||
Theorem | reltsub1 39265 | Subtraction from both sides of 'less than'. Compare ltsub1 11136. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶))) | ||
Theorem | reltsubadd2 39266 | 'Less than' relationship between addition and subtraction. Compare ltsubadd2 11111. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) | ||
Theorem | resubcan2 39267 | Cancellation law for real subtraction. Compare subcan2 10911. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | resubsub4 39268 | Law for double subtraction. Compare subsub4 10919. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶))) | ||
Theorem | rennncan2 39269 | Cancellation law for real subtraction. Compare nnncan2 10923. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵)) | ||
Theorem | renpncan3 39270 | Cancellation law for real subtraction. Compare npncan3 10924. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵)) | ||
Theorem | repnpcan 39271 | Cancellation law for addition and real subtraction. Compare pnpcan 10925. (Contributed by Steven Nguyen, 19-May-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶)) | ||
Theorem | reppncan 39272 | Cancellation law for mixed addition and real subtraction. Compare ppncan 10928. (Contributed by SN, 3-Sep-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵)) | ||
Theorem | resubidaddid1lem 39273 | Lemma for resubidaddid1 39274. A special case of npncan 10907. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶)) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶)) | ||
Theorem | resubidaddid1 39274 | Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵) | ||
Theorem | resubdi 39275 | Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶))) | ||
Theorem | re1m1e0m0 39276 | Equality of two left-additive identities. See resubidaddid1 39274. Uses ax-i2m1 10605. (Contributed by SN, 25-Dec-2023.) |
⊢ (1 −ℝ 1) = (0 −ℝ 0) | ||
Theorem | sn-00idlem1 39277 | Lemma for sn-00id 39280. (Contributed by SN, 25-Dec-2023.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴)) | ||
Theorem | sn-00idlem2 39278 | Lemma for sn-00id 39280. (Contributed by SN, 25-Dec-2023.) |
⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1) | ||
Theorem | sn-00idlem3 39279 | Lemma for sn-00id 39280. (Contributed by SN, 25-Dec-2023.) |
⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0) | ||
Theorem | sn-00id 39280 | 00id 10815 proven without ax-mulcom 10601 but using ax-1ne0 10606. (Though note that the current version of 00id 10815 can be changed to avoid ax-icn 10596, ax-addcl 10597, ax-mulcl 10599, ax-i2m1 10605, ax-cnre 10610. Most of this is by using 0cnALT3 39202 instead of 0cn 10633). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.) |
⊢ (0 + 0) = 0 | ||
Theorem | re0m0e0 39281 | Real number version of 0m0e0 11758 proven without ax-mulcom 10601. (Contributed by SN, 23-Jan-2024.) |
⊢ (0 −ℝ 0) = 0 | ||
Theorem | readdid2 39282 | Real number version of addid2 10823. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴) | ||
Theorem | sn-addid2 39283 | addid2 10823 without ax-mulcom 10601. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) | ||
Theorem | remul02 39284 | Real number version of mul02 10818 proven without ax-mulcom 10601. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0) | ||
Theorem | sn-0ne2 39285 | 0ne2 11845 without ax-mulcom 10601. (Contributed by SN, 23-Jan-2024.) |
⊢ 0 ≠ 2 | ||
Theorem | remul01 39286 | Real number version of mul01 10819 proven without ax-mulcom 10601. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0) | ||
Theorem | resubid 39287 | Subtraction of a real number from itself (compare subid 10905). (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 𝐴) = 0) | ||
Theorem | readdid1 39288 | Real number version of addid1 10820, without ax-mulcom 10601. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴) | ||
Theorem | resubid1 39289 | Real number version of subid1 10906, without ax-mulcom 10601. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 0) = 𝐴) | ||
Theorem | renegneg 39290 | A real number is equal to the negative of its negative. Compare negneg 10936. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (0 −ℝ (0 −ℝ 𝐴)) = 𝐴) | ||
Theorem | readdcan2 39291 | Commuted version of readdcan 10814 without ax-mulcom 10601. (Contributed by SN, 21-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | sn-ltaddpos 39292 | ltaddpos 11130 without ax-mulcom 10601. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))) | ||
Theorem | relt0neg1 39293 | Comparison of a real and its negative to zero. Compare lt0neg1 11146. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < (0 −ℝ 𝐴))) | ||
Theorem | relt0neg2 39294 | Comparison of a real and its negative to zero. Compare lt0neg2 11147. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (0 −ℝ 𝐴) < 0)) | ||
Theorem | sn-0lt1 39295 | 0lt1 11162 without ax-mulcom 10601. (Contributed by SN, 13-Feb-2024.) |
⊢ 0 < 1 | ||
Theorem | sn-ltp1 39296 | ltp1 11480 without ax-mulcom 10601. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1)) | ||
Theorem | remulinvcom 39297 | A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 10601. (Contributed by SN, 5-Feb-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) = 1) | ||
Theorem | remulid2 39298 | Commuted version of ax-1rid 10607 and real number version of mulid2 10640 without ax-mulcom 10601. (Contributed by SN, 5-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴) | ||
Theorem | remulcand 39299 | Commuted version of remulcan2d 39205 without ax-mulcom 10601. (Contributed by SN, 21-Feb-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)) | ||
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 39300 | Extend class notation with the projective space function. |
class ℙ𝕣𝕠𝕛 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |