This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ruclem12

Description: Lemma for ruc . The supremum of the increasing sequence 1st o. G is a real number that is not in the range of F . (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 )
ruc.6 
|- S = sup ( ran ( 1st o. G ) , RR , < )
Assertion ruclem12 
|- ( ph -> S e. ( RR \ ran F ) )

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 ruc.6 
 |-  S = sup ( ran ( 1st o. G ) , RR , < )
6 1 2 3 4 ruclem11 
 |-  ( ph -> ( ran ( 1st o. G ) C_ RR /\ ran ( 1st o. G ) =/= (/) /\ A. z e. ran ( 1st o. G ) z <_ 1 ) )
7 6 simp1d 
 |-  ( ph -> ran ( 1st o. G ) C_ RR )
8 6 simp2d 
 |-  ( ph -> ran ( 1st o. G ) =/= (/) )
9 1re 
 |-  1 e. RR
10 6 simp3d 
 |-  ( ph -> A. z e. ran ( 1st o. G ) z <_ 1 )
11 brralrspcev 
 |-  ( ( 1 e. RR /\ A. z e. ran ( 1st o. G ) z <_ 1 ) -> E. n e. RR A. z e. ran ( 1st o. G ) z <_ n )
12 9 10 11 sylancr 
 |-  ( ph -> E. n e. RR A. z e. ran ( 1st o. G ) z <_ n )
13 7 8 12 suprcld 
 |-  ( ph -> sup ( ran ( 1st o. G ) , RR , < ) e. RR )
14 5 13 eqeltrid 
 |-  ( ph -> S e. RR )
15 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> F : NN --> RR )
16 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> 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 ) >. ) ) )
17 1 2 3 4 ruclem6 
 |-  ( ph -> G : NN0 --> ( RR X. RR ) )
18 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
19 ffvelcdm 
 |-  ( ( G : NN0 --> ( RR X. RR ) /\ ( n - 1 ) e. NN0 ) -> ( G ` ( n - 1 ) ) e. ( RR X. RR ) )
20 17 18 19 syl2an 
 |-  ( ( ph /\ n e. NN ) -> ( G ` ( n - 1 ) ) e. ( RR X. RR ) )
21 xp1st 
 |-  ( ( G ` ( n - 1 ) ) e. ( RR X. RR ) -> ( 1st ` ( G ` ( n - 1 ) ) ) e. RR )
22 20 21 syl 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` ( n - 1 ) ) ) e. RR )
23 xp2nd 
 |-  ( ( G ` ( n - 1 ) ) e. ( RR X. RR ) -> ( 2nd ` ( G ` ( n - 1 ) ) ) e. RR )
24 20 23 syl 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` ( n - 1 ) ) ) e. RR )
25 1 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. RR )
26 eqid 
 |-  ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) = ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) )
27 eqid 
 |-  ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) = ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) )
28 1 2 3 4 ruclem8 
 |-  ( ( ph /\ ( n - 1 ) e. NN0 ) -> ( 1st ` ( G ` ( n - 1 ) ) ) < ( 2nd ` ( G ` ( n - 1 ) ) ) )
29 18 28 sylan2 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` ( n - 1 ) ) ) < ( 2nd ` ( G ` ( n - 1 ) ) ) )
30 15 16 22 24 25 26 27 29 ruclem3 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) < ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) \/ ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) < ( F ` n ) ) )
31 1 2 3 4 ruclem7 
 |-  ( ( ph /\ ( n - 1 ) e. NN0 ) -> ( G ` ( ( n - 1 ) + 1 ) ) = ( ( G ` ( n - 1 ) ) D ( F ` ( ( n - 1 ) + 1 ) ) ) )
32 18 31 sylan2 
 |-  ( ( ph /\ n e. NN ) -> ( G ` ( ( n - 1 ) + 1 ) ) = ( ( G ` ( n - 1 ) ) D ( F ` ( ( n - 1 ) + 1 ) ) ) )
33 nncn 
 |-  ( n e. NN -> n e. CC )
34 33 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. CC )
35 ax-1cn 
 |-  1 e. CC
36 npcan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) + 1 ) = n )
37 34 35 36 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( ( n - 1 ) + 1 ) = n )
38 37 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( G ` ( ( n - 1 ) + 1 ) ) = ( G ` n ) )
39 1st2nd2 
 |-  ( ( G ` ( n - 1 ) ) e. ( RR X. RR ) -> ( G ` ( n - 1 ) ) = <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. )
