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 
|- ( ph -> P e. Prime )
2sqmod.2 
|- ( ph -> A e. NN0 )
2sqmod.3 
|- ( ph -> B e. NN0 )
2sqmod.4 
|- ( ph -> C e. NN0 )
2sqmod.5 
|- ( ph -> D e. NN0 )
2sqmod.6 
|- ( ph -> A <_ B )
2sqmod.7 
|- ( ph -> C <_ D )
2sqmod.8 
|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = P )
2sqmod.9 
|- ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) = P )
Assertion 2sqmod 
|- ( ph -> ( A = C /\ B = D ) )

Proof

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