Metamath Proof Explorer

Theorem flt4lem7

Description: Convert flt4lem5f into a convenient form for nna4b4nsq . TODO-SN: The change to ( A gcd B ) = 1 points at some inefficiency in the lemmas. (Contributed by SN, 25-Aug-2024)

Ref Expression
Hypotheses flt4lem7.a 
|- ( ph -> A e. NN )
flt4lem7.b 
|- ( ph -> B e. NN )
flt4lem7.c 
|- ( ph -> C e. NN )
flt4lem7.1 
|- ( ph -> -. 2 || A )
flt4lem7.2 
|- ( ph -> ( A gcd B ) = 1 )
flt4lem7.3 
|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) )
Assertion flt4lem7 
|- ( ph -> E. l e. NN ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < C ) )

Proof

Step Hyp Ref Expression
1 flt4lem7.a 
 |-  ( ph -> A e. NN )
2 flt4lem7.b 
 |-  ( ph -> B e. NN )
3 flt4lem7.c 
 |-  ( ph -> C e. NN )
4 flt4lem7.1 
 |-  ( ph -> -. 2 || A )
5 flt4lem7.2 
 |-  ( ph -> ( A gcd B ) = 1 )
6 flt4lem7.3 
 |-  ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) )
7 breq1 
 |-  ( l = ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( l < C <-> ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) < C ) )
8 oveq1 
 |-  ( l = ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( l ^ 2 ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) )
9 8 eqeq2d 
 |-  ( l = ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) <-> ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) )
10 9 anbi2d 
 |-  ( l = ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) <-> ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) ) )
11 10 2rexbidv 
 |-  ( l = ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( E. m e. NN E. n e. NN ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) <-> E. m e. NN E. n e. NN ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) ) )
12 7 11 anbi12d 
 |-  ( l = ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( l < C /\ E. m e. NN E. n e. NN ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) <-> ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) < C /\ E. m e. NN E. n e. NN ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) ) ) )
13 eqid 
 |-  ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) = ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 )
14 eqid 
 |-  ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) = ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 )
15 eqid 
 |-  ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) = ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 )
16 eqid 
 |-  ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) = ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 )
17 1 nnsqcld 
 |-  ( ph -> ( A ^ 2 ) e. NN )
18 2 nnsqcld 
 |-  ( ph -> ( B ^ 2 ) e. NN )
19 2nn0 
 |-  2 e. NN0
20 19 a1i 
 |-  ( ph -> 2 e. NN0 )
21 1 nncnd 
 |-  ( ph -> A e. CC )
22 21 flt4lem 
 |-  ( ph -> ( A ^ 4 ) = ( ( A ^ 2 ) ^ 2 ) )
23 2 nncnd 
 |-  ( ph -> B e. CC )
24 23 flt4lem 
 |-  ( ph -> ( B ^ 4 ) = ( ( B ^ 2 ) ^ 2 ) )
25 22 24 oveq12d 
 |-  ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) )
26 25 6 eqtr3d 
 |-  ( ph -> ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) )
27 2nn 
 |-  2 e. NN
28 27 a1i 
 |-  ( ph -> 2 e. NN )
29 rppwr 
 |-  ( ( A e. NN /\ B e. NN /\ 2 e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 ) )
30 1 2 28 29 syl3anc 
 |-  ( ph -> ( ( A gcd B ) = 1 -> ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 ) )
31 5 30 mpd 
 |-  ( ph -> ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 )
32 17 18 3 20 26 31 fltaccoprm 
 |-  ( ph -> ( ( A ^ 2 ) gcd C ) = 1 )
33 1 nnzd 
 |-  ( ph -> A e. ZZ )
34 3 nnzd 
 |-  ( ph -> C e. ZZ )
35 rpexp 
 |-  ( ( A e. ZZ /\ C e. ZZ /\ 2 e. NN ) -> ( ( ( A ^ 2 ) gcd C ) = 1 <-> ( A gcd C ) = 1 ) )
36 33 34 28 35 syl3anc 
 |-  ( ph -> ( ( ( A ^ 2 ) gcd C ) = 1 <-> ( A gcd C ) = 1 ) )
37 32 36 mpbid 
 |-  ( ph -> ( A gcd C ) = 1 )
