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 28979
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 11229 . . . . . . 7 (𝜑𝐶 ∈ ℝ)
54adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 ∈ ℝ)
6 2sqmod.3 . . . . . . . 8 (𝜑𝐵 ∈ ℕ0)
76nn0red 11229 . . . . . . 7 (𝜑𝐵 ∈ ℝ)
87adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∈ ℝ)
93nn0ge0d 11231 . . . . . . 7 (𝜑 → 0 ≤ 𝐶)
109adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐶)
116nn0ge0d 11231 . . . . . . 7 (𝜑 → 0 ≤ 𝐵)
1211adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐵)
133nn0cnd 11230 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1413sqcld 12868 . . . . . . . 8 (𝜑 → (𝐶↑2) ∈ ℂ)
1514adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) ∈ ℂ)
166nn0cnd 11230 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
1716sqcld 12868 . . . . . . . 8 (𝜑 → (𝐵↑2) ∈ ℂ)
1817adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ)
19 2sqmod.2 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℕ0)
2019nn0cnd 11230 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
2120sqcld 12868 . . . . . . . . . . 11 (𝜑 → (𝐴↑2) ∈ ℂ)
22 2sqmod.5 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ ℕ0)
2322nn0cnd 11230 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℂ)
2423sqcld 12868 . . . . . . . . . . 11 (𝜑 → (𝐷↑2) ∈ ℂ)
25 2sqmod.8 . . . . . . . . . . . 12 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃)
26 2sqmod.9 . . . . . . . . . . . 12 (𝜑 → ((𝐶↑2) + (𝐷↑2)) = 𝑃)
2725, 26eqtr4d 2647 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = ((𝐶↑2) + (𝐷↑2)))
2821, 17, 14, 24, 27subaddeqd 10325 . . . . . . . . . 10 (𝜑 → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2)))
2928adantr 480 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2)))
3019nn0zd 11356 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℤ)
313nn0zd 11356 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℤ)
32 dvdsmul1 14841 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐶))
3330, 31, 32syl2anc 691 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∥ (𝐴 · 𝐶))
3433adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐴 · 𝐶))
3520, 13mulcld 9939 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
3635adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) ∈ ℂ)
3716, 23mulcld 9939 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
3837adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 · 𝐷) ∈ ℂ)
3919nn0red 11229 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
4039, 4remulcld 9949 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 · 𝐶) ∈ ℝ)
4122nn0red 11229 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷 ∈ ℝ)
427, 41remulcld 9949 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 · 𝐷) ∈ ℝ)
4340, 42resubcld 10337 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℝ)
4443recnd 9947 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ)
4544adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ)
4643sqge0d 12898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2))
47 2sqmod.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑃 ∈ ℙ)
486nn0zd 11356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐵 ∈ ℤ)
4947, 30, 48, 252sqn0 28977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐴 ≠ 0)
50 elnnne0 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐴 ∈ ℕ ↔ (𝐴 ∈ ℕ0𝐴 ≠ 0))
5119, 49, 50sylanbrc 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐴 ∈ ℕ)
5222nn0zd 11356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐷 ∈ ℤ)
5324, 14addcomd 10117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((𝐷↑2) + (𝐶↑2)) = ((𝐶↑2) + (𝐷↑2)))
5453, 26eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝐷↑2) + (𝐶↑2)) = 𝑃)
5547, 52, 31, 542sqn0 28977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐷 ≠ 0)
56 elnnne0 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐷 ∈ ℕ ↔ (𝐷 ∈ ℕ0𝐷 ≠ 0))
5722, 55, 56sylanbrc 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 ∈ ℕ)
5851, 57nnmulcld 10945 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 · 𝐷) ∈ ℕ)
5947, 31, 52, 262sqn0 28977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐶 ≠ 0)
60 elnnne0 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐶 ∈ ℕ ↔ (𝐶 ∈ ℕ0𝐶 ≠ 0))
613, 59, 60sylanbrc 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐶 ∈ ℕ)
6217, 21addcomd 10117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((𝐵↑2) + (𝐴↑2)) = ((𝐴↑2) + (𝐵↑2)))
6362, 25eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝐵↑2) + (𝐴↑2)) = 𝑃)
6447, 48, 30, 632sqn0 28977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ≠ 0)
65 elnnne0 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ ℕ ↔ (𝐵 ∈ ℕ0𝐵 ≠ 0))
666, 64, 65sylanbrc 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ ℕ)
6761, 66nnmulcld 10945 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐶 · 𝐵) ∈ ℕ)
6858, 67nnaddcld 10944 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℕ)
6968nnsqcld 12891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ)
7069nnred 10912 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℝ)
7143resqcld 12897 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℝ)
7270, 71addge02d 10495 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
7346, 72mpbid 221 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
7425, 26oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = (𝑃 · 𝑃))
75 bhmafibid1 28975 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
7639, 7, 4, 41, 75syl22anc 1319 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
7774, 76eqtr3d 2646 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
78 prmz 15227 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
7947, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑃 ∈ ℤ)
8079zcnd 11359 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℂ)
8180sqvald 12867 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑2) = (𝑃 · 𝑃))
8213, 16mulcomd 9940 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
8382oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
8483oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))
8584oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
8677, 81, 853eqtr4d 2654 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
8773, 86breqtrrd 4611 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2))
8887adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2))
8930, 52zmulcld 11364 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 · 𝐷) ∈ ℤ)
9031, 48zmulcld 11364 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐶 · 𝐵) ∈ ℤ)
9189, 90zaddcld 11362 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ)
92 dvdssqim 15111 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9379, 91, 92syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
94 zsqcl 12796 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℤ → (𝑃↑2) ∈ ℤ)
9579, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑2) ∈ ℤ)
96 dvdsle 14870 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃↑2) ∈ ℤ ∧ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9795, 69, 96syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9893, 97syld 46 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9998imp 444 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))
10095zred 11358 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) ∈ ℝ)
10170, 100letri3d 10058 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
102101adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
10388, 99, 102mpbir2and 959 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2))
10486adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
105103, 104eqtr2d 2645 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))
10670recnd 9947 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℂ)
10771recnd 9947 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℂ)
108106, 106, 107subadd2d 10290 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
109108adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
110105, 109mpbird 246 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2))
111106subidd 10259 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0)
112111adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0)
113110, 112eqtr3d 2646 . . . . . . . . . . . . . . . 16 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) = 0)
11445, 113sqeq0d 12869 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) = 0)
11536, 38, 114subeq0d 10279 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) = (𝐵 · 𝐷))
11634, 115breqtrd 4609 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐵 · 𝐷))
11747, 30, 48, 252sqcoprm 28978 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 gcd 𝐵) = 1)
118117adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 gcd 𝐵) = 1)
119 coprmdvds 15204 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
12030, 48, 52, 119syl3anc 1318 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
121120adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
122116, 118, 121mp2and 711 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐷)
123 dvdsle 14870 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐴𝐷𝐴𝐷))
12430, 57, 123syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐷𝐴𝐷))
125124adantr 480 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴𝐷𝐴𝐷))
126122, 125mpd 15 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐷)
12751nnrpd 11746 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ+)
128127rprege0d 11755 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
12922nn0ge0d 11231 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ 𝐷)
130 le2sq 12800 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷)) → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
131128, 41, 129, 130syl12anc 1316 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
132131adantr 480 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
133126, 132mpbid 221 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ≤ (𝐷↑2))
13451nnsqcld 12891 . . . . . . . . . . . . 13 (𝜑 → (𝐴↑2) ∈ ℕ)
135134nnred 10912 . . . . . . . . . . . 12 (𝜑 → (𝐴↑2) ∈ ℝ)
136 zsqcl 12796 . . . . . . . . . . . . . 14 (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
13752, 136syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐷↑2) ∈ ℤ)
138137zred 11358 . . . . . . . . . . . 12 (𝜑 → (𝐷↑2) ∈ ℝ)
139135, 138suble0d 10497 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2)))
140139adantr 480 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2)))
141133, 140mpbird 246 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) ≤ 0)
14229, 141eqbrtrrd 4607 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) ≤ 0)
143 dvdsmul1 14841 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → 𝐵 ∥ (𝐵 · 𝐷))
14448, 52, 143syl2anc 691 . . . . . . . . . . . . . 14 (𝜑𝐵 ∥ (𝐵 · 𝐷))
145144adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐵 · 𝐷))
146145, 115breqtrrd 4611 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐴 · 𝐶))
147 gcdcom 15073 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
14830, 48, 147syl2anc 691 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
149148, 117eqtr3d 2646 . . . . . . . . . . . . 13 (𝜑 → (𝐵 gcd 𝐴) = 1)
150149adantr 480 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 gcd 𝐴) = 1)
151 coprmdvds 15204 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
15248, 30, 31, 151syl3anc 1318 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
153152adantr 480 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
154146, 150, 153mp2and 711 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵𝐶)
155 dvdsle 14870 . . . . . . . . . . . . 13 ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) → (𝐵𝐶𝐵𝐶))
15648, 61, 155syl2anc 691 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐶𝐵𝐶))
157156adantr 480 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵𝐶𝐵𝐶))
158154, 157mpd 15 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵𝐶)
1597, 4, 11, 9le2sqd 12906 . . . . . . . . . . 11 (𝜑 → (𝐵𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2)))
160159adantr 480 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2)))
161158, 160mpbid 221 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ≤ (𝐶↑2))
1624resqcld 12897 . . . . . . . . . . 11 (𝜑 → (𝐶↑2) ∈ ℝ)
163 zsqcl 12796 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
16448, 163syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵↑2) ∈ ℤ)
165164zred 11358 . . . . . . . . . . 11 (𝜑 → (𝐵↑2) ∈ ℝ)
166162, 165subge0d 10496 . . . . . . . . . 10 (𝜑 → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2)))
167166adantr 480 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2)))
168161, 167mpbird 246 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐶↑2) − (𝐵↑2)))
169135, 138resubcld 10337 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) − (𝐷↑2)) ∈ ℝ)
17028, 169eqeltrrd 2689 . . . . . . . . . 10 (𝜑 → ((𝐶↑2) − (𝐵↑2)) ∈ ℝ)
171 0red 9920 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
172170, 171letri3d 10058 . . . . . . . . 9 (𝜑 → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2)))))
173172adantr 480 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2)))))
174142, 168, 173mpbir2and 959 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) = 0)
17515, 18, 174subeq0d 10279 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) = (𝐵↑2))
1765, 8, 10, 12, 175sq11d 12907 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 = 𝐵)
1772, 176breqtrrd 4611 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐶)
178 2sqmod.7 . . . . . 6 (𝜑𝐶𝐷)
179178adantr 480 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶𝐷)
18039adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∈ ℝ)
18141adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐷 ∈ ℝ)
18219nn0ge0d 11231 . . . . . . 7 (𝜑 → 0 ≤ 𝐴)
183182adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐴)
184129adantr 480 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐷)
18521adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ∈ ℂ)
18624adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ)
187168, 29breqtrrd 4611 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐴↑2) − (𝐷↑2)))
188169, 171letri3d 10058 . . . . . . . . 9 (𝜑 → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2)))))
189188adantr 480 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2)))))
190141, 187, 189mpbir2and 959 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = 0)
191185, 186, 190subeq0d 10279 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) = (𝐷↑2))
192180, 181, 183, 184, 191sq11d 12907 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐷)
193179, 192breqtrrd 4611 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶𝐴)
19439, 4letri3d 10058 . . . . 5 (𝜑 → (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴)))
195194adantr 480 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴)))
196177, 193, 195mpbir2and 959 . . 3 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐶)
19720adantr 480 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 ∈ ℂ)
19813adantr 480 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐶 ∈ ℂ)
19916adantr 480 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℂ)
20064adantr 480 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ≠ 0)
20141adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 ∈ ℝ)
2027adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℝ)
203129adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐷)
20411adantr 480 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐵)
20524adantr 480 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ)
20617adantr 480 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ)
207 prmnn 15226 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
20847, 207syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℕ)
209208nnne0d 10942 . . . . . . . . . . 11 (𝜑𝑃 ≠ 0)
210209neneqd 2787 . . . . . . . . . 10 (𝜑 → ¬ 𝑃 = 0)
211210adantr 480 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ¬ 𝑃 = 0)
21280, 24, 17subdid 10365 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))))
21380, 24mulcld 9939 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 · (𝐷↑2)) ∈ ℂ)
21421, 24mulcld 9939 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴↑2) · (𝐷↑2)) ∈ ℂ)
21580, 17mulcld 9939 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 · (𝐵↑2)) ∈ ℂ)
21614, 17mulcld 9939 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶↑2) · (𝐵↑2)) ∈ ℂ)
21717, 24mulcomd 9940 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵↑2) · (𝐷↑2)) = ((𝐷↑2) · (𝐵↑2)))
21825oveq1d 6564 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝑃 − (𝐴↑2)))
21921, 17pncan2d 10273 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝐵↑2))
220218, 219eqtr3d 2646 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 − (𝐴↑2)) = (𝐵↑2))
221220oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝐵↑2) · (𝐷↑2)))
22226oveq1d 6564 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝑃 − (𝐶↑2)))
22314, 24pncan2d 10273 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝐷↑2))
224222, 223eqtr3d 2646 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 − (𝐶↑2)) = (𝐷↑2))
225224oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝐷↑2) · (𝐵↑2)))
226217, 221, 2253eqtr4d 2654 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 − (𝐶↑2)) · (𝐵↑2)))
22780, 21, 24subdird 10366 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))))
22880, 14, 17subdird 10366 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2))))
229226, 227, 2283eqtr3d 2652 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2))))
230213, 214, 215, 216, 229subeqxfrd 28899 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
231212, 230eqtrd 2644 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
23220, 23sqmuld 12882 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐷)↑2) = ((𝐴↑2) · (𝐷↑2)))
23313, 16sqmuld 12882 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵)↑2) = ((𝐶↑2) · (𝐵↑2)))
234232, 233oveq12d 6567 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
23520, 23mulcld 9939 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
23613, 16mulcld 9939 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 · 𝐵) ∈ ℂ)
237 subsq 12834 . . . . . . . . . . . . . . 15 (((𝐴 · 𝐷) ∈ ℂ ∧ (𝐶 · 𝐵) ∈ ℂ) → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
238235, 236, 237syl2anc 691 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
239231, 234, 2383eqtr2d 2650 . . . . . . . . . . . . 13 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
240239adantr 480 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
241235adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) ∈ ℂ)
242 simpll 786 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → 𝜑)
243 simpr 476 . . . . . . . . . . . . . . . . 17 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵))
244243neqned 2789 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵))
24589, 90zsubcld 11363 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ)
246 dvdssqim 15111 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
24779, 245, 246syl2anc 691 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
248247imp 444 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
249248adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
25095adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝑃↑2) ∈ ℤ)
251245adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ)
252235adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ∈ ℂ)
253236adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐶 · 𝐵) ∈ ℂ)
254 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵))
255252, 253, 254subne0d 10280 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ≠ 0)
256251, 255znsqcld 28900 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ)
257 dvdsle 14870 . . . . . . . . . . . . . . . . . 18 (((𝑃↑2) ∈ ℤ ∧ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
258250, 256, 257syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
259258imp 444 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) ∧ (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
260242, 244, 249, 259syl21anc 1317 . . . . . . . . . . . . . . 15 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
26139, 41remulcld 9949 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐷) ∈ ℝ)
2624, 7remulcld 9949 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐶 · 𝐵) ∈ ℝ)
263261, 262resubcld 10337 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℝ)
264263resqcld 12897 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℝ)
26561nnrpd 11746 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐶 ∈ ℝ+)
266127, 265rpmulcld 11764 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐶) ∈ ℝ+)
26766nnrpd 11746 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ+)
26857nnrpd 11746 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐷 ∈ ℝ+)
269267, 268rpmulcld 11764 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐵 · 𝐷) ∈ ℝ+)
270266, 269rpaddcld 11763 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 · 𝐶) + (𝐵 · 𝐷)) ∈ ℝ+)
271 2z 11286 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℤ
272271a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℤ)
273270, 272rpexpcld 12894 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) ∈ ℝ+)
274264, 273ltaddrp2d 11782 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
275 bhmafibid2 28976 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27639, 7, 4, 41, 275syl22anc 1319 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27774, 276eqtr3d 2646 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27882oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = ((𝐴 · 𝐷) − (𝐵 · 𝐶)))
279278oveq1d 6564 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))
280279oveq2d 6565 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
281277, 280eqtr4d 2647 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
282274, 281breqtrrd 4611 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃 · 𝑃))
283282, 81breqtrrd 4611 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2))
284242, 283syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2))
285264, 100ltnled 10063 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
286242, 285syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
287284, 286mpbid 221 . . . . . . . . . . . . . . 15 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
288260, 287condan 831 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐶 · 𝐵))
289241, 288subeq0bd 10335 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = 0)
290289oveq2d 6565 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0))
291235, 236addcld 9938 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℂ)
292291mul01d 10114 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0)
293292adantr 480 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0)
294240, 290, 2933eqtrd 2648 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0)
29524, 17subcld 10271 . . . . . . . . . . . . 13 (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℂ)
29680, 295mul0ord 10556 . . . . . . . . . . . 12 (𝜑 → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)))
297296adantr 480 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)))
298294, 297mpbid 221 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0))
299298ord 391 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (¬ 𝑃 = 0 → ((𝐷↑2) − (𝐵↑2)) = 0))
300211, 299mpd 15 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐷↑2) − (𝐵↑2)) = 0)
301205, 206, 300subeq0d 10279 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) = (𝐵↑2))
302201, 202, 203, 204, 301sq11d 12907 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 = 𝐵)
303302oveq2d 6565 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐴 · 𝐵))
304303, 288eqtr3d 2646 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐵) = (𝐶 · 𝐵))
305197, 198, 199, 200, 304mulcan2ad 10542 . . 3 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 = 𝐶)
306137, 164zsubcld 11363 . . . . . 6 (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℤ)
307 dvdsmul1 14841 . . . . . 6 ((𝑃 ∈ ℤ ∧ ((𝐷↑2) − (𝐵↑2)) ∈ ℤ) → 𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2))))
30879, 306, 307syl2anc 691 . . . . 5 (𝜑𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2))))
309308, 239breqtrd 4609 . . . 4 (𝜑𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
310 euclemma 15263 . . . . 5 ((𝑃 ∈ ℙ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))))
31147, 91, 245, 310syl3anc 1318 . . . 4 (𝜑 → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))))
312309, 311mpbid 221 . . 3 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
313196, 305, 312mpjaodan 823 . 2 (𝜑𝐴 = 𝐶)
314313oveq1d 6564 . . . . 5 (𝜑 → (𝐴↑2) = (𝐶↑2))
315314oveq2d 6565 . . . 4 (𝜑 → (𝑃 − (𝐴↑2)) = (𝑃 − (𝐶↑2)))
316315, 220, 2243eqtr3d 2652 . . 3 (𝜑 → (𝐵↑2) = (𝐷↑2))
3177, 41, 11, 129, 316sq11d 12907 . 2 (𝜑𝐵 = 𝐷)
318313, 317jca 553 1 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383   = wceq 1475  wcel 1977  wne 2780   class class class wbr 4583  (class class class)co 6549  cc 9813  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953  cle 9954  cmin 10145  cn 10897  2c2 10947  0cn0 11169  cz 11254  cexp 12722  cdvds 14821   gcd cgcd 15054  cprime 15223
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-dvds 14822  df-gcd 15055  df-prm 15224
This theorem is referenced by:  2sqmo  28980
  Copyright terms: Public domain W3C validator