Theorem flt0

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

	Ref	Expression
Hypotheses	flt0.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	flt0.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	flt0.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	flt0.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	flt0.1	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
Assertion	flt0	⊢ ( 𝜑 → 𝑁 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		flt0.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		flt0.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		flt0.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		flt0.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		flt0.1	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
6		1p1e2	⊢ ( 1 + 1 ) = 2
7		1ne2	⊢ 1 ≠ 2
8	7	necomi	⊢ 2 ≠ 1
9	6 8	eqnetri	⊢ ( 1 + 1 ) ≠ 1
10	9	a1i	⊢ ( 𝜑 → ( 1 + 1 ) ≠ 1 )
11	1	exp0d	⊢ ( 𝜑 → ( 𝐴 ↑ 0 ) = 1 )
12	2	exp0d	⊢ ( 𝜑 → ( 𝐵 ↑ 0 ) = 1 )
13	11 12	oveq12d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 0 ) + ( 𝐵 ↑ 0 ) ) = ( 1 + 1 ) )
14	3	exp0d	⊢ ( 𝜑 → ( 𝐶 ↑ 0 ) = 1 )
15	10 13 14	3netr4d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 0 ) + ( 𝐵 ↑ 0 ) ) ≠ ( 𝐶 ↑ 0 ) )
16		oveq2	⊢ ( 𝑁 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 𝐴 ↑ 0 ) )
17		oveq2	⊢ ( 𝑁 = 0 → ( 𝐵 ↑ 𝑁 ) = ( 𝐵 ↑ 0 ) )
18	16 17	oveq12d	⊢ ( 𝑁 = 0 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 0 ) + ( 𝐵 ↑ 0 ) ) )
19		oveq2	⊢ ( 𝑁 = 0 → ( 𝐶 ↑ 𝑁 ) = ( 𝐶 ↑ 0 ) )
20	18 19	eqeq12d	⊢ ( 𝑁 = 0 → ( ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) ↔ ( ( 𝐴 ↑ 0 ) + ( 𝐵 ↑ 0 ) ) = ( 𝐶 ↑ 0 ) ) )
21	5 20	syl5ibcom	⊢ ( 𝜑 → ( 𝑁 = 0 → ( ( 𝐴 ↑ 0 ) + ( 𝐵 ↑ 0 ) ) = ( 𝐶 ↑ 0 ) ) )
22	21	imp	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 0 ) + ( 𝐵 ↑ 0 ) ) = ( 𝐶 ↑ 0 ) )
23	15 22	mteqand	⊢ ( 𝜑 → 𝑁 ≠ 0 )
24		elnnne0	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
25	4 23 24	sylanbrc	⊢ ( 𝜑 → 𝑁 ∈ ℕ )