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 
 |-  ( c = f -> ( c ^ 2 ) = ( f ^ 2 ) )
5 4 eqeq2d 
 |-  ( c = f -> ( ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) <-> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
6 5 anbi2d 
 |-  ( c = f -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) <-> ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
7 6 anbi2d 
 |-  ( c = f -> ( ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) <-> ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
8 7 2rexbidv 
 |-  ( c = f -> ( E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) <-> E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
9 oveq1 
 |-  ( c = g -> ( c ^ 2 ) = ( g ^ 2 ) )
10 9 eqeq2d 
 |-  ( c = g -> ( ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) <-> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( g ^ 2 ) ) )
11 10 anbi2d 
 |-  ( c = g -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) <-> ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( g ^ 2 ) ) ) )
12 11 anbi2d 
 |-  ( c = g -> ( ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) <-> ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( g ^ 2 ) ) ) ) )
13 12 2rexbidv 
 |-  ( c = g -> ( E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) <-> E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( g ^ 2 ) ) ) ) )
14 nnuz 
 |-  NN = ( ZZ>= ` 1 )
15 14 eqimssi 
 |-  NN C_ ( ZZ>= ` 1 )
16 15 a1i 
 |-  ( ph -> NN C_ ( ZZ>= ` 1 ) )
17 breq2 
 |-  ( d = h -> ( 2 || d <-> 2 || h ) )
18 17 notbid 
 |-  ( d = h -> ( -. 2 || d <-> -. 2 || h ) )
19 oveq1 
 |-  ( d = h -> ( d gcd e ) = ( h gcd e ) )
20 19 eqeq1d 
 |-  ( d = h -> ( ( d gcd e ) = 1 <-> ( h gcd e ) = 1 ) )
21 oveq1 
 |-  ( d = h -> ( d ^ 4 ) = ( h ^ 4 ) )
22 21 oveq1d 
 |-  ( d = h -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( h ^ 4 ) + ( e ^ 4 ) ) )
23 22 eqeq1d 
 |-  ( d = h -> ( ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) <-> ( ( h ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
24 20 23 anbi12d 
 |-  ( d = h -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( h gcd e ) = 1 /\ ( ( h ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
25 18 24 anbi12d 
 |-  ( d = h -> ( ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || h /\ ( ( h gcd e ) = 1 /\ ( ( h ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
26 oveq2 
 |-  ( e = i -> ( h gcd e ) = ( h gcd i ) )
27 26 eqeq1d 
 |-  ( e = i -> ( ( h gcd e ) = 1 <-> ( h gcd i ) = 1 ) )
28 oveq1 
 |-  ( e = i -> ( e ^ 4 ) = ( i ^ 4 ) )
29 28 oveq2d 
 |-  ( e = i -> ( ( h ^ 4 ) + ( e ^ 4 ) ) = ( ( h ^ 4 ) + ( i ^ 4 ) ) )
30 29 eqeq1d 
 |-  ( e = i -> ( ( ( h ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) <-> ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) )
31 27 30 anbi12d 
 |-  ( e = i -> ( ( ( h gcd e ) = 1 /\ ( ( h ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) )
32 31 anbi2d 
 |-  ( e = i -> ( ( -. 2 || h /\ ( ( h gcd e ) = 1 /\ ( ( h ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
33 25 32 cbvrex2vw 
 |-  ( E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) <-> E. h e. NN E. i e. NN ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) )
34 simplrl 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( h e. NN /\ i e. NN ) ) /\ ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) ) -> h e. NN )
35 simplrr 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( h e. NN /\ i e. NN ) ) /\ ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) ) -> i e. NN )
36 simpllr 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( h e. NN /\ i e. NN ) ) /\ ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) ) -> f e. NN )
37 simprl 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( h e. NN /\ i e. NN ) ) /\ ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) ) -> -. 2 || h )
38 simprrl 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( h e. NN /\ i e. NN ) ) /\ ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) ) -> ( h gcd i ) = 1 )
39 simprrr 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( h e. NN /\ i e. NN ) ) /\ ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) ) -> ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) )
40 34 35 36 37 38 39 flt4lem7 
 |-  ( ( ( ( ph /\ f e. NN ) /\ ( h e. NN /\ i e. NN ) ) /\ ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) ) -> E. g e. NN ( E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( g ^ 2 ) ) ) /\ g < f ) )
41 40 ex 
 |-  ( ( ( ph /\ f e. NN ) /\ ( h e. NN /\ i e. NN ) ) -> ( ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) -> E. g e. NN ( E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( g ^ 2 ) ) ) /\ g < f ) ) )
42 41 rexlimdvva 
 |-  ( ( ph /\ f e. NN ) -> ( E. h e. NN E. i e. NN ( -. 2 || h /\ ( ( h gcd i ) = 1 /\ ( ( h ^ 4 ) + ( i ^ 4 ) ) = ( f ^ 2 ) ) ) -> E. g e. NN ( E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( g ^ 2 ) ) ) /\ g < f ) ) )
43 33 42 biimtrid 
 |-  ( ( ph /\ f e. NN ) -> ( E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> E. g e. NN ( E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( g ^ 2 ) ) ) /\ g < f ) ) )
44 43 impr 
 |-  ( ( ph /\ ( f e. NN /\ E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) ) ) -> E. g e. NN ( E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( g ^ 2 ) ) ) /\ g < f ) )
45 8 13 16 44 infdesc 
 |-  ( ph -> { c e. NN | E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) } = (/) )
46 rabeq0 
 |-  ( { c e. NN | E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) } = (/) <-> A. c e. NN -. E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) )
47 45 46 sylib 
 |-  ( ph -> A. c e. NN -. E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) )
48 ralnex 
 |-  ( A. c e. NN -. E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) <-> -. E. c e. NN E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) )
49 47 48 sylib 
 |-  ( ph -> -. E. c e. NN E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) )
50 breq2 
 |-  ( d = a -> ( 2 || d <-> 2 || a ) )
51 50 notbid 
 |-  ( d = a -> ( -. 2 || d <-> -. 2 || a ) )
52 oveq1 
 |-  ( d = a -> ( d gcd e ) = ( a gcd e ) )
53 52 eqeq1d 
 |-  ( d = a -> ( ( d gcd e ) = 1 <-> ( a gcd e ) = 1 ) )
54 oveq1 
 |-  ( d = a -> ( d ^ 4 ) = ( a ^ 4 ) )
55 54 oveq1d 
 |-  ( d = a -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( a ^ 4 ) + ( e ^ 4 ) ) )
56 55 eqeq1d 
 |-  ( d = a -> ( ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) <-> ( ( a ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) )
57 53 56 anbi12d 
 |-  ( d = a -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) <-> ( ( a gcd e ) = 1 /\ ( ( a ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) )
58 51 57 anbi12d 
 |-  ( d = a -> ( ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) <-> ( -. 2 || a /\ ( ( a gcd e ) = 1 /\ ( ( a ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) ) )
59 oveq2 
 |-  ( e = b -> ( a gcd e ) = ( a gcd b ) )
60 59 eqeq1d 
 |-  ( e = b -> ( ( a gcd e ) = 1 <-> ( a gcd b ) = 1 ) )
61 oveq1 
 |-  ( e = b -> ( e ^ 4 ) = ( b ^ 4 ) )
62 61 oveq2d 
 |-  ( e = b -> ( ( a ^ 4 ) + ( e ^ 4 ) ) = ( ( a ^ 4 ) + ( b ^ 4 ) ) )
63 62 eqeq1d 
 |-  ( e = b -> ( ( ( a ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) <-> ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
64 60 63 anbi12d 
 |-  ( e = b -> ( ( ( a gcd e ) = 1 /\ ( ( a ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) <-> ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) )
65 64 anbi2d 
 |-  ( e = b -> ( ( -. 2 || a /\ ( ( a gcd e ) = 1 /\ ( ( a ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) <-> ( -. 2 || a /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) ) )
66 simprr 
 |-  ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) -> a e. NN )
67 66 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || a ) -> a e. NN )
68 simprl 
 |-  ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) -> b e. NN )
69 68 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || a ) -> b e. NN )
70 simpr 
 |-  ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
71 70 anim1ci 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || a ) -> ( -. 2 || a /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) )
72 58 65 67 69 71 2rspcedvdw 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || a ) -> E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) )
73 breq2 
 |-  ( d = b -> ( 2 || d <-> 2 || b ) )
74 73 notbid 
 |-  ( d = b -> ( -. 2 || d <-> -. 2 || b ) )
75 oveq1 
 |-  ( d = b -> ( d gcd e ) = ( b gcd e ) )
76 75 eqeq1d 
 |-  ( d = b -> ( ( d gcd e ) = 1 <-> ( b gcd e ) = 1 ) )
77 oveq1 
 |-  ( d = b -> ( d ^ 4 ) = ( b ^ 4 ) )
78 77 oveq1d 
 |-  ( d = b -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( b ^ 4 ) + ( e ^ 4 ) ) )
79 78 eqeq1d 
 |-  ( d = b -> ( ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) <-> ( ( b ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) )
80 76 79 anbi12d 
 |-  ( d = b -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) <-> ( ( b gcd e ) = 1 /\ ( ( b ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) )
81 74 80 anbi12d 
 |-  ( d = b -> ( ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) <-> ( -. 2 || b /\ ( ( b gcd e ) = 1 /\ ( ( b ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) ) )
82 oveq2 
 |-  ( e = a -> ( b gcd e ) = ( b gcd a ) )
83 82 eqeq1d 
 |-  ( e = a -> ( ( b gcd e ) = 1 <-> ( b gcd a ) = 1 ) )
84 oveq1 
 |-  ( e = a -> ( e ^ 4 ) = ( a ^ 4 ) )
85 84 oveq2d 
 |-  ( e = a -> ( ( b ^ 4 ) + ( e ^ 4 ) ) = ( ( b ^ 4 ) + ( a ^ 4 ) ) )
86 85 eqeq1d 
 |-  ( e = a -> ( ( ( b ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) <-> ( ( b ^ 4 ) + ( a ^ 4 ) ) = ( c ^ 2 ) ) )
87 83 86 anbi12d 
 |-  ( e = a -> ( ( ( b gcd e ) = 1 /\ ( ( b ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) <-> ( ( b gcd a ) = 1 /\ ( ( b ^ 4 ) + ( a ^ 4 ) ) = ( c ^ 2 ) ) ) )
88 87 anbi2d 
 |-  ( e = a -> ( ( -. 2 || b /\ ( ( b gcd e ) = 1 /\ ( ( b ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) <-> ( -. 2 || b /\ ( ( b gcd a ) = 1 /\ ( ( b ^ 4 ) + ( a ^ 4 ) ) = ( c ^ 2 ) ) ) ) )
89 68 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> b e. NN )
90 66 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> a e. NN )
91 simpr 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> -. 2 || b )
92 89 nnzd 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> b e. ZZ )
93 90 nnzd 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> a e. ZZ )
94 92 93 gcdcomd 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( b gcd a ) = ( a gcd b ) )
95 simplrl 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( a gcd b ) = 1 )
96 94 95 eqtrd 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( b gcd a ) = 1 )
97 4nn0 
 |-  4 e. NN0
98 97 a1i 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> 4 e. NN0 )
99 89 98 nnexpcld 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( b ^ 4 ) e. NN )
100 99 nncnd 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( b ^ 4 ) e. CC )
101 90 98 nnexpcld 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( a ^ 4 ) e. NN )
102 101 nncnd 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( a ^ 4 ) e. CC )
103 100 102 addcomd 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( ( b ^ 4 ) + ( a ^ 4 ) ) = ( ( a ^ 4 ) + ( b ^ 4 ) ) )
104 simplrr 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) )
105 103 104 eqtrd 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( ( b ^ 4 ) + ( a ^ 4 ) ) = ( c ^ 2 ) )
106 91 96 105 jca32 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> ( -. 2 || b /\ ( ( b gcd a ) = 1 /\ ( ( b ^ 4 ) + ( a ^ 4 ) ) = ( c ^ 2 ) ) ) )
107 81 88 89 90 106 2rspcedvdw 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ -. 2 || b ) -> E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) )
108 66 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ 2 || a ) -> a e. NN )
109 68 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ 2 || a ) -> b e. NN )
110 simpr 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ 2 || a ) -> 2 || a )
111 simplrl 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ 2 || a ) -> ( a gcd b ) = 1 )
112 108 109 110 111 flt4lem2 
 |-  ( ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) /\ 2 || a ) -> -. 2 || b )
113 112 ex 
 |-  ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( 2 || a -> -. 2 || b ) )
114 imor 
 |-  ( ( 2 || a -> -. 2 || b ) <-> ( -. 2 || a \/ -. 2 || b ) )
115 113 114 sylib 
 |-  ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( -. 2 || a \/ -. 2 || b ) )
116 72 107 115 mpjaodan 
 |-  ( ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) /\ ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) )
117 116 ex 
 |-  ( ( ( ph /\ c e. NN ) /\ ( b e. NN /\ a e. NN ) ) -> ( ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) -> E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) ) )
118 117 rexlimdvva 
 |-  ( ( ph /\ c e. NN ) -> ( E. b e. NN E. a e. NN ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) -> E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) ) )
119 118 reximdva 
 |-  ( ph -> ( E. c e. NN E. b e. NN E. a e. NN ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) -> E. c e. NN E. d e. NN E. e e. NN ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( c ^ 2 ) ) ) ) )
120 49 119 mtod 
 |-  ( ph -> -. E. c e. NN E. b e. NN E. a e. NN ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
121 rexcom13 
 |-  ( E. c e. NN E. b e. NN E. a e. NN ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) <-> E. a e. NN E. b e. NN E. c e. NN ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
122 120 121 sylnib 
 |-  ( ph -> -. E. a e. NN E. b e. NN E. c e. NN ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
123 oveq1 
 |-  ( a = ( A / ( A gcd B ) ) -> ( a gcd b ) = ( ( A / ( A gcd B ) ) gcd b ) )
124 123 eqeq1d 
 |-  ( a = ( A / ( A gcd B ) ) -> ( ( a gcd b ) = 1 <-> ( ( A / ( A gcd B ) ) gcd b ) = 1 ) )
125 oveq1 
 |-  ( a = ( A / ( A gcd B ) ) -> ( a ^ 4 ) = ( ( A / ( A gcd B ) ) ^ 4 ) )
126 125 oveq1d 
 |-  ( a = ( A / ( A gcd B ) ) -> ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( b ^ 4 ) ) )
127 126 eqeq1d 
 |-  ( a = ( A / ( A gcd B ) ) -> ( ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) <-> ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
128 124 127 anbi12d 
 |-  ( a = ( A / ( A gcd B ) ) -> ( ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) <-> ( ( ( A / ( A gcd B ) ) gcd b ) = 1 /\ ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) )
129 oveq2 
 |-  ( b = ( B / ( A gcd B ) ) -> ( ( A / ( A gcd B ) ) gcd b ) = ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) )
130 129 eqeq1d 
 |-  ( b = ( B / ( A gcd B ) ) -> ( ( ( A / ( A gcd B ) ) gcd b ) = 1 <-> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) )
131 oveq1 
 |-  ( b = ( B / ( A gcd B ) ) -> ( b ^ 4 ) = ( ( B / ( A gcd B ) ) ^ 4 ) )
132 131 oveq2d 
 |-  ( b = ( B / ( A gcd B ) ) -> ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( b ^ 4 ) ) = ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) )
133 132 eqeq1d 
 |-  ( b = ( B / ( A gcd B ) ) -> ( ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) <-> ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) = ( c ^ 2 ) ) )
134 130 133 anbi12d 
 |-  ( b = ( B / ( A gcd B ) ) -> ( ( ( ( A / ( A gcd B ) ) gcd b ) = 1 /\ ( ( ( A / ( A gcd B ) ) ^ 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 ^ 2 ) ) ) )
135 oveq1 
 |-  ( c = ( C / ( ( A gcd B ) ^ 2 ) ) -> ( c ^ 2 ) = ( ( C / ( ( A gcd B ) ^ 2 ) ) ^ 2 ) )
136 135 eqeq2d 
 |-  ( c = ( C / ( ( A gcd B ) ^ 2 ) ) -> ( ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) = ( c ^ 2 ) <-> ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) = ( ( C / ( ( A gcd B ) ^ 2 ) ) ^ 2 ) ) )
137 136 anbi2d 
 |-  ( c = ( C / ( ( A gcd B ) ^ 2 ) ) -> ( ( ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 /\ ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd 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 ) ) ) )
138 1 adantr 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> A e. NN )
139 2 adantr 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> B e. NN )
140 3 adantr 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> C e. NN )
141 simpr 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) )
142 138 139 140 141 flt4lem6 
 |-  ( ( ph /\ ( ( 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 ) ) )
143 142 simpld 
 |-  ( ( ph /\ ( ( 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 ) )
144 143 simp1d 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> ( A / ( A gcd B ) ) e. NN )
145 143 simp2d 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> ( B / ( A gcd B ) ) e. NN )
146 143 simp3d 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> ( C / ( ( A gcd B ) ^ 2 ) ) e. NN )
147 1 nnzd 
 |-  ( ph -> A e. ZZ )
148 147 adantr 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> A e. ZZ )
149 2 nnzd 
 |-  ( ph -> B e. ZZ )
150 149 adantr 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> B e. ZZ )
151 2 nnne0d 
 |-  ( ph -> B =/= 0 )
152 151 adantr 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> B =/= 0 )
153 divgcdcoprm0 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )
154 148 150 152 153 syl3anc 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )
155 142 simprd 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) = ( ( C / ( ( A gcd B ) ^ 2 ) ) ^ 2 ) )
156 154 155 jca 
 |-  ( ( ph /\ ( ( 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 ) ) )
157 128 134 137 144 145 146 156 3rspcedvdw 
 |-  ( ( ph /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) -> E. a e. NN E. b e. NN E. c e. NN ( ( a gcd b ) = 1 /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
158 122 157 mtand 
 |-  ( ph -> -. ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) )
159 158 neqned 
 |-  ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 2 ) )