Metamath Proof Explorer

Theorem flt4ALT

Description: Fermat's last theorem for the exponent four, derived from Fermat's right triangle theorem (which is not proved yet, see fermrtt: after a proof is available, the hypothesis flt4ALT.r can be removed - TODO-AV). (Contributed by AV, 15-Sep-2026) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 flt4.a 
 |-  ( ph -> A e. NN )
2 flt4.b 
 |-  ( ph -> B e. NN )
3 flt4.c 
 |-  ( ph -> C e. NN )
4 flt4ALT.r 
 |-  ( ph -> A. a e. NN A. b e. NN A. c e. NN ( ( a ^ 4 ) - ( b ^ 4 ) ) =/= ( c ^ 2 ) )
5 1 nnsqcld 
 |-  ( ph -> ( A ^ 2 ) e. NN )
6 3 2 5 3jca 
 |-  ( ph -> ( C e. NN /\ B e. NN /\ ( A ^ 2 ) e. NN ) )
7 oveq1 
 |-  ( a = C -> ( a ^ 4 ) = ( C ^ 4 ) )
8 7 oveq1d 
 |-  ( a = C -> ( ( a ^ 4 ) - ( b ^ 4 ) ) = ( ( C ^ 4 ) - ( b ^ 4 ) ) )
9 8 neeq1d 
 |-  ( a = C -> ( ( ( a ^ 4 ) - ( b ^ 4 ) ) =/= ( c ^ 2 ) <-> ( ( C ^ 4 ) - ( b ^ 4 ) ) =/= ( c ^ 2 ) ) )
10 oveq1 
 |-  ( b = B -> ( b ^ 4 ) = ( B ^ 4 ) )
11 10 oveq2d 
 |-  ( b = B -> ( ( C ^ 4 ) - ( b ^ 4 ) ) = ( ( C ^ 4 ) - ( B ^ 4 ) ) )
12 11 neeq1d 
 |-  ( b = B -> ( ( ( C ^ 4 ) - ( b ^ 4 ) ) =/= ( c ^ 2 ) <-> ( ( C ^ 4 ) - ( B ^ 4 ) ) =/= ( c ^ 2 ) ) )
13 oveq1 
 |-  ( c = ( A ^ 2 ) -> ( c ^ 2 ) = ( ( A ^ 2 ) ^ 2 ) )
14 13 neeq2d 
 |-  ( c = ( A ^ 2 ) -> ( ( ( C ^ 4 ) - ( B ^ 4 ) ) =/= ( c ^ 2 ) <-> ( ( C ^ 4 ) - ( B ^ 4 ) ) =/= ( ( A ^ 2 ) ^ 2 ) ) )
15 9 12 14 rspc3v 
 |-  ( ( C e. NN /\ B e. NN /\ ( A ^ 2 ) e. NN ) -> ( A. a e. NN A. b e. NN A. c e. NN ( ( a ^ 4 ) - ( b ^ 4 ) ) =/= ( c ^ 2 ) -> ( ( C ^ 4 ) - ( B ^ 4 ) ) =/= ( ( A ^ 2 ) ^ 2 ) ) )
16 6 4 15 sylc 
 |-  ( ph -> ( ( C ^ 4 ) - ( B ^ 4 ) ) =/= ( ( A ^ 2 ) ^ 2 ) )
17 16 neneqd 
 |-  ( ph -> -. ( ( C ^ 4 ) - ( B ^ 4 ) ) = ( ( A ^ 2 ) ^ 2 ) )
18 4nn0 
 |-  4 e. NN0
19 18 a1i 
 |-  ( ph -> 4 e. NN0 )
20 3 19 nnexpcld 
 |-  ( ph -> ( C ^ 4 ) e. NN )
21 20 nncnd 
 |-  ( ph -> ( C ^ 4 ) e. CC )
22 2 19 nnexpcld 
 |-  ( ph -> ( B ^ 4 ) e. NN )
23 22 nncnd 
 |-  ( ph -> ( B ^ 4 ) e. CC )
24 1 19 nnexpcld 
 |-  ( ph -> ( A ^ 4 ) e. NN )
25 24 nncnd 
 |-  ( ph -> ( A ^ 4 ) e. CC )
26 21 23 25 subadd2d 
 |-  ( ph -> ( ( ( C ^ 4 ) - ( B ^ 4 ) ) = ( A ^ 4 ) <-> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 4 ) ) )
27 1 nncnd 
 |-  ( ph -> A e. CC )
28 27 exp4sqsq 
 |-  ( ph -> ( A ^ 4 ) = ( ( A ^ 2 ) ^ 2 ) )
29 28 eqeq2d 
 |-  ( ph -> ( ( ( C ^ 4 ) - ( B ^ 4 ) ) = ( A ^ 4 ) <-> ( ( C ^ 4 ) - ( B ^ 4 ) ) = ( ( A ^ 2 ) ^ 2 ) ) )
30 26 29 bitr3d 
 |-  ( ph -> ( ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 4 ) <-> ( ( C ^ 4 ) - ( B ^ 4 ) ) = ( ( A ^ 2 ) ^ 2 ) ) )
31 17 30 mtbird 
 |-  ( ph -> -. ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 4 ) )
32 31 neqned 
 |-  ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 4 ) )