Theorem flt0

Description: A counterexample for FLT does not exist for N = 0 . (Contributed by SN, 20-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		flt0.a	$$⊢\phi \to A\in ℂ$$
2		flt0.b	$$⊢\phi \to B\in ℂ$$
3		flt0.c	$$⊢\phi \to C\in ℂ$$
4		flt0.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		flt0.1	$$⊢\phi \to A^N+B^N=C^N$$
6		1p1e2	$$⊢1+1=2$$
7		sn-1ne2	$$⊢1\ne 2$$
8	7	necomi	$$⊢2\ne 1$$
9	6 8	eqnetri	$$⊢1+1\ne 1$$
10	9	a1i	$$⊢\phi \to 1+1\ne 1$$
11	1	exp0d	$$⊢\phi \to A^0=1$$
12	2	exp0d	$$⊢\phi \to B^0=1$$
13	11 12	oveq12d	$$⊢\phi \to A^0+B^0=1+1$$
14	3	exp0d	$$⊢\phi \to C^0=1$$
15	10 13 14	3netr4d	$$⊢\phi \to A^0+B^0\ne C^0$$
16		oveq2	$$⊢N=0\to A^N=A^0$$
17		oveq2	$$⊢N=0\to B^N=B^0$$
18	16 17	oveq12d	$$⊢N=0\to A^N+B^N=A^0+B^0$$
19		oveq2	$$⊢N=0\to C^N=C^0$$
20	18 19	eqeq12d	$$⊢N=0\to \left(A^N+B^N=C^N\leftrightarrow A^0+B^0=C^0\right)$$
21	5 20	syl5ibcom	$$⊢\phi \to \left(N=0\to A^0+B^0=C^0\right)$$
22	21	imp	$$⊢\left(\phi \wedge N=0\right)\to A^0+B^0=C^0$$
23	15 22	mteqand	$$⊢\phi \to N\ne 0$$
24		elnnne0	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$
25	4 23 24	sylanbrc	$$⊢\phi \to N\in \mathbb{N}$$