Metamath Proof Explorer

Theorem 2sqmod

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)

Ref Expression
Hypotheses 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 2sqmod ( 𝜑 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 2sqmod.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2 2sqmod.2 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
3 2sqmod.3 ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
4 2sqmod.4 ⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
5 2sqmod.5 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
6 2sqmod.6 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
7 2sqmod.7 ⊢ ( 𝜑 → 𝐶 ≤ 𝐷 )
8 2sqmod.8 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 )
9 2sqmod.9 ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) = 𝑃 )
10 6 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ≤ 𝐵 )
11 4 nn0red ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐶 ∈ ℝ )
13 3 nn0red ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∈ ℝ )
15 4 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐶 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐶 )
17 3 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐵 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐵 )
19 4 nn0cnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
20 19 sqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
22 3 nn0cnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
23 22 sqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
25 2 nn0cnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
26 25 sqcld ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
27 5 nn0cnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
28 27 sqcld ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
29 8 9 eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
30 26 23 20 28 29 subaddeqd ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
32 2 nn0zd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
33 4 nn0zd ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
34 dvdsmul1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∥ ( 𝐴 · 𝐶 ) )
35 32 33 34 syl2anc ⊢ ( 𝜑 → 𝐴 ∥ ( 𝐴 · 𝐶 ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ∥ ( 𝐴 · 𝐶 ) )
37 25 19 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
39 22 27 mulcld ⊢ ( 𝜑 → ( 𝐵 · 𝐷 ) ∈ ℂ )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 · 𝐷 ) ∈ ℂ )
41 2 nn0red ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
42 41 11 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℝ )
43 5 nn0red ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
44 13 43 remulcld ⊢ ( 𝜑 → ( 𝐵 · 𝐷 ) ∈ ℝ )
45 42 44 resubcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ∈ ℝ )
46 45 recnd ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ∈ ℂ )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ∈ ℂ )
48 45 sqge0d ⊢ ( 𝜑 → 0 ≤ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) )
49 3 nn0zd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
50 1 32 49 8 2sqn0 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
51 elnnne0 ⊢ ( 𝐴 ∈ ℕ ↔ ( 𝐴 ∈ ℕ0 ∧ 𝐴 ≠ 0 ) )
52 2 50 51 sylanbrc ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
53 5 nn0zd ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
54 28 20 addcomd ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
55 54 9 eqtrd ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 )
56 1 53 33 55 2sqn0 ⊢ ( 𝜑 → 𝐷 ≠ 0 )
57 elnnne0 ⊢ ( 𝐷 ∈ ℕ ↔ ( 𝐷 ∈ ℕ0 ∧ 𝐷 ≠ 0 ) )
58 5 56 57 sylanbrc ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
59 52 58 nnmulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℕ )
60 1 33 53 9 2sqn0 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
61 elnnne0 ⊢ ( 𝐶 ∈ ℕ ↔ ( 𝐶 ∈ ℕ0 ∧ 𝐶 ≠ 0 ) )
62 4 60 61 sylanbrc ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
63 23 26 addcomd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
64 63 8 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = 𝑃 )
65 1 49 32 64 2sqn0 ⊢ ( 𝜑 → 𝐵 ≠ 0 )
66 elnnne0 ⊢ ( 𝐵 ∈ ℕ ↔ ( 𝐵 ∈ ℕ0 ∧ 𝐵 ≠ 0 ) )
67 3 65 66 sylanbrc ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
68 62 67 nnmulcld ⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℕ )
69 59 68 nnaddcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℕ )
70 69 nnsqcld ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℕ )
71 70 nnred ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℝ )
72 45 resqcld ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) ∈ ℝ )
73 71 72 addge02d ⊢ ( 𝜑 → ( 0 ≤ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) ↔ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) ) )
74 48 73 mpbid ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
75 8 9 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( 𝑃 · 𝑃 ) )
76 bhmafibid1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
77 41 13 11 43 76 syl22anc ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
78 75 77 eqtr3d ⊢ ( 𝜑 → ( 𝑃 · 𝑃 ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
79 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
80 1 79 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
81 80 zcnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
82 81 sqvald ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) = ( 𝑃 · 𝑃 ) )
83 19 22 mulcomd ⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) = ( 𝐵 · 𝐶 ) )
84 83 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) )
85 84 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) )
86 85 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
87 78 82 86 3eqtr4d ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
88 74 87 breqtrrd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( 𝑃 ↑ 2 ) )
89 88 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( 𝑃 ↑ 2 ) )
90 32 53 zmulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℤ )
91 33 49 zmulcld ⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℤ )
92 90 91 zaddcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℤ )
93 dvdssqim ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
94 80 92 93 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
95 zsqcl ⊢ ( 𝑃 ∈ ℤ → ( 𝑃 ↑ 2 ) ∈ ℤ )
96 80 95 syl ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℤ )
97 dvdsle ⊢ ( ( ( 𝑃 ↑ 2 ) ∈ ℤ ∧ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℕ ) → ( ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
98 96 70 97 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
99 94 98 syld ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
100 99 imp ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
101 96 zred ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℝ )
102 71 101 letri3d ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) = ( 𝑃 ↑ 2 ) ↔ ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( 𝑃 ↑ 2 ) ∧ ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) ) )
103 102 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) = ( 𝑃 ↑ 2 ) ↔ ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( 𝑃 ↑ 2 ) ∧ ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) ) )
104 89 100 103 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) = ( 𝑃 ↑ 2 ) )
105 87 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
106 104 105 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
107 71 recnd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℂ )
108 72 recnd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) ∈ ℂ )
109 107 107 108 subadd2d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) − ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) ↔ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
110 109 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) − ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) ↔ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
111 106 110 mpbird ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) − ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) )
112 107 subidd ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) − ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = 0 )
113 112 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) − ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = 0 )
114 111 113 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) = 0 )
115 47 114 sqeq0d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) = 0 )
116 38 40 115 subeq0d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐷 ) )
117 36 116 breqtrd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ∥ ( 𝐵 · 𝐷 ) )
118 1 32 49 8 2sqcoprm ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
119 118 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 gcd 𝐵 ) = 1 )
120 coprmdvds ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ( 𝐴 ∥ ( 𝐵 · 𝐷 ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐴 ∥ 𝐷 ) )
121 32 49 53 120 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 ∥ ( 𝐵 · 𝐷 ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐴 ∥ 𝐷 ) )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 ∥ ( 𝐵 · 𝐷 ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐴 ∥ 𝐷 ) )
123 117 119 122 mp2and ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ∥ 𝐷 )
124 dvdsle ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ∥ 𝐷 → 𝐴 ≤ 𝐷 ) )
125 32 58 124 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∥ 𝐷 → 𝐴 ≤ 𝐷 ) )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 ∥ 𝐷 → 𝐴 ≤ 𝐷 ) )
127 123 126 mpd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ≤ 𝐷 )
128 52 nnrpd ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
129 128 rprege0d ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
130 5 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐷 )
131 le2sq ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 ≤ 𝐷 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) ) )
132 129 43 130 131 syl12anc ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐷 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) ) )
133 132 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 ≤ 𝐷 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) ) )
134 127 133 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) )
135 52 nnsqcld ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℕ )
136 135 nnred ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℝ )
137 zsqcl ⊢ ( 𝐷 ∈ ℤ → ( 𝐷 ↑ 2 ) ∈ ℤ )
138 53 137 syl ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℤ )
139 138 zred ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℝ )
140 136 139 suble0d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ≤ 0 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) ) )
141 140 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ≤ 0 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) ) )
142 134 141 mpbird ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ≤ 0 )
143 31 142 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ≤ 0 )
144 dvdsmul1 ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → 𝐵 ∥ ( 𝐵 · 𝐷 ) )
145 49 53 144 syl2anc ⊢ ( 𝜑 → 𝐵 ∥ ( 𝐵 · 𝐷 ) )
146 145 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∥ ( 𝐵 · 𝐷 ) )
147 146 116 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∥ ( 𝐴 · 𝐶 ) )
148 32 49 gcdcomd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = ( 𝐵 gcd 𝐴 ) )
149 148 118 eqtr3d ⊢ ( 𝜑 → ( 𝐵 gcd 𝐴 ) = 1 )
150 149 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 gcd 𝐴 ) = 1 )
151 coprmdvds ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐵 ∥ ( 𝐴 · 𝐶 ) ∧ ( 𝐵 gcd 𝐴 ) = 1 ) → 𝐵 ∥ 𝐶 ) )
152 49 32 33 151 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 ∥ ( 𝐴 · 𝐶 ) ∧ ( 𝐵 gcd 𝐴 ) = 1 ) → 𝐵 ∥ 𝐶 ) )
153 152 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐵 ∥ ( 𝐴 · 𝐶 ) ∧ ( 𝐵 gcd 𝐴 ) = 1 ) → 𝐵 ∥ 𝐶 ) )
154 147 150 153 mp2and ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∥ 𝐶 )
155 dvdsle ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 ∥ 𝐶 → 𝐵 ≤ 𝐶 ) )
156 49 62 155 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∥ 𝐶 → 𝐵 ≤ 𝐶 ) )
157 156 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 ∥ 𝐶 → 𝐵 ≤ 𝐶 ) )
158 154 157 mpd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐵 ≤ 𝐶 )
159 13 11 17 15 le2sqd ⊢ ( 𝜑 → ( 𝐵 ≤ 𝐶 ↔ ( 𝐵 ↑ 2 ) ≤ ( 𝐶 ↑ 2 ) ) )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 ≤ 𝐶 ↔ ( 𝐵 ↑ 2 ) ≤ ( 𝐶 ↑ 2 ) ) )
161 158 160 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 ↑ 2 ) ≤ ( 𝐶 ↑ 2 ) )
162 11 resqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℝ )
163 zsqcl ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 2 ) ∈ ℤ )
164 49 163 syl ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℤ )
165 164 zred ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ )
166 162 165 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ↔ ( 𝐵 ↑ 2 ) ≤ ( 𝐶 ↑ 2 ) ) )
167 166 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 0 ≤ ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ↔ ( 𝐵 ↑ 2 ) ≤ ( 𝐶 ↑ 2 ) ) )
168 161 167 mpbird ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
169 136 139 resubcld ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ∈ ℝ )
170 30 169 eqeltrrd ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℝ )
171 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
172 170 171 letri3d ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
173 172 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
174 143 168 173 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 )
175 21 24 174 subeq0d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐶 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
176 12 14 16 18 175 sq11d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐶 = 𝐵 )
177 10 176 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ≤ 𝐶 )
178 7 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐶 ≤ 𝐷 )
179 41 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ∈ ℝ )
180 43 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐷 ∈ ℝ )
181 2 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐴 )
182 181 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐴 )
183 130 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐷 )
184 26 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
185 28 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐷 ↑ 2 ) ∈ ℂ )
186 168 31 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) )
187 169 171 letri3d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = 0 ↔ ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ) ) )
188 187 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = 0 ↔ ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ) ) )
189 142 186 188 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = 0 )
190 184 185 189 subeq0d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 ↑ 2 ) = ( 𝐷 ↑ 2 ) )
191 179 180 182 183 190 sq11d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 = 𝐷 )
192 178 191 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐶 ≤ 𝐴 )
193 41 11 letri3d ⊢ ( 𝜑 → ( 𝐴 = 𝐶 ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) ) )
194 193 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 = 𝐶 ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) ) )
195 177 192 194 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 = 𝐶 )
196 25 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐴 ∈ ℂ )
197 19 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐶 ∈ ℂ )
198 22 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∈ ℂ )
199 65 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐵 ≠ 0 )
200 43 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐷 ∈ ℝ )
201 13 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∈ ℝ )
202 130 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐷 )
203 17 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐵 )
204 28 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐷 ↑ 2 ) ∈ ℂ )
205 23 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
206 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
207 1 206 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
208 207 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
209 208 neneqd ⊢ ( 𝜑 → ¬ 𝑃 = 0 )
210 209 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ¬ 𝑃 = 0 )
211 81 28 23 subdid ⊢ ( 𝜑 → ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = ( ( 𝑃 · ( 𝐷 ↑ 2 ) ) − ( 𝑃 · ( 𝐵 ↑ 2 ) ) ) )
212 81 28 mulcld ⊢ ( 𝜑 → ( 𝑃 · ( 𝐷 ↑ 2 ) ) ∈ ℂ )
213 26 28 mulcld ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ∈ ℂ )
214 81 23 mulcld ⊢ ( 𝜑 → ( 𝑃 · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
215 20 23 mulcld ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
216 23 28 mulcomd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) = ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
217 8 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐴 ↑ 2 ) ) = ( 𝑃 − ( 𝐴 ↑ 2 ) ) )
218 26 23 pncan2d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐴 ↑ 2 ) ) = ( 𝐵 ↑ 2 ) )
219 217 218 eqtr3d ⊢ ( 𝜑 → ( 𝑃 − ( 𝐴 ↑ 2 ) ) = ( 𝐵 ↑ 2 ) )
220 219 oveq1d ⊢ ( 𝜑 → ( ( 𝑃 − ( 𝐴 ↑ 2 ) ) · ( 𝐷 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) )
221 9 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( 𝐶 ↑ 2 ) ) = ( 𝑃 − ( 𝐶 ↑ 2 ) ) )
222 20 28 pncan2d ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( 𝐶 ↑ 2 ) ) = ( 𝐷 ↑ 2 ) )
223 221 222 eqtr3d ⊢ ( 𝜑 → ( 𝑃 − ( 𝐶 ↑ 2 ) ) = ( 𝐷 ↑ 2 ) )
224 223 oveq1d ⊢ ( 𝜑 → ( ( 𝑃 − ( 𝐶 ↑ 2 ) ) · ( 𝐵 ↑ 2 ) ) = ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
225 216 220 224 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑃 − ( 𝐴 ↑ 2 ) ) · ( 𝐷 ↑ 2 ) ) = ( ( 𝑃 − ( 𝐶 ↑ 2 ) ) · ( 𝐵 ↑ 2 ) ) )
226 81 26 28 subdird ⊢ ( 𝜑 → ( ( 𝑃 − ( 𝐴 ↑ 2 ) ) · ( 𝐷 ↑ 2 ) ) = ( ( 𝑃 · ( 𝐷 ↑ 2 ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) )
227 81 20 23 subdird ⊢ ( 𝜑 → ( ( 𝑃 − ( 𝐶 ↑ 2 ) ) · ( 𝐵 ↑ 2 ) ) = ( ( 𝑃 · ( 𝐵 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
228 225 226 227 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑃 · ( 𝐷 ↑ 2 ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) = ( ( 𝑃 · ( 𝐵 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
229 212 213 214 215 228 subeqxfrd ⊢ ( 𝜑 → ( ( 𝑃 · ( 𝐷 ↑ 2 ) ) − ( 𝑃 · ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
230 211 229 eqtrd ⊢ ( 𝜑 → ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
231 25 27 sqmuld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) )
232 19 22 sqmuld ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
233 231 232 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) − ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
234 25 27 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℂ )
235 19 22 mulcld ⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℂ )
236 subsq ⊢ ( ( ( 𝐴 · 𝐷 ) ∈ ℂ ∧ ( 𝐶 · 𝐵 ) ∈ ℂ ) → ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) − ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
237 234 235 236 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) − ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
238 230 233 237 3eqtr2d ⊢ ( 𝜑 → ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
239 238 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
240 234 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
241 simpll ⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → 𝜑 )
242 simpr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) )
243 242 neqned ⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) )
244 90 91 zsubcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ∈ ℤ )
245 dvdssqim ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
246 80 244 245 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
247 246 imp ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
248 247 adantr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
249 96 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∈ ℤ )
250 244 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ∈ ℤ )
251 234 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
252 235 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
253 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) )
254 251 252 253 subne0d ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ≠ 0 )
255 250 254 znsqcld ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℕ )
256 dvdsle ⊢ ( ( ( 𝑃 ↑ 2 ) ∈ ℤ ∧ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℕ ) → ( ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
257 249 255 256 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
258 257 imp ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) ∧ ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
259 241 243 248 258 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
260 41 43 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℝ )
261 11 13 remulcld ⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℝ )
262 260 261 resubcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ∈ ℝ )
263 262 resqcld ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℝ )
264 62 nnrpd ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
265 128 264 rpmulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℝ+ )
266 67 nnrpd ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
267 58 nnrpd ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
268 266 267 rpmulcld ⊢ ( 𝜑 → ( 𝐵 · 𝐷 ) ∈ ℝ+ )
269 265 268 rpaddcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ∈ ℝ+ )
270 2z ⊢ 2 ∈ ℤ
271 270 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
272 269 271 rpexpcld ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) ∈ ℝ+ )
273 263 272 ltaddrp2d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
274 bhmafibid2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
275 41 13 11 43 274 syl22anc ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
276 75 275 eqtr3d ⊢ ( 𝜑 → ( 𝑃 · 𝑃 ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
277 83 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) = ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) )
278 277 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) = ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) )
279 278 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
280 276 279 eqtr4d ⊢ ( 𝜑 → ( 𝑃 · 𝑃 ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
281 273 280 breqtrrd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( 𝑃 · 𝑃 ) )
282 281 82 breqtrrd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( 𝑃 ↑ 2 ) )
283 241 282 syl ⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( 𝑃 ↑ 2 ) )
284 263 101 ltnled ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( 𝑃 ↑ 2 ) ↔ ¬ ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
285 241 284 syl ⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ( ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( 𝑃 ↑ 2 ) ↔ ¬ ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
286 283 285 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ¬ ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
287 259 286 condan ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) )
288 240 287 subeq0bd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) = 0 )
289 288 oveq2d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · 0 ) )
290 234 235 addcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℂ )
291 290 mul01d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · 0 ) = 0 )
292 291 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · 0 ) = 0 )
293 239 289 292 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = 0 )
294 28 23 subcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℂ )
295 81 294 mul0ord ⊢ ( 𝜑 → ( ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = 0 ↔ ( 𝑃 = 0 ∨ ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ) ) )
296 295 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = 0 ↔ ( 𝑃 = 0 ∨ ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ) ) )
297 293 296 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 = 0 ∨ ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ) )
298 297 ord ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ¬ 𝑃 = 0 → ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ) )
299 210 298 mpd ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 )
300 204 205 299 subeq0d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐷 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
301 200 201 202 203 300 sq11d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐷 = 𝐵 )
302 301 oveq2d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐷 ) = ( 𝐴 · 𝐵 ) )
303 302 287 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐵 ) = ( 𝐶 · 𝐵 ) )
304 196 197 198 199 303 mulcan2ad ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐴 = 𝐶 )
305 138 164 zsubcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℤ )
306 dvdsmul1 ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℤ ) → 𝑃 ∥ ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
307 80 305 306 syl2anc ⊢ ( 𝜑 → 𝑃 ∥ ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
308 307 238 breqtrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
309 euclemma ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℤ ∧ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ↔ ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∨ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ) )
310 1 92 244 309 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ↔ ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∨ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ) )
311 308 310 mpbid ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∨ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
312 195 304 311 mpjaodan ⊢ ( 𝜑 → 𝐴 = 𝐶 )
313 312 oveq1d ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐶 ↑ 2 ) )
314 313 oveq2d ⊢ ( 𝜑 → ( 𝑃 − ( 𝐴 ↑ 2 ) ) = ( 𝑃 − ( 𝐶 ↑ 2 ) ) )
315 314 219 223 3eqtr3d ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) = ( 𝐷 ↑ 2 ) )
316 13 43 17 130 315 sq11d ⊢ ( 𝜑 → 𝐵 = 𝐷 )
317 312 316 jca ⊢ ( 𝜑 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )