Metamath Proof Explorer

Theorem fltoprm

Description: Fermat's last theorem holds for any exponent greater than 2 if it holds for odd prime exponents. (Contributed by AV, 15-Sep-2026)

Ref Expression
Hypotheses fltoprm.a 
|- ( ph -> A e. NN )
fltoprm.b 
|- ( ph -> B e. NN )
fltoprm.c 
|- ( ph -> C e. NN )
fltoprm.n 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
fltoprm.r 
|- ( ph -> A. a e. NN A. b e. NN A. c e. NN A. p e. Prime ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) )
Assertion fltoprm 
|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) )

Proof

Step Hyp Ref Expression
1 fltoprm.a 
 |-  ( ph -> A e. NN )
2 fltoprm.b 
 |-  ( ph -> B e. NN )
3 fltoprm.c 
 |-  ( ph -> C e. NN )
4 fltoprm.n 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
5 fltoprm.r 
 |-  ( ph -> A. a e. NN A. b e. NN A. c e. NN A. p e. Prime ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) )
6 prmnn 
 |-  ( r e. Prime -> r e. NN )
7 3nn 
 |-  3 e. NN
8 eluznn 
 |-  ( ( 3 e. NN /\ N e. ( ZZ>= ` 3 ) ) -> N e. NN )
9 7 4 8 sylancr 
 |-  ( ph -> N e. NN )
10 nndivides 
 |-  ( ( r e. NN /\ N e. NN ) -> ( r || N <-> E. k e. NN ( k x. r ) = N ) )
11 6 9 10 syl2anr 
 |-  ( ( ph /\ r e. Prime ) -> ( r || N <-> E. k e. NN ( k x. r ) = N ) )
12 5 adantr 
 |-  ( ( ph /\ r e. Prime ) -> A. a e. NN A. b e. NN A. c e. NN A. p e. Prime ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) )
13 12 ad2antrr 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ k e. NN ) /\ 2 < r ) -> A. a e. NN A. b e. NN A. c e. NN A. p e. Prime ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) )
14 1 ad2antrr 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> A e. NN )
15 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
16 15 adantl 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> k e. NN0 )
17 14 16 nnexpcld 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( A ^ k ) e. NN )
18 2 ad2antrr 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> B e. NN )
19 18 16 nnexpcld 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( B ^ k ) e. NN )
20 3 ad2antrr 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> C e. NN )
21 20 16 nnexpcld 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( C ^ k ) e. NN )
22 17 19 21 3jca 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( ( A ^ k ) e. NN /\ ( B ^ k ) e. NN /\ ( C ^ k ) e. NN ) )
23 22 adantr 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ k e. NN ) /\ 2 < r ) -> ( ( A ^ k ) e. NN /\ ( B ^ k ) e. NN /\ ( C ^ k ) e. NN ) )
24 oveq1 
 |-  ( a = ( A ^ k ) -> ( a ^ p ) = ( ( A ^ k ) ^ p ) )
25 24 oveq1d 
 |-  ( a = ( A ^ k ) -> ( ( a ^ p ) + ( b ^ p ) ) = ( ( ( A ^ k ) ^ p ) + ( b ^ p ) ) )
26 25 neeq1d 
 |-  ( a = ( A ^ k ) -> ( ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) <-> ( ( ( A ^ k ) ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) )
27 26 imbi2d 
 |-  ( a = ( A ^ k ) -> ( ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) <-> ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) ) )
28 27 ralbidv 
 |-  ( a = ( A ^ k ) -> ( A. p e. Prime ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) <-> A. p e. Prime ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) ) )
29 oveq1 
 |-  ( b = ( B ^ k ) -> ( b ^ p ) = ( ( B ^ k ) ^ p ) )
30 29 oveq2d 
 |-  ( b = ( B ^ k ) -> ( ( ( A ^ k ) ^ p ) + ( b ^ p ) ) = ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) )
31 30 neeq1d 
 |-  ( b = ( B ^ k ) -> ( ( ( ( A ^ k ) ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) <-> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( c ^ p ) ) )
32 31 imbi2d 
 |-  ( b = ( B ^ k ) -> ( ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) <-> ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( c ^ p ) ) ) )
33 32 ralbidv 
 |-  ( b = ( B ^ k ) -> ( A. p e. Prime ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) <-> A. p e. Prime ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( c ^ p ) ) ) )
34 oveq1 
 |-  ( c = ( C ^ k ) -> ( c ^ p ) = ( ( C ^ k ) ^ p ) )
35 34 neeq2d 
 |-  ( c = ( C ^ k ) -> ( ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( c ^ p ) <-> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( ( C ^ k ) ^ p ) ) )
36 35 imbi2d 
 |-  ( c = ( C ^ k ) -> ( ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( c ^ p ) ) <-> ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( ( C ^ k ) ^ p ) ) ) )
37 36 ralbidv 
 |-  ( c = ( C ^ k ) -> ( A. p e. Prime ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( c ^ p ) ) <-> A. p e. Prime ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( ( C ^ k ) ^ p ) ) ) )
38 28 33 37 rspc3v 
 |-  ( ( ( A ^ k ) e. NN /\ ( B ^ k ) e. NN /\ ( C ^ k ) e. NN ) -> ( A. a e. NN A. b e. NN A. c e. NN A. p e. Prime ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> A. p e. Prime ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( ( C ^ k ) ^ p ) ) ) )
39 23 38 syl 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ k e. NN ) /\ 2 < r ) -> ( A. a e. NN A. b e. NN A. c e. NN A. p e. Prime ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> A. p e. Prime ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( ( C ^ k ) ^ p ) ) ) )
40 breq2 
 |-  ( p = r -> ( 2 < p <-> 2 < r ) )
41 oveq2 
 |-  ( p = r -> ( ( A ^ k ) ^ p ) = ( ( A ^ k ) ^ r ) )
42 oveq2 
 |-  ( p = r -> ( ( B ^ k ) ^ p ) = ( ( B ^ k ) ^ r ) )
43 41 42 oveq12d 
 |-  ( p = r -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) = ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) )
44 oveq2 
 |-  ( p = r -> ( ( C ^ k ) ^ p ) = ( ( C ^ k ) ^ r ) )
45 43 44 neeq12d 
 |-  ( p = r -> ( ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( ( C ^ k ) ^ p ) <-> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) )
46 40 45 imbi12d 
 |-  ( p = r -> ( ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( ( C ^ k ) ^ p ) ) <-> ( 2 < r -> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) ) )
47 46 rspcv 
 |-  ( r e. Prime -> ( A. p e. Prime ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( ( C ^ k ) ^ p ) ) -> ( 2 < r -> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) ) )
48 47 adantl 
 |-  ( ( ph /\ r e. Prime ) -> ( A. p e. Prime ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( ( C ^ k ) ^ p ) ) -> ( 2 < r -> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) ) )
49 48 ad2antrr 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ k e. NN ) /\ 2 < r ) -> ( A. p e. Prime ( 2 < p -> ( ( ( A ^ k ) ^ p ) + ( ( B ^ k ) ^ p ) ) =/= ( ( C ^ k ) ^ p ) ) -> ( 2 < r -> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) ) )
50 pm2.27 
 |-  ( 2 < r -> ( ( 2 < r -> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) -> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) )
51 50 adantl 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ k e. NN ) /\ 2 < r ) -> ( ( 2 < r -> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) -> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) )
52 39 49 51 3syld 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ k e. NN ) /\ 2 < r ) -> ( A. a e. NN A. b e. NN A. c e. NN A. p e. Prime ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) )
53 13 52 mpd 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ k e. NN ) /\ 2 < r ) -> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) )
54 1 nncnd 
 |-  ( ph -> A e. CC )
55 54 ad2antrr 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> A e. CC )
56 6 nnnn0d 
 |-  ( r e. Prime -> r e. NN0 )
57 56 adantl 
 |-  ( ( ph /\ r e. Prime ) -> r e. NN0 )
58 57 adantr 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> r e. NN0 )
59 55 58 16 expmuld 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( A ^ ( k x. r ) ) = ( ( A ^ k ) ^ r ) )
60 2 nncnd 
 |-  ( ph -> B e. CC )
61 60 ad2antrr 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> B e. CC )
62 61 58 16 expmuld 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( B ^ ( k x. r ) ) = ( ( B ^ k ) ^ r ) )
63 59 62 oveq12d 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( ( A ^ ( k x. r ) ) + ( B ^ ( k x. r ) ) ) = ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) )
64 3 nncnd 
 |-  ( ph -> C e. CC )
65 64 ad2antrr 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> C e. CC )
66 65 58 16 expmuld 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( C ^ ( k x. r ) ) = ( ( C ^ k ) ^ r ) )
67 63 66 neeq12d 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( ( ( A ^ ( k x. r ) ) + ( B ^ ( k x. r ) ) ) =/= ( C ^ ( k x. r ) ) <-> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) )
68 67 adantr 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ k e. NN ) /\ 2 < r ) -> ( ( ( A ^ ( k x. r ) ) + ( B ^ ( k x. r ) ) ) =/= ( C ^ ( k x. r ) ) <-> ( ( ( A ^ k ) ^ r ) + ( ( B ^ k ) ^ r ) ) =/= ( ( C ^ k ) ^ r ) ) )
69 53 68 mpbird 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ k e. NN ) /\ 2 < r ) -> ( ( A ^ ( k x. r ) ) + ( B ^ ( k x. r ) ) ) =/= ( C ^ ( k x. r ) ) )
70 oveq2 
 |-  ( ( k x. r ) = N -> ( A ^ ( k x. r ) ) = ( A ^ N ) )
71 oveq2 
 |-  ( ( k x. r ) = N -> ( B ^ ( k x. r ) ) = ( B ^ N ) )
72 70 71 oveq12d 
 |-  ( ( k x. r ) = N -> ( ( A ^ ( k x. r ) ) + ( B ^ ( k x. r ) ) ) = ( ( A ^ N ) + ( B ^ N ) ) )
73 oveq2 
 |-  ( ( k x. r ) = N -> ( C ^ ( k x. r ) ) = ( C ^ N ) )
74 72 73 neeq12d 
 |-  ( ( k x. r ) = N -> ( ( ( A ^ ( k x. r ) ) + ( B ^ ( k x. r ) ) ) =/= ( C ^ ( k x. r ) ) <-> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) )
75 69 74 syl5ibcom 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ k e. NN ) /\ 2 < r ) -> ( ( k x. r ) = N -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) )
76 75 ex 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( 2 < r -> ( ( k x. r ) = N -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) ) )
77 76 com23 
 |-  ( ( ( ph /\ r e. Prime ) /\ k e. NN ) -> ( ( k x. r ) = N -> ( 2 < r -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) ) )
78 77 rexlimdva 
 |-  ( ( ph /\ r e. Prime ) -> ( E. k e. NN ( k x. r ) = N -> ( 2 < r -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) ) )
79 11 78 sylbid 
 |-  ( ( ph /\ r e. Prime ) -> ( r || N -> ( 2 < r -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) ) )
80 79 impcomd 
 |-  ( ( ph /\ r e. Prime ) -> ( ( 2 < r /\ r || N ) -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) )
81 80 rexlimdva 
 |-  ( ph -> ( E. r e. Prime ( 2 < r /\ r || N ) -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) )
82 4 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ N = ( 2 ^ n ) ) -> N e. ( ZZ>= ` 3 ) )
83 simplr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ N = ( 2 ^ n ) ) -> n e. NN0 )
84 simpr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ N = ( 2 ^ n ) ) -> N = ( 2 ^ n ) )
85 fltoprmlem2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ n e. NN0 /\ N = ( 2 ^ n ) ) -> 4 || N )
86 82 83 84 85 syl3anc 
 |-  ( ( ( ph /\ n e. NN0 ) /\ N = ( 2 ^ n ) ) -> 4 || N )
