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 29425
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 481 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐵)
3 2sqmod.4 . . . . . . . 8 (𝜑𝐶 ∈ ℕ0)
43nn0red 11297 . . . . . . 7 (𝜑𝐶 ∈ ℝ)
54adantr 481 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 ∈ ℝ)
6 2sqmod.3 . . . . . . . 8 (𝜑𝐵 ∈ ℕ0)
76nn0red 11297 . . . . . . 7 (𝜑𝐵 ∈ ℝ)
87adantr 481 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∈ ℝ)
93nn0ge0d 11299 . . . . . . 7 (𝜑 → 0 ≤ 𝐶)
109adantr 481 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐶)
116nn0ge0d 11299 . . . . . . 7 (𝜑 → 0 ≤ 𝐵)
1211adantr 481 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐵)
133nn0cnd 11298 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
1413sqcld 12943 . . . . . . . 8 (𝜑 → (𝐶↑2) ∈ ℂ)
1514adantr 481 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) ∈ ℂ)
166nn0cnd 11298 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
1716sqcld 12943 . . . . . . . 8 (𝜑 → (𝐵↑2) ∈ ℂ)
1817adantr 481 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ)
19 2sqmod.2 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℕ0)
2019nn0cnd 11298 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
2120sqcld 12943 . . . . . . . . . . 11 (𝜑 → (𝐴↑2) ∈ ℂ)
22 2sqmod.5 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ ℕ0)
2322nn0cnd 11298 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℂ)
2423sqcld 12943 . . . . . . . . . . 11 (𝜑 → (𝐷↑2) ∈ ℂ)
25 2sqmod.8 . . . . . . . . . . . 12 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃)
26 2sqmod.9 . . . . . . . . . . . 12 (𝜑 → ((𝐶↑2) + (𝐷↑2)) = 𝑃)
2725, 26eqtr4d 2663 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) + (𝐵↑2)) = ((𝐶↑2) + (𝐷↑2)))
2821, 17, 14, 24, 27subaddeqd 10391 . . . . . . . . . 10 (𝜑 → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2)))
2928adantr 481 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2)))
3019nn0zd 11424 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℤ)
313nn0zd 11424 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℤ)
32 dvdsmul1 14922 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐶))
3330, 31, 32syl2anc 692 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∥ (𝐴 · 𝐶))
3433adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐴 · 𝐶))
3520, 13mulcld 10005 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
3635adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) ∈ ℂ)
3716, 23mulcld 10005 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
3837adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 · 𝐷) ∈ ℂ)
3919nn0red 11297 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
4039, 4remulcld 10015 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 · 𝐶) ∈ ℝ)
4122nn0red 11297 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷 ∈ ℝ)
427, 41remulcld 10015 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 · 𝐷) ∈ ℝ)
4340, 42resubcld 10403 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℝ)
4443recnd 10013 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ)
4544adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ)
4643sqge0d 12973 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2))
47 2sqmod.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑃 ∈ ℙ)
486nn0zd 11424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐵 ∈ ℤ)
4947, 30, 48, 252sqn0 29423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐴 ≠ 0)
50 elnnne0 11251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐴 ∈ ℕ ↔ (𝐴 ∈ ℕ0𝐴 ≠ 0))
5119, 49, 50sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐴 ∈ ℕ)
5222nn0zd 11424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐷 ∈ ℤ)
5324, 14addcomd 10183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((𝐷↑2) + (𝐶↑2)) = ((𝐶↑2) + (𝐷↑2)))
5453, 26eqtrd 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝐷↑2) + (𝐶↑2)) = 𝑃)
5547, 52, 31, 542sqn0 29423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐷 ≠ 0)
56 elnnne0 11251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐷 ∈ ℕ ↔ (𝐷 ∈ ℕ0𝐷 ≠ 0))
5722, 55, 56sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 ∈ ℕ)
5851, 57nnmulcld 11013 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 · 𝐷) ∈ ℕ)
5947, 31, 52, 262sqn0 29423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐶 ≠ 0)
60 elnnne0 11251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐶 ∈ ℕ ↔ (𝐶 ∈ ℕ0𝐶 ≠ 0))
613, 59, 60sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐶 ∈ ℕ)
6217, 21addcomd 10183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((𝐵↑2) + (𝐴↑2)) = ((𝐴↑2) + (𝐵↑2)))
6362, 25eqtrd 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝐵↑2) + (𝐴↑2)) = 𝑃)
6447, 48, 30, 632sqn0 29423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ≠ 0)
65 elnnne0 11251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ ℕ ↔ (𝐵 ∈ ℕ0𝐵 ≠ 0))
666, 64, 65sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ ℕ)
6761, 66nnmulcld 11013 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐶 · 𝐵) ∈ ℕ)
6858, 67nnaddcld 11012 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℕ)
6968nnsqcld 12966 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ)
7069nnred 10980 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℝ)
7143resqcld 12972 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℝ)
7270, 71addge02d 10561 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
7346, 72mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
7425, 26oveq12d 6623 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = (𝑃 · 𝑃))
75 bhmafibid1 29421 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
7639, 7, 4, 41, 75syl22anc 1324 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
7774, 76eqtr3d 2662 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
78 prmz 15308 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
7947, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑃 ∈ ℤ)
8079zcnd 11427 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℂ)
8180sqvald 12942 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑2) = (𝑃 · 𝑃))
8213, 16mulcomd 10006 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
8382oveq2d 6621 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
8483oveq1d 6620 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))
8584oveq2d 6621 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
8677, 81, 853eqtr4d 2670 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
8773, 86breqtrrd 4646 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2))
8887adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2))
8930, 52zmulcld 11432 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 · 𝐷) ∈ ℤ)
9031, 48zmulcld 11432 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐶 · 𝐵) ∈ ℤ)
9189, 90zaddcld 11430 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ)
92 dvdssqim 15192 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9379, 91, 92syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
94 zsqcl 12871 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℤ → (𝑃↑2) ∈ ℤ)
9579, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑2) ∈ ℤ)
96 dvdsle 14951 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃↑2) ∈ ℤ ∧ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9795, 69, 96syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9893, 97syld 47 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
9998imp 445 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))
10095zred 11426 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) ∈ ℝ)
10170, 100letri3d 10124 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
102101adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))))
10388, 99, 102mpbir2and 956 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2))
10486adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
105103, 104eqtr2d 2661 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))
10670recnd 10013 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℂ)
10771recnd 10013 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℂ)
108106, 106, 107subadd2d 10356 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
109108adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))
110105, 109mpbird 247 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2))
111106subidd 10325 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0)
112111adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0)
113110, 112eqtr3d 2662 . . . . . . . . . . . . . . . 16 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) = 0)
11445, 113sqeq0d 12944 . . . . . . . . . . . . . . 15 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) = 0)
11536, 38, 114subeq0d 10345 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) = (𝐵 · 𝐷))
11634, 115breqtrd 4644 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐵 · 𝐷))
11747, 30, 48, 252sqcoprm 29424 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 gcd 𝐵) = 1)
118117adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 gcd 𝐵) = 1)
119 coprmdvds 15285 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
12030, 48, 52, 119syl3anc 1323 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
121120adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴𝐷))
122116, 118, 121mp2and 714 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐷)
123 dvdsle 14951 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐴𝐷𝐴𝐷))
12430, 57, 123syl2anc 692 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐷𝐴𝐷))
125124adantr 481 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴𝐷𝐴𝐷))
126122, 125mpd 15 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐷)
12751nnrpd 11814 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ+)
128127rprege0d 11823 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
12922nn0ge0d 11299 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ 𝐷)
130 le2sq 12875 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷)) → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
131128, 41, 129, 130syl12anc 1321 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
132131adantr 481 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2)))
133126, 132mpbid 222 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ≤ (𝐷↑2))
13451nnsqcld 12966 . . . . . . . . . . . . 13 (𝜑 → (𝐴↑2) ∈ ℕ)
135134nnred 10980 . . . . . . . . . . . 12 (𝜑 → (𝐴↑2) ∈ ℝ)
136 zsqcl 12871 . . . . . . . . . . . . . 14 (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
13752, 136syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐷↑2) ∈ ℤ)
138137zred 11426 . . . . . . . . . . . 12 (𝜑 → (𝐷↑2) ∈ ℝ)
139135, 138suble0d 10563 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2)))
140139adantr 481 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2)))
141133, 140mpbird 247 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) ≤ 0)
14229, 141eqbrtrrd 4642 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) ≤ 0)
143 dvdsmul1 14922 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → 𝐵 ∥ (𝐵 · 𝐷))
14448, 52, 143syl2anc 692 . . . . . . . . . . . . . 14 (𝜑𝐵 ∥ (𝐵 · 𝐷))
145144adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐵 · 𝐷))
146145, 115breqtrrd 4646 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐴 · 𝐶))
147 gcdcom 15154 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
14830, 48, 147syl2anc 692 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
149148, 117eqtr3d 2662 . . . . . . . . . . . . 13 (𝜑 → (𝐵 gcd 𝐴) = 1)
150149adantr 481 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 gcd 𝐴) = 1)
151 coprmdvds 15285 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
15248, 30, 31, 151syl3anc 1323 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
153152adantr 481 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵𝐶))
154146, 150, 153mp2and 714 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵𝐶)
155 dvdsle 14951 . . . . . . . . . . . . 13 ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) → (𝐵𝐶𝐵𝐶))
15648, 61, 155syl2anc 692 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐶𝐵𝐶))
157156adantr 481 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵𝐶𝐵𝐶))
158154, 157mpd 15 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵𝐶)
1597, 4, 11, 9le2sqd 12981 . . . . . . . . . . 11 (𝜑 → (𝐵𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2)))
160159adantr 481 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2)))
161158, 160mpbid 222 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ≤ (𝐶↑2))
1624resqcld 12972 . . . . . . . . . . 11 (𝜑 → (𝐶↑2) ∈ ℝ)
163 zsqcl 12871 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
16448, 163syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵↑2) ∈ ℤ)
165164zred 11426 . . . . . . . . . . 11 (𝜑 → (𝐵↑2) ∈ ℝ)
166162, 165subge0d 10562 . . . . . . . . . 10 (𝜑 → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2)))
167166adantr 481 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2)))
168161, 167mpbird 247 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐶↑2) − (𝐵↑2)))
169135, 138resubcld 10403 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) − (𝐷↑2)) ∈ ℝ)
17028, 169eqeltrrd 2705 . . . . . . . . . 10 (𝜑 → ((𝐶↑2) − (𝐵↑2)) ∈ ℝ)
171 0red 9986 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
172170, 171letri3d 10124 . . . . . . . . 9 (𝜑 → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2)))))
173172adantr 481 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2)))))
174142, 168, 173mpbir2and 956 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) = 0)
17515, 18, 174subeq0d 10345 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) = (𝐵↑2))
1765, 8, 10, 12, 175sq11d 12982 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 = 𝐵)
1772, 176breqtrrd 4646 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴𝐶)
178 2sqmod.7 . . . . . 6 (𝜑𝐶𝐷)
179178adantr 481 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶𝐷)
18039adantr 481 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∈ ℝ)
18141adantr 481 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐷 ∈ ℝ)
18219nn0ge0d 11299 . . . . . . 7 (𝜑 → 0 ≤ 𝐴)
183182adantr 481 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐴)
184129adantr 481 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐷)
18521adantr 481 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ∈ ℂ)
18624adantr 481 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ)
187168, 29breqtrrd 4646 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐴↑2) − (𝐷↑2)))
188169, 171letri3d 10124 . . . . . . . . 9 (𝜑 → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2)))))
189188adantr 481 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2)))))
190141, 187, 189mpbir2and 956 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = 0)
191185, 186, 190subeq0d 10345 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) = (𝐷↑2))
192180, 181, 183, 184, 191sq11d 12982 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐷)
193179, 192breqtrrd 4646 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶𝐴)
19439, 4letri3d 10124 . . . . 5 (𝜑 → (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴)))
195194adantr 481 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴)))
196177, 193, 195mpbir2and 956 . . 3 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐶)
19720adantr 481 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 ∈ ℂ)
19813adantr 481 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐶 ∈ ℂ)
19916adantr 481 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℂ)
20064adantr 481 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ≠ 0)
20141adantr 481 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 ∈ ℝ)
2027adantr 481 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℝ)
203129adantr 481 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐷)
20411adantr 481 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐵)
20524adantr 481 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ)
20617adantr 481 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ)
207 prmnn 15307 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
20847, 207syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℕ)
209208nnne0d 11010 . . . . . . . . . . 11 (𝜑𝑃 ≠ 0)
210209neneqd 2801 . . . . . . . . . 10 (𝜑 → ¬ 𝑃 = 0)
211210adantr 481 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ¬ 𝑃 = 0)
21280, 24, 17subdid 10431 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))))
21380, 24mulcld 10005 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 · (𝐷↑2)) ∈ ℂ)
21421, 24mulcld 10005 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴↑2) · (𝐷↑2)) ∈ ℂ)
21580, 17mulcld 10005 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 · (𝐵↑2)) ∈ ℂ)
21614, 17mulcld 10005 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶↑2) · (𝐵↑2)) ∈ ℂ)
21717, 24mulcomd 10006 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵↑2) · (𝐷↑2)) = ((𝐷↑2) · (𝐵↑2)))
21825oveq1d 6620 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝑃 − (𝐴↑2)))
21921, 17pncan2d 10339 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝐵↑2))
220218, 219eqtr3d 2662 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 − (𝐴↑2)) = (𝐵↑2))
221220oveq1d 6620 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝐵↑2) · (𝐷↑2)))
22226oveq1d 6620 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝑃 − (𝐶↑2)))
22314, 24pncan2d 10339 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝐷↑2))
224222, 223eqtr3d 2662 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 − (𝐶↑2)) = (𝐷↑2))
225224oveq1d 6620 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝐷↑2) · (𝐵↑2)))
226217, 221, 2253eqtr4d 2670 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 − (𝐶↑2)) · (𝐵↑2)))
22780, 21, 24subdird 10432 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))))
22880, 14, 17subdird 10432 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2))))
229226, 227, 2283eqtr3d 2668 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2))))
230213, 214, 215, 216, 229subeqxfrd 29345 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
231212, 230eqtrd 2660 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
23220, 23sqmuld 12957 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐷)↑2) = ((𝐴↑2) · (𝐷↑2)))
23313, 16sqmuld 12957 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵)↑2) = ((𝐶↑2) · (𝐵↑2)))
234232, 233oveq12d 6623 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2))))
23520, 23mulcld 10005 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
23613, 16mulcld 10005 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 · 𝐵) ∈ ℂ)
237 subsq 12909 . . . . . . . . . . . . . . 15 (((𝐴 · 𝐷) ∈ ℂ ∧ (𝐶 · 𝐵) ∈ ℂ) → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
238235, 236, 237syl2anc 692 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
239231, 234, 2383eqtr2d 2666 . . . . . . . . . . . . 13 (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
240239adantr 481 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
241235adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) ∈ ℂ)
242 simpll 789 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → 𝜑)
243 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵))
244243neqned 2803 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵))
24589, 90zsubcld 11431 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ)
246 dvdssqim 15192 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
24779, 245, 246syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
248247imp 445 . . . . . . . . . . . . . . . . 17 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
249248adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
25095adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝑃↑2) ∈ ℤ)
251245adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ)
252235adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ∈ ℂ)
253236adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐶 · 𝐵) ∈ ℂ)
254 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵))
255252, 253, 254subne0d 10346 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ≠ 0)
256251, 255znsqcld 29346 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ)
257 dvdsle 14951 . . . . . . . . . . . . . . . . . 18 (((𝑃↑2) ∈ ℤ ∧ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
258250, 256, 257syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
259258imp 445 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) ∧ (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
260242, 244, 249, 259syl21anc 1322 . . . . . . . . . . . . . . 15 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
26139, 41remulcld 10015 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐷) ∈ ℝ)
2624, 7remulcld 10015 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐶 · 𝐵) ∈ ℝ)
263261, 262resubcld 10403 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℝ)
264263resqcld 12972 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℝ)
26561nnrpd 11814 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐶 ∈ ℝ+)
266127, 265rpmulcld 11832 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 · 𝐶) ∈ ℝ+)
26766nnrpd 11814 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ+)
26857nnrpd 11814 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐷 ∈ ℝ+)
269267, 268rpmulcld 11832 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐵 · 𝐷) ∈ ℝ+)
270266, 269rpaddcld 11831 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 · 𝐶) + (𝐵 · 𝐷)) ∈ ℝ+)
271 2z 11354 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℤ
272271a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℤ)
273270, 272rpexpcld 12969 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) ∈ ℝ+)
274264, 273ltaddrp2d 11850 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
275 bhmafibid2 29422 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27639, 7, 4, 41, 275syl22anc 1324 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27774, 276eqtr3d 2662 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
27882oveq2d 6621 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = ((𝐴 · 𝐷) − (𝐵 · 𝐶)))
279278oveq1d 6620 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))
280279oveq2d 6621 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)))
281277, 280eqtr4d 2663 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
282274, 281breqtrrd 4646 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃 · 𝑃))
283282, 81breqtrrd 4646 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2))
284242, 283syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2))
285264, 100ltnled 10129 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
286242, 285syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)))
287284, 286mpbid 222 . . . . . . . . . . . . . . 15 (((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))
288260, 287condan 834 . . . . . . . . . . . . . 14 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐶 · 𝐵))
289241, 288subeq0bd 10401 . . . . . . . . . . . . 13 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = 0)
290289oveq2d 6621 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0))
291235, 236addcld 10004 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℂ)
292291mul01d 10180 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0)
293292adantr 481 . . . . . . . . . . . 12 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0)
294240, 290, 2933eqtrd 2664 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0)
29524, 17subcld 10337 . . . . . . . . . . . . 13 (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℂ)
29680, 295mul0ord 10622 . . . . . . . . . . . 12 (𝜑 → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)))
297296adantr 481 . . . . . . . . . . 11 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)))
298294, 297mpbid 222 . . . . . . . . . 10 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0))
299298ord 392 . . . . . . . . 9 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (¬ 𝑃 = 0 → ((𝐷↑2) − (𝐵↑2)) = 0))
300211, 299mpd 15 . . . . . . . 8 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐷↑2) − (𝐵↑2)) = 0)
301205, 206, 300subeq0d 10345 . . . . . . 7 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) = (𝐵↑2))
302201, 202, 203, 204, 301sq11d 12982 . . . . . 6 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 = 𝐵)
303302oveq2d 6621 . . . . 5 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐴 · 𝐵))
304303, 288eqtr3d 2662 . . . 4 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐵) = (𝐶 · 𝐵))
305197, 198, 199, 200, 304mulcan2ad 10608 . . 3 ((𝜑𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 = 𝐶)
306137, 164zsubcld 11431 . . . . . 6 (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℤ)
307 dvdsmul1 14922 . . . . . 6 ((𝑃 ∈ ℤ ∧ ((𝐷↑2) − (𝐵↑2)) ∈ ℤ) → 𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2))))
30879, 306, 307syl2anc 692 . . . . 5 (𝜑𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2))))
309308, 239breqtrd 4644 . . . 4 (𝜑𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
310 euclemma 15344 . . . . 5 ((𝑃 ∈ ℙ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))))
31147, 91, 245, 310syl3anc 1323 . . . 4 (𝜑 → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))))
312309, 311mpbid 222 . . 3 (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))))
313196, 305, 312mpjaodan 826 . 2 (𝜑𝐴 = 𝐶)
314313oveq1d 6620 . . . . 5 (𝜑 → (𝐴↑2) = (𝐶↑2))
315314oveq2d 6621 . . . 4 (𝜑 → (𝑃 − (𝐴↑2)) = (𝑃 − (𝐶↑2)))
316315, 220, 2243eqtr3d 2668 . . 3 (𝜑 → (𝐵↑2) = (𝐷↑2))
3177, 41, 11, 129, 316sq11d 12982 . 2 (𝜑𝐵 = 𝐷)
318313, 317jca 554 1 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1992  wne 2796   class class class wbr 4618  (class class class)co 6605  cc 9879  cr 9880  0cc0 9881  1c1 9882   + caddc 9884   · cmul 9886   < clt 10019  cle 10020  cmin 10211  cn 10965  2c2 11015  0cn0 11237  cz 11322  cexp 12797  cdvds 14902   gcd cgcd 15135  cprime 15304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958  ax-pre-sup 9959
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-2o 7507  df-oadd 7510  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-sup 8293  df-inf 8294  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-nn 10966  df-2 11024  df-3 11025  df-n0 11238  df-z 11323  df-uz 11632  df-rp 11777  df-fl 12530  df-mod 12606  df-seq 12739  df-exp 12798  df-cj 13768  df-re 13769  df-im 13770  df-sqrt 13904  df-abs 13905  df-dvds 14903  df-gcd 15136  df-prm 15305
This theorem is referenced by:  2sqmo  29426
  Copyright terms: Public domain W3C validator