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 ( 𝜑𝐴 ⊆ ℕ0 )
sadval.b ( 𝜑𝐵 ⊆ ℕ0 )
sadval.c 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚𝐴 , 𝑚𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
Assertion sadc0 ( 𝜑 → ¬ ∅ ∈ ( 𝐶 ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 sadval.a ( 𝜑𝐴 ⊆ ℕ0 )
2 sadval.b ( 𝜑𝐵 ⊆ ℕ0 )
3 sadval.c 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚𝐴 , 𝑚𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4 noel ¬ ∅ ∈ ∅
5 3 fveq1i ( 𝐶 ‘ 0 ) = ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚𝐴 , 𝑚𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 )
6 0z 0 ∈ ℤ
7 seq1 ( 0 ∈ ℤ → ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚𝐴 , 𝑚𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) = ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) )
8 6 7 ax-mp ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚𝐴 , 𝑚𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) = ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 )
9 0nn0 0 ∈ ℕ0
10 iftrue ( 𝑛 = 0 → if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) = ∅ )
11 eqid ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) )
12 0ex ∅ ∈ V
13 10 11 12 fvmpt ( 0 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) = ∅ )
14 9 13 ax-mp ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) = ∅
15 5 8 14 3eqtri ( 𝐶 ‘ 0 ) = ∅
16 15 eleq2i ( ∅ ∈ ( 𝐶 ‘ 0 ) ↔ ∅ ∈ ∅ )
17 4 16 mtbir ¬ ∅ ∈ ( 𝐶 ‘ 0 )
18 17 a1i ( 𝜑 → ¬ ∅ ∈ ( 𝐶 ‘ 0 ) )