Metamath Proof Explorer

Theorem ruclem6

Description: Lemma for ruc . Domain and range 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 ruclem6 
|- ( ph -> G : NN0 --> ( RR X. RR ) )

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 seq1 
 |-  ( 0 e. ZZ -> ( seq 0 ( D , C ) ` 0 ) = ( C ` 0 ) )
8 6 7 ax-mp 
 |-  ( seq 0 ( D , C ) ` 0 ) = ( C ` 0 )
9 5 8 eqtri 
 |-  ( G ` 0 ) = ( C ` 0 )
10 1 2 3 4 ruclem4 
 |-  ( ph -> ( G ` 0 ) = <. 0 , 1 >. )
11 9 10 eqtr3id 
 |-  ( ph -> ( C ` 0 ) = <. 0 , 1 >. )
12 0re 
 |-  0 e. RR
13 1re 
 |-  1 e. RR
14 opelxpi 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> <. 0 , 1 >. e. ( RR X. RR ) )
15 12 13 14 mp2an 
 |-  <. 0 , 1 >. e. ( RR X. RR )
16 11 15 eqeltrdi 
 |-  ( ph -> ( C ` 0 ) e. ( RR X. RR ) )
17 1st2nd2 
 |-  ( z e. ( RR X. RR ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
18 17 ad2antrl 
 |-  ( ( ph /\ ( z e. ( RR X. RR ) /\ w e. RR ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
19 18 oveq1d 
 |-  ( ( ph /\ ( z e. ( RR X. RR ) /\ w e. RR ) ) -> ( z D w ) = ( <. ( 1st ` z ) , ( 2nd ` z ) >. D w ) )
20 1 adantr 
 |-  ( ( ph /\ ( z e. ( RR X. RR ) /\ w e. RR ) ) -> F : NN --> RR )
21 2 adantr 
 |-  ( ( ph /\ ( z e. ( RR X. RR ) /\ w e. RR ) ) -> 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 ) >. ) ) )
22 xp1st 
 |-  ( z e. ( RR X. RR ) -> ( 1st ` z ) e. RR )
23 22 ad2antrl 
 |-  ( ( ph /\ ( z e. ( RR X. RR ) /\ w e. RR ) ) -> ( 1st ` z ) e. RR )
24 xp2nd 
 |-  ( z e. ( RR X. RR ) -> ( 2nd ` z ) e. RR )
25 24 ad2antrl 
 |-  ( ( ph /\ ( z e. ( RR X. RR ) /\ w e. RR ) ) -> ( 2nd ` z ) e. RR )
26 simprr 
 |-  ( ( ph /\ ( z e. ( RR X. RR ) /\ w e. RR ) ) -> w e. RR )
27 eqid 
 |-  ( 1st ` ( <. ( 1st ` z ) , ( 2nd ` z ) >. D w ) ) = ( 1st ` ( <. ( 1st ` z ) , ( 2nd ` z ) >. D w ) )
28 eqid 
 |-  ( 2nd ` ( <. ( 1st ` z ) , ( 2nd ` z ) >. D w ) ) = ( 2nd ` ( <. ( 1st ` z ) , ( 2nd ` z ) >. D w ) )
29 20 21 23 25 26 27 28 ruclem1 
 |-  ( ( ph /\ ( z e. ( RR X. RR ) /\ w e. RR ) ) -> ( ( <. ( 1st ` z ) , ( 2nd ` z ) >. D w ) e. ( RR X. RR ) /\ ( 1st ` ( <. ( 1st ` z ) , ( 2nd ` z ) >. D w ) ) = if ( ( ( ( 1st ` z ) + ( 2nd ` z ) ) / 2 ) < w , ( 1st ` z ) , ( ( ( ( ( 1st ` z ) + ( 2nd ` z ) ) / 2 ) + ( 2nd ` z ) ) / 2 ) ) /\ ( 2nd ` ( <. ( 1st ` z ) , ( 2nd ` z ) >. D w ) ) = if ( ( ( ( 1st ` z ) + ( 2nd ` z ) ) / 2 ) < w , ( ( ( 1st ` z ) + ( 2nd ` z ) ) / 2 ) , ( 2nd ` z ) ) ) )
30 29 simp1d 
 |-  ( ( ph /\ ( z e. ( RR X. RR ) /\ w e. RR ) ) -> ( <. ( 1st ` z ) , ( 2nd ` z ) >. D w ) e. ( RR X. RR ) )
31 19 30 eqeltrd 
 |-  ( ( ph /\ ( z e. ( RR X. RR ) /\ w e. RR ) ) -> ( z D w ) e. ( RR X. RR ) )
32 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
33 0zd 
 |-  ( ph -> 0 e. ZZ )
34 0p1e1 
 |-  ( 0 + 1 ) = 1
35 34 fveq2i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
36 nnuz 
 |-  NN = ( ZZ>= ` 1 )
37 35 36 eqtr4i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = NN
38 37 eleq2i 
 |-  ( z e. ( ZZ>= ` ( 0 + 1 ) ) <-> z e. NN )
39 3 equncomi 
 |-  C = ( F u. { <. 0 , <. 0 , 1 >. >. } )
40 39 fveq1i 
 |-  ( C ` z ) = ( ( F u. { <. 0 , <. 0 , 1 >. >. } ) ` z )
41 nnne0 
 |-  ( z e. NN -> z =/= 0 )
42 41 necomd 
 |-  ( z e. NN -> 0 =/= z )
43 fvunsn 
 |-  ( 0 =/= z -> ( ( F u. { <. 0 , <. 0 , 1 >. >. } ) ` z ) = ( F ` z ) )
44 42 43 syl 
 |-  ( z e. NN -> ( ( F u. { <. 0 , <. 0 , 1 >. >. } ) ` z ) = ( F ` z ) )
45 40 44 syl5eq 
 |-  ( z e. NN -> ( C ` z ) = ( F ` z ) )
46 45 adantl 
 |-  ( ( ph /\ z e. NN ) -> ( C ` z ) = ( F ` z ) )
47 1 ffvelrnda 
 |-  ( ( ph /\ z e. NN ) -> ( F ` z ) e. RR )
48 46 47 eqeltrd 
 |-  ( ( ph /\ z e. NN ) -> ( C ` z ) e. RR )
49 38 48 sylan2b 
 |-  ( ( ph /\ z e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( C ` z ) e. RR )
50 16 31 32 33 49 seqf2 
 |-  ( ph -> seq 0 ( D , C ) : NN0 --> ( RR X. RR ) )
51 4 feq1i 
 |-  ( G : NN0 --> ( RR X. RR ) <-> seq 0 ( D , C ) : NN0 --> ( RR X. RR ) )
52 50 51 sylibr 
 |-  ( ph -> G : NN0 --> ( RR X. RR ) )