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

Metamath Proof Explorer

Theorem flt0

Description: A counterexample for FLT does not exist for N = 0 . (Contributed by SN, 20-Aug-2024)

Ref Expression
Hypotheses flt0.a 
|- ( ph -> A e. CC )
flt0.b 
|- ( ph -> B e. CC )
flt0.c 
|- ( ph -> C e. CC )
flt0.n 
|- ( ph -> N e. NN0 )
flt0.1 
|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
Assertion flt0 
|- ( ph -> N e. NN )

Proof

Step Hyp Ref Expression
1 flt0.a 
 |-  ( ph -> A e. CC )
2 flt0.b 
 |-  ( ph -> B e. CC )
3 flt0.c 
 |-  ( ph -> C e. CC )
4 flt0.n 
 |-  ( ph -> N e. NN0 )
5 flt0.1 
 |-  ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
6 1p1e2 
 |-  ( 1 + 1 ) = 2
7 sn-1ne2 
 |-  1 =/= 2
8 7 necomi 
 |-  2 =/= 1
9 6 8 eqnetri 
 |-  ( 1 + 1 ) =/= 1
10 9 a1i 
 |-  ( ph -> ( 1 + 1 ) =/= 1 )
11 1 exp0d 
 |-  ( ph -> ( A ^ 0 ) = 1 )
12 2 exp0d 
 |-  ( ph -> ( B ^ 0 ) = 1 )
13 11 12 oveq12d 
 |-  ( ph -> ( ( A ^ 0 ) + ( B ^ 0 ) ) = ( 1 + 1 ) )
14 3 exp0d 
 |-  ( ph -> ( C ^ 0 ) = 1 )
15 10 13 14 3netr4d 
 |-  ( ph -> ( ( A ^ 0 ) + ( B ^ 0 ) ) =/= ( C ^ 0 ) )
16 oveq2 
 |-  ( N = 0 -> ( A ^ N ) = ( A ^ 0 ) )
17 oveq2 
 |-  ( N = 0 -> ( B ^ N ) = ( B ^ 0 ) )
18 16 17 oveq12d 
 |-  ( N = 0 -> ( ( A ^ N ) + ( B ^ N ) ) = ( ( A ^ 0 ) + ( B ^ 0 ) ) )
19 oveq2 
 |-  ( N = 0 -> ( C ^ N ) = ( C ^ 0 ) )
20 18 19 eqeq12d 
 |-  ( N = 0 -> ( ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) <-> ( ( A ^ 0 ) + ( B ^ 0 ) ) = ( C ^ 0 ) ) )
21 5 20 syl5ibcom 
 |-  ( ph -> ( N = 0 -> ( ( A ^ 0 ) + ( B ^ 0 ) ) = ( C ^ 0 ) ) )
22 21 imp 
 |-  ( ( ph /\ N = 0 ) -> ( ( A ^ 0 ) + ( B ^ 0 ) ) = ( C ^ 0 ) )
23 15 22 mteqand 
 |-  ( ph -> N =/= 0 )
24 elnnne0 
 |-  ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
25 4 23 24 sylanbrc 
 |-  ( ph -> N e. NN )