40 20 39 syl 
 |-  ( ( ph /\ n e. NN ) -> ( G ` ( n - 1 ) ) = <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. )
41 37 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( F ` ( ( n - 1 ) + 1 ) ) = ( F ` n ) )
42 40 41 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( G ` ( n - 1 ) ) D ( F ` ( ( n - 1 ) + 1 ) ) ) = ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) )
43 32 38 42 3eqtr3d 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) = ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) )
44 43 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) )
45 44 breq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) < ( 1st ` ( G ` n ) ) <-> ( F ` n ) < ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) ) )
46 43 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) )
47 46 breq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( 2nd ` ( G ` n ) ) < ( F ` n ) <-> ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) < ( F ` n ) ) )
48 45 47 orbi12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( F ` n ) < ( 1st ` ( G ` n ) ) \/ ( 2nd ` ( G ` n ) ) < ( F ` n ) ) <-> ( ( F ` n ) < ( 1st ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) \/ ( 2nd ` ( <. ( 1st ` ( G ` ( n - 1 ) ) ) , ( 2nd ` ( G ` ( n - 1 ) ) ) >. D ( F ` n ) ) ) < ( F ` n ) ) ) )
49 30 48 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) < ( 1st ` ( G ` n ) ) \/ ( 2nd ` ( G ` n ) ) < ( F ` n ) ) )
50 7 adantr 
 |-  ( ( ph /\ n e. NN ) -> ran ( 1st o. G ) C_ RR )
51 8 adantr 
 |-  ( ( ph /\ n e. NN ) -> ran ( 1st o. G ) =/= (/) )
52 12 adantr 
 |-  ( ( ph /\ n e. NN ) -> E. n e. RR A. z e. ran ( 1st o. G ) z <_ n )
53 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
54 fvco3 
 |-  ( ( G : NN0 --> ( RR X. RR ) /\ n e. NN0 ) -> ( ( 1st o. G ) ` n ) = ( 1st ` ( G ` n ) ) )
55 17 53 54 syl2an 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st o. G ) ` n ) = ( 1st ` ( G ` n ) ) )
56 17 adantr 
 |-  ( ( ph /\ n e. NN ) -> G : NN0 --> ( RR X. RR ) )
57 1stcof 
 |-  ( G : NN0 --> ( RR X. RR ) -> ( 1st o. G ) : NN0 --> RR )
58 ffn 
 |-  ( ( 1st o. G ) : NN0 --> RR -> ( 1st o. G ) Fn NN0 )
59 56 57 58 3syl 
 |-  ( ( ph /\ n e. NN ) -> ( 1st o. G ) Fn NN0 )
60 53 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. NN0 )
61 fnfvelrn 
 |-  ( ( ( 1st o. G ) Fn NN0 /\ n e. NN0 ) -> ( ( 1st o. G ) ` n ) e. ran ( 1st o. G ) )
62 59 60 61 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st o. G ) ` n ) e. ran ( 1st o. G ) )
63 55 62 eqeltrrd 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) e. ran ( 1st o. G ) )
64 50 51 52 63 suprubd 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) <_ sup ( ran ( 1st o. G ) , RR , < ) )
65 64 5 breqtrrdi 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) <_ S )
66 ffvelcdm 
 |-  ( ( G : NN0 --> ( RR X. RR ) /\ n e. NN0 ) -> ( G ` n ) e. ( RR X. RR ) )
67 17 53 66 syl2an 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. ( RR X. RR ) )
68 xp1st 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( 1st ` ( G ` n ) ) e. RR )
69 67 68 syl 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) e. RR )
70 14 adantr 
 |-  ( ( ph /\ n e. NN ) -> S e. RR )
71 ltletr 
 |-  ( ( ( F ` n ) e. RR /\ ( 1st ` ( G ` n ) ) e. RR /\ S e. RR ) -> ( ( ( F ` n ) < ( 1st ` ( G ` n ) ) /\ ( 1st ` ( G ` n ) ) <_ S ) -> ( F ` n ) < S ) )
72 25 69 70 71 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( F ` n ) < ( 1st ` ( G ` n ) ) /\ ( 1st ` ( G ` n ) ) <_ S ) -> ( F ` n ) < S ) )
73 65 72 mpan2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) < ( 1st ` ( G ` n ) ) -> ( F ` n ) < S ) )
74 fvco3 
 |-  ( ( G : NN0 --> ( RR X. RR ) /\ k e. NN0 ) -> ( ( 1st o. G ) ` k ) = ( 1st ` ( G ` k ) ) )
75 56 74 sylan 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( ( 1st o. G ) ` k ) = ( 1st ` ( G ` k ) ) )
76 56 ffvelcdmda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( G ` k ) e. ( RR X. RR ) )
77 xp1st 
 |-  ( ( G ` k ) e. ( RR X. RR ) -> ( 1st ` ( G ` k ) ) e. RR )
