Metamath Proof Explorer

Theorem sadc0

Description: The initial element of the carry sequence is F. . (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Hypotheses sadval.a ⊢ φ → A ⊆ ℕ 0
sadval.b ⊢ φ → B ⊆ ℕ 0
sadval.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
Assertion sadc0 ⊢ φ → ¬ ∅ ∈ C ⁡ 0

Proof

Step Hyp Ref Expression
1 sadval.a ⊢ φ → A ⊆ ℕ 0
2 sadval.b ⊢ φ → B ⊆ ℕ 0
3 sadval.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
4 noel ⊢ ¬ ∅ ∈ ∅
5 3 fveq1i ⊢ C ⁡ 0 = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
6 0z ⊢ 0 ∈ ℤ
7 seq1 ⊢ 0 ∈ ℤ → seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 = n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
8 6 7 ax-mp ⊢ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 = n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
9 0nn0 ⊢ 0 ∈ ℕ 0
10 iftrue ⊢ n = 0 → if n = 0 ∅ n − 1 = ∅
11 eqid ⊢ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 = n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
12 0ex ⊢ ∅ ∈ V
13 10 11 12 fvmpt ⊢ 0 ∈ ℕ 0 → n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 = ∅
14 9 13 ax-mp ⊢ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 = ∅
15 5 8 14 3eqtri ⊢ C ⁡ 0 = ∅
16 15 eleq2i ⊢ ∅ ∈ C ⁡ 0 ↔ ∅ ∈ ∅
17 4 16 mtbir ⊢ ¬ ∅ ∈ C ⁡ 0
18 17 a1i ⊢ φ → ¬ ∅ ∈ C ⁡ 0