87 86 ex 
 |-  ( ( ph /\ n e. NN0 ) -> ( N = ( 2 ^ n ) -> 4 || N ) )
88 4nn 
 |-  4 e. NN
89 9 88 jctil 
 |-  ( ph -> ( 4 e. NN /\ N e. NN ) )
90 89 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> ( 4 e. NN /\ N e. NN ) )
91 nndivides 
 |-  ( ( 4 e. NN /\ N e. NN ) -> ( 4 || N <-> E. k e. NN ( k x. 4 ) = N ) )
92 90 91 syl 
 |-  ( ( ph /\ n e. NN0 ) -> ( 4 || N <-> E. k e. NN ( k x. 4 ) = N ) )
93 1 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> A e. NN )
94 15 adantl 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> k e. NN0 )
95 93 94 nnexpcld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> ( A ^ k ) e. NN )
96 2 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> B e. NN )
97 96 94 nnexpcld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> ( B ^ k ) e. NN )
98 3 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> C e. NN )
99 98 94 nnexpcld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> ( C ^ k ) e. NN )
100 95 97 99 flt4 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> ( ( ( A ^ k ) ^ 4 ) + ( ( B ^ k ) ^ 4 ) ) =/= ( ( C ^ k ) ^ 4 ) )
101 54 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> A e. CC )
102 4nn0 
 |-  4 e. NN0
