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 ∈ ℝ ⟼ ⦋ 1 st ⁡ x + 2 nd ⁡ x 2 / m⦌ if m < y 1 st ⁡ x m m + 2 nd ⁡ x 2 2 nd ⁡ x
ruc.4 ⊢ C = 0 0 1 ∪ F
ruc.5 ⊢ G = seq 0 D C
ruclem9.6 ⊢ φ → M ∈ ℕ 0
ruclem9.7 ⊢ φ → N ∈ ℤ ≥ M
Assertion ruclem9 ⊢ φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ N ∧ 2 nd ⁡ G ⁡ N ≤ 2 nd ⁡ G ⁡ M

Proof

Step Hyp Ref Expression
1 ruc.1 ⊢ φ → F : ℕ ⟶ ℝ
2 ruc.2 ⊢ φ → D = x ∈ ℝ 2 , y ∈ ℝ ⟼ ⦋ 1 st ⁡ x + 2 nd ⁡ x 2 / m⦌ if m < y 1 st ⁡ x m m + 2 nd ⁡ x 2 2 nd ⁡ x
3 ruc.4 ⊢ C = 0 0 1 ∪ F
4 ruc.5 ⊢ G = seq 0 D C
5 ruclem9.6 ⊢ φ → M ∈ ℕ 0
6 ruclem9.7 ⊢ φ → N ∈ ℤ ≥ M
7 2fveq3 ⊢ k = M → 1 st ⁡ G ⁡ k = 1 st ⁡ G ⁡ M
8 7 breq2d ⊢ k = M → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ↔ 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ M
9 2fveq3 ⊢ k = M → 2 nd ⁡ G ⁡ k = 2 nd ⁡ G ⁡ M
10 9 breq1d ⊢ k = M → 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ 2 nd ⁡ G ⁡ M ≤ 2 nd ⁡ G ⁡ M
11 8 10 anbi12d ⊢ k = M → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ∧ 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ M ∧ 2 nd ⁡ G ⁡ M ≤ 2 nd ⁡ G ⁡ M
12 11 imbi2d ⊢ k = M → φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ∧ 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ M ∧ 2 nd ⁡ G ⁡ M ≤ 2 nd ⁡ G ⁡ M
13 2fveq3 ⊢ k = n → 1 st ⁡ G ⁡ k = 1 st ⁡ G ⁡ n
14 13 breq2d ⊢ k = n → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ↔ 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n
15 2fveq3 ⊢ k = n → 2 nd ⁡ G ⁡ k = 2 nd ⁡ G ⁡ n
16 15 breq1d ⊢ k = n → 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ 2 nd ⁡ G ⁡ n ≤ 2 nd ⁡ G ⁡ M
17 14 16 anbi12d ⊢ k = n → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ∧ 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n ∧ 2 nd ⁡ G ⁡ n ≤ 2 nd ⁡ G ⁡ M
18 17 imbi2d ⊢ k = n → φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ∧ 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n ∧ 2 nd ⁡ G ⁡ n ≤ 2 nd ⁡ G ⁡ M
19 2fveq3 ⊢ k = n + 1 → 1 st ⁡ G ⁡ k = 1 st ⁡ G ⁡ n + 1
20 19 breq2d ⊢ k = n + 1 → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ↔ 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n + 1
21 2fveq3 ⊢ k = n + 1 → 2 nd ⁡ G ⁡ k = 2 nd ⁡ G ⁡ n + 1
22 21 breq1d ⊢ k = n + 1 → 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ M
23 20 22 anbi12d ⊢ k = n + 1 → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ∧ 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n + 1 ∧ 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ M
24 23 imbi2d ⊢ k = n + 1 → φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ∧ 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n + 1 ∧ 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ M
25 2fveq3 ⊢ k = N → 1 st ⁡ G ⁡ k = 1 st ⁡ G ⁡ N
26 25 breq2d ⊢ k = N → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ↔ 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ N
27 2fveq3 ⊢ k = N → 2 nd ⁡ G ⁡ k = 2 nd ⁡ G ⁡ N
28 27 breq1d ⊢ k = N → 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ 2 nd ⁡ G ⁡ N ≤ 2 nd ⁡ G ⁡ M
29 26 28 anbi12d ⊢ k = N → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ∧ 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ N ∧ 2 nd ⁡ G ⁡ N ≤ 2 nd ⁡ G ⁡ M
30 29 imbi2d ⊢ k = N → φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ k ∧ 2 nd ⁡ G ⁡ k ≤ 2 nd ⁡ G ⁡ M ↔ φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ N ∧ 2 nd ⁡ G ⁡ N ≤ 2 nd ⁡ G ⁡ M
31 1 2 3 4 ruclem6 ⊢ φ → G : ℕ 0 ⟶ ℝ 2
32 31 5 ffvelrnd ⊢ φ → G ⁡ M ∈ ℝ 2
33 xp1st ⊢ G ⁡ M ∈ ℝ 2 → 1 st ⁡ G ⁡ M ∈ ℝ
34 32 33 syl ⊢ φ → 1 st ⁡ G ⁡ M ∈ ℝ
35 34 leidd ⊢ φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ M
36 xp2nd ⊢ G ⁡ M ∈ ℝ 2 → 2 nd ⁡ G ⁡ M ∈ ℝ
37 32 36 syl ⊢ φ → 2 nd ⁡ G ⁡ M ∈ ℝ
38 37 leidd ⊢ φ → 2 nd ⁡ G ⁡ M ≤ 2 nd ⁡ G ⁡ M
39 35 38 jca ⊢ φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ M ∧ 2 nd ⁡ G ⁡ M ≤ 2 nd ⁡ G ⁡ M
40 1 adantr ⊢ φ ∧ n ∈ ℤ ≥ M → F : ℕ ⟶ ℝ
41 2 adantr ⊢ φ ∧ n ∈ ℤ ≥ M → D = x ∈ ℝ 2 , y ∈ ℝ ⟼ ⦋ 1 st ⁡ x + 2 nd ⁡ x 2 / m⦌ if m < y 1 st ⁡ x m m + 2 nd ⁡ x 2 2 nd ⁡ 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 ffvelrnd ⊢ φ ∧ n ∈ ℤ ≥ M → G ⁡ n ∈ ℝ 2
46 xp1st ⊢ G ⁡ n ∈ ℝ 2 → 1 st ⁡ G ⁡ n ∈ ℝ
47 45 46 syl ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ n ∈ ℝ
48 xp2nd ⊢ G ⁡ n ∈ ℝ 2 → 2 nd ⁡ G ⁡ n ∈ ℝ
49 45 48 syl ⊢ φ ∧ n ∈ ℤ ≥ M → 2 nd ⁡ G ⁡ n ∈ ℝ
50 nn0p1nn ⊢ n ∈ ℕ 0 → n + 1 ∈ ℕ
51 44 50 syl ⊢ φ ∧ n ∈ ℤ ≥ M → n + 1 ∈ ℕ
52 40 51 ffvelrnd ⊢ φ ∧ n ∈ ℤ ≥ M → F ⁡ n + 1 ∈ ℝ
53 eqid ⊢ 1 st ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1 = 1 st ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1
54 eqid ⊢ 2 nd ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1 = 2 nd ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1
55 1 2 3 4 ruclem8 ⊢ φ ∧ n ∈ ℕ 0 → 1 st ⁡ G ⁡ n < 2 nd ⁡ G ⁡ n
56 44 55 syldan ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ n < 2 nd ⁡ G ⁡ n
57 40 41 47 49 52 53 54 56 ruclem2 ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ n ≤ 1 st ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1 ∧ 1 st ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1 < 2 nd ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1 ∧ 2 nd ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ n
58 57 simp1d ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ n ≤ 1 st ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1
59 1 2 3 4 ruclem7 ⊢ φ ∧ n ∈ ℕ 0 → G ⁡ n + 1 = G ⁡ n D F ⁡ n + 1
60 44 59 syldan ⊢ φ ∧ n ∈ ℤ ≥ M → G ⁡ n + 1 = G ⁡ n D F ⁡ n + 1
61 1st2nd2 ⊢ G ⁡ n ∈ ℝ 2 → G ⁡ n = 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n
62 45 61 syl ⊢ φ ∧ n ∈ ℤ ≥ M → G ⁡ n = 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n
63 62 oveq1d ⊢ φ ∧ n ∈ ℤ ≥ M → G ⁡ n D F ⁡ n + 1 = 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1
64 60 63 eqtrd ⊢ φ ∧ n ∈ ℤ ≥ M → G ⁡ n + 1 = 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1
65 64 fveq2d ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ n + 1 = 1 st ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1
66 58 65 breqtrrd ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ n ≤ 1 st ⁡ G ⁡ n + 1
67 34 adantr ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ M ∈ ℝ
68 peano2nn0 ⊢ n ∈ ℕ 0 → n + 1 ∈ ℕ 0
69 44 68 syl ⊢ φ ∧ n ∈ ℤ ≥ M → n + 1 ∈ ℕ 0
70 42 69 ffvelrnd ⊢ φ ∧ n ∈ ℤ ≥ M → G ⁡ n + 1 ∈ ℝ 2
71 xp1st ⊢ G ⁡ n + 1 ∈ ℝ 2 → 1 st ⁡ G ⁡ n + 1 ∈ ℝ
72 70 71 syl ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ n + 1 ∈ ℝ
73 letr ⊢ 1 st ⁡ G ⁡ M ∈ ℝ ∧ 1 st ⁡ G ⁡ n ∈ ℝ ∧ 1 st ⁡ G ⁡ n + 1 ∈ ℝ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n ∧ 1 st ⁡ G ⁡ n ≤ 1 st ⁡ G ⁡ n + 1 → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n + 1
74 67 47 72 73 syl3anc ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n ∧ 1 st ⁡ G ⁡ n ≤ 1 st ⁡ G ⁡ n + 1 → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n + 1
75 66 74 mpan2d ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n + 1
76 64 fveq2d ⊢ φ ∧ n ∈ ℤ ≥ M → 2 nd ⁡ G ⁡ n + 1 = 2 nd ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1
77 57 simp3d ⊢ φ ∧ n ∈ ℤ ≥ M → 2 nd ⁡ 1 st ⁡ G ⁡ n 2 nd ⁡ G ⁡ n D F ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ n
78 76 77 eqbrtrd ⊢ φ ∧ n ∈ ℤ ≥ M → 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ n
79 xp2nd ⊢ G ⁡ n + 1 ∈ ℝ 2 → 2 nd ⁡ G ⁡ n + 1 ∈ ℝ
80 70 79 syl ⊢ φ ∧ n ∈ ℤ ≥ M → 2 nd ⁡ G ⁡ n + 1 ∈ ℝ
81 37 adantr ⊢ φ ∧ n ∈ ℤ ≥ M → 2 nd ⁡ G ⁡ M ∈ ℝ
82 letr ⊢ 2 nd ⁡ G ⁡ n + 1 ∈ ℝ ∧ 2 nd ⁡ G ⁡ n ∈ ℝ ∧ 2 nd ⁡ G ⁡ M ∈ ℝ → 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ n ∧ 2 nd ⁡ G ⁡ n ≤ 2 nd ⁡ G ⁡ M → 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ M
83 80 49 81 82 syl3anc ⊢ φ ∧ n ∈ ℤ ≥ M → 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ n ∧ 2 nd ⁡ G ⁡ n ≤ 2 nd ⁡ G ⁡ M → 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ M
84 78 83 mpand ⊢ φ ∧ n ∈ ℤ ≥ M → 2 nd ⁡ G ⁡ n ≤ 2 nd ⁡ G ⁡ M → 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ M
85 75 84 anim12d ⊢ φ ∧ n ∈ ℤ ≥ M → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n ∧ 2 nd ⁡ G ⁡ n ≤ 2 nd ⁡ G ⁡ M → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n + 1 ∧ 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ M
86 85 expcom ⊢ n ∈ ℤ ≥ M → φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n ∧ 2 nd ⁡ G ⁡ n ≤ 2 nd ⁡ G ⁡ M → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n + 1 ∧ 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ M
87 86 a2d ⊢ n ∈ ℤ ≥ M → φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n ∧ 2 nd ⁡ G ⁡ n ≤ 2 nd ⁡ G ⁡ M → φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ n + 1 ∧ 2 nd ⁡ G ⁡ n + 1 ≤ 2 nd ⁡ G ⁡ M
88 12 18 24 30 39 87 uzind4i ⊢ N ∈ ℤ ≥ M → φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ N ∧ 2 nd ⁡ G ⁡ N ≤ 2 nd ⁡ G ⁡ M
89 6 88 mpcom ⊢ φ → 1 st ⁡ G ⁡ M ≤ 1 st ⁡ G ⁡ N ∧ 2 nd ⁡ G ⁡ N ≤ 2 nd ⁡ G ⁡ M