Metamath Proof Explorer

Theorem ruclem4

Description: Lemma for ruc . Initial value of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014)

Ref Expression
Hypotheses ruc.1 
|- ( ph -> F : NN --> RR )
ruc.2 
|- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )
ruc.4 
|- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )
ruc.5 
|- G = seq 0 ( D , C )
Assertion ruclem4 
|- ( ph -> ( G ` 0 ) = <. 0 , 1 >. )

Proof

Step Hyp Ref Expression
1 ruc.1 
 |-  ( ph -> F : NN --> RR )
2 ruc.2 
 |-  ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )
3 ruc.4 
 |-  C = ( { <. 0 , <. 0 , 1 >. >. } u. F )
4 ruc.5 
 |-  G = seq 0 ( D , C )
5 4 fveq1i 
 |-  ( G ` 0 ) = ( seq 0 ( D , C ) ` 0 )
6 0z 
 |-  0 e. ZZ
7 ffn 
 |-  ( F : NN --> RR -> F Fn NN )
8 fnresdm 
 |-  ( F Fn NN -> ( F |` NN ) = F )
9 1 7 8 3syl 
 |-  ( ph -> ( F |` NN ) = F )
10 dfn2 
 |-  NN = ( NN0 \ { 0 } )
11 10 reseq2i 
 |-  ( F |` NN ) = ( F |` ( NN0 \ { 0 } ) )
12 9 11 eqtr3di 
 |-  ( ph -> F = ( F |` ( NN0 \ { 0 } ) ) )
13 12 uneq2d 
 |-  ( ph -> ( { <. 0 , <. 0 , 1 >. >. } u. F ) = ( { <. 0 , <. 0 , 1 >. >. } u. ( F |` ( NN0 \ { 0 } ) ) ) )
14 3 13 eqtrid 
 |-  ( ph -> C = ( { <. 0 , <. 0 , 1 >. >. } u. ( F |` ( NN0 \ { 0 } ) ) ) )
15 14 fveq1d 
 |-  ( ph -> ( C ` 0 ) = ( ( { <. 0 , <. 0 , 1 >. >. } u. ( F |` ( NN0 \ { 0 } ) ) ) ` 0 ) )
16 c0ex 
 |-  0 e. _V
17 16 a1i 
 |-  ( T. -> 0 e. _V )
18 opex 
 |-  <. 0 , 1 >. e. _V
19 18 a1i 
 |-  ( T. -> <. 0 , 1 >. e. _V )
20 eqid 
 |-  ( { <. 0 , <. 0 , 1 >. >. } u. ( F |` ( NN0 \ { 0 } ) ) ) = ( { <. 0 , <. 0 , 1 >. >. } u. ( F |` ( NN0 \ { 0 } ) ) )
21 17 19 20 fvsnun1 
 |-  ( T. -> ( ( { <. 0 , <. 0 , 1 >. >. } u. ( F |` ( NN0 \ { 0 } ) ) ) ` 0 ) = <. 0 , 1 >. )
22 21 mptru 
 |-  ( ( { <. 0 , <. 0 , 1 >. >. } u. ( F |` ( NN0 \ { 0 } ) ) ) ` 0 ) = <. 0 , 1 >.
23 15 22 eqtrdi 
 |-  ( ph -> ( C ` 0 ) = <. 0 , 1 >. )
24 6 23 seq1i 
 |-  ( ph -> ( seq 0 ( D , C ) ` 0 ) = <. 0 , 1 >. )
25 5 24 eqtrid 
 |-  ( ph -> ( G ` 0 ) = <. 0 , 1 >. )