38 13 14 15 16 1 2 3 4 37 6 flt4lem5e 
 |-  ( ph -> ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = 1 /\ ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) = 1 /\ ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) = 1 ) /\ ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. NN /\ ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. NN /\ ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) e. NN ) /\ ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) x. ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) x. ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) ) = ( ( B / 2 ) ^ 2 ) /\ ( B / 2 ) e. NN ) ) )
39 38 simp2d 
 |-  ( ph -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. NN /\ ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. NN /\ ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) e. NN ) )
40 39 simp3d 
 |-  ( ph -> ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) e. NN )
41 38 simp3d 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) x. ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) x. ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) ) = ( ( B / 2 ) ^ 2 ) /\ ( B / 2 ) e. NN ) )
42 41 simprd 
 |-  ( ph -> ( B / 2 ) e. NN )
43 gcdnncl 
 |-  ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) e. NN /\ ( B / 2 ) e. NN ) -> ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. NN )
44 40 42 43 syl2anc 
 |-  ( ph -> ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. NN )
45 44 nnred 
 |-  ( ph -> ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. RR )
46 42 nnred 
 |-  ( ph -> ( B / 2 ) e. RR )
47 3 nnred 
 |-  ( ph -> C e. RR )
48 40 nnzd 
 |-  ( ph -> ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) e. ZZ )
49 48 42 gcdle2d 
 |-  ( ph -> ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) <_ ( B / 2 ) )
50 2 nnred 
 |-  ( ph -> B e. RR )
51 2 nnrpd 
 |-  ( ph -> B e. RR+ )
52 rphalflt 
 |-  ( B e. RR+ -> ( B / 2 ) < B )
53 51 52 syl 
 |-  ( ph -> ( B / 2 ) < B )
54 18 nnred 
 |-  ( ph -> ( B ^ 2 ) e. RR )
55 4nn0 
 |-  4 e. NN0
56 55 a1i 
 |-  ( ph -> 4 e. NN0 )
57 2 56 nnexpcld 
 |-  ( ph -> ( B ^ 4 ) e. NN )
58 57 nnred 
 |-  ( ph -> ( B ^ 4 ) e. RR )
59 3 nnsqcld 
 |-  ( ph -> ( C ^ 2 ) e. NN )
60 59 nnred 
 |-  ( ph -> ( C ^ 2 ) e. RR )
61 2lt4 
 |-  2 < 4
62 2z 
 |-  2 e. ZZ
63 62 a1i 
 |-  ( ph -> 2 e. ZZ )
64 4z 
 |-  4 e. ZZ
65 64 a1i 
 |-  ( ph -> 4 e. ZZ )
66 1red 
 |-  ( ph -> 1 e. RR )
67 2re 
 |-  2 e. RR
68 67 a1i 
 |-  ( ph -> 2 e. RR )
69 1lt2 
 |-  1 < 2
70 69 a1i 
 |-  ( ph -> 1 < 2 )
71 2t1e2 
 |-  ( 2 x. 1 ) = 2
72 42 nnge1d 
 |-  ( ph -> 1 <_ ( B / 2 ) )
73 2rp 
 |-  2 e. RR+
74 73 a1i 
 |-  ( ph -> 2 e. RR+ )
75 66 50 74 lemuldiv2d 
 |-  ( ph -> ( ( 2 x. 1 ) <_ B <-> 1 <_ ( B / 2 ) ) )
76 72 75 mpbird 
 |-  ( ph -> ( 2 x. 1 ) <_ B )
77 71 76 eqbrtrrid 
 |-  ( ph -> 2 <_ B )
78 66 68 50 70 77 ltletrd 
 |-  ( ph -> 1 < B )
79 50 63 65 78 ltexp2d 
 |-  ( ph -> ( 2 < 4 <-> ( B ^ 2 ) < ( B ^ 4 ) ) )
80 61 79 mpbii 
 |-  ( ph -> ( B ^ 2 ) < ( B ^ 4 ) )
81 1 56 nnexpcld 
 |-  ( ph -> ( A ^ 4 ) e. NN )
82 81 nngt0d 
 |-  ( ph -> 0 < ( A ^ 4 ) )
83 81 nnred 
 |-  ( ph -> ( A ^ 4 ) e. RR )
84 83 58 ltaddpos2d 
 |-  ( ph -> ( 0 < ( A ^ 4 ) <-> ( B ^ 4 ) < ( ( A ^ 4 ) + ( B ^ 4 ) ) ) )
85 82 84 mpbid 
 |-  ( ph -> ( B ^ 4 ) < ( ( A ^ 4 ) + ( B ^ 4 ) ) )
86 85 6 breqtrd 
 |-  ( ph -> ( B ^ 4 ) < ( C ^ 2 ) )
87 54 58 60 80 86 lttrd 
 |-  ( ph -> ( B ^ 2 ) < ( C ^ 2 ) )
88 3 nnrpd 
 |-  ( ph -> C e. RR+ )
89 51 88 28 ltexp1d 
 |-  ( ph -> ( B < C <-> ( B ^ 2 ) < ( C ^ 2 ) ) )
90 87 89 mpbird 
 |-  ( ph -> B < C )
91 46 50 47 53 90 lttrd 
 |-  ( ph -> ( B / 2 ) < C )
92 45 46 47 49 91 lelttrd 
 |-  ( ph -> ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) < C )
93 oveq1 
 |-  ( m = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( m gcd n ) = ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd n ) )
94 93 eqeq1d 
 |-  ( m = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( m gcd n ) = 1 <-> ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd n ) = 1 ) )
95 oveq1 
 |-  ( m = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( m ^ 4 ) = ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) )
96 95 oveq1d 
 |-  ( m = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( n ^ 4 ) ) )
97 96 eqeq1d 
 |-  ( m = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) <-> ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) )
98 94 97 anbi12d 
 |-  ( m = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) <-> ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd n ) = 1 /\ ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) ) )
99 oveq2 
 |-  ( n = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd n ) = ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) )
100 99 eqeq1d 
 |-  ( n = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd n ) = 1 <-> ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) = 1 ) )
101 oveq1 
 |-  ( n = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( n ^ 4 ) = ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) )
102 101 oveq2d 
 |-  ( n = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) ) )
103 102 eqeq1d 
 |-  ( n = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) <-> ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) )
104 100 103 anbi12d 
 |-  ( n = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) -> ( ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd n ) = 1 /\ ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) <-> ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) = 1 /\ ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) ) )
105 39 simp1d 
 |-  ( ph -> ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. NN )
106 gcdnncl 
 |-  ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. NN /\ ( B / 2 ) e. NN ) -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. NN )
107 105 42 106 syl2anc 
 |-  ( ph -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. NN )
108 39 simp2d 
 |-  ( ph -> ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. NN )
109 gcdnncl 
 |-  ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. NN /\ ( B / 2 ) e. NN ) -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. NN )
110 108 42 109 syl2anc 
 |-  ( ph -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. NN )
111 105 nnzd 
 |-  ( ph -> ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. ZZ )
112 42 nnzd 
 |-  ( ph -> ( B / 2 ) e. ZZ )
113 110 nnzd 
 |-  ( ph -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. ZZ )
114 gcdass 
 |-  ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. ZZ /\ ( B / 2 ) e. ZZ /\ ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. ZZ ) -> ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( B / 2 ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) ) )
115 111 112 113 114 syl3anc 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( B / 2 ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) ) )
116 108 nnzd 
 |-  ( ph -> ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. ZZ )
117 gcdass 
 |-  ( ( ( B / 2 ) e. ZZ /\ ( B / 2 ) e. ZZ /\ ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. ZZ ) -> ( ( ( B / 2 ) gcd ( B / 2 ) ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = ( ( B / 2 ) gcd ( ( B / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) ) )
118 112 112 116 117 syl3anc 
 |-  ( ph -> ( ( ( B / 2 ) gcd ( B / 2 ) ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = ( ( B / 2 ) gcd ( ( B / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) ) )
119 42 nnnn0d 
 |-  ( ph -> ( B / 2 ) e. NN0 )
120 gcdnn0id 
 |-  ( ( B / 2 ) e. NN0 -> ( ( B / 2 ) gcd ( B / 2 ) ) = ( B / 2 ) )
121 119 120 syl 
 |-  ( ph -> ( ( B / 2 ) gcd ( B / 2 ) ) = ( B / 2 ) )
122 121 oveq1d 
 |-  ( ph -> ( ( ( B / 2 ) gcd ( B / 2 ) ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = ( ( B / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) )
123 112 116 gcdcomd 
 |-  ( ph -> ( ( B / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) )
124 122 123 eqtr2d 
 |-  ( ph -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) = ( ( ( B / 2 ) gcd ( B / 2 ) ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) )
125 116 112 gcdcomd 
 |-  ( ph -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) = ( ( B / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) )
126 125 oveq2d 
 |-  ( ph -> ( ( B / 2 ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) = ( ( B / 2 ) gcd ( ( B / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) ) )
127 118 124 126 3eqtr4rd 
 |-  ( ph -> ( ( B / 2 ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) )
128 127 oveq2d 
 |-  ( ph -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( B / 2 ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) ) = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) )
129 38 simp1d 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = 1 /\ ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) = 1 /\ ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) = 1 ) )
130 129 simp1d 
 |-  ( ph -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = 1 )
131 130 oveq1d 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) gcd ( B / 2 ) ) = ( 1 gcd ( B / 2 ) ) )
132 gcdass 
 |-  ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. ZZ /\ ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) e. ZZ /\ ( B / 2 ) e. ZZ ) -> ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) gcd ( B / 2 ) ) = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) )
133 111 116 112 132 syl3anc 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) gcd ( B / 2 ) ) = ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) )
134 1gcd 
 |-  ( ( B / 2 ) e. ZZ -> ( 1 gcd ( B / 2 ) ) = 1 )
135 112 134 syl 
 |-  ( ph -> ( 1 gcd ( B / 2 ) ) = 1 )
136 131 133 135 3eqtr3d 
 |-  ( ph -> ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) = 1 )
137 115 128 136 3eqtrd 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) = 1 )
138 13 14 15 16 1 2 3 4 37 6 flt4lem5f 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) = ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) ) )
139 138 eqcomd 
 |-  ( ph -> ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) )
