Metamath Proof Explorer

Theorem fltoprmgt3

Description: Fermat's last theorem holds for any exponent greater than 2 if it holds for all odd prime exponents greater than 3. (TODO-AV: after a proof is available for N = 3 , see flt3, the hypothesis fltoprmgt3.3 can be removed.) (Contributed by AV, 15-Sep-2026)

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

Proof

Step Hyp Ref Expression
1 fltoprmgt3.a 
 |-  ( ph -> A e. NN )
2 fltoprmgt3.b 
 |-  ( ph -> B e. NN )
3 fltoprmgt3.c 
 |-  ( ph -> C e. NN )
4 fltoprmgt3.n 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
5 fltoprmgt3.r 
 |-  ( ph -> A. a e. NN A. b e. NN A. c e. NN A. p e. Prime ( 3 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) )
6 fltoprmgt3.3 
 |-  ( ph -> ( ( a ^ 3 ) + ( b ^ 3 ) ) =/= ( c ^ 3 ) )
7 prmz 
 |-  ( p e. Prime -> p e. ZZ )
8 2z 
 |-  2 e. ZZ
9 8 a1i 
 |-  ( p e. ZZ -> 2 e. ZZ )
10 id 
 |-  ( p e. ZZ -> p e. ZZ )
11 9 10 zltp1led 
 |-  ( p e. ZZ -> ( 2 < p <-> ( 2 + 1 ) <_ p ) )
12 2p1e3 
 |-  ( 2 + 1 ) = 3
13 12 breq1i 
 |-  ( ( 2 + 1 ) <_ p <-> 3 <_ p )
14 13 a1i 
 |-  ( p e. ZZ -> ( ( 2 + 1 ) <_ p <-> 3 <_ p ) )
15 3re 
 |-  3 e. RR
16 15 a1i 
 |-  ( p e. ZZ -> 3 e. RR )
17 zre 
 |-  ( p e. ZZ -> p e. RR )
18 16 17 leloed 
 |-  ( p e. ZZ -> ( 3 <_ p <-> ( 3 < p \/ 3 = p ) ) )
19 11 14 18 3bitrd 
 |-  ( p e. ZZ -> ( 2 < p <-> ( 3 < p \/ 3 = p ) ) )
20 7 19 syl 
 |-  ( p e. Prime -> ( 2 < p <-> ( 3 < p \/ 3 = p ) ) )
21 20 adantl 
 |-  ( ( c e. NN /\ p e. Prime ) -> ( 2 < p <-> ( 3 < p \/ 3 = p ) ) )
22 21 adantl 
 |-  ( ( ( ph /\ ( a e. NN /\ b e. NN ) ) /\ ( c e. NN /\ p e. Prime ) ) -> ( 2 < p <-> ( 3 < p \/ 3 = p ) ) )
23 pm2.27 
 |-  ( 3 < p -> ( ( 3 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) )
24 23 a1i 
 |-  ( ( ( ph /\ ( a e. NN /\ b e. NN ) ) /\ ( c e. NN /\ p e. Prime ) ) -> ( 3 < p -> ( ( 3 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) ) )
25 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( a e. NN /\ b e. NN ) ) /\ ( c e. NN /\ p e. Prime ) ) /\ 3 = p ) -> ( ( a ^ 3 ) + ( b ^ 3 ) ) =/= ( c ^ 3 ) )
26 oveq2 
 |-  ( 3 = p -> ( a ^ 3 ) = ( a ^ p ) )
27 oveq2 
 |-  ( 3 = p -> ( b ^ 3 ) = ( b ^ p ) )
28 26 27 oveq12d 
 |-  ( 3 = p -> ( ( a ^ 3 ) + ( b ^ 3 ) ) = ( ( a ^ p ) + ( b ^ p ) ) )
29 oveq2 
 |-  ( 3 = p -> ( c ^ 3 ) = ( c ^ p ) )
30 28 29 neeq12d 
 |-  ( 3 = p -> ( ( ( a ^ 3 ) + ( b ^ 3 ) ) =/= ( c ^ 3 ) <-> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) )
31 30 adantl 
 |-  ( ( ( ( ph /\ ( a e. NN /\ b e. NN ) ) /\ ( c e. NN /\ p e. Prime ) ) /\ 3 = p ) -> ( ( ( a ^ 3 ) + ( b ^ 3 ) ) =/= ( c ^ 3 ) <-> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) )
32 25 31 mpbid 
 |-  ( ( ( ( ph /\ ( a e. NN /\ b e. NN ) ) /\ ( c e. NN /\ p e. Prime ) ) /\ 3 = p ) -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) )
33 32 a1d 
 |-  ( ( ( ( ph /\ ( a e. NN /\ b e. NN ) ) /\ ( c e. NN /\ p e. Prime ) ) /\ 3 = p ) -> ( ( 3 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) )
34 33 ex 
 |-  ( ( ( ph /\ ( a e. NN /\ b e. NN ) ) /\ ( c e. NN /\ p e. Prime ) ) -> ( 3 = p -> ( ( 3 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) ) )
35 24 34 jaod 
 |-  ( ( ( ph /\ ( a e. NN /\ b e. NN ) ) /\ ( c e. NN /\ p e. Prime ) ) -> ( ( 3 < p \/ 3 = p ) -> ( ( 3 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) ) )
36 22 35 sylbid 
 |-  ( ( ( ph /\ ( a e. NN /\ b e. NN ) ) /\ ( c e. NN /\ p e. Prime ) ) -> ( 2 < p -> ( ( 3 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) ) )
37 36 com23 
 |-  ( ( ( ph /\ ( a e. NN /\ b e. NN ) ) /\ ( c e. NN /\ p e. Prime ) ) -> ( ( 3 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) ) )
38 37 ralimdvva 
 |-  ( ( ph /\ ( a e. NN /\ b e. NN ) ) -> ( A. c e. NN A. p e. Prime ( 3 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> A. c e. NN A. p e. Prime ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) ) )
39 38 ralimdvva 
 |-  ( ph -> ( A. a e. NN A. b e. NN A. c e. NN A. p e. Prime ( 3 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) -> A. a e. NN A. b e. NN A. c e. NN A. p e. Prime ( 2 < p -> ( ( a ^ p ) + ( b ^ p ) ) =/= ( c ^ p ) ) ) )
40 5 39 mpd 
 |-  ( 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 ) ) )
41 1 2 3 4 40 fltoprm 
 |-  ( ph -> ( ( A ^ N ) + ( B ^ N ) ) =/= ( C ^ N ) )