Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2sqmod Structured version   Visualization version   GIF version

Theorem 2sqmod 29949
Description: Given two decompositions of a prime as a sum of two squares, show that they are equal. (Contributed by Thierry Arnoux, 2-Feb-2020.)
Hypotheses
Ref Expression
2sqmod.1 (𝜑𝑃 ∈ ℙ)
2sqmod.2 (𝜑𝐴 ∈ ℕ0)
2sqmod.3 (𝜑𝐵 ∈ ℕ0)
2sqmod.4 (𝜑𝐶 ∈ ℕ0)
2sqmod.5 (𝜑𝐷 ∈ ℕ0)
2sqmod.6 (𝜑𝐴𝐵)
2sqmod.7 (𝜑𝐶𝐷)
2sqmod.8 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃)
2sqmod.9 (𝜑 → ((𝐶↑2) + (𝐷↑2)) = 𝑃)
Assertion
Ref Expression
2sqmod (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))

Proof of Theorem 2sqmod
StepHypRef Expression
1 2sqmod.6 . . . . . 6 (𝜑𝐴𝐵)
21adantr 472 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐵)
3 2sqmod.4 . . . . . . . 8 (𝜑𝐶 ∈ ℕ0)
43nn0red 11536 . . . . . . 7 (𝜑𝐶 ∈ ℝ)
54adantr 472 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 ∈ ℝ)
6 2sqmod.3 . . . . . . . 8 (𝜑𝐵 ∈ ℕ0)
76nn0red 11536 . . . . . . 7 (𝜑𝐵 ∈ ℝ)
87adantr 472 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∈ ℝ)
93nn0ge0d 11538 . . . . . . 7 (𝜑 → 0 ≤ 𝐶)
109adantr 472 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐶)
116nn0ge0d 11538 . . . . . . 7 (𝜑 → 0 ≤ 𝐵)
1211adantr 472 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐵)
133nn0cnd 11537 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1413sqcld 13192 . . . . . . . 8 (𝜑 → (𝐶↑2) ∈ ℂ)
1514adantr 472 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) ∈ ℂ)
166nn0cnd 11537 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
1716sqcld 13192 . . . . . . . 8 (𝜑 → (𝐵↑2) ∈ ℂ)
1817adantr 472 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ)
19 2sqmod.2 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℕ0)
2019nn0cnd 11537 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
2120sqcld 13192 . . . . . . . . . . 11 (𝜑 → (𝐴↑2) ∈ ℂ)
22 2sqmod.5 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ ℕ0)
2322nn0cnd 11537 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℂ)
2423sqcld 13192 . . . . . . . . . . 11 (𝜑 → (𝐷↑2) ∈ ℂ)
25 2sqmod.8 . . . . . . . . . . . 12 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃)
26 2sqmod.9 . . . . . . . . . . . 12 (𝜑 → ((𝐶↑2) + (𝐷↑2)) = 𝑃)
2725, 26eqtr4d 2789 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = ((𝐶↑2) + (𝐷↑2)))
2821, 17, 14, 24, 27subaddeqd 10630 . . . . . . . . . 10 (𝜑 → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2)))
2928adantr 472 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2)))
3019nn0zd 11664 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℤ)
313nn0zd 11664 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℤ)
32 dvdsmul1 15197 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐶))
3330, 31, 32syl2anc 696 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∥ (𝐴 · 𝐶))
3433adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐴 · 𝐶))
3520, 13mulcld 10244 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
3635adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) ∈ ℂ)
3716, 23mulcld 10244 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
3837adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 · 𝐷) ∈ ℂ)
3919nn0red 11536 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
4039, 4remulcld 10254 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 · 𝐶) ∈ ℝ)
4122nn0red 11536 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷 ∈ ℝ)
427, 41remulcld 10254 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 · 𝐷) ∈ ℝ)
4340, 42resubcld 10642 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℝ)
4443recnd 10252 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ)
4544adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ)
4643sqge0d 13222 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2))
47 2sqmod.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑃 ∈ ℙ)
486nn0zd 11664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐵 ∈ ℤ)
4947, 30, 48, 252sqn0 29947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐴 ≠ 0)
50 elnnne0 11490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐴 ∈ ℕ ↔ (𝐴 ∈ ℕ0𝐴 ≠ 0))
5119, 49, 50sylanbrc 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐴 ∈ ℕ)
5222nn0zd 11664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐷 ∈ ℤ)
5324, 14addcomd 10422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((𝐷↑2) + (𝐶↑2)) = ((𝐶↑2) + (𝐷↑2)))
5453, 26eqtrd 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝐷↑2) + (𝐶↑2)) = 𝑃)
5547, 52, 31, 542sqn0 29947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐷 ≠ 0)
56 elnnne0 11490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐷 ∈ ℕ ↔ (𝐷 ∈ ℕ0𝐷 ≠ 0))
5722, 55, 56sylanbrc 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 ∈ ℕ)
5851, 57nnmulcld 11252 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 · 𝐷) ∈ ℕ)
5947, 31, 52, 262sqn0 29947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐶 ≠ 0)
60 elnnne0 11490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐶 ∈ ℕ ↔ (𝐶 ∈ ℕ0𝐶 ≠ 0))
613, 59, 60sylanbrc 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐶 ∈ ℕ)
6217, 21addcomd 10422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((𝐵↑2) + (𝐴↑2)) = ((𝐴↑2) + (𝐵↑2)))
6362, 25eqtrd 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝐵↑2) + (𝐴↑2)) = 𝑃)
6447, 48, 30, 632sqn0 29947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ≠ 0)
65 elnnne0 11490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ ℕ ↔ (𝐵 ∈ ℕ0𝐵 ≠ 0))
666, 64, 65sylanbrc 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ ℕ)
6761, 66nnmulcld 11252 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐶 · 𝐵) ∈ ℕ)
6858, 67nnaddcld 11251 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℕ)
6968nnsqcld 13215 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ)
7069nnred 11219 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℝ)
7143resqcld 13221 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℝ)
7270, 71addge02d 10800 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
7346, 72mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
7425, 26oveq12d 6823 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = (𝑃 · 𝑃))
75 bhmafibid1 29945 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
7639, 7, 4, 41, 75syl22anc 1474 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
7774, 76eqtr3d 2788 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
78 prmz 15583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
7947, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑃 ∈ ℤ)
8079zcnd 11667 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℂ)
8180sqvald 13191 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑2) = (𝑃 · 𝑃))
8213, 16mulcomd 10245 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
8382oveq2d 6821 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
8483oveq1d 6820 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))
8584oveq2d 6821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
8677, 81, 853eqtr4d 2796 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
8773, 86breqtrrd 4824 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2))
8887adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2))
8930, 52zmulcld 11672 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 · 𝐷) ∈ ℤ)
9031, 48zmulcld 11672 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐶 · 𝐵) ∈ ℤ)
9189, 90zaddcld 11670 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ)
92 dvdssqim 15467 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9379, 91, 92syl2anc 696 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
94 zsqcl 13120 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℤ → (𝑃↑2) ∈ ℤ)
9579, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑2) ∈ ℤ)
96 dvdsle 15226 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃↑2) ∈ ℤ ∧ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9795, 69, 96syl2anc 696 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9893, 97syld 47 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9998imp 444 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))
10095zred 11666 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) ∈ ℝ)
10170, 100letri3d 10363 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
102101adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
10388, 99, 102mpbir2and 995 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2))
10486adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
105103, 104eqtr2d 2787 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))
10670recnd 10252 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℂ)
10771recnd 10252 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℂ)
108106, 106, 107subadd2d 10595 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
109108adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
110105, 109mpbird 247 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2))
111106subidd 10564 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0)
112111adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0)
113110, 112eqtr3d 2788 . . . . . . . . . . . . . . . 16 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) = 0)
11445, 113sqeq0d 13193 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) = 0)
11536, 38, 114subeq0d 10584 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) = (𝐵 · 𝐷))
11634, 115breqtrd 4822 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐵 · 𝐷))
11747, 30, 48, 252sqcoprm 29948 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 gcd 𝐵) = 1)
118117adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 gcd 𝐵) = 1)
119 coprmdvds 15560 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
12030, 48, 52, 119syl3anc 1473 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
121120adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
122116, 118, 121mp2and 717 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐷)
123 dvdsle 15226 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐴𝐷𝐴𝐷))
12430, 57, 123syl2anc 696 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐷𝐴𝐷))
125124adantr 472 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴𝐷𝐴𝐷))
126122, 125mpd 15 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐷)
12751nnrpd 12055 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ+)
128127rprege0d 12064 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
12922nn0ge0d 11538 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ 𝐷)
130 le2sq 13124 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷)) → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
131128, 41, 129, 130syl12anc 1471 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
132131adantr 472 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
133126, 132mpbid 222 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ≤ (𝐷↑2))
13451nnsqcld 13215 . . . . . . . . . . . . 13 (𝜑 → (𝐴↑2) ∈ ℕ)
135134nnred 11219 . . . . . . . . . . . 12 (𝜑 → (𝐴↑2) ∈ ℝ)
136 zsqcl 13120 . . . . . . . . . . . . . 14 (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
13752, 136syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐷↑2) ∈ ℤ)
138137zred 11666 . . . . . . . . . . . 12 (𝜑 → (𝐷↑2) ∈ ℝ)
139135, 138suble0d 10802 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2)))
140139adantr 472 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2)))
141133, 140mpbird 247 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) ≤ 0)
14229, 141eqbrtrrd 4820 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) ≤ 0)
143 dvdsmul1 15197 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → 𝐵 ∥ (𝐵 · 𝐷))
14448, 52, 143syl2anc 696 . . . . . . . . . . . . . 14 (𝜑𝐵 ∥ (𝐵 · 𝐷))
145144adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐵 · 𝐷))
146145, 115breqtrrd 4824 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐴 · 𝐶))
147 gcdcom 15429 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
14830, 48, 147syl2anc 696 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
149148, 117eqtr3d 2788 . . . . . . . . . . . . 13 (𝜑 → (𝐵 gcd 𝐴) = 1)
150149adantr 472 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 gcd 𝐴) = 1)
151 coprmdvds 15560 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
15248, 30, 31, 151syl3anc 1473 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
153152adantr 472 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
154146, 150, 153mp2and 717 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵𝐶)
155 dvdsle 15226 . . . . . . . . . . . . 13 ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) → (𝐵𝐶𝐵𝐶))
15648, 61, 155syl2anc 696 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐶𝐵𝐶))
157156adantr 472 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵𝐶𝐵𝐶))
158154, 157mpd 15 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵𝐶)
1597, 4, 11, 9le2sqd 13230 . . . . . . . . . . 11 (𝜑 → (𝐵𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2)))
160159adantr 472 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2)))
161158, 160mpbid 222 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ≤ (𝐶↑2))
1624resqcld 13221 . . . . . . . . . . 11 (𝜑 → (𝐶↑2) ∈ ℝ)
163 zsqcl 13120 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
16448, 163syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵↑2) ∈ ℤ)
165164zred 11666 . . . . . . . . . . 11 (𝜑 → (𝐵↑2) ∈ ℝ)
166162, 165subge0d 10801 . . . . . . . . . 10 (𝜑 → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2)))
167166adantr 472 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2)))
168161, 167mpbird 247 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐶↑2) − (𝐵↑2)))
169135, 138resubcld 10642 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) − (𝐷↑2)) ∈ ℝ)
17028, 169eqeltrrd 2832 . . . . . . . . . 10 (𝜑 → ((𝐶↑2) − (𝐵↑2)) ∈ ℝ)
171 0red 10225 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
172170, 171letri3d 10363 . . . . . . . . 9 (𝜑 → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2)))))
173172adantr 472 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2)))))
174142, 168, 173mpbir2and 995 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) = 0)
17515, 18, 174subeq0d 10584 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) = (𝐵↑2))
1765, 8, 10, 12, 175sq11d 13231 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 = 𝐵)
1772, 176breqtrrd 4824 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐶)
178 2sqmod.7 . . . . . 6 (𝜑𝐶𝐷)
179178adantr 472 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶𝐷)
18039adantr 472 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∈ ℝ)
18141adantr 472 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐷 ∈ ℝ)
18219nn0ge0d 11538 . . . . . . 7 (𝜑 → 0 ≤ 𝐴)
183182adantr 472 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐴)
184129adantr 472 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐷)
18521adantr 472 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ∈ ℂ)
18624adantr 472 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ)
187168, 29breqtrrd 4824 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐴↑2) − (𝐷↑2)))
188169, 171letri3d 10363 . . . . . . . . 9 (𝜑 → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2)))))
189188adantr 472 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2)))))
190141, 187, 189mpbir2and 995 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = 0)
191185, 186, 190subeq0d 10584 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) = (𝐷↑2))
192180, 181, 183, 184, 191sq11d 13231 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐷)
193179, 192breqtrrd 4824 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶𝐴)
19439, 4letri3d 10363 . . . . 5 (𝜑 → (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴)))
195194adantr 472 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴)))
196177, 193, 195mpbir2and 995 . . 3 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐶)
19720adantr 472 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 ∈ ℂ)
19813adantr 472 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐶 ∈ ℂ)
19916adantr 472 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℂ)
20064adantr 472 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ≠ 0)
20141adantr 472 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 ∈ ℝ)
2027adantr 472 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℝ)
203129adantr 472 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐷)
20411adantr 472 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐵)
20524adantr 472 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ)
20617adantr 472 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ)
207 prmnn 15582 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
20847, 207syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℕ)
209208nnne0d 11249 . . . . . . . . . . 11 (𝜑𝑃 ≠ 0)
210209neneqd 2929 . . . . . . . . . 10 (𝜑 → ¬ 𝑃 = 0)
211210adantr 472 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ¬ 𝑃 = 0)
21280, 24, 17subdid 10670 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))))
21380, 24mulcld 10244 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 · (𝐷↑2)) ∈ ℂ)
21421, 24mulcld 10244 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴↑2) · (𝐷↑2)) ∈ ℂ)
21580, 17mulcld 10244 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 · (𝐵↑2)) ∈ ℂ)
21614, 17mulcld 10244 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶↑2) · (𝐵↑2)) ∈ ℂ)
21717, 24mulcomd 10245 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵↑2) · (𝐷↑2)) = ((𝐷↑2) · (𝐵↑2)))
21825oveq1d 6820 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝑃 − (𝐴↑2)))
21921, 17pncan2d 10578 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝐵↑2))
220218, 219eqtr3d 2788 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 − (𝐴↑2)) = (𝐵↑2))
221220oveq1d 6820 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝐵↑2) · (𝐷↑2)))
22226oveq1d 6820 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝑃 − (𝐶↑2)))
22314, 24pncan2d 10578 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝐷↑2))
224222, 223eqtr3d 2788 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 − (𝐶↑2)) = (𝐷↑2))
225224oveq1d 6820 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝐷↑2) · (𝐵↑2)))
226217, 221, 2253eqtr4d 2796 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 − (𝐶↑2)) · (𝐵↑2)))
22780, 21, 24subdird 10671 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))))
22880, 14, 17subdird 10671 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2))))
229226, 227, 2283eqtr3d 2794 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2))))
230213, 214, 215, 216, 229subeqxfrd 29812 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
231212, 230eqtrd 2786 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
23220, 23sqmuld 13206 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐷)↑2) = ((𝐴↑2) · (𝐷↑2)))
23313, 16sqmuld 13206 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵)↑2) = ((𝐶↑2) · (𝐵↑2)))
234232, 233oveq12d 6823 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
23520, 23mulcld 10244 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
23613, 16mulcld 10244 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 · 𝐵) ∈ ℂ)
237 subsq 13158 . . . . . . . . . . . . . . 15 (((𝐴 · 𝐷) ∈ ℂ ∧ (𝐶 · 𝐵) ∈ ℂ) → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
238235, 236, 237syl2anc 696 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
239231, 234, 2383eqtr2d 2792 . . . . . . . . . . . . 13 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
240239adantr 472 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
241235adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) ∈ ℂ)
242 simpll 807 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → 𝜑)
243 simpr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵))
244243neqned 2931 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵))
24589, 90zsubcld 11671 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ)
246 dvdssqim 15467 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
24779, 245, 246syl2anc 696 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
248247imp 444 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
249248adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
25095adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝑃↑2) ∈ ℤ)
251245adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ)
252235adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ∈ ℂ)
253236adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐶 · 𝐵) ∈ ℂ)
254 simpr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵))
255252, 253, 254subne0d 10585 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ≠ 0)
256251, 255znsqcld 29813 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ)
257 dvdsle 15226 . . . . . . . . . . . . . . . . . 18 (((𝑃↑2) ∈ ℤ ∧ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
258250, 256, 257syl2anc 696 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
259258imp 444 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) ∧ (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
260242, 244, 249, 259syl21anc 1472 . . . . . . . . . . . . . . 15 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
26139, 41remulcld 10254 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐷) ∈ ℝ)
2624, 7remulcld 10254 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐶 · 𝐵) ∈ ℝ)
263261, 262resubcld 10642 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℝ)
264263resqcld 13221 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℝ)
26561nnrpd 12055 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐶 ∈ ℝ+)
266127, 265rpmulcld 12073 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐶) ∈ ℝ+)
26766nnrpd 12055 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ+)
26857nnrpd 12055 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐷 ∈ ℝ+)
269267, 268rpmulcld 12073 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐵 · 𝐷) ∈ ℝ+)
270266, 269rpaddcld 12072 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 · 𝐶) + (𝐵 · 𝐷)) ∈ ℝ+)
271 2z 11593 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℤ
272271a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℤ)
273270, 272rpexpcld 13218 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) ∈ ℝ+)
274264, 273ltaddrp2d 12091 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
275 bhmafibid2 29946 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27639, 7, 4, 41, 275syl22anc 1474 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27774, 276eqtr3d 2788 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27882oveq2d 6821 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = ((𝐴 · 𝐷) − (𝐵 · 𝐶)))
279278oveq1d 6820 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))
280279oveq2d 6821 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
281277, 280eqtr4d 2789 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
282274, 281breqtrrd 4824 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃 · 𝑃))
283282, 81breqtrrd 4824 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2))
284242, 283syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2))
285264, 100ltnled 10368 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
286242, 285syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
287284, 286mpbid 222 . . . . . . . . . . . . . . 15 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
288260, 287condan 870 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐶 · 𝐵))
289241, 288subeq0bd 10640 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = 0)
290289oveq2d 6821 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0))
291235, 236addcld 10243 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℂ)
292291mul01d 10419 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0)
293292adantr 472 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0)
294240, 290, 2933eqtrd 2790 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0)
29524, 17subcld 10576 . . . . . . . . . . . . 13 (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℂ)
29680, 295mul0ord 10861 . . . . . . . . . . . 12 (𝜑 → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)))
297296adantr 472 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)))
298294, 297mpbid 222 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0))
299298ord 391 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (¬ 𝑃 = 0 → ((𝐷↑2) − (𝐵↑2)) = 0))
300211, 299mpd 15 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐷↑2) − (𝐵↑2)) = 0)
301205, 206, 300subeq0d 10584 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) = (𝐵↑2))
302201, 202, 203, 204, 301sq11d 13231 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 = 𝐵)
303302oveq2d 6821 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐴 · 𝐵))
304303, 288eqtr3d 2788 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐵) = (𝐶 · 𝐵))
305197, 198, 199, 200, 304mulcan2ad 10847 . . 3 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 = 𝐶)
306137, 164zsubcld 11671 . . . . . 6 (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℤ)
307 dvdsmul1 15197 . . . . . 6 ((𝑃 ∈ ℤ ∧ ((𝐷↑2) − (𝐵↑2)) ∈ ℤ) → 𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2))))
30879, 306, 307syl2anc 696 . . . . 5 (𝜑𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2))))
309308, 239breqtrd 4822 . . . 4 (𝜑𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
310 euclemma 15619 . . . . 5 ((𝑃 ∈ ℙ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))))
31147, 91, 245, 310syl3anc 1473 . . . 4 (𝜑 → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))))
312309, 311mpbid 222 . . 3 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
313196, 305, 312mpjaodan 862 . 2 (𝜑𝐴 = 𝐶)
314313oveq1d 6820 . . . . 5 (𝜑 → (𝐴↑2) = (𝐶↑2))
315314oveq2d 6821 . . . 4 (𝜑 → (𝑃 − (𝐴↑2)) = (𝑃 − (𝐶↑2)))
316315, 220, 2243eqtr3d 2794 . . 3 (𝜑 → (𝐵↑2) = (𝐷↑2))
3177, 41, 11, 129, 316sq11d 13231 . 2 (𝜑𝐵 = 𝐷)
318313, 317jca 555 1 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1624  wcel 2131  wne 2924   class class class wbr 4796  (class class class)co 6805  cc 10118  cr 10119  0cc0 10120  1c1 10121   + caddc 10123   · cmul 10125   < clt 10258  cle 10259  cmin 10450  cn 11204  2c2 11254  0cn0 11476  cz 11561  cexp 13046  cdvds 15174   gcd cgcd 15410  cprime 15579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-om 7223  df-2nd 7326  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-2o 7722  df-er 7903  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-sup 8505  df-inf 8506  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-n0 11477  df-z 11562  df-uz 11872  df-rp 12018  df-fl 12779  df-mod 12855  df-seq 12988  df-exp 13047  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-dvds 15175  df-gcd 15411  df-prm 15580
This theorem is referenced by:  2sqmo  29950
  Copyright terms: Public domain W3C validator