![]() |
Metamath
Proof Explorer Theorem List (p. 423 of 486) | < 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-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sn-addcan2d 42201 | addcan2d 11468 without ax-mulcom 11222. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | reixi 42202 | ixi 11893 without ax-mulcom 11222. (Contributed by SN, 5-May-2024.) |
⊢ (i · i) = (0 −ℝ 1) | ||
Theorem | rei4 42203 | i4 14222 without ax-mulcom 11222. (Contributed by SN, 27-May-2024.) |
⊢ ((i · i) · (i · i)) = 1 | ||
Theorem | sn-addid0 42204 | A number that sums to itself is zero. Compare addid0 11683, readdridaddlidd 42078. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐴) = 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
Theorem | sn-mul01 42205 | mul01 11443 without ax-mulcom 11222. (Contributed by SN, 5-May-2024.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0) | ||
Theorem | sn-subeu 42206* | negeu 11500 without ax-mulcom 11222 and complex number version of resubeu 42157. (Contributed by SN, 5-May-2024.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵) | ||
Theorem | sn-subcl 42207 | subcl 11509 without ax-mulcom 11222. (Contributed by SN, 5-May-2024.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) | ||
Theorem | sn-subf 42208 | subf 11512 without ax-mulcom 11222. (Contributed by SN, 5-May-2024.) |
⊢ − :(ℂ × ℂ)⟶ℂ | ||
Theorem | resubeqsub 42209 | Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (𝐴 − 𝐵)) | ||
Theorem | subresre 42210 | Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.) |
⊢ −ℝ = ( − ↾ (ℝ × ℝ)) | ||
Theorem | addinvcom 42211 | A number commutes with its additive inverse. Compare remulinvcom 42212. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 0) ⇒ ⊢ (𝜑 → (𝐵 + 𝐴) = 0) | ||
Theorem | remulinvcom 42212 | A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 11222. (Contributed by SN, 5-Feb-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) = 1) | ||
Theorem | remullid 42213 | Commuted version of ax-1rid 11228 without ax-mulcom 11222. (Contributed by SN, 5-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴) | ||
Theorem | sn-1ticom 42214 | Lemma for sn-mullid 42215 and sn-it1ei 42216. (Contributed by SN, 27-May-2024.) |
⊢ (1 · i) = (i · 1) | ||
Theorem | sn-mullid 42215 | mullid 11263 without ax-mulcom 11222. (Contributed by SN, 27-May-2024.) |
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | ||
Theorem | sn-it1ei 42216 | it1ei 42116 without ax-mulcom 11222. (See sn-mullid 42215 for commuted version). (Contributed by SN, 1-Jun-2024.) |
⊢ (i · 1) = i | ||
Theorem | ipiiie0 42217 | The multiplicative inverse of i (per i4 14222) is also its additive inverse. (Contributed by SN, 30-Jun-2024.) |
⊢ (i + (i · (i · i))) = 0 | ||
Theorem | remulcand 42218 | Commuted version of remulcan2d 42077 without ax-mulcom 11222. (Contributed by SN, 21-Feb-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | sn-0tie0 42219 | Lemma for sn-mul02 42220. Commuted version of sn-it0e0 42195. (Contributed by SN, 30-Jun-2024.) |
⊢ (0 · i) = 0 | ||
Theorem | sn-mul02 42220 | mul02 11442 without ax-mulcom 11222. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 11222 for an outline. (Contributed by SN, 30-Jun-2024.) |
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) | ||
Theorem | sn-ltaddpos 42221 | ltaddpos 11754 without ax-mulcom 11222. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))) | ||
Theorem | sn-ltaddneg 42222 | ltaddneg 11479 without ax-mulcom 11222. (Contributed by SN, 25-Jan-2025.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵)) | ||
Theorem | reposdif 42223 | Comparison of two numbers whose difference is positive. Compare posdif 11757. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 −ℝ 𝐴))) | ||
Theorem | relt0neg1 42224 | Comparison of a real and its negative to zero. Compare lt0neg1 11770. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < (0 −ℝ 𝐴))) | ||
Theorem | relt0neg2 42225 | Comparison of a real and its negative to zero. Compare lt0neg2 11771. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (0 −ℝ 𝐴) < 0)) | ||
Theorem | sn-addlt0d 42226 | The sum of negative numbers is negative. (Contributed by SN, 25-Jan-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) & ⊢ (𝜑 → 𝐵 < 0) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < 0) | ||
Theorem | sn-addgt0d 42227 | The sum of positive numbers is positive. Proof of addgt0d 11839 without ax-mulcom 11222. (Contributed by SN, 25-Jan-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 + 𝐵)) | ||
Theorem | sn-nnne0 42228 | nnne0 12298 without ax-mulcom 11222. (Contributed by SN, 25-Jan-2025.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) | ||
Theorem | reelznn0nn 42229 | elznn0nn 12624 restated using df-resub 42146. (Contributed by SN, 25-Jan-2025.) |
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ (0 −ℝ 𝑁) ∈ ℕ))) | ||
Theorem | nn0addcom 42230 | Addition is commutative for nonnegative integers. Proven without ax-mulcom 11222. (Contributed by SN, 1-Feb-2025.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | zaddcomlem 42231 | Lemma for zaddcom 42232. (Contributed by SN, 1-Feb-2025.) |
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | zaddcom 42232 | Addition is commutative for integers. Proven without ax-mulcom 11222. (Contributed by SN, 25-Jan-2025.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | renegmulnnass 42233 | Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((0 −ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁))) | ||
Theorem | nn0mulcom 42234 | Multiplication is commutative for nonnegative integers. Proven without ax-mulcom 11222. (Contributed by SN, 25-Jan-2025.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | zmulcomlem 42235 | Lemma for zmulcom 42236. (Contributed by SN, 25-Jan-2025.) |
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | zmulcom 42236 | Multiplication is commutative for integers. Proven without ax-mulcom 11222. From this result and grpcominv1 41987, we can show that rationals commute under multiplication without using ax-mulcom 11222. (Contributed by SN, 25-Jan-2025.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | mulgt0con1dlem 42237 | Lemma for mulgt0con1d 42238. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (0 < 𝐴 → 0 < 𝐵)) & ⊢ (𝜑 → (𝐴 = 0 → 𝐵 = 0)) ⇒ ⊢ (𝜑 → (𝐵 < 0 → 𝐴 < 0)) | ||
Theorem | mulgt0con1d 42238 | Counterpart to mulgt0con2d 42239, though not a lemma of anything. This is the first use of ax-pre-mulgt0 11235. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐵) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ (𝜑 → 𝐴 < 0) | ||
Theorem | mulgt0con2d 42239 | Lemma for mulgt0b2d 42240 and contrapositive of mulgt0 11341. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ (𝜑 → 𝐵 < 0) | ||
Theorem | mulgt0b2d 42240 | Biconditional, deductive form of mulgt0 11341. The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi 42176 does not have a commuted form. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵))) | ||
Theorem | sn-ltmul2d 42241 | ltmul2d 13112 without ax-mulcom 11222. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐶) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) < (𝐶 · 𝐵) ↔ 𝐴 < 𝐵)) | ||
Theorem | sn-ltmulgt11d 42242 | ltmulgt11d 13105 without ax-mulcom 11222. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴))) | ||
Theorem | sn-0lt1 42243 | 0lt1 11786 without ax-mulcom 11222. (Contributed by SN, 13-Feb-2024.) |
⊢ 0 < 1 | ||
Theorem | sn-ltp1 42244 | ltp1 12105 without ax-mulcom 11222. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1)) | ||
Theorem | sn-mulgt1d 42245 | mulgt1d 12202 without ax-mulcom 11222. (Contributed by SN, 26-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 1 < 𝐵) ⇒ ⊢ (𝜑 → 1 < (𝐴 · 𝐵)) | ||
Theorem | reneg1lt0 42246 | Lemma for sn-inelr 42247. (Contributed by SN, 1-Jun-2024.) |
⊢ (0 −ℝ 1) < 0 | ||
Theorem | sn-inelr 42247 | inelr 12254 without ax-mulcom 11222. (Contributed by SN, 1-Jun-2024.) |
⊢ ¬ i ∈ ℝ | ||
Theorem | sn-itrere 42248 | i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024.) |
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0)) | ||
Theorem | sn-retire 42249 | Commuted version of sn-itrere 42248. (Contributed by SN, 27-Jun-2024.) |
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0)) | ||
Theorem | cnreeu 42250 | The reals in the expression given by cnre 11261 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.) |
⊢ (𝜑 → 𝑟 ∈ ℝ) & ⊢ (𝜑 → 𝑠 ∈ ℝ) & ⊢ (𝜑 → 𝑡 ∈ ℝ) & ⊢ (𝜑 → 𝑢 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) ↔ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))) | ||
Theorem | sn-sup2 42251* | sup2 12222 with exactly the same proof except for using sn-ltp1 42244 instead of ltp1 12105, saving ax-mulcom 11222. (Contributed by SN, 26-Jun-2024.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | sn-sup3d 42252* | sup3 12223 without ax-mulcom 11222, proven trivially from sn-sup2 42251. (Contributed by SN, 29-Jun-2025.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | sn-suprcld 42253* | suprcld 12229 without ax-mulcom 11222, proven trivially from sn-sup3d 42252. (Contributed by SN, 29-Jun-2025.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ) | ||
Theorem | sn-suprubd 42254* | suprubd 12228 without ax-mulcom 11222, proven trivially from sn-suprcld 42253. (Contributed by SN, 29-Jun-2025.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < )) | ||
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 42255 | Extend class notation with the projective space function. |
class ℙ𝕣𝕠𝕛 | ||
Definition | df-prjsp 42256* | 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, making equivalent rational multiples of real numbers). Compare df-lsatoms 38674. (Contributed by BJ and SN, 29-Apr-2023.) |
⊢ ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})) | ||
Theorem | prjspval 42257* | 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 42258* | Utility theorem regarding the relation used in ℙ𝕣𝕠𝕛. (Contributed by Steven Nguyen, 29-Apr-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} ⇒ ⊢ (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌))) | ||
Theorem | prjspertr 42259* | The relation in ℙ𝕣𝕠𝕛 is transitive. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ ((𝑉 ∈ LMod ∧ (𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍)) → 𝑋 ∼ 𝑍) | ||
Theorem | prjsperref 42260* | The relation in ℙ𝕣𝕠𝕛 is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑉 ∈ LMod → (𝑋 ∈ 𝐵 ↔ 𝑋 ∼ 𝑋)) | ||
Theorem | prjspersym 42261* | The relation in ℙ𝕣𝕠𝕛 is symmetric. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) → 𝑌 ∼ 𝑋) | ||
Theorem | prjsper 42262* | The relation used to define ℙ𝕣𝕠𝕛 is an equivalence relation. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑉 ∈ LVec → ∼ Er 𝐵) | ||
Theorem | prjspreln0 42263* | Two nonzero vectors are equivalent by a nonzero scalar. (Contributed by Steven Nguyen, 31-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ (𝑉 ∈ LVec → (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑚 · 𝑌)))) | ||
Theorem | prjspvs 42264* | A nonzero multiple of a vector is equivalent to the vector. (Contributed by Steven Nguyen, 6-Jun-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ (𝐾 ∖ { 0 })) → (𝑁 · 𝑋) ∼ 𝑋) | ||
Theorem | prjsprellsp 42265* | Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑁 = (LSpan‘𝑉) ⇒ ⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∼ 𝑌 ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) | ||
Theorem | prjspeclsp 42266* | The vectors equivalent to a vector 𝑋 are the nonzero vectors in the span of 𝑋. (Contributed by Steven Nguyen, 6-Jun-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑁 = (LSpan‘𝑉) ⇒ ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → [𝑋] ∼ = ((𝑁‘{𝑋}) ∖ {(0g‘𝑉)})) | ||
Theorem | prjspval2 42267* | Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ 0 = (0g‘𝑉) & ⊢ 𝐵 = ((Base‘𝑉) ∖ { 0 }) & ⊢ 𝑁 = (LSpan‘𝑉) ⇒ ⊢ (𝑉 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑉) = ∪ 𝑧 ∈ 𝐵 {((𝑁‘{𝑧}) ∖ { 0 })}) | ||
Syntax | cprjspn 42268 | Extend class notation with the n-dimensional projective space function. |
class ℙ𝕣𝕠𝕛n | ||
Definition | df-prjspn 42269* | Define the n-dimensional projective space function. A projective space of dimension 1 is a projective line, and a projective space of dimension 2 is a projective plane. Compare df-ehl 25405. This space is considered n-dimensional because the vector space (𝑘 freeLMod (0...𝑛)) is (n+1)-dimensional and the ℙ𝕣𝕠𝕛 function returns equivalence classes with respect to a linear (1-dimensional) relation. (Contributed by BJ and Steven Nguyen, 29-Apr-2023.) |
⊢ ℙ𝕣𝕠𝕛n = (𝑛 ∈ ℕ0, 𝑘 ∈ DivRing ↦ (ℙ𝕣𝕠𝕛‘(𝑘 freeLMod (0...𝑛)))) | ||
Theorem | prjspnval 42270 | Value of the n-dimensional projective space function. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛n𝐾) = (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁)))) | ||
Theorem | prjspnerlem 42271* | A lemma showing that the equivalence relation used in prjspnval2 42272 and the equivalence relation used in prjspval 42257 are equal, but only with the antecedent 𝐾 ∈ DivRing. (Contributed by SN, 15-Jul-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ (𝐾 ∈ DivRing → ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))}) | ||
Theorem | prjspnval2 42272* | Value of the n-dimensional projective space function, expanded. (Contributed by Steven Nguyen, 15-Jul-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛n𝐾) = (𝐵 / ∼ )) | ||
Theorem | prjspner 42273* | The relation used to define ℙ𝕣𝕠𝕛 (and indirectly ℙ𝕣𝕠𝕛n through df-prjspn 42269) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr 42259 and prjspersym 42261 (see prjspnerlem 42271). Several theorems are covered in one thanks to the theorems around df-er 8734. (Contributed by SN, 14-Aug-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ (𝜑 → 𝐾 ∈ DivRing) ⇒ ⊢ (𝜑 → ∼ Er 𝐵) | ||
Theorem | prjspnvs 42274* | A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs 42264 (see prjspnerlem 42271). (Contributed by SN, 8-Aug-2024.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐶 · 𝑋) ∼ 𝑋) | ||
Theorem | prjspnssbas 42275 | A projective point spans a subset of the (nonzero) affine points. (Contributed by SN, 17-Jan-2025.) |
⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾) & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑃 ⊆ 𝒫 𝐵) | ||
Theorem | prjspnn0 42276 | A projective point is nonempty. (Contributed by SN, 17-Jan-2025.) |
⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾) & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) | ||
Theorem | 0prjspnlem 42277 | Lemma for 0prjspn 42282. The given unit vector is a nonzero vector. (Contributed by Steven Nguyen, 16-Jul-2023.) |
⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑊 = (𝐾 freeLMod (0...0)) & ⊢ 1 = ((𝐾 unitVec (0...0))‘0) ⇒ ⊢ (𝐾 ∈ DivRing → 1 ∈ 𝐵) | ||
Theorem | prjspnfv01 42278* | Any vector is equivalent to a vector whose zeroth coordinate is 0 or 1 (proof of the value of the zeroth coordinate). (Contributed by SN, 13-Aug-2023.) |
⊢ 𝐹 = (𝑏 ∈ 𝐵 ↦ if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏))) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐾) & ⊢ 1 = (1r‘𝐾) & ⊢ 𝐼 = (invr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹‘𝑋)‘0) = if((𝑋‘0) = 0 , 0 , 1 )) | ||
Theorem | prjspner01 42279* | Any vector is equivalent to a vector whose zeroth coordinate is 0 or 1 (proof of the equivalence). (Contributed by SN, 13-Aug-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐹 = (𝑏 ∈ 𝐵 ↦ if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏))) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ 0 = (0g‘𝐾) & ⊢ 𝐼 = (invr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 ∼ (𝐹‘𝑋)) | ||
Theorem | prjspner1 42280* | Two vectors whose zeroth coordinate is nonzero are equivalent if and only if they have the same representative in the (n-1)-dimensional affine subspace { x0 = 1 } . For example, vectors in 3D space whose 𝑥 coordinate is nonzero are equivalent iff they intersect at the plane 𝑥 = 1 at the same point (also see section header). (Contributed by SN, 13-Aug-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐹 = (𝑏 ∈ 𝐵 ↦ if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏))) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ 0 = (0g‘𝐾) & ⊢ 𝐼 = (invr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋‘0) ≠ 0 ) & ⊢ (𝜑 → (𝑌‘0) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 ∼ 𝑌 ↔ (𝐹‘𝑋) = (𝐹‘𝑌))) | ||
Theorem | 0prjspnrel 42281* | In the zero-dimensional projective space, all vectors are equivalent to the unit vector. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ 𝑊 = (𝐾 freeLMod (0...0)) & ⊢ 1 = ((𝐾 unitVec (0...0))‘0) ⇒ ⊢ ((𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵) → 𝑋 ∼ 1 ) | ||
Theorem | 0prjspn 42282 | A zero-dimensional projective space has only 1 point. (Contributed by Steven Nguyen, 9-Jun-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0...0)) & ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) ⇒ ⊢ (𝐾 ∈ DivRing → (0ℙ𝕣𝕠𝕛n𝐾) = {𝐵}) | ||
Syntax | cprjcrv 42283 | Extend class notation with the projective curve function. |
class ℙ𝕣𝕠𝕛Crv | ||
Definition | df-prjcrv 42284* | Define the projective curve function. This takes a homogeneous polynomial and outputs the homogeneous coordinates where the polynomial evaluates to zero (the "zero set"). (In other words, scalar multiples are collapsed into the same projective point. See mhphf4 42072 and prjspvs 42264). (Contributed by SN, 23-Nov-2024.) |
⊢ ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})) | ||
Theorem | prjcrvfval 42285* | Value of the projective curve function. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝐻 = ((0...𝑁) mHomP 𝐾) & ⊢ 𝐸 = ((0...𝑁) eval 𝐾) & ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾) & ⊢ 0 = (0g‘𝐾) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ Field) ⇒ ⊢ (𝜑 → (𝑁ℙ𝕣𝕠𝕛Crv𝐾) = (𝑓 ∈ ∪ ran 𝐻 ↦ {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝑓) “ 𝑝) = { 0 }})) | ||
Theorem | prjcrvval 42286* | Value of the projective curve function. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝐻 = ((0...𝑁) mHomP 𝐾) & ⊢ 𝐸 = ((0...𝑁) eval 𝐾) & ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾) & ⊢ 0 = (0g‘𝐾) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ ∪ ran 𝐻) ⇒ ⊢ (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘𝐹) = {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝐹) “ 𝑝) = { 0 }}) | ||
Theorem | prjcrv0 42287 | The "curve" (zero set) corresponding to the zero polynomial contains all coordinates. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑌 = ((0...𝑁) mPoly 𝐾) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ Field) ⇒ ⊢ (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘ 0 ) = 𝑃) | ||
Theorem | dffltz 42288* | Fermat's Last Theorem (FLT) for nonzero integers is equivalent to the original scope of natural numbers. The backwards direction takes (𝑎↑𝑛) + (𝑏↑𝑛) = (𝑐↑𝑛), and adds the negative of any negative term to both sides, thus creating the corresponding equation with only positive integers. There are six combinations of negativity, so the proof is particularly long. (Contributed by Steven Nguyen, 27-Feb-2023.) |
⊢ (∀𝑛 ∈ (ℤ≥‘3)∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ∀𝑧 ∈ ℕ ((𝑥↑𝑛) + (𝑦↑𝑛)) ≠ (𝑧↑𝑛) ↔ ∀𝑛 ∈ (ℤ≥‘3)∀𝑎 ∈ (ℤ ∖ {0})∀𝑏 ∈ (ℤ ∖ {0})∀𝑐 ∈ (ℤ ∖ {0})((𝑎↑𝑛) + (𝑏↑𝑛)) ≠ (𝑐↑𝑛)) | ||
Theorem | fltmul 42289 | A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (There does not seem to be a standard term for Fermat or Pythagorean triples extended to any 𝑁 ∈ ℕ0, so the label is more about the context in which this theorem is used). (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → (((𝑆 · 𝐴)↑𝑁) + ((𝑆 · 𝐵)↑𝑁)) = ((𝑆 · 𝐶)↑𝑁)) | ||
Theorem | fltdiv 42290 | A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝑆 ≠ 0) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → (((𝐴 / 𝑆)↑𝑁) + ((𝐵 / 𝑆)↑𝑁)) = ((𝐶 / 𝑆)↑𝑁)) | ||
Theorem | flt0 42291 | A counterexample for FLT does not exist for 𝑁 = 0. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℕ) | ||
Theorem | fltdvdsabdvdsc 42292 | Any factor of both 𝐴 and 𝐵 also divides 𝐶. This establishes the validity of fltabcoprmex 42293. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐶) | ||
Theorem | fltabcoprmex 42293 | A counterexample to FLT implies a counterexample to FLT with 𝐴, 𝐵 (assigned to 𝐴 / (𝐴 gcd 𝐵) and 𝐵 / (𝐴 gcd 𝐵)) coprime (by divgcdcoprm0 16666). (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) + ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = ((𝐶 / (𝐴 gcd 𝐵))↑𝑁)) | ||
Theorem | fltaccoprm 42294 | A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐴, 𝐶 coprime. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) | ||
Theorem | fltbccoprm 42295 | A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐵, 𝐶 coprime. Proven from fltaccoprm 42294 using commutativity of addition. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐵 gcd 𝐶) = 1) | ||
Theorem | fltabcoprm 42296 | A counterexample to FLT with 𝐴, 𝐶 coprime also has 𝐴, 𝐵 coprime. Converse of fltaccoprm 42294. (Contributed by SN, 22-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) | ||
Theorem | infdesc 42297* | Infinite descent. The hypotheses say that 𝑆 is lower bounded, and that if 𝜓 holds for an integer in 𝑆, it holds for a smaller integer in 𝑆. By infinite descent, eventually we cannot go any smaller, therefore 𝜓 holds for no integer in 𝑆. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → 𝑆 ⊆ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝜒)) → ∃𝑧 ∈ 𝑆 (𝜃 ∧ 𝑧 < 𝑥)) ⇒ ⊢ (𝜑 → {𝑦 ∈ 𝑆 ∣ 𝜓} = ∅) | ||
Theorem | fltne 42298 | If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | flt4lem 42299 | Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2)) | ||
Theorem | flt4lem1 42300 | Satisfy the antecedent used in several pythagtrip 16836 lemmas, with 𝐴, 𝐶 coprime rather than 𝐴, 𝐵. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝐴) & ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) ⇒ ⊢ (𝜑 → ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |