Metamath Proof Explorer

Theorem flt4lem7

Description: Convert flt4lem5f into a convenient form for nna4b4nsq . (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 13 14 15 16 1 2 3 4 5 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 ) ) )
18 17 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 ) )
19 18 simp3d 
 |-  ( ph -> ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) e. NN )
20 17 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 ) )
21 20 simprd 
 |-  ( ph -> ( B / 2 ) e. NN )
22 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 )
23 19 21 22 syl2anc 
 |-  ( ph -> ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. NN )
24 23 nnred 
 |-  ( ph -> ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) e. RR )
25 21 nnred 
 |-  ( ph -> ( B / 2 ) e. RR )
26 3 nnred 
 |-  ( ph -> C e. RR )
27 19 nnzd 
 |-  ( ph -> ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) e. ZZ )
28 27 21 gcdle2d 
 |-  ( ph -> ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) <_ ( B / 2 ) )
29 2 nnred 
 |-  ( ph -> B e. RR )
30 2 nnrpd 
 |-  ( ph -> B e. RR+ )
31 rphalflt 
 |-  ( B e. RR+ -> ( B / 2 ) < B )
32 30 31 syl 
 |-  ( ph -> ( B / 2 ) < B )
33 2 nnsqcld 
 |-  ( ph -> ( B ^ 2 ) e. NN )
34 33 nnred 
 |-  ( ph -> ( B ^ 2 ) e. RR )
35 4nn0 
 |-  4 e. NN0
36 35 a1i 
 |-  ( ph -> 4 e. NN0 )
37 2 36 nnexpcld 
 |-  ( ph -> ( B ^ 4 ) e. NN )
38 37 nnred 
 |-  ( ph -> ( B ^ 4 ) e. RR )
39 3 nnsqcld 
 |-  ( ph -> ( C ^ 2 ) e. NN )
40 39 nnred 
 |-  ( ph -> ( C ^ 2 ) e. RR )
41 2lt4 
 |-  2 < 4
42 2z 
 |-  2 e. ZZ
43 42 a1i 
 |-  ( ph -> 2 e. ZZ )
44 4z 
 |-  4 e. ZZ
45 44 a1i 
 |-  ( ph -> 4 e. ZZ )
46 1red 
 |-  ( ph -> 1 e. RR )
47 21 nnge1d 
 |-  ( ph -> 1 <_ ( B / 2 ) )
48 46 25 29 47 32 lelttrd 
 |-  ( ph -> 1 < B )
49 29 43 45 48 ltexp2d 
 |-  ( ph -> ( 2 < 4 <-> ( B ^ 2 ) < ( B ^ 4 ) ) )
50 41 49 mpbii 
 |-  ( ph -> ( B ^ 2 ) < ( B ^ 4 ) )
51 1 36 nnexpcld 
 |-  ( ph -> ( A ^ 4 ) e. NN )
52 51 nngt0d 
 |-  ( ph -> 0 < ( A ^ 4 ) )
53 51 nnred 
 |-  ( ph -> ( A ^ 4 ) e. RR )
54 53 38 ltaddpos2d 
 |-  ( ph -> ( 0 < ( A ^ 4 ) <-> ( B ^ 4 ) < ( ( A ^ 4 ) + ( B ^ 4 ) ) ) )
55 52 54 mpbid 
 |-  ( ph -> ( B ^ 4 ) < ( ( A ^ 4 ) + ( B ^ 4 ) ) )
56 55 6 breqtrd 
 |-  ( ph -> ( B ^ 4 ) < ( C ^ 2 ) )
57 34 38 40 50 56 lttrd 
 |-  ( ph -> ( B ^ 2 ) < ( C ^ 2 ) )
58 3 nnrpd 
 |-  ( ph -> C e. RR+ )
59 2nn 
 |-  2 e. NN
60 59 a1i 
 |-  ( ph -> 2 e. NN )
61 30 58 60 ltexp1d 
 |-  ( ph -> ( B < C <-> ( B ^ 2 ) < ( C ^ 2 ) ) )
62 57 61 mpbird 
 |-  ( ph -> B < C )
63 25 29 26 32 62 lttrd 
 |-  ( ph -> ( B / 2 ) < C )
64 24 25 26 28 63 lelttrd 
 |-  ( ph -> ( ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) gcd ( B / 2 ) ) < C )
65 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 ) )
66 65 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 ) )
67 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 ) )
68 67 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 ) ) )
69 68 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 ) ) )
70 66 69 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 ) ) ) )
71 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 ) ) ) )
72 71 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 ) )
73 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 ) )
74 73 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 ) ) )
75 74 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 ) ) )
76 72 75 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 ) ) ) )
77 18 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 )
78 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 )
79 77 21 78 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 )
80 18 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 )
81 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 )
82 80 21 81 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 )
83 77 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 )
84 21 nnzd 
 |-  ( ph -> ( B / 2 ) e. ZZ )
85 82 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 )
86 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 ) ) ) ) )
87 83 84 85 86 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 ) ) ) ) )
88 80 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 )
89 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 ) ) ) )
90 84 84 88 89 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 ) ) ) )
91 21 nnnn0d 
 |-  ( ph -> ( B / 2 ) e. NN0 )
92 gcdnn0id 
 |-  ( ( B / 2 ) e. NN0 -> ( ( B / 2 ) gcd ( B / 2 ) ) = ( B / 2 ) )
93 91 92 syl 
 |-  ( ph -> ( ( B / 2 ) gcd ( B / 2 ) ) = ( B / 2 ) )
94 93 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 ) ) )
95 84 88 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 ) ) )
96 94 95 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 ) ) )
97 88 84 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 ) ) )
98 97 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 ) ) ) )
99 90 96 98 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 ) ) )
100 99 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 ) ) ) )
101 17 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 ) )
102 101 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 )
103 102 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 ) ) )
104 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 ) ) ) )
105 83 88 84 104 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 ) ) ) )
106 1gcd 
 |-  ( ( B / 2 ) e. ZZ -> ( 1 gcd ( B / 2 ) ) = 1 )
107 84 106 syl 
 |-  ( ph -> ( 1 gcd ( B / 2 ) ) = 1 )
108 103 105 107 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 )
109 87 100 108 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 )
110 13 14 15 16 1 2 3 4 5 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 ) ) )
111 110 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 ) )
112 109 111 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 ) ) )
113 70 76 79 82 112 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 ) ) )
114 64 113 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 ) ) ) )
115 12 23 114 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 ) ) ) )
116 breq2 
 |-  ( g = m -> ( 2 || g <-> 2 || m ) )
117 116 notbid 
 |-  ( g = m -> ( -. 2 || g <-> -. 2 || m ) )
118 oveq1 
 |-  ( g = m -> ( g gcd h ) = ( m gcd h ) )
119 118 eqeq1d 
 |-  ( g = m -> ( ( g gcd h ) = 1 <-> ( m gcd h ) = 1 ) )
120 oveq1 
 |-  ( g = m -> ( g ^ 4 ) = ( m ^ 4 ) )
121 120 oveq1d 
 |-  ( g = m -> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( ( m ^ 4 ) + ( h ^ 4 ) ) )
122 121 eqeq1d 
 |-  ( g = m -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) <-> ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) )
123 119 122 anbi12d 
 |-  ( g = m -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) <-> ( ( m gcd h ) = 1 /\ ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) )
124 117 123 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 ) ) ) ) )
125 oveq2 
 |-  ( h = n -> ( m gcd h ) = ( m gcd n ) )
126 125 eqeq1d 
 |-  ( h = n -> ( ( m gcd h ) = 1 <-> ( m gcd n ) = 1 ) )
127 oveq1 
 |-  ( h = n -> ( h ^ 4 ) = ( n ^ 4 ) )
128 127 oveq2d 
 |-  ( h = n -> ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( ( m ^ 4 ) + ( n ^ 4 ) ) )
129 128 eqeq1d 
 |-  ( h = n -> ( ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) <-> ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) )
130 126 129 anbi12d 
 |-  ( h = n -> ( ( ( m gcd h ) = 1 /\ ( ( m ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) <-> ( ( m gcd n ) = 1 /\ ( ( m ^ 4 ) + ( n ^ 4 ) ) = ( l ^ 2 ) ) ) )
131 130 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 ) ) ) ) )
132 simprl 
 |-  ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) -> m e. NN )
