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

Metamath Proof Explorer

Theorem fltdiv

Description: A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (Contributed by SN, 20-Aug-2024)

Ref Expression
Hypotheses fltdiv.s 
|- ( ph -> S e. CC )
fltdiv.0 
|- ( ph -> S =/= 0 )
fltdiv.a 
|- ( ph -> A e. CC )
fltdiv.b 
|- ( ph -> B e. CC )
fltdiv.c 
|- ( ph -> C e. CC )
fltdiv.n 
|- ( ph -> N e. NN0 )
fltdiv.1 
|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
Assertion fltdiv 
|- ( ph -> ( ( ( A / S ) ^ N ) + ( ( B / S ) ^ N ) ) = ( ( C / S ) ^ N ) )

Proof

Step Hyp Ref Expression
1 fltdiv.s 
 |-  ( ph -> S e. CC )
2 fltdiv.0 
 |-  ( ph -> S =/= 0 )
3 fltdiv.a 
 |-  ( ph -> A e. CC )
4 fltdiv.b 
 |-  ( ph -> B e. CC )
5 fltdiv.c 
 |-  ( ph -> C e. CC )
6 fltdiv.n 
 |-  ( ph -> N e. NN0 )
7 fltdiv.1 
 |-  ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
8 3 6 expcld 
 |-  ( ph -> ( A ^ N ) e. CC )
9 4 6 expcld 
 |-  ( ph -> ( B ^ N ) e. CC )
10 1 6 expcld 
 |-  ( ph -> ( S ^ N ) e. CC )
11 6 nn0zd 
 |-  ( ph -> N e. ZZ )
12 1 2 11 expne0d 
 |-  ( ph -> ( S ^ N ) =/= 0 )
13 8 9 10 12 divdird 
 |-  ( ph -> ( ( ( A ^ N ) + ( B ^ N ) ) / ( S ^ N ) ) = ( ( ( A ^ N ) / ( S ^ N ) ) + ( ( B ^ N ) / ( S ^ N ) ) ) )
14 7 oveq1d 
 |-  ( ph -> ( ( ( A ^ N ) + ( B ^ N ) ) / ( S ^ N ) ) = ( ( C ^ N ) / ( S ^ N ) ) )
15 13 14 eqtr3d 
 |-  ( ph -> ( ( ( A ^ N ) / ( S ^ N ) ) + ( ( B ^ N ) / ( S ^ N ) ) ) = ( ( C ^ N ) / ( S ^ N ) ) )
16 3 1 2 6 expdivd 
 |-  ( ph -> ( ( A / S ) ^ N ) = ( ( A ^ N ) / ( S ^ N ) ) )
17 4 1 2 6 expdivd 
 |-  ( ph -> ( ( B / S ) ^ N ) = ( ( B ^ N ) / ( S ^ N ) ) )
18 16 17 oveq12d 
 |-  ( ph -> ( ( ( A / S ) ^ N ) + ( ( B / S ) ^ N ) ) = ( ( ( A ^ N ) / ( S ^ N ) ) + ( ( B ^ N ) / ( S ^ N ) ) ) )
19 5 1 2 6 expdivd 
 |-  ( ph -> ( ( C / S ) ^ N ) = ( ( C ^ N ) / ( S ^ N ) ) )
20 15 18 19 3eqtr4d 
 |-  ( ph -> ( ( ( A / S ) ^ N ) + ( ( B / S ) ^ N ) ) = ( ( C / S ) ^ N ) )