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

Theorem 2sqmod 26015
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 483 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐵)
3 2sqmod.4 . . . . . . . 8 (𝜑𝐶 ∈ ℕ0)
43nn0red 11959 . . . . . . 7 (𝜑𝐶 ∈ ℝ)
54adantr 483 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 ∈ ℝ)
6 2sqmod.3 . . . . . . . 8 (𝜑𝐵 ∈ ℕ0)
76nn0red 11959 . . . . . . 7 (𝜑𝐵 ∈ ℝ)
87adantr 483 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∈ ℝ)
93nn0ge0d 11961 . . . . . . 7 (𝜑 → 0 ≤ 𝐶)
109adantr 483 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐶)
116nn0ge0d 11961 . . . . . . 7 (𝜑 → 0 ≤ 𝐵)
1211adantr 483 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐵)
133nn0cnd 11960 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1413sqcld 13511 . . . . . . . 8 (𝜑 → (𝐶↑2) ∈ ℂ)
1514adantr 483 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) ∈ ℂ)
166nn0cnd 11960 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
1716sqcld 13511 . . . . . . . 8 (𝜑 → (𝐵↑2) ∈ ℂ)
1817adantr 483 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ)
19 2sqmod.2 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℕ0)
2019nn0cnd 11960 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
2120sqcld 13511 . . . . . . . . . . 11 (𝜑 → (𝐴↑2) ∈ ℂ)
22 2sqmod.5 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ ℕ0)
2322nn0cnd 11960 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℂ)
2423sqcld 13511 . . . . . . . . . . 11 (𝜑 → (𝐷↑2) ∈ ℂ)
25 2sqmod.8 . . . . . . . . . . . 12 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃)
26 2sqmod.9 . . . . . . . . . . . 12 (𝜑 → ((𝐶↑2) + (𝐷↑2)) = 𝑃)
2725, 26eqtr4d 2862 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = ((𝐶↑2) + (𝐷↑2)))
2821, 17, 14, 24, 27subaddeqd 11058 . . . . . . . . . 10 (𝜑 → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2)))
2928adantr 483 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2)))
3019nn0zd 12088 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℤ)
313nn0zd 12088 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℤ)
32 dvdsmul1 15634 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐶))
3330, 31, 32syl2anc 586 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∥ (𝐴 · 𝐶))
3433adantr 483 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐴 · 𝐶))
3520, 13mulcld 10664 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
3635adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) ∈ ℂ)
3716, 23mulcld 10664 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
3837adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 · 𝐷) ∈ ℂ)
3919nn0red 11959 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
4039, 4remulcld 10674 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 · 𝐶) ∈ ℝ)
4122nn0red 11959 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷 ∈ ℝ)
427, 41remulcld 10674 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 · 𝐷) ∈ ℝ)
4340, 42resubcld 11071 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℝ)
4443recnd 10672 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ)
4544adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ)
4643sqge0d 13615 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2))
47 2sqmod.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑃 ∈ ℙ)
486nn0zd 12088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐵 ∈ ℤ)
4947, 30, 48, 252sqn0 26013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐴 ≠ 0)
50 elnnne0 11914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐴 ∈ ℕ ↔ (𝐴 ∈ ℕ0𝐴 ≠ 0))
5119, 49, 50sylanbrc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐴 ∈ ℕ)
5222nn0zd 12088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐷 ∈ ℤ)
5324, 14addcomd 10845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((𝐷↑2) + (𝐶↑2)) = ((𝐶↑2) + (𝐷↑2)))
5453, 26eqtrd 2859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝐷↑2) + (𝐶↑2)) = 𝑃)
5547, 52, 31, 542sqn0 26013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐷 ≠ 0)
56 elnnne0 11914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐷 ∈ ℕ ↔ (𝐷 ∈ ℕ0𝐷 ≠ 0))
5722, 55, 56sylanbrc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 ∈ ℕ)
5851, 57nnmulcld 11693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 · 𝐷) ∈ ℕ)
5947, 31, 52, 262sqn0 26013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐶 ≠ 0)
60 elnnne0 11914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐶 ∈ ℕ ↔ (𝐶 ∈ ℕ0𝐶 ≠ 0))
613, 59, 60sylanbrc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐶 ∈ ℕ)
6217, 21addcomd 10845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((𝐵↑2) + (𝐴↑2)) = ((𝐴↑2) + (𝐵↑2)))
6362, 25eqtrd 2859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝐵↑2) + (𝐴↑2)) = 𝑃)
6447, 48, 30, 632sqn0 26013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ≠ 0)
65 elnnne0 11914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ ℕ ↔ (𝐵 ∈ ℕ0𝐵 ≠ 0))
666, 64, 65sylanbrc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ ℕ)
6761, 66nnmulcld 11693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐶 · 𝐵) ∈ ℕ)
6858, 67nnaddcld 11692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℕ)
6968nnsqcld 13608 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ)
7069nnred 11656 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℝ)
7143resqcld 13614 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℝ)
7270, 71addge02d 11232 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
7346, 72mpbid 234 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
7425, 26oveq12d 7177 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = (𝑃 · 𝑃))
75 bhmafibid1 14828 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
7639, 7, 4, 41, 75syl22anc 836 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
7774, 76eqtr3d 2861 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
78 prmz 16022 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
7947, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑃 ∈ ℤ)
8079zcnd 12091 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℂ)
8180sqvald 13510 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑2) = (𝑃 · 𝑃))
8213, 16mulcomd 10665 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
8382oveq2d 7175 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
8483oveq1d 7174 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))
8584oveq2d 7175 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
8677, 81, 853eqtr4d 2869 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
8773, 86breqtrrd 5097 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2))
8887adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2))
8930, 52zmulcld 12096 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 · 𝐷) ∈ ℤ)
9031, 48zmulcld 12096 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐶 · 𝐵) ∈ ℤ)
9189, 90zaddcld 12094 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ)
92 dvdssqim 15907 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9379, 91, 92syl2anc 586 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
94 zsqcl 13497 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℤ → (𝑃↑2) ∈ ℤ)
9579, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑2) ∈ ℤ)
96 dvdsle 15663 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃↑2) ∈ ℤ ∧ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9795, 69, 96syl2anc 586 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9893, 97syld 47 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9998imp 409 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))
10095zred 12090 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) ∈ ℝ)
10170, 100letri3d 10785 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
102101adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
10388, 99, 102mpbir2and 711 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2))
10486adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
105103, 104eqtr2d 2860 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))
10670recnd 10672 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℂ)
10771recnd 10672 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℂ)
108106, 106, 107subadd2d 11019 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
109108adantr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
110105, 109mpbird 259 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2))
111106subidd 10988 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0)
112111adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0)
113110, 112eqtr3d 2861 . . . . . . . . . . . . . . . 16 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) = 0)
11445, 113sqeq0d 13512 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) = 0)
11536, 38, 114subeq0d 11008 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) = (𝐵 · 𝐷))
11634, 115breqtrd 5095 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐵 · 𝐷))
11747, 30, 48, 252sqcoprm 26014 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 gcd 𝐵) = 1)
118117adantr 483 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 gcd 𝐵) = 1)
119 coprmdvds 16000 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
12030, 48, 52, 119syl3anc 1367 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
121120adantr 483 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
122116, 118, 121mp2and 697 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐷)
123 dvdsle 15663 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐴𝐷𝐴𝐷))
12430, 57, 123syl2anc 586 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐷𝐴𝐷))
125124adantr 483 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴𝐷𝐴𝐷))
126122, 125mpd 15 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐷)
12751nnrpd 12432 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ+)
128127rprege0d 12441 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
12922nn0ge0d 11961 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ 𝐷)
130 le2sq 13502 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷)) → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
131128, 41, 129, 130syl12anc 834 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
132131adantr 483 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
133126, 132mpbid 234 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ≤ (𝐷↑2))
13451nnsqcld 13608 . . . . . . . . . . . . 13 (𝜑 → (𝐴↑2) ∈ ℕ)
135134nnred 11656 . . . . . . . . . . . 12 (𝜑 → (𝐴↑2) ∈ ℝ)
136 zsqcl 13497 . . . . . . . . . . . . . 14 (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
13752, 136syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐷↑2) ∈ ℤ)
138137zred 12090 . . . . . . . . . . . 12 (𝜑 → (𝐷↑2) ∈ ℝ)
139135, 138suble0d 11234 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2)))
140139adantr 483 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2)))
141133, 140mpbird 259 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) ≤ 0)
14229, 141eqbrtrrd 5093 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) ≤ 0)
143 dvdsmul1 15634 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → 𝐵 ∥ (𝐵 · 𝐷))
14448, 52, 143syl2anc 586 . . . . . . . . . . . . . 14 (𝜑𝐵 ∥ (𝐵 · 𝐷))
145144adantr 483 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐵 · 𝐷))
146145, 115breqtrrd 5097 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐴 · 𝐶))
147 gcdcom 15865 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
14830, 48, 147syl2anc 586 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
149148, 117eqtr3d 2861 . . . . . . . . . . . . 13 (𝜑 → (𝐵 gcd 𝐴) = 1)
150149adantr 483 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 gcd 𝐴) = 1)
151 coprmdvds 16000 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
15248, 30, 31, 151syl3anc 1367 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
153152adantr 483 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
154146, 150, 153mp2and 697 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵𝐶)
155 dvdsle 15663 . . . . . . . . . . . . 13 ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) → (𝐵𝐶𝐵𝐶))
15648, 61, 155syl2anc 586 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐶𝐵𝐶))
157156adantr 483 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵𝐶𝐵𝐶))
158154, 157mpd 15 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵𝐶)
1597, 4, 11, 9le2sqd 13623 . . . . . . . . . . 11 (𝜑 → (𝐵𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2)))
160159adantr 483 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2)))
161158, 160mpbid 234 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ≤ (𝐶↑2))
1624resqcld 13614 . . . . . . . . . . 11 (𝜑 → (𝐶↑2) ∈ ℝ)
163 zsqcl 13497 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
16448, 163syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵↑2) ∈ ℤ)
165164zred 12090 . . . . . . . . . . 11 (𝜑 → (𝐵↑2) ∈ ℝ)
166162, 165subge0d 11233 . . . . . . . . . 10 (𝜑 → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2)))
167166adantr 483 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2)))
168161, 167mpbird 259 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐶↑2) − (𝐵↑2)))
169135, 138resubcld 11071 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) − (𝐷↑2)) ∈ ℝ)
17028, 169eqeltrrd 2917 . . . . . . . . . 10 (𝜑 → ((𝐶↑2) − (𝐵↑2)) ∈ ℝ)
171 0red 10647 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
172170, 171letri3d 10785 . . . . . . . . 9 (𝜑 → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2)))))
173172adantr 483 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2)))))
174142, 168, 173mpbir2and 711 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) = 0)
17515, 18, 174subeq0d 11008 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) = (𝐵↑2))
1765, 8, 10, 12, 175sq11d 13624 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 = 𝐵)
1772, 176breqtrrd 5097 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐶)
178 2sqmod.7 . . . . . 6 (𝜑𝐶𝐷)
179178adantr 483 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶𝐷)
18039adantr 483 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∈ ℝ)
18141adantr 483 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐷 ∈ ℝ)
18219nn0ge0d 11961 . . . . . . 7 (𝜑 → 0 ≤ 𝐴)
183182adantr 483 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐴)
184129adantr 483 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐷)
18521adantr 483 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ∈ ℂ)
18624adantr 483 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ)
187168, 29breqtrrd 5097 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐴↑2) − (𝐷↑2)))
188169, 171letri3d 10785 . . . . . . . . 9 (𝜑 → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2)))))
189188adantr 483 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2)))))
190141, 187, 189mpbir2and 711 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = 0)
191185, 186, 190subeq0d 11008 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) = (𝐷↑2))
192180, 181, 183, 184, 191sq11d 13624 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐷)
193179, 192breqtrrd 5097 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶𝐴)
19439, 4letri3d 10785 . . . . 5 (𝜑 → (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴)))
195194adantr 483 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴)))
196177, 193, 195mpbir2and 711 . . 3 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐶)
19720adantr 483 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 ∈ ℂ)
19813adantr 483 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐶 ∈ ℂ)
19916adantr 483 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℂ)
20064adantr 483 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ≠ 0)
20141adantr 483 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 ∈ ℝ)
2027adantr 483 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℝ)
203129adantr 483 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐷)
20411adantr 483 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐵)
20524adantr 483 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ)
20617adantr 483 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ)
207 prmnn 16021 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
20847, 207syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℕ)
209208nnne0d 11690 . . . . . . . . . . 11 (𝜑𝑃 ≠ 0)
210209neneqd 3024 . . . . . . . . . 10 (𝜑 → ¬ 𝑃 = 0)
211210adantr 483 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ¬ 𝑃 = 0)
21280, 24, 17subdid 11099 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))))
21380, 24mulcld 10664 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 · (𝐷↑2)) ∈ ℂ)
21421, 24mulcld 10664 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴↑2) · (𝐷↑2)) ∈ ℂ)
21580, 17mulcld 10664 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 · (𝐵↑2)) ∈ ℂ)
21614, 17mulcld 10664 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶↑2) · (𝐵↑2)) ∈ ℂ)
21717, 24mulcomd 10665 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵↑2) · (𝐷↑2)) = ((𝐷↑2) · (𝐵↑2)))
21825oveq1d 7174 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝑃 − (𝐴↑2)))
21921, 17pncan2d 11002 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝐵↑2))
220218, 219eqtr3d 2861 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 − (𝐴↑2)) = (𝐵↑2))
221220oveq1d 7174 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝐵↑2) · (𝐷↑2)))
22226oveq1d 7174 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝑃 − (𝐶↑2)))
22314, 24pncan2d 11002 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝐷↑2))
224222, 223eqtr3d 2861 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 − (𝐶↑2)) = (𝐷↑2))
225224oveq1d 7174 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝐷↑2) · (𝐵↑2)))
226217, 221, 2253eqtr4d 2869 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 − (𝐶↑2)) · (𝐵↑2)))
22780, 21, 24subdird 11100 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))))
22880, 14, 17subdird 11100 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2))))
229226, 227, 2283eqtr3d 2867 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2))))
230213, 214, 215, 216, 229subeqxfrd 11052 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
231212, 230eqtrd 2859 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
23220, 23sqmuld 13525 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐷)↑2) = ((𝐴↑2) · (𝐷↑2)))
23313, 16sqmuld 13525 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵)↑2) = ((𝐶↑2) · (𝐵↑2)))
234232, 233oveq12d 7177 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
23520, 23mulcld 10664 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
23613, 16mulcld 10664 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 · 𝐵) ∈ ℂ)
237 subsq 13575 . . . . . . . . . . . . . . 15 (((𝐴 · 𝐷) ∈ ℂ ∧ (𝐶 · 𝐵) ∈ ℂ) → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
238235, 236, 237syl2anc 586 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
239231, 234, 2383eqtr2d 2865 . . . . . . . . . . . . 13 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
240239adantr 483 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
241235adantr 483 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) ∈ ℂ)
242 simpll 765 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → 𝜑)
243 simpr 487 . . . . . . . . . . . . . . . . 17 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵))
244243neqned 3026 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵))
24589, 90zsubcld 12095 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ)
246 dvdssqim 15907 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
24779, 245, 246syl2anc 586 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
248247imp 409 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
249248adantr 483 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
25095adantr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝑃↑2) ∈ ℤ)
251245adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ)
252235adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ∈ ℂ)
253236adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐶 · 𝐵) ∈ ℂ)
254 simpr 487 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵))
255252, 253, 254subne0d 11009 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ≠ 0)
256251, 255znsqcld 13529 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ)
257 dvdsle 15663 . . . . . . . . . . . . . . . . . 18 (((𝑃↑2) ∈ ℤ ∧ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
258250, 256, 257syl2anc 586 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
259258imp 409 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) ∧ (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
260242, 244, 249, 259syl21anc 835 . . . . . . . . . . . . . . 15 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
26139, 41remulcld 10674 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐷) ∈ ℝ)
2624, 7remulcld 10674 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐶 · 𝐵) ∈ ℝ)
263261, 262resubcld 11071 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℝ)
264263resqcld 13614 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℝ)
26561nnrpd 12432 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐶 ∈ ℝ+)
266127, 265rpmulcld 12450 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐶) ∈ ℝ+)
26766nnrpd 12432 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ+)
26857nnrpd 12432 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐷 ∈ ℝ+)
269267, 268rpmulcld 12450 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐵 · 𝐷) ∈ ℝ+)
270266, 269rpaddcld 12449 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 · 𝐶) + (𝐵 · 𝐷)) ∈ ℝ+)
271 2z 12017 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℤ
272271a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℤ)
273270, 272rpexpcld 13611 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) ∈ ℝ+)
274264, 273ltaddrp2d 12468 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
275 bhmafibid2 14829 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27639, 7, 4, 41, 275syl22anc 836 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27774, 276eqtr3d 2861 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27882oveq2d 7175 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = ((𝐴 · 𝐷) − (𝐵 · 𝐶)))
279278oveq1d 7174 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))
280279oveq2d 7175 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
281277, 280eqtr4d 2862 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
282274, 281breqtrrd 5097 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃 · 𝑃))
283282, 81breqtrrd 5097 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2))
284242, 283syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2))
285264, 100ltnled 10790 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
286242, 285syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
287284, 286mpbid 234 . . . . . . . . . . . . . . 15 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
288260, 287condan 816 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐶 · 𝐵))
289241, 288subeq0bd 11069 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = 0)
290289oveq2d 7175 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0))
291235, 236addcld 10663 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℂ)
292291mul01d 10842 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0)
293292adantr 483 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0)
294240, 290, 2933eqtrd 2863 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0)
29524, 17subcld 11000 . . . . . . . . . . . . 13 (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℂ)
29680, 295mul0ord 11293 . . . . . . . . . . . 12 (𝜑 → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)))
297296adantr 483 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)))
298294, 297mpbid 234 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0))
299298ord 860 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (¬ 𝑃 = 0 → ((𝐷↑2) − (𝐵↑2)) = 0))
300211, 299mpd 15 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐷↑2) − (𝐵↑2)) = 0)
301205, 206, 300subeq0d 11008 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) = (𝐵↑2))
302201, 202, 203, 204, 301sq11d 13624 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 = 𝐵)
303302oveq2d 7175 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐴 · 𝐵))
304303, 288eqtr3d 2861 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐵) = (𝐶 · 𝐵))
305197, 198, 199, 200, 304mulcan2ad 11279 . . 3 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 = 𝐶)
306137, 164zsubcld 12095 . . . . . 6 (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℤ)
307 dvdsmul1 15634 . . . . . 6 ((𝑃 ∈ ℤ ∧ ((𝐷↑2) − (𝐵↑2)) ∈ ℤ) → 𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2))))
30879, 306, 307syl2anc 586 . . . . 5 (𝜑𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2))))
309308, 239breqtrd 5095 . . . 4 (𝜑𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
310 euclemma 16060 . . . . 5 ((𝑃 ∈ ℙ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))))
31147, 91, 245, 310syl3anc 1367 . . . 4 (𝜑 → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))))
312309, 311mpbid 234 . . 3 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
313196, 305, 312mpjaodan 955 . 2 (𝜑𝐴 = 𝐶)
314313oveq1d 7174 . . . . 5 (𝜑 → (𝐴↑2) = (𝐶↑2))
315314oveq2d 7175 . . . 4 (𝜑 → (𝑃 − (𝐴↑2)) = (𝑃 − (𝐶↑2)))
316315, 220, 2243eqtr3d 2867 . . 3 (𝜑 → (𝐵↑2) = (𝐷↑2))
3177, 41, 11, 129, 316sq11d 13624 . 2 (𝜑𝐵 = 𝐷)
318313, 317jca 514 1 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843   = wceq 1536  wcel 2113  wne 3019   class class class wbr 5069  (class class class)co 7159  cc 10538  cr 10539  0cc0 10540  1c1 10541   + caddc 10543   · cmul 10545   < clt 10678  cle 10679  cmin 10873  cn 11641  2c2 11695  0cn0 11900  cz 11984  cexp 13432  cdvds 15610   gcd cgcd 15846  cprime 16018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-cnex 10596  ax-resscn 10597  ax-1cn 10598  ax-icn 10599  ax-addcl 10600  ax-addrcl 10601  ax-mulcl 10602  ax-mulrcl 10603  ax-mulcom 10604  ax-addass 10605  ax-mulass 10606  ax-distr 10607  ax-i2m1 10608  ax-1ne0 10609  ax-1rid 10610  ax-rnegex 10611  ax-rrecex 10612  ax-cnre 10613  ax-pre-lttri 10614  ax-pre-lttrn 10615  ax-pre-ltadd 10616  ax-pre-mulgt0 10617  ax-pre-sup 10618
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7117  df-ov 7162  df-oprab 7163  df-mpo 7164  df-om 7584  df-2nd 7693  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-2o 8106  df-er 8292  df-en 8513  df-dom 8514  df-sdom 8515  df-fin 8516  df-sup 8909  df-inf 8910  df-pnf 10680  df-mnf 10681  df-xr 10682  df-ltxr 10683  df-le 10684  df-sub 10875  df-neg 10876  df-div 11301  df-nn 11642  df-2 11703  df-3 11704  df-n0 11901  df-z 11985  df-uz 12247  df-rp 12393  df-fl 13165  df-mod 13241  df-seq 13373  df-exp 13433  df-cj 14461  df-re 14462  df-im 14463  df-sqrt 14597  df-abs 14598  df-dvds 15611  df-gcd 15847  df-prm 16019
This theorem is referenced by:  2sqmo  26016
  Copyright terms: Public domain W3C validator