78 76 77 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( 1st ` ( G ` k ) ) e. RR )
79 xp2nd 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( 2nd ` ( G ` n ) ) e. RR )
80 67 79 syl 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) e. RR )
81 80 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( 2nd ` ( G ` n ) ) e. RR )
82 15 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> F : NN --> RR )
83 16 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ k 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 ) >. ) ) )
84 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> k e. NN0 )
85 60 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> n e. NN0 )
86 82 83 3 4 84 85 ruclem10 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( 1st ` ( G ` k ) ) < ( 2nd ` ( G ` n ) ) )
87 78 81 86 ltled 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( 1st ` ( G ` k ) ) <_ ( 2nd ` ( G ` n ) ) )
88 75 87 eqbrtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN0 ) -> ( ( 1st o. G ) ` k ) <_ ( 2nd ` ( G ` n ) ) )
89 88 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. k e. NN0 ( ( 1st o. G ) ` k ) <_ ( 2nd ` ( G ` n ) ) )
90 breq1 
 |-  ( z = ( ( 1st o. G ) ` k ) -> ( z <_ ( 2nd ` ( G ` n ) ) <-> ( ( 1st o. G ) ` k ) <_ ( 2nd ` ( G ` n ) ) ) )
91 90 ralrn 
 |-  ( ( 1st o. G ) Fn NN0 -> ( A. z e. ran ( 1st o. G ) z <_ ( 2nd ` ( G ` n ) ) <-> A. k e. NN0 ( ( 1st o. G ) ` k ) <_ ( 2nd ` ( G ` n ) ) ) )
92 59 91 syl 
 |-  ( ( ph /\ n e. NN ) -> ( A. z e. ran ( 1st o. G ) z <_ ( 2nd ` ( G ` n ) ) <-> A. k e. NN0 ( ( 1st o. G ) ` k ) <_ ( 2nd ` ( G ` n ) ) ) )
93 89 92 mpbird 
 |-  ( ( ph /\ n e. NN ) -> A. z e. ran ( 1st o. G ) z <_ ( 2nd ` ( G ` n ) ) )
94 suprleub 
 |-  ( ( ( ran ( 1st o. G ) C_ RR /\ ran ( 1st o. G ) =/= (/) /\ E. n e. RR A. z e. ran ( 1st o. G ) z <_ n ) /\ ( 2nd ` ( G ` n ) ) e. RR ) -> ( sup ( ran ( 1st o. G ) , RR , < ) <_ ( 2nd ` ( G ` n ) ) <-> A. z e. ran ( 1st o. G ) z <_ ( 2nd ` ( G ` n ) ) ) )
95 50 51 52 80 94 syl31anc 
 |-  ( ( ph /\ n e. NN ) -> ( sup ( ran ( 1st o. G ) , RR , < ) <_ ( 2nd ` ( G ` n ) ) <-> A. z e. ran ( 1st o. G ) z <_ ( 2nd ` ( G ` n ) ) ) )
96 93 95 mpbird 
 |-  ( ( ph /\ n e. NN ) -> sup ( ran ( 1st o. G ) , RR , < ) <_ ( 2nd ` ( G ` n ) ) )
97 5 96 eqbrtrid 
 |-  ( ( ph /\ n e. NN ) -> S <_ ( 2nd ` ( G ` n ) ) )
98 lelttr 
 |-  ( ( S e. RR /\ ( 2nd ` ( G ` n ) ) e. RR /\ ( F ` n ) e. RR ) -> ( ( S <_ ( 2nd ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) < ( F ` n ) ) -> S < ( F ` n ) ) )
99 70 80 25 98 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( S <_ ( 2nd ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) < ( F ` n ) ) -> S < ( F ` n ) ) )
100 97 99 mpand 
 |-  ( ( ph /\ n e. NN ) -> ( ( 2nd ` ( G ` n ) ) < ( F ` n ) -> S < ( F ` n ) ) )
101 73 100 orim12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( F ` n ) < ( 1st ` ( G ` n ) ) \/ ( 2nd ` ( G ` n ) ) < ( F ` n ) ) -> ( ( F ` n ) < S \/ S < ( F ` n ) ) ) )
102 49 101 mpd 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) < S \/ S < ( F ` n ) ) )
103 25 70 lttri2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) =/= S <-> ( ( F ` n ) < S \/ S < ( F ` n ) ) ) )
104 102 103 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) =/= S )
105 104 neneqd 
 |-  ( ( ph /\ n e. NN ) -> -. ( F ` n ) = S )
106 105 nrexdv 
 |-  ( ph -> -. E. n e. NN ( F ` n ) = S )
107 risset 
 |-  ( S e. ran F <-> E. z e. ran F z = S )
108 ffn 
 |-  ( F : NN --> RR -> F Fn NN )
109 eqeq1 
 |-  ( z = ( F ` n ) -> ( z = S <-> ( F ` n ) = S ) )
110 109 rexrn 
 |-  ( F Fn NN -> ( E. z e. ran F z = S <-> E. n e. NN ( F ` n ) = S ) )
111 1 108 110 3syl 
 |-  ( ph -> ( E. z e. ran F z = S <-> E. n e. NN ( F ` n ) = S ) )
112 107 111 bitrid 
 |-  ( ph -> ( S e. ran F <-> E. n e. NN ( F ` n ) = S ) )
113 106 112 mtbird 
 |-  ( ph -> -. S e. ran F )
114 14 113 eldifd 
 |-  ( ph -> S e. ( RR \ ran F ) )