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=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=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=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
4 noel ⊢¬∅∈∅
5 3 fveq1i ⊢C⁡0=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡0
6 0z ⊢0∈ℤ
7 seq1 ⊢0∈ℤ→seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡0=n∈ℕ0⟼ifn=0∅n−1⁡0
8 6 7 ax-mp ⊢seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡0=n∈ℕ0⟼ifn=0∅n−1⁡0
9 0nn0 ⊢0∈ℕ0
10 iftrue ⊢n=0→ifn=0∅n−1=∅
11 eqid ⊢n∈ℕ0⟼ifn=0∅n−1=n∈ℕ0⟼ifn=0∅n−1
12 0ex ⊢∅∈V
13 10 11 12 fvmpt ⊢0∈ℕ0→n∈ℕ0⟼ifn=0∅n−1⁡0=∅
14 9 13 ax-mp ⊢n∈ℕ0⟼ifn=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