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 ⊢ φ → 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
Assertion ruclem8 ⊢ φ ∧ N ∈ ℕ 0 → 1 st ⁡ G ⁡ N < 2 nd ⁡ G ⁡ N

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