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	$⊢ φ \to S \in ℂ$
	fltdiv.0	$⊢ φ \to S \neq 0$
	fltdiv.a	$⊢ φ \to A \in ℂ$
	fltdiv.b	$⊢ φ \to B \in ℂ$
	fltdiv.c	$⊢ φ \to C \in ℂ$
	fltdiv.n	$⊢ φ \to N \in ℕ_{0}$
	fltdiv.1	$⊢ φ \to A^{N} + B^{N} = C^{N}$
Assertion	fltdiv	$⊢ φ \to {(\frac{A}{S})}^{N} + {(\frac{B}{S})}^{N} = {(\frac{C}{S})}^{N}$

Proof

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

Metamath Proof Explorer

Theorem fltdiv

Proof