This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nna4b4nsq

Description: Strengthening of Fermat's last theorem for exponent 4, where the sum is only assumed to be a square. (Contributed by SN, 23-Aug-2024)

Ref Expression
Hypotheses nna4b4nsq.a 
|- ( ph -> A e. NN )
nna4b4nsq.b 
|- ( ph -> B e. NN )
nna4b4nsq.c 
|- ( ph -> C e. NN )
Assertion nna4b4nsq 
|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 2 ) )

Proof

Step Hyp Ref Expression
1 nna4b4nsq.a 
 |-  ( ph -> A e. NN )
2 nna4b4nsq.b 
 |-  ( ph -> B e. NN )
3 nna4b4nsq.c 
 |-  ( ph -> C e. NN )
4 oveq1 
 |-  ( a = A -> ( a ^ 4 ) = ( A ^ 4 ) )
5 4 oveq1d 
 |-  ( a = A -> ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( ( A ^ 4 ) + ( b ^ 4 ) ) )
6 5 eqeq1d 
 |-  ( a = A -> ( ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) <-> ( ( A ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
7 oveq1 
 |-  ( b = B -> ( b ^ 4 ) = ( B ^ 4 ) )
8 7 oveq2d 
 |-  ( b = B -> ( ( A ^ 4 ) + ( b ^ 4 ) ) = ( ( A ^ 4 ) + ( B ^ 4 ) ) )
9 8 eqeq1d 
 |-  ( b = B -> ( ( ( A ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) <-> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) ) )
10 1 ad2antrr 
 |-  ( ( ( ph /\ c e. NN ) /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) ) -> A e. NN )
11 2 ad2antrr 
 |-  ( ( ( ph /\ c e. NN ) /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) ) -> B e. NN )
12 simpr 
 |-  ( ( ( ph /\ c e. NN ) /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) ) -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) )
13 6 9 10 11 12 2rspcedvdw 
 |-  ( ( ( ph /\ c e. NN ) /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) ) -> E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) )
14 13 ex 
 |-  ( ( ph /\ c e. NN ) -> ( ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) -> E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
15 14 ss2rabdv 
 |-  ( ph -> { c e. NN | ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) } C_ { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } )
16 oveq1 
 |-  ( f = i -> ( f ^ 2 ) = ( i ^ 2 ) )
17 16 eqeq2d 
 |-  ( f = i -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) )
18 17 anbi2d 
 |-  ( f = i -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) )
19 18 anbi2d 
 |-  ( f = i -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) ) )
20 19 2rexbidv 
 |-  ( f = i -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) ) )
21 oveq1 
 |-  ( f = l -> ( f ^ 2 ) = ( l ^ 2 ) )
22 21 eqeq2d 
 |-  ( f = l -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) )
23 22 anbi2d 
 |-  ( f = l -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) )
24 23 anbi2d 
 |-  ( f = l -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) ) )
25 24 2rexbidv 
 |-  ( f = l -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) ) )
26 nnuz 
 |-  NN = ( ZZ>= ` 1 )
27 26 eqimssi 
 |-  NN C_ ( ZZ>= ` 1 )
