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	$$⊢\phi \to S\in ℂ$$
	fltdiv.0	$$⊢\phi \to S\ne 0$$
	fltdiv.a	$$⊢\phi \to A\in ℂ$$
	fltdiv.b	$$⊢\phi \to B\in ℂ$$
	fltdiv.c	$$⊢\phi \to C\in ℂ$$
	fltdiv.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	fltdiv.1	$$⊢\phi \to A^N+B^N=C^N$$
Assertion	fltdiv	$$⊢\phi \to {\left(\frac{A}{S}\right)}^N+{\left(\frac{B}{S}\right)}^N={\left(\frac{C}{S}\right)}^N$$

Proof

Step	Hyp	Ref	Expression
1		fltdiv.s	$$⊢\phi \to S\in ℂ$$
2		fltdiv.0	$$⊢\phi \to S\ne 0$$
3		fltdiv.a	$$⊢\phi \to A\in ℂ$$
4		fltdiv.b	$$⊢\phi \to B\in ℂ$$
5		fltdiv.c	$$⊢\phi \to C\in ℂ$$
6		fltdiv.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		fltdiv.1	$$⊢\phi \to A^N+B^N=C^N$$
8	3 6	expcld	$$⊢\phi \to A^N\in ℂ$$
9	4 6	expcld	$$⊢\phi \to B^N\in ℂ$$
10	1 6	expcld	$$⊢\phi \to S^N\in ℂ$$
11	6	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
12	1 2 11	expne0d	$$⊢\phi \to S^N\ne 0$$
13	8 9 10 12	divdird	$$⊢\phi \to \frac{A^N+B^N}{S^N}=\left(\frac{A^N}{S^N}\right)+\left(\frac{B^N}{S^N}\right)$$
14	7	oveq1d	$$⊢\phi \to \frac{A^N+B^N}{S^N}=\frac{C^N}{S^N}$$
15	13 14	eqtr3d	$$⊢\phi \to \left(\frac{A^N}{S^N}\right)+\left(\frac{B^N}{S^N}\right)=\frac{C^N}{S^N}$$
16	3 1 2 6	expdivd	$$⊢\phi \to {\left(\frac{A}{S}\right)}^N=\frac{A^N}{S^N}$$
17	4 1 2 6	expdivd	$$⊢\phi \to {\left(\frac{B}{S}\right)}^N=\frac{B^N}{S^N}$$
18	16 17	oveq12d	$$⊢\phi \to {\left(\frac{A}{S}\right)}^N+{\left(\frac{B}{S}\right)}^N=\left(\frac{A^N}{S^N}\right)+\left(\frac{B^N}{S^N}\right)$$
19	5 1 2 6	expdivd	$$⊢\phi \to {\left(\frac{C}{S}\right)}^N=\frac{C^N}{S^N}$$
20	15 18 19	3eqtr4d	$$⊢\phi \to {\left(\frac{A}{S}\right)}^N+{\left(\frac{B}{S}\right)}^N={\left(\frac{C}{S}\right)}^N$$