133 132 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 )
134 simprr 
 |-  ( ( ( ( ph /\ l e. NN ) /\ l < C ) /\ ( m e. NN /\ n e. NN ) ) -> n e. NN )
135 134 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 )
136 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 )
137 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 ) ) )
138 136 137 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 ) ) ) )
139 124 131 133 135 138 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 ) ) ) )
140 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 )
141 139 140 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 ) )
142 breq2 
 |-  ( g = n -> ( 2 || g <-> 2 || n ) )
143 142 notbid 
 |-  ( g = n -> ( -. 2 || g <-> -. 2 || n ) )
144 oveq1 
 |-  ( g = n -> ( g gcd h ) = ( n gcd h ) )
145 144 eqeq1d 
 |-  ( g = n -> ( ( g gcd h ) = 1 <-> ( n gcd h ) = 1 ) )
146 oveq1 
 |-  ( g = n -> ( g ^ 4 ) = ( n ^ 4 ) )
147 146 oveq1d 
 |-  ( g = n -> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( ( n ^ 4 ) + ( h ^ 4 ) ) )
148 147 eqeq1d 
 |-  ( g = n -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) <-> ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) )
149 145 148 anbi12d 
 |-  ( g = n -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) <-> ( ( n gcd h ) = 1 /\ ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) )
150 143 149 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 ) ) ) ) )
151 oveq2 
 |-  ( h = m -> ( n gcd h ) = ( n gcd m ) )
152 151 eqeq1d 
 |-  ( h = m -> ( ( n gcd h ) = 1 <-> ( n gcd m ) = 1 ) )
153 oveq1 
 |-  ( h = m -> ( h ^ 4 ) = ( m ^ 4 ) )
154 153 oveq2d 
 |-  ( h = m -> ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( ( n ^ 4 ) + ( m ^ 4 ) ) )
155 154 eqeq1d 
 |-  ( h = m -> ( ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) <-> ( ( n ^ 4 ) + ( m ^ 4 ) ) = ( l ^ 2 ) ) )
156 152 155 anbi12d 
 |-  ( h = m -> ( ( ( n gcd h ) = 1 /\ ( ( n ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) <-> ( ( n gcd m ) = 1 /\ ( ( n ^ 4 ) + ( m ^ 4 ) ) = ( l ^ 2 ) ) ) )
157 156 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 ) ) ) ) )
158 134 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 )
159 132 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 ) -> m e. NN )
160 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 )
161 158 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 )
162 159 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 )
163 161 162 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 ) )
164 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 )
165 163 164 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 )
166 35 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 )
167 158 166 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 )
168 167 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 )
169 159 166 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 )
170 169 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 )
171 168 170 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 ) ) )
172 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 ) )
173 171 172 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 ) )
174 160 165 173 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 ) ) ) )
175 150 157 158 159 174 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 ) ) ) )
176 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 )
177 175 176 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 ) )
178 132 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 )
179 178 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 )
180 134 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 )
181 180 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 )
182 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 )
183 182 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 )
184 59 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 )
185 dvdsexp2im 
 |-  ( ( 2 e. ZZ /\ m e. ZZ /\ 2 e. NN ) -> ( 2 || m -> 2 || ( m ^ 2 ) ) )
186 42 183 184 185 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 ) ) )
187 186 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 ) )
188 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 )
189 59 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 )
190 rppwr 
 |-  ( ( m e. NN /\ n e. NN /\ 2 e. NN ) -> ( ( m gcd n ) = 1 -> ( ( m ^ 2 ) gcd ( n ^ 2 ) ) = 1 ) )
191 178 180 189 190 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 ) )
192 188 191 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 )
193 179 181 187 192 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 ) )
194 180 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 )
195 dvdsexp2im 
 |-  ( ( 2 e. ZZ /\ n e. ZZ /\ 2 e. NN ) -> ( 2 || n -> 2 || ( n ^ 2 ) ) )
196 42 194 189 195 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 ) ) )
197 193 196 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 )
198 197 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 ) )
199 imor 
 |-  ( ( 2 || m -> -. 2 || n ) <-> ( -. 2 || m \/ -. 2 || n ) )
200 198 199 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 ) )
201 141 177 200 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 ) )
202 201 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 ) ) )
203 202 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 ) ) )
204 203 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 ) ) )
205 204 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 ) ) )
206 115 205 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 ) )