Metamath Proof Explorer

Theorem ruclem10

Description: Lemma for ruc . Every first component of the G sequence is less than every second component. That is, the sequences form a chain a_1 < a_2 < ... < b_2 < b_1, where a_i are the first components and b_i are the second components. (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 )
ruclem10.6 
|- ( ph -> M e. NN0 )
ruclem10.7 
|- ( ph -> N e. NN0 )
Assertion ruclem10 
|- ( ph -> ( 1st ` ( G ` M ) ) < ( 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 ruclem10.6 
 |-  ( ph -> M e. NN0 )
6 ruclem10.7 
 |-  ( ph -> N e. NN0 )
7 1 2 3 4 ruclem6 
 |-  ( ph -> G : NN0 --> ( RR X. RR ) )
8 7 5 ffvelcdmd 
 |-  ( ph -> ( G ` M ) e. ( RR X. RR ) )
9 xp1st 
 |-  ( ( G ` M ) e. ( RR X. RR ) -> ( 1st ` ( G ` M ) ) e. RR )
10 8 9 syl 
 |-  ( ph -> ( 1st ` ( G ` M ) ) e. RR )
11 6 5 ifcld 
 |-  ( ph -> if ( M <_ N , N , M ) e. NN0 )
12 7 11 ffvelcdmd 
 |-  ( ph -> ( G ` if ( M <_ N , N , M ) ) e. ( RR X. RR ) )
13 xp1st 
 |-  ( ( G ` if ( M <_ N , N , M ) ) e. ( RR X. RR ) -> ( 1st ` ( G ` if ( M <_ N , N , M ) ) ) e. RR )
14 12 13 syl 
 |-  ( ph -> ( 1st ` ( G ` if ( M <_ N , N , M ) ) ) e. RR )
15 7 6 ffvelcdmd 
 |-  ( ph -> ( G ` N ) e. ( RR X. RR ) )
16 xp2nd 
 |-  ( ( G ` N ) e. ( RR X. RR ) -> ( 2nd ` ( G ` N ) ) e. RR )
17 15 16 syl 
 |-  ( ph -> ( 2nd ` ( G ` N ) ) e. RR )
18 5 nn0red 
 |-  ( ph -> M e. RR )
19 6 nn0red 
 |-  ( ph -> N e. RR )
20 max1 
 |-  ( ( M e. RR /\ N e. RR ) -> M <_ if ( M <_ N , N , M ) )
21 18 19 20 syl2anc 
 |-  ( ph -> M <_ if ( M <_ N , N , M ) )
22 5 nn0zd 
 |-  ( ph -> M e. ZZ )
23 11 nn0zd 
 |-  ( ph -> if ( M <_ N , N , M ) e. ZZ )
24 eluz 
 |-  ( ( M e. ZZ /\ if ( M <_ N , N , M ) e. ZZ ) -> ( if ( M <_ N , N , M ) e. ( ZZ>= ` M ) <-> M <_ if ( M <_ N , N , M ) ) )
25 22 23 24 syl2anc 
 |-  ( ph -> ( if ( M <_ N , N , M ) e. ( ZZ>= ` M ) <-> M <_ if ( M <_ N , N , M ) ) )
26 21 25 mpbird 
 |-  ( ph -> if ( M <_ N , N , M ) e. ( ZZ>= ` M ) )
27 1 2 3 4 5 26 ruclem9 
 |-  ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` if ( M <_ N , N , M ) ) ) /\ ( 2nd ` ( G ` if ( M <_ N , N , M ) ) ) <_ ( 2nd ` ( G ` M ) ) ) )
28 27 simpld 
 |-  ( ph -> ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` if ( M <_ N , N , M ) ) ) )
29 xp2nd 
 |-  ( ( G ` if ( M <_ N , N , M ) ) e. ( RR X. RR ) -> ( 2nd ` ( G ` if ( M <_ N , N , M ) ) ) e. RR )
30 12 29 syl 
 |-  ( ph -> ( 2nd ` ( G ` if ( M <_ N , N , M ) ) ) e. RR )
31 1 2 3 4 ruclem8 
 |-  ( ( ph /\ if ( M <_ N , N , M ) e. NN0 ) -> ( 1st ` ( G ` if ( M <_ N , N , M ) ) ) < ( 2nd ` ( G ` if ( M <_ N , N , M ) ) ) )
32 11 31 mpdan 
 |-  ( ph -> ( 1st ` ( G ` if ( M <_ N , N , M ) ) ) < ( 2nd ` ( G ` if ( M <_ N , N , M ) ) ) )
33 max2 
 |-  ( ( M e. RR /\ N e. RR ) -> N <_ if ( M <_ N , N , M ) )
34 18 19 33 syl2anc 
 |-  ( ph -> N <_ if ( M <_ N , N , M ) )
35 6 nn0zd 
 |-  ( ph -> N e. ZZ )
36 eluz 
 |-  ( ( N e. ZZ /\ if ( M <_ N , N , M ) e. ZZ ) -> ( if ( M <_ N , N , M ) e. ( ZZ>= ` N ) <-> N <_ if ( M <_ N , N , M ) ) )
37 35 23 36 syl2anc 
 |-  ( ph -> ( if ( M <_ N , N , M ) e. ( ZZ>= ` N ) <-> N <_ if ( M <_ N , N , M ) ) )
38 34 37 mpbird 
 |-  ( ph -> if ( M <_ N , N , M ) e. ( ZZ>= ` N ) )
39 1 2 3 4 6 38 ruclem9 
 |-  ( ph -> ( ( 1st ` ( G ` N ) ) <_ ( 1st ` ( G ` if ( M <_ N , N , M ) ) ) /\ ( 2nd ` ( G ` if ( M <_ N , N , M ) ) ) <_ ( 2nd ` ( G ` N ) ) ) )
40 39 simprd 
 |-  ( ph -> ( 2nd ` ( G ` if ( M <_ N , N , M ) ) ) <_ ( 2nd ` ( G ` N ) ) )
41 14 30 17 32 40 ltletrd 
 |-  ( ph -> ( 1st ` ( G ` if ( M <_ N , N , M ) ) ) < ( 2nd ` ( G ` N ) ) )
42 10 14 17 28 41 lelttrd 
 |-  ( ph -> ( 1st ` ( G ` M ) ) < ( 2nd ` ( G ` N ) ) )