This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flt0

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

Ref Expression
Hypotheses flt0.a ⊢ φ → A ∈ ℂ
flt0.b ⊢ φ → B ∈ ℂ
flt0.c ⊢ φ → C ∈ ℂ
flt0.n ⊢ φ → N ∈ ℕ 0
flt0.1 ⊢ φ → A N + B N = C N
Assertion flt0 ⊢ φ → N ∈ ℕ

Proof

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