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 ⊢φ→F:ℕ⟶ℝ
ruc.2 ⊢φ→D=x∈ℝ2,y∈ℝ⟼⦋1st⁡x+2nd⁡x2/m⦌ifm<y1st⁡xmm+2nd⁡x22nd⁡x
ruc.4 ⊢C=001∪F
ruc.5 ⊢G=seq0DC
ruclem9.6 ⊢φ→M∈ℕ0
ruclem9.7 ⊢φ→N∈ℤ≥M
Assertion ruclem9 ⊢φ→1st⁡G⁡M≤1st⁡G⁡N∧2nd⁡G⁡N≤2nd⁡G⁡M

Proof

Step Hyp Ref Expression
1 ruc.1 ⊢φ→F:ℕ⟶ℝ
2 ruc.2 ⊢φ→D=x∈ℝ2,y∈ℝ⟼⦋1st⁡x+2nd⁡x2/m⦌ifm<y1st⁡xmm+2nd⁡x22nd⁡x
3 ruc.4 ⊢C=001∪F
4 ruc.5 ⊢G=seq0DC
5 ruclem9.6 ⊢φ→M∈ℕ0
6 ruclem9.7 ⊢φ→N∈ℤ≥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→φ→1st⁡G⁡M≤1st⁡G⁡k∧2nd⁡G⁡k≤2nd⁡G⁡M↔φ→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→φ→1st⁡G⁡M≤1st⁡G⁡k∧2nd⁡G⁡k≤2nd⁡G⁡M↔φ→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→φ→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
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→φ→1st⁡G⁡M≤1st⁡G⁡k∧2nd⁡G⁡k≤2nd⁡G⁡M↔φ→1st⁡G⁡M≤1st⁡G⁡N∧2nd⁡G⁡N≤2nd⁡G⁡M
31 1 2 3 4 ruclem6 ⊢φ→G:ℕ0⟶ℝ2
32 31 5 ffvelcdmd ⊢φ→G⁡M∈ℝ2
33 xp1st ⊢G⁡M∈ℝ2→1st⁡G⁡M∈ℝ
34 32 33 syl ⊢φ→1st⁡G⁡M∈ℝ
35 34 leidd ⊢φ→1st⁡G⁡M≤1st⁡G⁡M
36 xp2nd ⊢G⁡M∈ℝ2→2nd⁡G⁡M∈ℝ
37 32 36 syl ⊢φ→2nd⁡G⁡M∈ℝ
38 37 leidd ⊢φ→2nd⁡G⁡M≤2nd⁡G⁡M
39 35 38 jca ⊢φ→1st⁡G⁡M≤1st⁡G⁡M∧2nd⁡G⁡M≤2nd⁡G⁡M
40 1 adantr ⊢φ∧n∈ℤ≥M→F:ℕ⟶ℝ
41 2 adantr ⊢φ∧n∈ℤ≥M→D=x∈ℝ2,y∈ℝ⟼⦋1st⁡x+2nd⁡x2/m⦌ifm<y1st⁡xmm+2nd⁡x22nd⁡x
42 31 adantr ⊢φ∧n∈ℤ≥M→G:ℕ0⟶ℝ2
43 eluznn0 ⊢M∈ℕ0∧n∈ℤ≥M→n∈ℕ0
44 5 43 sylan ⊢φ∧n∈ℤ≥M→n∈ℕ0
45 42 44 ffvelcdmd ⊢φ∧n∈ℤ≥M→G⁡n∈ℝ2
46 xp1st ⊢G⁡n∈ℝ2→1st⁡G⁡n∈ℝ
47 45 46 syl ⊢φ∧n∈ℤ≥M→1st⁡G⁡n∈ℝ
48 xp2nd ⊢G⁡n∈ℝ2→2nd⁡G⁡n∈ℝ
49 45 48 syl ⊢φ∧n∈ℤ≥M→2nd⁡G⁡n∈ℝ
50 nn0p1nn ⊢n∈ℕ0→n+1∈ℕ
51 44 50 syl ⊢φ∧n∈ℤ≥M→n+1∈ℕ
52 40 51 ffvelcdmd ⊢φ∧n∈ℤ≥M→F⁡n+1∈ℝ
53 eqid ⊢1st⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1=1st⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1
54 eqid ⊢2nd⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1=2nd⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1
55 1 2 3 4 ruclem8 ⊢φ∧n∈ℕ0→1st⁡G⁡n<2nd⁡G⁡n
56 44 55 syldan ⊢φ∧n∈ℤ≥M→1st⁡G⁡n<2nd⁡G⁡n
57 40 41 47 49 52 53 54 56 ruclem2 ⊢φ∧n∈ℤ≥M→1st⁡G⁡n≤1st⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1∧1st⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1<2nd⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1∧2nd⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1≤2nd⁡G⁡n
58 57 simp1d ⊢φ∧n∈ℤ≥M→1st⁡G⁡n≤1st⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1
59 1 2 3 4 ruclem7 ⊢φ∧n∈ℕ0→G⁡n+1=G⁡nDF⁡n+1
60 44 59 syldan ⊢φ∧n∈ℤ≥M→G⁡n+1=G⁡nDF⁡n+1
61 1st2nd2 ⊢G⁡n∈ℝ2→G⁡n=1st⁡G⁡n2nd⁡G⁡n
62 45 61 syl ⊢φ∧n∈ℤ≥M→G⁡n=1st⁡G⁡n2nd⁡G⁡n
63 62 oveq1d ⊢φ∧n∈ℤ≥M→G⁡nDF⁡n+1=1st⁡G⁡n2nd⁡G⁡nDF⁡n+1
64 60 63 eqtrd ⊢φ∧n∈ℤ≥M→G⁡n+1=1st⁡G⁡n2nd⁡G⁡nDF⁡n+1
65 64 fveq2d ⊢φ∧n∈ℤ≥M→1st⁡G⁡n+1=1st⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1
66 58 65 breqtrrd ⊢φ∧n∈ℤ≥M→1st⁡G⁡n≤1st⁡G⁡n+1
67 34 adantr ⊢φ∧n∈ℤ≥M→1st⁡G⁡M∈ℝ
68 peano2nn0 ⊢n∈ℕ0→n+1∈ℕ0
69 44 68 syl ⊢φ∧n∈ℤ≥M→n+1∈ℕ0
70 42 69 ffvelcdmd ⊢φ∧n∈ℤ≥M→G⁡n+1∈ℝ2
71 xp1st ⊢G⁡n+1∈ℝ2→1st⁡G⁡n+1∈ℝ
72 70 71 syl ⊢φ∧n∈ℤ≥M→1st⁡G⁡n+1∈ℝ
73 letr ⊢1st⁡G⁡M∈ℝ∧1st⁡G⁡n∈ℝ∧1st⁡G⁡n+1∈ℝ→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 ⊢φ∧n∈ℤ≥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 ⊢φ∧n∈ℤ≥M→1st⁡G⁡M≤1st⁡G⁡n→1st⁡G⁡M≤1st⁡G⁡n+1
76 64 fveq2d ⊢φ∧n∈ℤ≥M→2nd⁡G⁡n+1=2nd⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1
77 57 simp3d ⊢φ∧n∈ℤ≥M→2nd⁡1st⁡G⁡n2nd⁡G⁡nDF⁡n+1≤2nd⁡G⁡n
78 76 77 eqbrtrd ⊢φ∧n∈ℤ≥M→2nd⁡G⁡n+1≤2nd⁡G⁡n
79 xp2nd ⊢G⁡n+1∈ℝ2→2nd⁡G⁡n+1∈ℝ
80 70 79 syl ⊢φ∧n∈ℤ≥M→2nd⁡G⁡n+1∈ℝ
81 37 adantr ⊢φ∧n∈ℤ≥M→2nd⁡G⁡M∈ℝ
82 letr ⊢2nd⁡G⁡n+1∈ℝ∧2nd⁡G⁡n∈ℝ∧2nd⁡G⁡M∈ℝ→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 ⊢φ∧n∈ℤ≥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 ⊢φ∧n∈ℤ≥M→2nd⁡G⁡n≤2nd⁡G⁡M→2nd⁡G⁡n+1≤2nd⁡G⁡M
85 75 84 anim12d ⊢φ∧n∈ℤ≥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∈ℤ≥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
87 86 a2d ⊢n∈ℤ≥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
88 12 18 24 30 39 87 uzind4i ⊢N∈ℤ≥M→φ→1st⁡G⁡M≤1st⁡G⁡N∧2nd⁡G⁡N≤2nd⁡G⁡M
89 6 88 mpcom ⊢φ→1st⁡G⁡M≤1st⁡G⁡N∧2nd⁡G⁡N≤2nd⁡G⁡M