103 102 a1i 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> 4 e. NN0 )
104 101 103 94 expmuld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> ( A ^ ( k x. 4 ) ) = ( ( A ^ k ) ^ 4 ) )
105 2 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> B e. NN )
106 105 nncnd 
 |-  ( ( ph /\ n e. NN0 ) -> B e. CC )
107 106 adantr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> B e. CC )
108 107 103 94 expmuld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> ( B ^ ( k x. 4 ) ) = ( ( B ^ k ) ^ 4 ) )
109 104 108 oveq12d 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> ( ( A ^ ( k x. 4 ) ) + ( B ^ ( k x. 4 ) ) ) = ( ( ( A ^ k ) ^ 4 ) + ( ( B ^ k ) ^ 4 ) ) )
110 64 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> C e. CC )
111 110 103 94 expmuld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> ( C ^ ( k x. 4 ) ) = ( ( C ^ k ) ^ 4 ) )
112 100 109 111 3netr4d 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> ( ( A ^ ( k x. 4 ) ) + ( B ^ ( k x. 4 ) ) ) =/= ( C ^ ( k x. 4 ) ) )
113 oveq2 
 |-  ( ( k x. 4 ) = N -> ( A ^ ( k x. 4 ) ) = ( A ^ N ) )
114 oveq2 
 |-  ( ( k x. 4 ) = N -> ( B ^ ( k x. 4 ) ) = ( B ^ N ) )
115 113 114 oveq12d 
 |-  ( ( k x. 4 ) = N -> ( ( A ^ ( k x. 4 ) ) + ( B ^ ( k x. 4 ) ) ) = ( ( A ^ N ) + ( B ^ N ) ) )
116 oveq2 
 |-  ( ( k x. 4 ) = N -> ( C ^ ( k x. 4 ) ) = ( C ^ N ) )
117 115 116 neeq12d 
 |-  ( ( k x. 4 ) = N -> ( ( ( A ^ ( k x. 4 ) ) + ( B ^ ( k x. 4 ) ) ) =/= ( C ^ ( k x. 4 ) ) <-> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) )
118 112 117 syl5ibcom 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. NN ) -> ( ( k x. 4 ) = N -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) )
119 118 rexlimdva 
 |-  ( ( ph /\ n e. NN0 ) -> ( E. k e. NN ( k x. 4 ) = N -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) )
120 92 119 sylbid 
 |-  ( ( ph /\ n e. NN0 ) -> ( 4 || N -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) )
121 87 120 syld 
 |-  ( ( ph /\ n e. NN0 ) -> ( N = ( 2 ^ n ) -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) )
122 121 rexlimdva 
 |-  ( ph -> ( E. n e. NN0 N = ( 2 ^ n ) -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) ) )
123 fltoprmlem1 
 |-  ( N e. NN -> ( E. r e. Prime ( 2 < r /\ r || N ) \/ E. n e. NN0 N = ( 2 ^ n ) ) )
124 9 123 syl 
 |-  ( ph -> ( E. r e. Prime ( 2 < r /\ r || N ) \/ E. n e. NN0 N = ( 2 ^ n ) ) )
125 81 122 124 mpjaod 
 |-  ( ph -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) )