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 ) )