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 , so the label is more about the context in which this theorem is used). (Contributed by SN, 20-Aug-2024)

	Ref	Expression
Hypotheses	fltmul.s	$⊢ φ \to S \in ℂ$
	fltmul.a	$⊢ φ \to A \in ℂ$
	fltmul.b	$⊢ φ \to B \in ℂ$
	fltmul.c	$⊢ φ \to C \in ℂ$
	fltmul.n	$⊢ φ \to N \in ℕ_{0}$
	fltmul.1	$⊢ φ \to A^{N} + B^{N} = C^{N}$
Assertion	fltmul	$⊢ φ \to {S A}^{N} + {S B}^{N} = {S C}^{N}$

Proof

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

Metamath Proof Explorer

Theorem fltmul

Proof