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

Metamath Proof Explorer

Theorem ruclem9

Description: Lemma for ruc . The first components of the G sequence are increasing, and the second components are decreasing. (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 )
ruclem9.6 
|- ( ph -> M e. NN0 )
ruclem9.7 
|- ( ph -> N e. ( ZZ>= ` M ) )
Assertion ruclem9 
|- ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` N ) ) /\ ( 2nd ` ( G ` N ) ) <_ ( 2nd ` ( G ` M ) ) ) )

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 ruclem9.6 
 |-  ( ph -> M e. NN0 )
6 ruclem9.7 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
7 2fveq3 
 |-  ( k = M -> ( 1st ` ( G ` k ) ) = ( 1st ` ( G ` M ) ) )
8 7 breq2d 
 |-  ( k = M -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) <-> ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` M ) ) ) )
9 2fveq3 
 |-  ( k = M -> ( 2nd ` ( G ` k ) ) = ( 2nd ` ( G ` M ) ) )
10 9 breq1d 
 |-  ( k = M -> ( ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) <-> ( 2nd ` ( G ` M ) ) <_ ( 2nd ` ( G ` M ) ) ) )
11 8 10 anbi12d 
 |-  ( k = M -> ( ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) /\ ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) ) <-> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` M ) ) /\ ( 2nd ` ( G ` M ) ) <_ ( 2nd ` ( G ` M ) ) ) ) )
12 11 imbi2d 
 |-  ( k = M -> ( ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) /\ ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) ) ) <-> ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` M ) ) /\ ( 2nd ` ( G ` M ) ) <_ ( 2nd ` ( G ` M ) ) ) ) ) )
13 2fveq3 
 |-  ( k = n -> ( 1st ` ( G ` k ) ) = ( 1st ` ( G ` n ) ) )
14 13 breq2d 
 |-  ( k = n -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) <-> ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` n ) ) ) )
15 2fveq3 
 |-  ( k = n -> ( 2nd ` ( G ` k ) ) = ( 2nd ` ( G ` n ) ) )
16 15 breq1d 
 |-  ( k = n -> ( ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) <-> ( 2nd ` ( G ` n ) ) <_ ( 2nd ` ( G ` M ) ) ) )
17 14 16 anbi12d 
 |-  ( k = n -> ( ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) /\ ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) ) <-> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) <_ ( 2nd ` ( G ` M ) ) ) ) )
18 17 imbi2d 
 |-  ( k = n -> ( ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) /\ ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) ) ) <-> ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) <_ ( 2nd ` ( G ` M ) ) ) ) ) )
19 2fveq3 
 |-  ( k = ( n + 1 ) -> ( 1st ` ( G ` k ) ) = ( 1st ` ( G ` ( n + 1 ) ) ) )
20 19 breq2d 
 |-  ( k = ( n + 1 ) -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) <-> ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) ) )
21 2fveq3 
 |-  ( k = ( n + 1 ) -> ( 2nd ` ( G ` k ) ) = ( 2nd ` ( G ` ( n + 1 ) ) ) )
22 21 breq1d 
 |-  ( k = ( n + 1 ) -> ( ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) <-> ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` M ) ) ) )
23 20 22 anbi12d 
 |-  ( k = ( n + 1 ) -> ( ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) /\ ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) ) <-> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) /\ ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` M ) ) ) ) )
24 23 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) /\ ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) ) ) <-> ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) /\ ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` M ) ) ) ) ) )
25 2fveq3 
 |-  ( k = N -> ( 1st ` ( G ` k ) ) = ( 1st ` ( G ` N ) ) )
26 25 breq2d 
 |-  ( k = N -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) <-> ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` N ) ) ) )
27 2fveq3 
 |-  ( k = N -> ( 2nd ` ( G ` k ) ) = ( 2nd ` ( G ` N ) ) )
28 27 breq1d 
 |-  ( k = N -> ( ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) <-> ( 2nd ` ( G ` N ) ) <_ ( 2nd ` ( G ` M ) ) ) )
29 26 28 anbi12d 
 |-  ( k = N -> ( ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) /\ ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) ) <-> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` N ) ) /\ ( 2nd ` ( G ` N ) ) <_ ( 2nd ` ( G ` M ) ) ) ) )
30 29 imbi2d 
 |-  ( k = N -> ( ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` k ) ) /\ ( 2nd ` ( G ` k ) ) <_ ( 2nd ` ( G ` M ) ) ) ) <-> ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` N ) ) /\ ( 2nd ` ( G ` N ) ) <_ ( 2nd ` ( G ` M ) ) ) ) ) )
31 1 2 3 4 ruclem6 
 |-  ( ph -> G : NN0 --> ( RR X. RR ) )
32 31 5 ffvelcdmd 
 |-  ( ph -> ( G ` M ) e. ( RR X. RR ) )
