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 ) )