MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2sqmod Structured version   Visualization version   GIF version

Theorem 2sqmod 27495
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 480 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐵)
3 2sqmod.4 . . . . . . . 8 (𝜑𝐶 ∈ ℕ0)
43nn0red 12586 . . . . . . 7 (𝜑𝐶 ∈ ℝ)
54adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 ∈ ℝ)
6 2sqmod.3 . . . . . . . 8 (𝜑𝐵 ∈ ℕ0)
76nn0red 12586 . . . . . . 7 (𝜑𝐵 ∈ ℝ)
87adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∈ ℝ)
93nn0ge0d 12588 . . . . . . 7 (𝜑 → 0 ≤ 𝐶)
109adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐶)
116nn0ge0d 12588 . . . . . . 7 (𝜑 → 0 ≤ 𝐵)
1211adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐵)
133nn0cnd 12587 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1413sqcld 14181 . . . . . . . 8 (𝜑 → (𝐶↑2) ∈ ℂ)
1514adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) ∈ ℂ)
166nn0cnd 12587 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
1716sqcld 14181 . . . . . . . 8 (𝜑 → (𝐵↑2) ∈ ℂ)
1817adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ)
19 2sqmod.2 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℕ0)
2019nn0cnd 12587 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
2120sqcld 14181 . . . . . . . . . . 11 (𝜑 → (𝐴↑2) ∈ ℂ)
22 2sqmod.5 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ ℕ0)
2322nn0cnd 12587 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℂ)
2423sqcld 14181 . . . . . . . . . . 11 (𝜑 → (𝐷↑2) ∈ ℂ)
25 2sqmod.8 . . . . . . . . . . . 12 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃)
26 2sqmod.9 . . . . . . . . . . . 12 (𝜑 → ((𝐶↑2) + (𝐷↑2)) = 𝑃)
2725, 26eqtr4d 2778 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = ((𝐶↑2) + (𝐷↑2)))
2821, 17, 14, 24, 27subaddeqd 11676 . . . . . . . . . 10 (𝜑 → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2)))
2928adantr 480 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2)))
3019nn0zd 12637 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℤ)
313nn0zd 12637 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℤ)
32 dvdsmul1 16312 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐶))
3330, 31, 32syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∥ (𝐴 · 𝐶))
3433adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐴 · 𝐶))
3520, 13mulcld 11279 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
3635adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) ∈ ℂ)
3716, 23mulcld 11279 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
3837adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 · 𝐷) ∈ ℂ)
3919nn0red 12586 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
4039, 4remulcld 11289 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 · 𝐶) ∈ ℝ)
4122nn0red 12586 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷 ∈ ℝ)
427, 41remulcld 11289 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 · 𝐷) ∈ ℝ)
4340, 42resubcld 11689 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℝ)
4443recnd 11287 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ)
4544adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ)
4643sqge0d 14174 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2))
47 2sqmod.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑃 ∈ ℙ)
486nn0zd 12637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐵 ∈ ℤ)
4947, 30, 48, 252sqn0 27493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐴 ≠ 0)
50 elnnne0 12538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐴 ∈ ℕ ↔ (𝐴 ∈ ℕ0𝐴 ≠ 0))
5119, 49, 50sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐴 ∈ ℕ)
5222nn0zd 12637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐷 ∈ ℤ)
5324, 14addcomd 11461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((𝐷↑2) + (𝐶↑2)) = ((𝐶↑2) + (𝐷↑2)))
5453, 26eqtrd 2775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝐷↑2) + (𝐶↑2)) = 𝑃)
5547, 52, 31, 542sqn0 27493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐷 ≠ 0)
56 elnnne0 12538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐷 ∈ ℕ ↔ (𝐷 ∈ ℕ0𝐷 ≠ 0))
5722, 55, 56sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 ∈ ℕ)
5851, 57nnmulcld 12317 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 · 𝐷) ∈ ℕ)
5947, 31, 52, 262sqn0 27493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐶 ≠ 0)
60 elnnne0 12538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐶 ∈ ℕ ↔ (𝐶 ∈ ℕ0𝐶 ≠ 0))
613, 59, 60sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐶 ∈ ℕ)
6217, 21addcomd 11461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((𝐵↑2) + (𝐴↑2)) = ((𝐴↑2) + (𝐵↑2)))
6362, 25eqtrd 2775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝐵↑2) + (𝐴↑2)) = 𝑃)
6447, 48, 30, 632sqn0 27493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ≠ 0)
65 elnnne0 12538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ ℕ ↔ (𝐵 ∈ ℕ0𝐵 ≠ 0))
666, 64, 65sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ ℕ)
6761, 66nnmulcld 12317 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐶 · 𝐵) ∈ ℕ)
6858, 67nnaddcld 12316 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℕ)
6968nnsqcld 14280 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ)
7069nnred 12279 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℝ)
7143resqcld 14162 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℝ)
7270, 71addge02d 11850 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
7346, 72mpbid 232 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
7425, 26oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = (𝑃 · 𝑃))
75 bhmafibid1 15501 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
7639, 7, 4, 41, 75syl22anc 839 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
7774, 76eqtr3d 2777 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
78 prmz 16709 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
7947, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑃 ∈ ℤ)
8079zcnd 12721 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℂ)
8180sqvald 14180 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑2) = (𝑃 · 𝑃))
8213, 16mulcomd 11280 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
8382oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
8483oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))
8584oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
8677, 81, 853eqtr4d 2785 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
8773, 86breqtrrd 5176 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2))
8887adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2))
8930, 52zmulcld 12726 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 · 𝐷) ∈ ℤ)
9031, 48zmulcld 12726 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐶 · 𝐵) ∈ ℤ)
9189, 90zaddcld 12724 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ)
92 dvdssqim 16588 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9379, 91, 92syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
94 zsqcl 14166 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℤ → (𝑃↑2) ∈ ℤ)
9579, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑2) ∈ ℤ)
96 dvdsle 16344 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃↑2) ∈ ℤ ∧ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9795, 69, 96syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9893, 97syld 47 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9998imp 406 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))
10095zred 12720 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) ∈ ℝ)
10170, 100letri3d 11401 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
102101adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
10388, 99, 102mpbir2and 713 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2))
10486adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
105103, 104eqtr2d 2776 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))
10670recnd 11287 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℂ)
10771recnd 11287 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℂ)
108106, 106, 107subadd2d 11637 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
109108adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
110105, 109mpbird 257 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2))
111106subidd 11606 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0)
112111adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0)
113110, 112eqtr3d 2777 . . . . . . . . . . . . . . . 16 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) = 0)
11445, 113sqeq0d 14182 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) = 0)
11536, 38, 114subeq0d 11626 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) = (𝐵 · 𝐷))
11634, 115breqtrd 5174 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐵 · 𝐷))
11747, 30, 48, 252sqcoprm 27494 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 gcd 𝐵) = 1)
118117adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 gcd 𝐵) = 1)
119 coprmdvds 16687 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
12030, 48, 52, 119syl3anc 1370 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
121120adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
122116, 118, 121mp2and 699 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐷)
123 dvdsle 16344 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐴𝐷𝐴𝐷))
12430, 57, 123syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐷𝐴𝐷))
125124adantr 480 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴𝐷𝐴𝐷))
126122, 125mpd 15 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐷)
12751nnrpd 13073 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ+)
128127rprege0d 13082 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
12922nn0ge0d 12588 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ 𝐷)
130 le2sq 14171 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷)) → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
131128, 41, 129, 130syl12anc 837 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
132131adantr 480 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
133126, 132mpbid 232 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ≤ (𝐷↑2))
13451nnsqcld 14280 . . . . . . . . . . . . 13 (𝜑 → (𝐴↑2) ∈ ℕ)
135134nnred 12279 . . . . . . . . . . . 12 (𝜑 → (𝐴↑2) ∈ ℝ)
136 zsqcl 14166 . . . . . . . . . . . . . 14 (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
13752, 136syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐷↑2) ∈ ℤ)
138137zred 12720 . . . . . . . . . . . 12 (𝜑 → (𝐷↑2) ∈ ℝ)
139135, 138suble0d 11852 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2)))
140139adantr 480 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2)))
141133, 140mpbird 257 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) ≤ 0)
14229, 141eqbrtrrd 5172 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) ≤ 0)
143 dvdsmul1 16312 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → 𝐵 ∥ (𝐵 · 𝐷))
14448, 52, 143syl2anc 584 . . . . . . . . . . . . . 14 (𝜑𝐵 ∥ (𝐵 · 𝐷))
145144adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐵 · 𝐷))
146145, 115breqtrrd 5176 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐴 · 𝐶))
14730, 48gcdcomd 16548 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
148147, 117eqtr3d 2777 . . . . . . . . . . . . 13 (𝜑 → (𝐵 gcd 𝐴) = 1)
149148adantr 480 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 gcd 𝐴) = 1)
150 coprmdvds 16687 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
15148, 30, 31, 150syl3anc 1370 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
152151adantr 480 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
153146, 149, 152mp2and 699 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵𝐶)
154 dvdsle 16344 . . . . . . . . . . . . 13 ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) → (𝐵𝐶𝐵𝐶))
15548, 61, 154syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐶𝐵𝐶))
156155adantr 480 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵𝐶𝐵𝐶))
157153, 156mpd 15 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵𝐶)
1587, 4, 11, 9le2sqd 14293 . . . . . . . . . . 11 (𝜑 → (𝐵𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2)))
159158adantr 480 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2)))
160157, 159mpbid 232 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ≤ (𝐶↑2))
1614resqcld 14162 . . . . . . . . . . 11 (𝜑 → (𝐶↑2) ∈ ℝ)
162 zsqcl 14166 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
16348, 162syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵↑2) ∈ ℤ)
164163zred 12720 . . . . . . . . . . 11 (𝜑 → (𝐵↑2) ∈ ℝ)
165161, 164subge0d 11851 . . . . . . . . . 10 (𝜑 → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2)))
166165adantr 480 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2)))
167160, 166mpbird 257 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐶↑2) − (𝐵↑2)))
168135, 138resubcld 11689 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) − (𝐷↑2)) ∈ ℝ)
16928, 168eqeltrrd 2840 . . . . . . . . . 10 (𝜑 → ((𝐶↑2) − (𝐵↑2)) ∈ ℝ)
170 0red 11262 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
171169, 170letri3d 11401 . . . . . . . . 9 (𝜑 → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2)))))
172171adantr 480 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2)))))
173142, 167, 172mpbir2and 713 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) = 0)
17415, 18, 173subeq0d 11626 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) = (𝐵↑2))
1755, 8, 10, 12, 174sq11d 14294 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 = 𝐵)
1762, 175breqtrrd 5176 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐶)
177 2sqmod.7 . . . . . 6 (𝜑𝐶𝐷)
178177adantr 480 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶𝐷)
17939adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∈ ℝ)
18041adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐷 ∈ ℝ)
18119nn0ge0d 12588 . . . . . . 7 (𝜑 → 0 ≤ 𝐴)
182181adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐴)
183129adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐷)
18421adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ∈ ℂ)
18524adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ)
186167, 29breqtrrd 5176 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐴↑2) − (𝐷↑2)))
187168, 170letri3d 11401 . . . . . . . . 9 (𝜑 → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2)))))
188187adantr 480 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2)))))
189141, 186, 188mpbir2and 713 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = 0)
190184, 185, 189subeq0d 11626 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) = (𝐷↑2))
191179, 180, 182, 183, 190sq11d 14294 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐷)
192178, 191breqtrrd 5176 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶𝐴)
19339, 4letri3d 11401 . . . . 5 (𝜑 → (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴)))
194193adantr 480 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴)))
195176, 192, 194mpbir2and 713 . . 3 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐶)
19620adantr 480 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 ∈ ℂ)
19713adantr 480 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐶 ∈ ℂ)
19816adantr 480 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℂ)
19964adantr 480 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ≠ 0)
20041adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 ∈ ℝ)
2017adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℝ)
202129adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐷)
20311adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐵)
20424adantr 480 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ)
20517adantr 480 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ)
206 prmnn 16708 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
20747, 206syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℕ)
208207nnne0d 12314 . . . . . . . . . . 11 (𝜑𝑃 ≠ 0)
209208neneqd 2943 . . . . . . . . . 10 (𝜑 → ¬ 𝑃 = 0)
210209adantr 480 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ¬ 𝑃 = 0)
21180, 24, 17subdid 11717 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))))
21280, 24mulcld 11279 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 · (𝐷↑2)) ∈ ℂ)
21321, 24mulcld 11279 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴↑2) · (𝐷↑2)) ∈ ℂ)
21480, 17mulcld 11279 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 · (𝐵↑2)) ∈ ℂ)
21514, 17mulcld 11279 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶↑2) · (𝐵↑2)) ∈ ℂ)
21617, 24mulcomd 11280 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵↑2) · (𝐷↑2)) = ((𝐷↑2) · (𝐵↑2)))
21725oveq1d 7446 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝑃 − (𝐴↑2)))
21821, 17pncan2d 11620 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝐵↑2))
219217, 218eqtr3d 2777 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 − (𝐴↑2)) = (𝐵↑2))
220219oveq1d 7446 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝐵↑2) · (𝐷↑2)))
22126oveq1d 7446 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝑃 − (𝐶↑2)))
22214, 24pncan2d 11620 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝐷↑2))
223221, 222eqtr3d 2777 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 − (𝐶↑2)) = (𝐷↑2))
224223oveq1d 7446 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝐷↑2) · (𝐵↑2)))
225216, 220, 2243eqtr4d 2785 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 − (𝐶↑2)) · (𝐵↑2)))
22680, 21, 24subdird 11718 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))))
22780, 14, 17subdird 11718 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2))))
228225, 226, 2273eqtr3d 2783 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2))))
229212, 213, 214, 215, 228subeqxfrd 11670 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
230211, 229eqtrd 2775 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
23120, 23sqmuld 14195 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐷)↑2) = ((𝐴↑2) · (𝐷↑2)))
23213, 16sqmuld 14195 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵)↑2) = ((𝐶↑2) · (𝐵↑2)))
233231, 232oveq12d 7449 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
23420, 23mulcld 11279 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
23513, 16mulcld 11279 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 · 𝐵) ∈ ℂ)
236 subsq 14246 . . . . . . . . . . . . . . 15 (((𝐴 · 𝐷) ∈ ℂ ∧ (𝐶 · 𝐵) ∈ ℂ) → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
237234, 235, 236syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
238230, 233, 2373eqtr2d 2781 . . . . . . . . . . . . 13 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
239238adantr 480 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
240234adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) ∈ ℂ)
241 simpll 767 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → 𝜑)
242 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵))
243242neqned 2945 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵))
24489, 90zsubcld 12725 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ)
245 dvdssqim 16588 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
24679, 244, 245syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
247246imp 406 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
248247adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
24995adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝑃↑2) ∈ ℤ)
250244adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ)
251234adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ∈ ℂ)
252235adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐶 · 𝐵) ∈ ℂ)
253 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵))
254251, 252, 253subne0d 11627 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ≠ 0)
255250, 254znsqcld 14199 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ)
256 dvdsle 16344 . . . . . . . . . . . . . . . . . 18 (((𝑃↑2) ∈ ℤ ∧ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
257249, 255, 256syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
258257imp 406 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) ∧ (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
259241, 243, 248, 258syl21anc 838 . . . . . . . . . . . . . . 15 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
26039, 41remulcld 11289 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐷) ∈ ℝ)
2614, 7remulcld 11289 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐶 · 𝐵) ∈ ℝ)
262260, 261resubcld 11689 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℝ)
263262resqcld 14162 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℝ)
26461nnrpd 13073 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐶 ∈ ℝ+)
265127, 264rpmulcld 13091 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐶) ∈ ℝ+)
26666nnrpd 13073 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ+)
26757nnrpd 13073 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐷 ∈ ℝ+)
268266, 267rpmulcld 13091 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐵 · 𝐷) ∈ ℝ+)
269265, 268rpaddcld 13090 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 · 𝐶) + (𝐵 · 𝐷)) ∈ ℝ+)
270 2z 12647 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℤ
271270a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℤ)
272269, 271rpexpcld 14283 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) ∈ ℝ+)
273263, 272ltaddrp2d 13109 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
274 bhmafibid2 15502 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27539, 7, 4, 41, 274syl22anc 839 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27674, 275eqtr3d 2777 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27782oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = ((𝐴 · 𝐷) − (𝐵 · 𝐶)))
278277oveq1d 7446 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))
279278oveq2d 7447 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
280276, 279eqtr4d 2778 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
281273, 280breqtrrd 5176 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃 · 𝑃))
282281, 81breqtrrd 5176 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2))
283241, 282syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2))
284263, 100ltnled 11406 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
285241, 284syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
286283, 285mpbid 232 . . . . . . . . . . . . . . 15 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
287259, 286condan 818 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐶 · 𝐵))
288240, 287subeq0bd 11687 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = 0)
289288oveq2d 7447 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0))
290234, 235addcld 11278 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℂ)
291290mul01d 11458 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0)
292291adantr 480 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0)
293239, 289, 2923eqtrd 2779 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0)
29424, 17subcld 11618 . . . . . . . . . . . . 13 (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℂ)
29580, 294mul0ord 11911 . . . . . . . . . . . 12 (𝜑 → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)))
296295adantr 480 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)))
297293, 296mpbid 232 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0))
298297ord 864 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (¬ 𝑃 = 0 → ((𝐷↑2) − (𝐵↑2)) = 0))
299210, 298mpd 15 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐷↑2) − (𝐵↑2)) = 0)
300204, 205, 299subeq0d 11626 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) = (𝐵↑2))
301200, 201, 202, 203, 300sq11d 14294 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 = 𝐵)
302301oveq2d 7447 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐴 · 𝐵))
303302, 287eqtr3d 2777 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐵) = (𝐶 · 𝐵))
304196, 197, 198, 199, 303mulcan2ad 11897 . . 3 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 = 𝐶)
305137, 163zsubcld 12725 . . . . . 6 (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℤ)
306 dvdsmul1 16312 . . . . . 6 ((𝑃 ∈ ℤ ∧ ((𝐷↑2) − (𝐵↑2)) ∈ ℤ) → 𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2))))
30779, 305, 306syl2anc 584 . . . . 5 (𝜑𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2))))
308307, 238breqtrd 5174 . . . 4 (𝜑𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
309 euclemma 16747 . . . . 5 ((𝑃 ∈ ℙ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))))
31047, 91, 244, 309syl3anc 1370 . . . 4 (𝜑 → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))))
311308, 310mpbid 232 . . 3 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
312195, 304, 311mpjaodan 960 . 2 (𝜑𝐴 = 𝐶)
313312oveq1d 7446 . . . . 5 (𝜑 → (𝐴↑2) = (𝐶↑2))
314313oveq2d 7447 . . . 4 (𝜑 → (𝑃 − (𝐴↑2)) = (𝑃 − (𝐶↑2)))
315314, 219, 2233eqtr3d 2783 . . 3 (𝜑 → (𝐵↑2) = (𝐷↑2))
3167, 41, 11, 129, 315sq11d 14294 . 2 (𝜑𝐵 = 𝐷)
317312, 316jca 511 1 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847   = wceq 1537  wcel 2106  wne 2938   class class class wbr 5148  (class class class)co 7431  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156   · cmul 11158   < clt 11293  cle 11294  cmin 11490  cn 12264  2c2 12319  0cn0 12524  cz 12611  cexp 14099  cdvds 16287   gcd cgcd 16528  cprime 16705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-sup 9480  df-inf 9481  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12612  df-uz 12877  df-rp 13033  df-fl 13829  df-mod 13907  df-seq 14040  df-exp 14100  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-dvds 16288  df-gcd 16529  df-prm 16706
This theorem is referenced by:  2sqmo  27496
  Copyright terms: Public domain W3C validator