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	⊢ ( 𝜑 → 𝑆 ∈ ℂ )
	fltdiv.0	⊢ ( 𝜑 → 𝑆 ≠ 0 )
	fltdiv.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	fltdiv.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	fltdiv.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	fltdiv.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	fltdiv.1	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
Assertion	fltdiv	⊢ ( 𝜑 → ( ( ( 𝐴 / 𝑆 ) ↑ 𝑁 ) + ( ( 𝐵 / 𝑆 ) ↑ 𝑁 ) ) = ( ( 𝐶 / 𝑆 ) ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fltdiv.s	⊢ ( 𝜑 → 𝑆 ∈ ℂ )
2		fltdiv.0	⊢ ( 𝜑 → 𝑆 ≠ 0 )
3		fltdiv.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4		fltdiv.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
5		fltdiv.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6		fltdiv.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7		fltdiv.1	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
8	3 6	expcld	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
9	4 6	expcld	⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) ∈ ℂ )
10	1 6	expcld	⊢ ( 𝜑 → ( 𝑆 ↑ 𝑁 ) ∈ ℂ )
11	6	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
12	1 2 11	expne0d	⊢ ( 𝜑 → ( 𝑆 ↑ 𝑁 ) ≠ 0 )
13	8 9 10 12	divdird	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) / ( 𝑆 ↑ 𝑁 ) ) = ( ( ( 𝐴 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) + ( ( 𝐵 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) ) )
14	7	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) / ( 𝑆 ↑ 𝑁 ) ) = ( ( 𝐶 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) )
15	13 14	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) + ( ( 𝐵 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) ) = ( ( 𝐶 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) )
16	3 1 2 6	expdivd	⊢ ( 𝜑 → ( ( 𝐴 / 𝑆 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) )
17	4 1 2 6	expdivd	⊢ ( 𝜑 → ( ( 𝐵 / 𝑆 ) ↑ 𝑁 ) = ( ( 𝐵 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) )
18	16 17	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐴 / 𝑆 ) ↑ 𝑁 ) + ( ( 𝐵 / 𝑆 ) ↑ 𝑁 ) ) = ( ( ( 𝐴 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) + ( ( 𝐵 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) ) )
19	5 1 2 6	expdivd	⊢ ( 𝜑 → ( ( 𝐶 / 𝑆 ) ↑ 𝑁 ) = ( ( 𝐶 ↑ 𝑁 ) / ( 𝑆 ↑ 𝑁 ) ) )
20	15 18 19	3eqtr4d	⊢ ( 𝜑 → ( ( ( 𝐴 / 𝑆 ) ↑ 𝑁 ) + ( ( 𝐵 / 𝑆 ) ↑ 𝑁 ) ) = ( ( 𝐶 / 𝑆 ) ↑ 𝑁 ) )