Metamath Proof Explorer

Theorem ruclem7

Description: Lemma for ruc . Successor value for 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 ruclem7 
|- ( ( ph /\ N e. NN0 ) -> ( G ` ( N + 1 ) ) = ( ( G ` N ) D ( F ` ( N + 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 simpr 
 |-  ( ( ph /\ N e. NN0 ) -> N e. NN0 )
6 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
7 5 6 eleqtrdi 
 |-  ( ( ph /\ N e. NN0 ) -> N e. ( ZZ>= ` 0 ) )
8 seqp1 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( seq 0 ( D , C ) ` ( N + 1 ) ) = ( ( seq 0 ( D , C ) ` N ) D ( C ` ( N + 1 ) ) ) )
9 7 8 syl 
 |-  ( ( ph /\ N e. NN0 ) -> ( seq 0 ( D , C ) ` ( N + 1 ) ) = ( ( seq 0 ( D , C ) ` N ) D ( C ` ( N + 1 ) ) ) )
10 4 fveq1i 
 |-  ( G ` ( N + 1 ) ) = ( seq 0 ( D , C ) ` ( N + 1 ) )
11 4 fveq1i 
 |-  ( G ` N ) = ( seq 0 ( D , C ) ` N )
12 11 oveq1i 
 |-  ( ( G ` N ) D ( C ` ( N + 1 ) ) ) = ( ( seq 0 ( D , C ) ` N ) D ( C ` ( N + 1 ) ) )
13 9 10 12 3eqtr4g 
 |-  ( ( ph /\ N e. NN0 ) -> ( G ` ( N + 1 ) ) = ( ( G ` N ) D ( C ` ( N + 1 ) ) ) )
14 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
15 14 adantl 
 |-  ( ( ph /\ N e. NN0 ) -> ( N + 1 ) e. NN )
16 15 nnne0d 
 |-  ( ( ph /\ N e. NN0 ) -> ( N + 1 ) =/= 0 )
17 16 necomd 
 |-  ( ( ph /\ N e. NN0 ) -> 0 =/= ( N + 1 ) )
18 3 equncomi 
 |-  C = ( F u. { <. 0 , <. 0 , 1 >. >. } )
19 18 fveq1i 
 |-  ( C ` ( N + 1 ) ) = ( ( F u. { <. 0 , <. 0 , 1 >. >. } ) ` ( N + 1 ) )
20 fvunsn 
 |-  ( 0 =/= ( N + 1 ) -> ( ( F u. { <. 0 , <. 0 , 1 >. >. } ) ` ( N + 1 ) ) = ( F ` ( N + 1 ) ) )
21 19 20 syl5eq 
 |-  ( 0 =/= ( N + 1 ) -> ( C ` ( N + 1 ) ) = ( F ` ( N + 1 ) ) )
22 17 21 syl 
 |-  ( ( ph /\ N e. NN0 ) -> ( C ` ( N + 1 ) ) = ( F ` ( N + 1 ) ) )
23 22 oveq2d 
 |-  ( ( ph /\ N e. NN0 ) -> ( ( G ` N ) D ( C ` ( N + 1 ) ) ) = ( ( G ` N ) D ( F ` ( N + 1 ) ) ) )
24 13 23 eqtrd 
 |-  ( ( ph /\ N e. NN0 ) -> ( G ` ( N + 1 ) ) = ( ( G ` N ) D ( F ` ( N + 1 ) ) ) )