28 27 a1i 
 |-  ( ph -> NN C_ ( ZZ>= ` 1 ) )
29 breq2 
 |-  ( g = j -> ( 2 || g <-> 2 || j ) )
30 29 notbid 
 |-  ( g = j -> ( -. 2 || g <-> -. 2 || j ) )
31 oveq1 
 |-  ( g = j -> ( g gcd h ) = ( j gcd h ) )
32 31 eqeq1d 
 |-  ( g = j -> ( ( g gcd h ) = 1 <-> ( j gcd h ) = 1 ) )
33 oveq1 
 |-  ( g = j -> ( g ^ 4 ) = ( j ^ 4 ) )
34 33 oveq1d 
 |-  ( g = j -> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( ( j ^ 4 ) + ( h ^ 4 ) ) )
35 34 eqeq1d 
 |-  ( g = j -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) <-> ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) )
36 32 35 anbi12d 
 |-  ( g = j -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) <-> ( ( j gcd h ) = 1 /\ ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) )
37 30 36 anbi12d 
 |-  ( g = j -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) <-> ( -. 2 || j /\ ( ( j gcd h ) = 1 /\ ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) ) )
38 oveq2 
 |-  ( h = k -> ( j gcd h ) = ( j gcd k ) )
39 38 eqeq1d 
 |-  ( h = k -> ( ( j gcd h ) = 1 <-> ( j gcd k ) = 1 ) )
40 oveq1 
 |-  ( h = k -> ( h ^ 4 ) = ( k ^ 4 ) )
41 40 oveq2d 
 |-  ( h = k -> ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( ( j ^ 4 ) + ( k ^ 4 ) ) )
42 41 eqeq1d 
 |-  ( h = k -> ( ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) <-> ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) )
43 39 42 anbi12d 
 |-  ( h = k -> ( ( ( j gcd h ) = 1 /\ ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) <-> ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) )
44 43 anbi2d 
 |-  ( h = k -> ( ( -. 2 || j /\ ( ( j gcd h ) = 1 /\ ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) <-> ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) )
45 37 44 cbvrex2vw 
 |-  ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) <-> E. j e. NN E. k e. NN ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) )
46 simplrl 
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> j e. NN )
47 simplrr 
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> k e. NN )
48 simpllr 
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> i e. NN )
49 simprl 
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> -. 2 || j )
50 simprrl 
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> ( j gcd k ) = 1 )
51 simprrr 
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) )
52 46 47 48 49 50 51 flt4lem7 
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 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 < i ) )
53 52 ex 
 |-  ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) -> ( ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 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 < i ) ) )
54 53 rexlimdvva 
 |-  ( ( ph /\ i e. NN ) -> ( E. j e. NN E. k e. NN ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 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 < i ) ) )
55 45 54 biimtrid 
 |-  ( ( ph /\ i e. NN ) -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 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 < i ) ) )
56 55 impr 
 |-  ( ( ph /\ ( i e. NN /\ E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 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 < i ) )
57 20 25 28 56 infdesc 
 |-  ( ph -> { f e. NN | E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) } = (/) )
58 breq2 
 |-  ( g = d -> ( 2 || g <-> 2 || d ) )
59 58 notbid 
 |-  ( g = d -> ( -. 2 || g <-> -. 2 || d ) )
60 oveq1 
 |-  ( g = d -> ( g gcd h ) = ( d gcd h ) )
61 60 eqeq1d 
 |-  ( g = d -> ( ( g gcd h ) = 1 <-> ( d gcd h ) = 1 ) )
62 oveq1 
 |-  ( g = d -> ( g ^ 4 ) = ( d ^ 4 ) )
63 62 oveq1d 
 |-  ( g = d -> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( ( d ^ 4 ) + ( h ^ 4 ) ) )
64 63 eqeq1d 
 |-  ( g = d -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) )
65 61 64 anbi12d 
 |-  ( g = d -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( d gcd h ) = 1 /\ ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
66 59 65 anbi12d 
 |-  ( g = d -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || d /\ ( ( d gcd h ) = 1 /\ ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
67 oveq2 
 |-  ( h = e -> ( d gcd h ) = ( d gcd e ) )
68 67 eqeq1d 
 |-  ( h = e -> ( ( d gcd h ) = 1 <-> ( d gcd e ) = 1 ) )
69 oveq1 
 |-  ( h = e -> ( h ^ 4 ) = ( e ^ 4 ) )
70 69 oveq2d 
 |-  ( h = e -> ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( ( d ^ 4 ) + ( e ^ 4 ) ) )
71 70 eqeq1d 
 |-  ( h = e -> ( ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
72 68 71 anbi12d 
 |-  ( h = e -> ( ( ( d gcd h ) = 1 /\ ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
73 72 anbi2d 
 |-  ( h = e -> ( ( -. 2 || d /\ ( ( d gcd h ) = 1 /\ ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
74 simprl 
 |-  ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) -> d e. NN )
75 74 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> d e. NN )
76 simprr 
 |-  ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) -> e e. NN )
77 76 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> e e. NN )
78 simpr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> -. 2 || d )
79 simplr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
80 78 79 jca 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
81 66 73 75 77 80 2rspcedvdw 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
82 breq2 
 |-  ( g = e -> ( 2 || g <-> 2 || e ) )
83 82 notbid 
 |-  ( g = e -> ( -. 2 || g <-> -. 2 || e ) )
84 oveq1 
 |-  ( g = e -> ( g gcd h ) = ( e gcd h ) )
85 84 eqeq1d 
 |-  ( g = e -> ( ( g gcd h ) = 1 <-> ( e gcd h ) = 1 ) )
86 oveq1 
 |-  ( g = e -> ( g ^ 4 ) = ( e ^ 4 ) )
87 86 oveq1d 
 |-  ( g = e -> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( ( e ^ 4 ) + ( h ^ 4 ) ) )
88 87 eqeq1d 
 |-  ( g = e -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) )
89 85 88 anbi12d 
 |-  ( g = e -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( e gcd h ) = 1 /\ ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
90 83 89 anbi12d 
 |-  ( g = e -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || e /\ ( ( e gcd h ) = 1 /\ ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
91 oveq2 
 |-  ( h = d -> ( e gcd h ) = ( e gcd d ) )
92 91 eqeq1d 
 |-  ( h = d -> ( ( e gcd h ) = 1 <-> ( e gcd d ) = 1 ) )
93 oveq1 
 |-  ( h = d -> ( h ^ 4 ) = ( d ^ 4 ) )
94 93 oveq2d 
 |-  ( h = d -> ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( ( e ^ 4 ) + ( d ^ 4 ) ) )
95 94 eqeq1d 
 |-  ( h = d -> ( ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( f ^ 2 ) ) )
96 92 95 anbi12d 
 |-  ( h = d -> ( ( ( e gcd h ) = 1 /\ ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( e gcd d ) = 1 /\ ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( f ^ 2 ) ) ) )
97 96 anbi2d 
 |-  ( h = d -> ( ( -. 2 || e /\ ( ( e gcd h ) = 1 /\ ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || e /\ ( ( e gcd d ) = 1 /\ ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
98 76 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> e e. NN )
99 74 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> d e. NN )
100 simpr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> -. 2 || e )
101 98 nnzd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> e e. ZZ )
102 99 nnzd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> d e. ZZ )
103 101 102 gcdcomd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( e gcd d ) = ( d gcd e ) )
104 simplrl 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( d gcd e ) = 1 )
105 103 104 eqtrd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( e gcd d ) = 1 )
106 4nn0 
 |-  4 e. NN0
107 106 a1i 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> 4 e. NN0 )
108 98 107 nnexpcld 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( e ^ 4 ) e. NN )
109 108 nncnd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( e ^ 4 ) e. CC )
110 99 107 nnexpcld 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( d ^ 4 ) e. NN )
111 110 nncnd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( d ^ 4 ) e. CC )
112 109 111 addcomd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( ( d ^ 4 ) + ( e ^ 4 ) ) )
113 simplrr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) )
114 112 113 eqtrd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( f ^ 2 ) )
115 100 105 114 jca32 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( -. 2 || e /\ ( ( e gcd d ) = 1 /\ ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( f ^ 2 ) ) ) )
116 90 97 98 99 115 2rspcedvdw 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
117 74 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> d e. NN )
118 117 nnsqcld 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( d ^ 2 ) e. NN )
119 76 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> e e. NN )
120 119 nnsqcld 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( e ^ 2 ) e. NN )
121 simp-4r 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> f e. NN )
122 2z 
 |-  2 e. ZZ
123 simplrl 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> d e. NN )
124 123 nnzd 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> d e. ZZ )
125 2nn 
 |-  2 e. NN
126 125 a1i 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> 2 e. NN )
127 dvdsexp2im 
 |-  ( ( 2 e. ZZ /\ d e. ZZ /\ 2 e. NN ) -> ( 2 || d -> 2 || ( d ^ 2 ) ) )
128 122 124 126 127 mp3an2i 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> ( 2 || d -> 2 || ( d ^ 2 ) ) )
129 128 imp 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> 2 || ( d ^ 2 ) )
130 2nn0 
 |-  2 e. NN0
131 130 a1i 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> 2 e. NN0 )
132 117 nncnd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> d e. CC )
133 132 flt4lem 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( d ^ 4 ) = ( ( d ^ 2 ) ^ 2 ) )
134 119 nncnd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> e e. CC )
135 134 flt4lem 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( e ^ 4 ) = ( ( e ^ 2 ) ^ 2 ) )
136 133 135 oveq12d 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( ( d ^ 2 ) ^ 2 ) + ( ( e ^ 2 ) ^ 2 ) ) )
137 simplrr 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) )
138 136 137 eqtr3d 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( ( d ^ 2 ) ^ 2 ) + ( ( e ^ 2 ) ^ 2 ) ) = ( f ^ 2 ) )
139 simplrl 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( d gcd e ) = 1 )
140 125 a1i 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> 2 e. NN )
141 rppwr 
 |-  ( ( d e. NN /\ e e. NN /\ 2 e. NN ) -> ( ( d gcd e ) = 1 -> ( ( d ^ 2 ) gcd ( e ^ 2 ) ) = 1 ) )
142 117 119 140 141 syl3anc 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( d gcd e ) = 1 -> ( ( d ^ 2 ) gcd ( e ^ 2 ) ) = 1 ) )
143 139 142 mpd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( d ^ 2 ) gcd ( e ^ 2 ) ) = 1 )
144 118 120 121 131 138 143 fltaccoprm 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( d ^ 2 ) gcd f ) = 1 )
145 118 120 121 129 144 138 flt4lem2 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> -. 2 || ( e ^ 2 ) )
146 119 nnzd 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> e e. ZZ )
147 dvdsexp2im 
 |-  ( ( 2 e. ZZ /\ e e. ZZ /\ 2 e. NN ) -> ( 2 || e -> 2 || ( e ^ 2 ) ) )
148 122 146 140 147 mp3an2i 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( 2 || e -> 2 || ( e ^ 2 ) ) )
149 145 148 mtod 
 |-  ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> -. 2 || e )
150 149 ex 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> ( 2 || d -> -. 2 || e ) )
151 imor 
 |-  ( ( 2 || d -> -. 2 || e ) <-> ( -. 2 || d \/ -. 2 || e ) )
152 150 151 sylib 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> ( -. 2 || d \/ -. 2 || e ) )
153 81 116 152 mpjaodan 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
154 153 ex 
 |-  ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
155 154 rexlimdvva 
 |-  ( ( ph /\ f e. NN ) -> ( E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
156 155 reximdva 
 |-  ( ph -> ( E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) -> E. f e. NN E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
157 156 con3d 
 |-  ( ph -> ( -. E. f e. NN E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) -> -. E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
158 ralnex 
 |-  ( A. f e. NN -. E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> -. E. f e. NN E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
159 ralnex 
 |-  ( A. f e. NN -. E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) <-> -. E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
160 157 158 159 3imtr4g 
 |-  ( ph -> ( A. f e. NN -. E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) -> A. f e. NN -. E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
161 rabeq0 
 |-  ( { f e. NN | E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) } = (/) <-> A. f e. NN -. E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
162 rabeq0 
 |-  ( { f e. NN | E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) } = (/) <-> A. f e. NN -. E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
163 160 161 162 3imtr4g 
 |-  ( ph -> ( { f e. NN | E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) } = (/) -> { f e. NN | E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) } = (/) ) )
164 57 163 mpd 
 |-  ( ph -> { f e. NN | E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) } = (/) )
165 oveq1 
 |-  ( f = ( c / ( ( a gcd b ) ^ 2 ) ) -> ( f ^ 2 ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) )
166 165 eqeq2d 
 |-  ( f = ( c / ( ( a gcd b ) ^ 2 ) ) -> ( ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) <-> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) )
167 166 anbi2d 
 |-  ( f = ( c / ( ( a gcd b ) ^ 2 ) ) -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) ) )
168 oveq1 
 |-  ( d = ( a / ( a gcd b ) ) -> ( d gcd e ) = ( ( a / ( a gcd b ) ) gcd e ) )
169 168 eqeq1d 
 |-  ( d = ( a / ( a gcd b ) ) -> ( ( d gcd e ) = 1 <-> ( ( a / ( a gcd b ) ) gcd e ) = 1 ) )
170 oveq1 
 |-  ( d = ( a / ( a gcd b ) ) -> ( d ^ 4 ) = ( ( a / ( a gcd b ) ) ^ 4 ) )
171 170 oveq1d 
 |-  ( d = ( a / ( a gcd b ) ) -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) )
172 171 eqeq1d 
 |-  ( d = ( a / ( a gcd b ) ) -> ( ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) <-> ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) )
173 169 172 anbi12d 
 |-  ( d = ( a / ( a gcd b ) ) -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) <-> ( ( ( a / ( a gcd b ) ) gcd e ) = 1 /\ ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) ) )
174 oveq2 
 |-  ( e = ( b / ( a gcd b ) ) -> ( ( a / ( a gcd b ) ) gcd e ) = ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) )
175 174 eqeq1d 
 |-  ( e = ( b / ( a gcd b ) ) -> ( ( ( a / ( a gcd b ) ) gcd e ) = 1 <-> ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) = 1 ) )
176 oveq1 
 |-  ( e = ( b / ( a gcd b ) ) -> ( e ^ 4 ) = ( ( b / ( a gcd b ) ) ^ 4 ) )
177 176 oveq2d 
 |-  ( e = ( b / ( a gcd b ) ) -> ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) = ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) )
178 177 eqeq1d 
 |-  ( e = ( b / ( a gcd b ) ) -> ( ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) <-> ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) )
179 175 178 anbi12d 
 |-  ( e = ( b / ( a gcd b ) ) -> ( ( ( ( a / ( a gcd b ) ) gcd e ) = 1 /\ ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) <-> ( ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) = 1 /\ ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) ) )
180 simplrr 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> a e. NN )
181 simprl 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> b e. NN )
182 simplrl 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> c e. NN )
183 simprr 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) )
184 180 181 182 183 flt4lem6 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( ( a / ( a gcd b ) ) e. NN /\ ( b / ( a gcd b ) ) e. NN /\ ( c / ( ( a gcd b ) ^ 2 ) ) e. NN ) /\ ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) )
185 184 simpld 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( a / ( a gcd b ) ) e. NN /\ ( b / ( a gcd b ) ) e. NN /\ ( c / ( ( a gcd b ) ^ 2 ) ) e. NN ) )
186 185 simp3d 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( c / ( ( a gcd b ) ^ 2 ) ) e. NN )
187 185 simp1d 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( a / ( a gcd b ) ) e. NN )
188 185 simp2d 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( b / ( a gcd b ) ) e. NN )
189 180 nnzd 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> a e. ZZ )
190 181 nnzd 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> b e. ZZ )
191 181 nnne0d 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> b =/= 0 )
192 divgcdcoprm0 
 |-  ( ( a e. ZZ /\ b e. ZZ /\ b =/= 0 ) -> ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) = 1 )
193 189 190 191 192 syl3anc 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) = 1 )
194 184 simprd 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) )
195 193 194 jca 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) = 1 /\ ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) )
196 167 173 179 186 187 188 195 3rspcedvdw 
 |-  ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
197 196 rexlimdvaa 
 |-  ( ( ph /\ ( c e. NN /\ a e. NN ) ) -> ( E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) -> E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
198 197 rexlimdvva 
 |-  ( ph -> ( E. c e. NN E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) -> E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
199 198 con3d 
 |-  ( ph -> ( -. E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) -> -. E. c e. NN E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
200 ralnex 
 |-  ( A. c e. NN -. E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) <-> -. E. c e. NN E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) )
201 199 159 200 3imtr4g 
 |-  ( ph -> ( A. f e. NN -. E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) -> A. c e. NN -. E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
202 rabeq0 
 |-  ( { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } = (/) <-> A. c e. NN -. E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) )
203 201 162 202 3imtr4g 
 |-  ( ph -> ( { f e. NN | E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) } = (/) -> { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } = (/) ) )
204 164 203 mpd 
 |-  ( ph -> { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } = (/) )
205 sseq0 
 |-  ( ( { c e. NN | ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) } C_ { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } /\ { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } = (/) ) -> { c e. NN | ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) } = (/) )
206 15 204 205 syl2anc 
 |-  ( ph -> { c e. NN | ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) } = (/) )
207 rabeq0 
 |-  ( { c e. NN | ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) } = (/) <-> A. c e. NN -. ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) )
208 206 207 sylib 
 |-  ( ph -> A. c e. NN -. ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) )
209 oveq1 
 |-  ( c = C -> ( c ^ 2 ) = ( C ^ 2 ) )
210 209 eqeq2d 
 |-  ( c = C -> ( ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) <-> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) )
211 210 necon3bbid 
 |-  ( c = C -> ( -. ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) <-> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 2 ) ) )
212 211 rspcv 
 |-  ( C e. NN -> ( A. c e. NN -. ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 2 ) ) )
213 3 208 212 sylc 
 |-  ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 2 ) )