33 xp1st 
 |-  ( ( G ` M ) e. ( RR X. RR ) -> ( 1st ` ( G ` M ) ) e. RR )
34 32 33 syl 
 |-  ( ph -> ( 1st ` ( G ` M ) ) e. RR )
35 34 leidd 
 |-  ( ph -> ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` M ) ) )
36 xp2nd 
 |-  ( ( G ` M ) e. ( RR X. RR ) -> ( 2nd ` ( G ` M ) ) e. RR )
37 32 36 syl 
 |-  ( ph -> ( 2nd ` ( G ` M ) ) e. RR )
38 37 leidd 
 |-  ( ph -> ( 2nd ` ( G ` M ) ) <_ ( 2nd ` ( G ` M ) ) )
39 35 38 jca 
 |-  ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` M ) ) /\ ( 2nd ` ( G ` M ) ) <_ ( 2nd ` ( G ` M ) ) ) )
40 1 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> F : NN --> RR )
41 2 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> 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 ) >. ) ) )
42 31 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> G : NN0 --> ( RR X. RR ) )
43 eluznn0 
 |-  ( ( M e. NN0 /\ n e. ( ZZ>= ` M ) ) -> n e. NN0 )
44 5 43 sylan 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> n e. NN0 )
45 42 44 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( G ` n ) e. ( RR X. RR ) )
46 xp1st 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( 1st ` ( G ` n ) ) e. RR )
47 45 46 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 1st ` ( G ` n ) ) e. RR )
48 xp2nd 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( 2nd ` ( G ` n ) ) e. RR )
49 45 48 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 2nd ` ( G ` n ) ) e. RR )
50 nn0p1nn 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN )
51 44 50 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( n + 1 ) e. NN )
52 40 51 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( F ` ( n + 1 ) ) e. RR )
53 eqid 
 |-  ( 1st ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) = ( 1st ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) )
54 eqid 
 |-  ( 2nd ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) = ( 2nd ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) )
55 1 2 3 4 ruclem8 
 |-  ( ( ph /\ n e. NN0 ) -> ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) )
56 44 55 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 1st ` ( G ` n ) ) < ( 2nd ` ( G ` n ) ) )
57 40 41 47 49 52 53 54 56 ruclem2 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( 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 ) ) ) )
58 57 simp1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 1st ` ( G ` n ) ) <_ ( 1st ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) )
59 1 2 3 4 ruclem7 
 |-  ( ( ph /\ n e. NN0 ) -> ( G ` ( n + 1 ) ) = ( ( G ` n ) D ( F ` ( n + 1 ) ) ) )
60 44 59 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( G ` ( n + 1 ) ) = ( ( G ` n ) D ( F ` ( n + 1 ) ) ) )
61 1st2nd2 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( G ` n ) = <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. )
62 45 61 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( G ` n ) = <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. )
63 62 oveq1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( G ` n ) D ( F ` ( n + 1 ) ) ) = ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) )
64 60 63 eqtrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( G ` ( n + 1 ) ) = ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) )
65 64 fveq2d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 1st ` ( G ` ( n + 1 ) ) ) = ( 1st ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) )
66 58 65 breqtrrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 1st ` ( G ` n ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) )
67 34 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 1st ` ( G ` M ) ) e. RR )
68 peano2nn0 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN0 )
69 44 68 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( n + 1 ) e. NN0 )
70 42 69 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( G ` ( n + 1 ) ) e. ( RR X. RR ) )
71 xp1st 
 |-  ( ( G ` ( n + 1 ) ) e. ( RR X. RR ) -> ( 1st ` ( G ` ( n + 1 ) ) ) e. RR )
72 70 71 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 1st ` ( G ` ( n + 1 ) ) ) e. RR )
73 letr 
 |-  ( ( ( 1st ` ( G ` M ) ) e. RR /\ ( 1st ` ( G ` n ) ) e. RR /\ ( 1st ` ( G ` ( n + 1 ) ) ) e. RR ) -> ( ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` n ) ) /\ ( 1st ` ( G ` n ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) ) -> ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) ) )
74 67 47 72 73 syl3anc 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` n ) ) /\ ( 1st ` ( G ` n ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) ) -> ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) ) )
75 66 74 mpan2d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` n ) ) -> ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) ) )
76 64 fveq2d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 2nd ` ( G ` ( n + 1 ) ) ) = ( 2nd ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) )
77 57 simp3d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 2nd ` ( <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. D ( F ` ( n + 1 ) ) ) ) <_ ( 2nd ` ( G ` n ) ) )
78 76 77 eqbrtrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` n ) ) )
79 xp2nd 
 |-  ( ( G ` ( n + 1 ) ) e. ( RR X. RR ) -> ( 2nd ` ( G ` ( n + 1 ) ) ) e. RR )
80 70 79 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 2nd ` ( G ` ( n + 1 ) ) ) e. RR )
81 37 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( 2nd ` ( G ` M ) ) e. RR )
82 letr 
 |-  ( ( ( 2nd ` ( G ` ( n + 1 ) ) ) e. RR /\ ( 2nd ` ( G ` n ) ) e. RR /\ ( 2nd ` ( G ` M ) ) e. RR ) -> ( ( ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) <_ ( 2nd ` ( G ` M ) ) ) -> ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` M ) ) ) )
83 80 49 81 82 syl3anc 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) <_ ( 2nd ` ( G ` M ) ) ) -> ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` M ) ) ) )
84 78 83 mpand 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( 2nd ` ( G ` n ) ) <_ ( 2nd ` ( G ` M ) ) -> ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` M ) ) ) )
85 75 84 anim12d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) <_ ( 2nd ` ( G ` M ) ) ) -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) /\ ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` M ) ) ) ) )
86 85 expcom 
 |-  ( n e. ( ZZ>= ` M ) -> ( ph -> ( ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) <_ ( 2nd ` ( G ` M ) ) ) -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) /\ ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` M ) ) ) ) ) )
87 86 a2d 
 |-  ( n e. ( ZZ>= ` M ) -> ( ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` n ) ) /\ ( 2nd ` ( G ` n ) ) <_ ( 2nd ` ( G ` M ) ) ) ) -> ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` ( n + 1 ) ) ) /\ ( 2nd ` ( G ` ( n + 1 ) ) ) <_ ( 2nd ` ( G ` M ) ) ) ) ) )
88 12 18 24 30 39 87 uzind4i 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` N ) ) /\ ( 2nd ` ( G ` N ) ) <_ ( 2nd ` ( G ` M ) ) ) ) )
89 6 88 mpcom 
 |-  ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` N ) ) /\ ( 2nd ` ( G ` N ) ) <_ ( 2nd ` ( G ` M ) ) ) )