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 
|- ( ph -> A C_ NN0 )
sadval.b 
|- ( ph -> B C_ NN0 )
sadval.c 
|- C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
Assertion sadc0 
|- ( ph -> -. (/) e. ( C ` 0 ) )

Proof

Step Hyp Ref Expression
1 sadval.a 
 |-  ( ph -> A C_ NN0 )
2 sadval.b 
 |-  ( ph -> B C_ NN0 )
3 sadval.c 
 |-  C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
4 noel 
 |-  -. (/) e. (/)
5 3 fveq1i 
 |-  ( C ` 0 ) = ( seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 )
6 0z 
 |-  0 e. ZZ
7 seq1 
 |-  ( 0 e. ZZ -> ( seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) = ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) )
8 6 7 ax-mp 
 |-  ( seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) = ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 )
9 0nn0 
 |-  0 e. NN0
10 iftrue 
 |-  ( n = 0 -> if ( n = 0 , (/) , ( n - 1 ) ) = (/) )
11 eqid 
 |-  ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) = ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) )
12 0ex 
 |-  (/) e. _V
13 10 11 12 fvmpt 
 |-  ( 0 e. NN0 -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) = (/) )
14 9 13 ax-mp 
 |-  ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) = (/)
15 5 8 14 3eqtri 
 |-  ( C ` 0 ) = (/)
16 15 eleq2i 
 |-  ( (/) e. ( C ` 0 ) <-> (/) e. (/) )
17 4 16 mtbir 
 |-  -. (/) e. ( C ` 0 )
18 17 a1i 
 |-  ( ph -> -. (/) e. ( C ` 0 ) )