Theorem fltmul

Description: A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (There does not seem to be a standard term for Fermat or Pythagorean triples extended to any N e. NN0 , hence the label is more about the context in which this theorem is used). (Contributed by SN, 20-Aug-2024)

	Ref	Expression
Hypotheses	fltmul.s	$$⊢\phi \to S\in ℂ$$
	fltmul.a	$$⊢\phi \to A\in ℂ$$
	fltmul.b	$$⊢\phi \to B\in ℂ$$
	fltmul.c	$$⊢\phi \to C\in ℂ$$
	fltmul.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	fltmul.1	$$⊢\phi \to A^N+B^N=C^N$$
Assertion	fltmul	$$⊢\phi \to {SA}^N+{SB}^N={SC}^N$$

Proof

Step	Hyp	Ref	Expression
1		fltmul.s	$$⊢\phi \to S\in ℂ$$
2		fltmul.a	$$⊢\phi \to A\in ℂ$$
3		fltmul.b	$$⊢\phi \to B\in ℂ$$
4		fltmul.c	$$⊢\phi \to C\in ℂ$$
5		fltmul.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
6		fltmul.1	$$⊢\phi \to A^N+B^N=C^N$$
7	1 5	expcld	$$⊢\phi \to S^N\in ℂ$$
8	2 5	expcld	$$⊢\phi \to A^N\in ℂ$$
9	3 5	expcld	$$⊢\phi \to B^N\in ℂ$$
10	7 8 9	adddid	$$⊢\phi \to S^N\left(A^N+B^N\right)=S^N{A}^N+S^N{B}^N$$
11	6	oveq2d	$$⊢\phi \to S^N\left(A^N+B^N\right)=S^N{C}^N$$
12	10 11	eqtr3d	$$⊢\phi \to S^N{A}^N+S^N{B}^N=S^N{C}^N$$
13	1 2 5	mulexpd	$$⊢\phi \to {SA}^N=S^N{A}^N$$
14	1 3 5	mulexpd	$$⊢\phi \to {SB}^N=S^N{B}^N$$
15	13 14	oveq12d	$$⊢\phi \to {SA}^N+{SB}^N=S^N{A}^N+S^N{B}^N$$
16	1 4 5	mulexpd	$$⊢\phi \to {SC}^N=S^N{C}^N$$
17	12 15 16	3eqtr4d	$$⊢\phi \to {SA}^N+{SB}^N={SC}^N$$