140 137 139 jca 
 |-  ( ph -> ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) gcd ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ) = 1 /\ ( ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) + ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) + ( ( ( ( ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) + ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) - ( sqrt ` ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) - ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) )
141 98 104 107 110 140 2rspcedvdw 
 |-  ( ph -> E. m e. NN E. n e. NN ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) )
142 92 141 jca 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) < C /\ E. m e. NN E. n e. NN ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) ^ 2 ) ) ) )
143 12 44 142 rspcedvdw 
 |-  ( ph -> E. l e. NN ( l < C /\ E. m e. NN E. n e. NN ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) )
144 breq2 
 |-  ( g = m -> ( 2 || g <-> 2 || m ) )
145 144 notbid 
 |-  ( g = m -> ( -. 2 || g <-> -. 2 || m ) )
146 oveq1 
 |-  ( g = m -> ( g gcd h ) = ( m gcd h ) )
147 146 eqeq1d 
 |-  ( g = m -> ( ( g gcd h ) = 1 <-> ( m gcd h ) = 1 ) )
148 oveq1 
 |-  ( g = m -> ( g ^ 4 ) = ( m ^ 4 ) )
149 148 oveq1d 
 |-  ( g = m -> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( ( m ^ 4 ) + ( h ^ 4 ) ) )
150 149 eqeq1d 
 |-  ( g = m -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) <-> ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) )
151 147 150 anbi12d 
 |-  ( g = m -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) <-> ( ( m gcd h ) = 1 /\ ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) )
152 145 151 anbi12d 
 |-  ( g = m -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) <-> ( -. 2 || m /\ ( ( m gcd h ) = 1 /\ ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) ) )
153 oveq2 
 |-  ( h = n -> ( m gcd h ) = ( m gcd n ) )
154 153 eqeq1d 
 |-  ( h = n -> ( ( m gcd h ) = 1 <-> ( m gcd n ) = 1 ) )
155 oveq1 
 |-  ( h = n -> ( h ^ 4 ) = ( n ^ 4 ) )
156 155 oveq2d 
 |-  ( h = n -> ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( ( m ^ 4 ) + ( n ^ 4 ) ) )
157 156 eqeq1d 
 |-  ( h = n -> ( ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) <-> ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) )
158 154 157 anbi12d 
 |-  ( h = n -> ( ( ( m gcd h ) = 1 /\ ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) <-> ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) )
159 158 anbi2d 
 |-  ( h = n -> ( ( -. 2 || m /\ ( ( m gcd h ) = 1 /\ ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) <-> ( -. 2 || m /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) ) )
160 simplrl 
 |-  ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) -> m e. NN )
161 160 adantr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || m ) -> m e. NN )
162 simprr 
 |-  ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) -> n e. NN )
163 162 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || m ) -> n e. NN )
164 simpr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || m ) -> -. 2 || m )
165 simplr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || m ) -> ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) )
166 164 165 jca 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || m ) -> ( -. 2 || m /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) )
167 152 159 161 163 166 2rspcedvdw 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || m ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) )
168 simp-4r 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || m ) -> l < C )
169 167 168 jca 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || m ) -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < C ) )
170 breq2 
 |-  ( g = n -> ( 2 || g <-> 2 || n ) )
171 170 notbid 
 |-  ( g = n -> ( -. 2 || g <-> -. 2 || n ) )
172 oveq1 
 |-  ( g = n -> ( g gcd h ) = ( n gcd h ) )
173 172 eqeq1d 
 |-  ( g = n -> ( ( g gcd h ) = 1 <-> ( n gcd h ) = 1 ) )
174 oveq1 
 |-  ( g = n -> ( g ^ 4 ) = ( n ^ 4 ) )
175 174 oveq1d 
 |-  ( g = n -> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( ( n ^ 4 ) + ( h ^ 4 ) ) )
176 175 eqeq1d 
 |-  ( g = n -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) <-> ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) )
177 173 176 anbi12d 
 |-  ( g = n -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) <-> ( ( n gcd h ) = 1 /\ ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) )
178 171 177 anbi12d 
 |-  ( g = n -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) <-> ( -. 2 || n /\ ( ( n gcd h ) = 1 /\ ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) ) )
179 oveq2 
 |-  ( h = m -> ( n gcd h ) = ( n gcd m ) )
180 179 eqeq1d 
 |-  ( h = m -> ( ( n gcd h ) = 1 <-> ( n gcd m ) = 1 ) )
181 oveq1 
 |-  ( h = m -> ( h ^ 4 ) = ( m ^ 4 ) )
182 181 oveq2d 
 |-  ( h = m -> ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( ( n ^ 4 ) + ( m ^ 4 ) ) )
183 182 eqeq1d 
 |-  ( h = m -> ( ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) <-> ( ( n ^ 4 ) + ( m ^ 4 ) ) = ( l ^ 2 ) ) )
184 180 183 anbi12d 
 |-  ( h = m -> ( ( ( n gcd h ) = 1 /\ ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) <-> ( ( n gcd m ) = 1 /\ ( ( n ^ 4 ) + ( m ^ 4 ) ) = ( l ^ 2 ) ) ) )
185 184 anbi2d 
 |-  ( h = m -> ( ( -. 2 || n /\ ( ( n gcd h ) = 1 /\ ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) <-> ( -. 2 || n /\ ( ( n gcd m ) = 1 /\ ( ( n ^ 4 ) + ( m ^ 4 ) ) = ( l ^ 2 ) ) ) ) )
186 162 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> n e. NN )
187 160 adantr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> m e. NN )
188 simpr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> -. 2 || n )
189 186 nnzd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> n e. ZZ )
190 187 nnzd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> m e. ZZ )
191 189 190 gcdcomd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( n gcd m ) = ( m gcd n ) )
192 simplrl 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( m gcd n ) = 1 )
193 191 192 eqtrd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( n gcd m ) = 1 )
194 55 a1i 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> 4 e. NN0 )
195 186 194 nnexpcld 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( n ^ 4 ) e. NN )
196 195 nncnd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( n ^ 4 ) e. CC )
197 187 194 nnexpcld 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( m ^ 4 ) e. NN )
198 197 nncnd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( m ^ 4 ) e. CC )
199 196 198 addcomd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( ( n ^ 4 ) + ( m ^ 4 ) ) = ( ( m ^ 4 ) + ( n ^ 4 ) ) )
200 simplrr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) )
201 199 200 eqtrd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( ( n ^ 4 ) + ( m ^ 4 ) ) = ( l ^ 2 ) )
202 188 193 201 jca32 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( -. 2 || n /\ ( ( n gcd m ) = 1 /\ ( ( n ^ 4 ) + ( m ^ 4 ) ) = ( l ^ 2 ) ) ) )
203 178 185 186 187 202 2rspcedvdw 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) )
204 simp-4r 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> l < C )
205 203 204 jca 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ -. 2 || n ) -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < C ) )
206 simprl 
 |-  ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) -> m e. NN )
207 206 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> m e. NN )
208 207 nnsqcld 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( m ^ 2 ) e. NN )
209 162 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> n e. NN )
210 209 nnsqcld 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( n ^ 2 ) e. NN )
211 simp-5r 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> l e. NN )
212 160 nnzd 
 |-  ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) -> m e. ZZ )
213 27 a1i 
 |-  ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) -> 2 e. NN )
214 dvdsexp2im 
 |-  ( ( 2 e. ZZ /\ m e. ZZ /\ 2 e. NN ) -> ( 2 || m -> 2 || ( m ^ 2 ) ) )
215 62 212 213 214 mp3an2i 
 |-  ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) -> ( 2 || m -> 2 || ( m ^ 2 ) ) )
216 215 imp 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> 2 || ( m ^ 2 ) )
217 19 a1i 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> 2 e. NN0 )
218 207 nncnd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> m e. CC )
219 218 flt4lem 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( m ^ 4 ) = ( ( m ^ 2 ) ^ 2 ) )
220 209 nncnd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> n e. CC )
221 220 flt4lem 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( n ^ 4 ) = ( ( n ^ 2 ) ^ 2 ) )
222 219 221 oveq12d 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( ( ( m ^ 2 ) ^ 2 ) + ( ( n ^ 2 ) ^ 2 ) ) )
223 simplrr 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) )
224 222 223 eqtr3d 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( ( ( m ^ 2 ) ^ 2 ) + ( ( n ^ 2 ) ^ 2 ) ) = ( l ^ 2 ) )
225 simplrl 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( m gcd n ) = 1 )
226 27 a1i 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> 2 e. NN )
227 rppwr 
 |-  ( ( m e. NN /\ n e. NN /\ 2 e. NN ) -> ( ( m gcd n ) = 1 -> ( ( m ^ 2 ) gcd ( n ^ 2 ) ) = 1 ) )
228 207 209 226 227 syl3anc 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( ( m gcd n ) = 1 -> ( ( m ^ 2 ) gcd ( n ^ 2 ) ) = 1 ) )
229 225 228 mpd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( ( m ^ 2 ) gcd ( n ^ 2 ) ) = 1 )
230 208 210 211 217 224 229 fltaccoprm 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( ( m ^ 2 ) gcd l ) = 1 )
231 208 210 211 216 230 224 flt4lem2 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> -. 2 || ( n ^ 2 ) )
232 209 nnzd 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> n e. ZZ )
233 dvdsexp2im 
 |-  ( ( 2 e. ZZ /\ n e. ZZ /\ 2 e. NN ) -> ( 2 || n -> 2 || ( n ^ 2 ) ) )
234 62 232 226 233 mp3an2i 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> ( 2 || n -> 2 || ( n ^ 2 ) ) )
235 231 234 mtod 
 |-  ( ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) /\ 2 || m ) -> -. 2 || n )
236 235 ex 
 |-  ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) -> ( 2 || m -> -. 2 || n ) )
237 imor 
 |-  ( ( 2 || m -> -. 2 || n ) <-> ( -. 2 || m \/ -. 2 || n ) )
238 236 237 sylib 
 |-  ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) -> ( -. 2 || m \/ -. 2 || n ) )
239 169 205 238 mpjaodan 
 |-  ( ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) /\ ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < C ) )
240 239 ex 
 |-  ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) -> ( ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < C ) ) )
241 240 rexlimdvva 
 |-  ( ( ( ph /\ l e. NN ) /\ l < C ) -> ( E. m e. NN E. n e. NN ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < C ) ) )
242 241 expimpd 
 |-  ( ( ph /\ l e. NN ) -> ( ( l < C /\ E. m e. NN E. n e. NN ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < C ) ) )
243 242 reximdva 
 |-  ( ph -> ( E. l e. NN ( l < C /\ E. m e. NN E. n e. NN ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) -> E. l e. NN ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < C ) ) )
244 143 243 mpd 
 |-  ( ph -> E. l e. NN ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < C ) )