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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
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 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 ⊢ ( 𝜑 → ( 𝐴 ↑ 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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )