Metamath Proof Explorer

Theorem ruclem8

Description: Lemma for ruc . The intervals of the G sequence are all nonempty. (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 ruclem8 
|- ( ( ph /\ N e. NN0 ) -> ( 1st ` ( G ` N ) ) < ( 2nd ` ( G ` N ) ) )

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 2fveq3 
 |-  ( k = 0 -> ( 1st ` ( G ` k ) ) = ( 1st ` ( G ` 0 ) ) )
6 2fveq3 
 |-  ( k = 0 -> ( 2nd ` ( G ` k ) ) = ( 2nd ` ( G ` 0 ) ) )
7 5 6 breq12d 
 |-  ( k = 0 -> ( ( 1st ` ( G ` k ) ) < ( 2nd ` ( G ` k ) ) <-> ( 1st ` ( G ` 0 ) ) < ( 2nd ` ( G ` 0 ) ) ) )
8 7 imbi2d 
 |-  ( k = 0 -> ( ( ph -> ( 1st ` ( G ` k ) ) < ( 2nd ` ( G ` k ) ) ) <-> ( ph -> ( 1st ` ( G ` 0 ) ) < ( 2nd ` ( G ` 0 ) ) ) ) )
9 2fveq3 
 |-  ( k = n -> ( 1st ` ( G ` k ) ) = ( 1st ` ( G ` n ) ) )
10 2fveq3 
 |-  ( k = n -> ( 2nd ` ( G ` k ) ) = ( 2nd ` ( G ` n ) ) )
11 9 10 breq12d 
 |-  ( k = n -> ( ( 1st ` ( G ` k ) ) < ( 2nd ` ( G ` k ) ) <-> ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) )
12 11 imbi2d 
 |-  ( k = n -> ( ( ph -> ( 1st ` ( G ` k ) ) < ( 2nd ` ( G ` k ) ) ) <-> ( ph -> ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) )
13 2fveq3 
 |-  ( k = ( n + 1 ) -> ( 1st ` ( G ` k ) ) = ( 1st ` ( G ` ( n + 1 ) ) ) )
14 2fveq3 
 |-  ( k = ( n + 1 ) -> ( 2nd ` ( G ` k ) ) = ( 2nd ` ( G ` ( n + 1 ) ) ) )
15 13 14 breq12d 
 |-  ( k = ( n + 1 ) -> ( ( 1st ` ( G ` k ) ) < ( 2nd ` ( G ` k ) ) <-> ( 1st ` ( G ` ( n + 1 ) ) ) < ( 2nd ` ( G ` ( n + 1 ) ) ) ) )
16 15 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( ph -> ( 1st ` ( G ` k ) ) < ( 2nd ` ( G ` k ) ) ) <-> ( ph -> ( 1st ` ( G ` ( n + 1 ) ) ) < ( 2nd ` ( G ` ( n + 1 ) ) ) ) ) )
17 2fveq3 
 |-  ( k = N -> ( 1st ` ( G ` k ) ) = ( 1st ` ( G ` N ) ) )
18 2fveq3 
 |-  ( k = N -> ( 2nd ` ( G ` k ) ) = ( 2nd ` ( G ` N ) ) )
19 17 18 breq12d 
 |-  ( k = N -> ( ( 1st ` ( G ` k ) ) < ( 2nd ` ( G ` k ) ) <-> ( 1st ` ( G ` N ) ) < ( 2nd ` ( G ` N ) ) ) )
20 19 imbi2d 
 |-  ( k = N -> ( ( ph -> ( 1st ` ( G ` k ) ) < ( 2nd ` ( G ` k ) ) ) <-> ( ph -> ( 1st ` ( G ` N ) ) < ( 2nd ` ( G ` N ) ) ) ) )
21 0lt1 
 |-  0 < 1
22 21 a1i 
 |-  ( ph -> 0 < 1 )
23 1 2 3 4 ruclem4 
 |-  ( ph -> ( G ` 0 ) = <. 0 , 1 >. )
24 23 fveq2d 
 |-  ( ph -> ( 1st ` ( G ` 0 ) ) = ( 1st ` <. 0 , 1 >. ) )
25 c0ex 
 |-  0 e. _V
26 1ex 
 |-  1 e. _V
27 25 26 op1st 
 |-  ( 1st ` <. 0 , 1 >. ) = 0
28 24 27 eqtrdi 
 |-  ( ph -> ( 1st ` ( G ` 0 ) ) = 0 )
29 23 fveq2d 
 |-  ( ph -> ( 2nd ` ( G ` 0 ) ) = ( 2nd ` <. 0 , 1 >. ) )
30 25 26 op2nd 
 |-  ( 2nd ` <. 0 , 1 >. ) = 1
31 29 30 eqtrdi 
 |-  ( ph -> ( 2nd ` ( G ` 0 ) ) = 1 )
32 22 28 31 3brtr4d 
 |-  ( ph -> ( 1st ` ( G ` 0 ) ) < ( 2nd ` ( G ` 0 ) ) )
33 1 adantr 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> F : NN --> RR )
34 2 adantr 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> 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 ) >. ) ) )
35 1 2 3 4 ruclem6 
 |-  ( ph -> G : NN0 --> ( RR X. RR ) )
36 35 ffvelrnda 
 |-  ( ( ph /\ n e. NN0 ) -> ( G ` n ) e. ( RR X. RR ) )
37 36 adantrr 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( G ` n ) e. ( RR X. RR ) )
38 xp1st 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( 1st ` ( G ` n ) ) e. RR )
39 37 38 syl 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( 1st ` ( G ` n ) ) e. RR )
40 xp2nd 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( 2nd ` ( G ` n ) ) e. RR )
41 37 40 syl 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( 2nd ` ( G ` n ) ) e. RR )
42 nn0p1nn 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN )
43 ffvelrn 
 |-  ( ( F : NN --> RR /\ ( n + 1 ) e. NN ) -> ( F ` ( n + 1 ) ) e. RR )
44 1 42 43 syl2an 
 |-  ( ( ph /\ n e. NN0 ) -> ( F ` ( n + 1 ) ) e. RR )
45 44 adantrr 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( F ` ( n + 1 ) ) e. RR )
46 eqid 
 |-  ( 1st ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) = ( 1st ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) )
47 eqid 
 |-  ( 2nd ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) = ( 2nd ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) )
48 simprr 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) )
49 33 34 39 41 45 46 47 48 ruclem2 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( ( 1st ` ( G ` n ) ) <_ ( 1st ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) /\ ( 1st ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) < ( 2nd ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) /\ ( 2nd ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) <_ ( 2nd ` ( G ` n ) ) ) )
50 49 simp2d 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( 1st ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) < ( 2nd ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) )
51 1 2 3 4 ruclem7 
 |-  ( ( ph /\ n e. NN0 ) -> ( G ` ( n + 1 ) ) = ( ( G ` n ) D ( F ` ( n + 1 ) ) ) )
52 51 adantrr 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( G ` ( n + 1 ) ) = ( ( G ` n ) D ( F ` ( n + 1 ) ) ) )
53 1st2nd2 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( G ` n ) = <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. )
54 37 53 syl 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( G ` n ) = <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. )
55 54 oveq1d 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( ( G ` n ) D ( F ` ( n + 1 ) ) ) = ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) )
56 52 55 eqtrd 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( G ` ( n + 1 ) ) = ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) )
57 56 fveq2d 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( 1st ` ( G ` ( n + 1 ) ) ) = ( 1st ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) )
58 56 fveq2d 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( 2nd ` ( G ` ( n + 1 ) ) ) = ( 2nd ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) )
59 50 57 58 3brtr4d 
 |-  ( ( ph /\ ( n e. NN0 /\ ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) ) -> ( 1st ` ( G ` ( n + 1 ) ) ) < ( 2nd ` ( G ` ( n + 1 ) ) ) )
60 59 expr 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) -> ( 1st ` ( G ` ( n + 1 ) ) ) < ( 2nd ` ( G ` ( n + 1 ) ) ) ) )
61 60 expcom 
 |-  ( n e. NN0 -> ( ph -> ( ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) -> ( 1st ` ( G ` ( n + 1 ) ) ) < ( 2nd ` ( G ` ( n + 1 ) ) ) ) ) )
62 61 a2d 
 |-  ( n e. NN0 -> ( ( ph -> ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) ) -> ( ph -> ( 1st ` ( G ` ( n + 1 ) ) ) < ( 2nd ` ( G ` ( n + 1 ) ) ) ) ) )
63 8 12 16 20 32 62 nn0ind 
 |-  ( N e. NN0 -> ( ph -> ( 1st ` ( G ` N ) ) < ( 2nd ` ( G ` N ) ) ) )
64 63 impcom 
 |-  ( ( ph /\ N e. NN0 ) -> ( 1st ` ( G ` N ) ) < ( 2nd ` ( G ` N ) ) )