Metamath Proof Explorer

Theorem ruclem11

Description: Lemma for ruc . Closure lemmas for supremum. (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 ruclem11 
|- ( ph -> ( ran ( 1st o. G ) C_ RR /\ ran ( 1st o. G ) =/= (/) /\ A. z e. ran ( 1st o. G ) z <_ 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 1 2 3 4 ruclem6 
 |-  ( ph -> G : NN0 --> ( RR X. RR ) )
6 1stcof 
 |-  ( G : NN0 --> ( RR X. RR ) -> ( 1st o. G ) : NN0 --> RR )
7 5 6 syl 
 |-  ( ph -> ( 1st o. G ) : NN0 --> RR )
8 7 frnd 
 |-  ( ph -> ran ( 1st o. G ) C_ RR )
9 7 fdmd 
 |-  ( ph -> dom ( 1st o. G ) = NN0 )
10 0nn0 
 |-  0 e. NN0
11 ne0i 
 |-  ( 0 e. NN0 -> NN0 =/= (/) )
12 10 11 mp1i 
 |-  ( ph -> NN0 =/= (/) )
13 9 12 eqnetrd 
 |-  ( ph -> dom ( 1st o. G ) =/= (/) )
14 dm0rn0 
 |-  ( dom ( 1st o. G ) = (/) <-> ran ( 1st o. G ) = (/) )
15 14 necon3bii 
 |-  ( dom ( 1st o. G ) =/= (/) <-> ran ( 1st o. G ) =/= (/) )
16 13 15 sylib 
 |-  ( ph -> ran ( 1st o. G ) =/= (/) )
17 fvco3 
 |-  ( ( G : NN0 --> ( RR X. RR ) /\ n e. NN0 ) -> ( ( 1st o. G ) ` n ) = ( 1st ` ( G ` n ) ) )
18 5 17 sylan 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( 1st o. G ) ` n ) = ( 1st ` ( G ` n ) ) )
19 1 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> F : NN --> RR )
20 2 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> 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 ) >. ) ) )
21 simpr 
 |-  ( ( ph /\ n e. NN0 ) -> n e. NN0 )
22 10 a1i 
 |-  ( ( ph /\ n e. NN0 ) -> 0 e. NN0 )
23 19 20 3 4 21 22 ruclem10 
 |-  ( ( ph /\ n e. NN0 ) -> ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` 0 ) ) )
24 1 2 3 4 ruclem4 
 |-  ( ph -> ( G ` 0 ) = <. 0 , 1 >. )
25 24 fveq2d 
 |-  ( ph -> ( 2nd ` ( G ` 0 ) ) = ( 2nd ` <. 0 , 1 >. ) )
26 c0ex 
 |-  0 e. _V
27 1ex 
 |-  1 e. _V
28 26 27 op2nd 
 |-  ( 2nd ` <. 0 , 1 >. ) = 1
29 25 28 eqtrdi 
 |-  ( ph -> ( 2nd ` ( G ` 0 ) ) = 1 )
30 29 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> ( 2nd ` ( G ` 0 ) ) = 1 )
31 23 30 breqtrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( 1st ` ( G ` n ) ) < 1 )
32 5 ffvelrnda 
 |-  ( ( ph /\ n e. NN0 ) -> ( G ` n ) e. ( RR X. RR ) )
33 xp1st 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( 1st ` ( G ` n ) ) e. RR )
34 32 33 syl 
 |-  ( ( ph /\ n e. NN0 ) -> ( 1st ` ( G ` n ) ) e. RR )
35 1re 
 |-  1 e. RR
36 ltle 
 |-  ( ( ( 1st ` ( G ` n ) ) e. RR /\ 1 e. RR ) -> ( ( 1st ` ( G ` n ) ) < 1 -> ( 1st ` ( G ` n ) ) <_ 1 ) )
37 34 35 36 sylancl 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( 1st ` ( G ` n ) ) < 1 -> ( 1st ` ( G ` n ) ) <_ 1 ) )
38 31 37 mpd 
 |-  ( ( ph /\ n e. NN0 ) -> ( 1st ` ( G ` n ) ) <_ 1 )
39 18 38 eqbrtrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( 1st o. G ) ` n ) <_ 1 )
40 39 ralrimiva 
 |-  ( ph -> A. n e. NN0 ( ( 1st o. G ) ` n ) <_ 1 )
41 7 ffnd 
 |-  ( ph -> ( 1st o. G ) Fn NN0 )
42 breq1 
 |-  ( z = ( ( 1st o. G ) ` n ) -> ( z <_ 1 <-> ( ( 1st o. G ) ` n ) <_ 1 ) )
43 42 ralrn 
 |-  ( ( 1st o. G ) Fn NN0 -> ( A. z e. ran ( 1st o. G ) z <_ 1 <-> A. n e. NN0 ( ( 1st o. G ) ` n ) <_ 1 ) )
44 41 43 syl 
 |-  ( ph -> ( A. z e. ran ( 1st o. G ) z <_ 1 <-> A. n e. NN0 ( ( 1st o. G ) ` n ) <_ 1 ) )
45 40 44 mpbird 
 |-  ( ph -> A. z e. ran ( 1st o. G ) z <_ 1 )
46 8 16 45 3jca 
 |-  ( ph -> ( ran ( 1st o. G ) C_ RR /\ ran ( 1st o. G ) =/= (/) /\ A. z e. ran ( 1st o. G ) z <_ 1 ) )