Step | Hyp | Ref
| Expression |
1 | | ruc.1 |
. . . . 5
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
2 | | ruc.2 |
. . . . 5
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
3 | | ruc.4 |
. . . . 5
⊢ 𝐶 = ({〈0, 〈0,
1〉〉} ∪ 𝐹) |
4 | | ruc.5 |
. . . . 5
⊢ 𝐺 = seq0(𝐷, 𝐶) |
5 | 1, 2, 3, 4 | ruclem6 14803 |
. . . 4
⊢ (𝜑 → 𝐺:ℕ0⟶(ℝ ×
ℝ)) |
6 | | 1stcof 7087 |
. . . 4
⊢ (𝐺:ℕ0⟶(ℝ ×
ℝ) → (1st ∘ 𝐺):ℕ0⟶ℝ) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (𝜑 → (1st ∘
𝐺):ℕ0⟶ℝ) |
8 | | frn 5966 |
. . 3
⊢
((1st ∘ 𝐺):ℕ0⟶ℝ →
ran (1st ∘ 𝐺) ⊆ ℝ) |
9 | 7, 8 | syl 17 |
. 2
⊢ (𝜑 → ran (1st
∘ 𝐺) ⊆
ℝ) |
10 | | fdm 5964 |
. . . . 5
⊢
((1st ∘ 𝐺):ℕ0⟶ℝ →
dom (1st ∘ 𝐺) = ℕ0) |
11 | 7, 10 | syl 17 |
. . . 4
⊢ (𝜑 → dom (1st
∘ 𝐺) =
ℕ0) |
12 | | 0nn0 11184 |
. . . . 5
⊢ 0 ∈
ℕ0 |
13 | | ne0i 3880 |
. . . . 5
⊢ (0 ∈
ℕ0 → ℕ0 ≠ ∅) |
14 | 12, 13 | mp1i 13 |
. . . 4
⊢ (𝜑 → ℕ0 ≠
∅) |
15 | 11, 14 | eqnetrd 2849 |
. . 3
⊢ (𝜑 → dom (1st
∘ 𝐺) ≠
∅) |
16 | | dm0rn0 5263 |
. . . 4
⊢ (dom
(1st ∘ 𝐺)
= ∅ ↔ ran (1st ∘ 𝐺) = ∅) |
17 | 16 | necon3bii 2834 |
. . 3
⊢ (dom
(1st ∘ 𝐺)
≠ ∅ ↔ ran (1st ∘ 𝐺) ≠ ∅) |
18 | 15, 17 | sylib 207 |
. 2
⊢ (𝜑 → ran (1st
∘ 𝐺) ≠
∅) |
19 | | fvco3 6185 |
. . . . . 6
⊢ ((𝐺:ℕ0⟶(ℝ ×
ℝ) ∧ 𝑛 ∈
ℕ0) → ((1st ∘ 𝐺)‘𝑛) = (1st ‘(𝐺‘𝑛))) |
20 | 5, 19 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((1st ∘ 𝐺)‘𝑛) = (1st ‘(𝐺‘𝑛))) |
21 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝐹:ℕ⟶ℝ) |
22 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
23 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
24 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ∈
ℕ0) |
25 | 21, 22, 3, 4, 23, 24 | ruclem10 14807 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘0))) |
26 | 1, 2, 3, 4 | ruclem4 14802 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘0) = 〈0,
1〉) |
27 | 26 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘(𝐺‘0)) =
(2nd ‘〈0, 1〉)) |
28 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
29 | | 1ex 9914 |
. . . . . . . . . 10
⊢ 1 ∈
V |
30 | 28, 29 | op2nd 7068 |
. . . . . . . . 9
⊢
(2nd ‘〈0, 1〉) = 1 |
31 | 27, 30 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘(𝐺‘0)) =
1) |
32 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2nd ‘(𝐺‘0)) = 1) |
33 | 25, 32 | breqtrd 4609 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(1st ‘(𝐺‘𝑛)) < 1) |
34 | 5 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ (ℝ ×
ℝ)) |
35 | | xp1st 7089 |
. . . . . . . 8
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(1st ‘(𝐺‘𝑛)) ∈ ℝ) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(1st ‘(𝐺‘𝑛)) ∈ ℝ) |
37 | | 1re 9918 |
. . . . . . 7
⊢ 1 ∈
ℝ |
38 | | ltle 10005 |
. . . . . . 7
⊢
(((1st ‘(𝐺‘𝑛)) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((1st ‘(𝐺‘𝑛)) < 1 → (1st
‘(𝐺‘𝑛)) ≤ 1)) |
39 | 36, 37, 38 | sylancl 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((1st ‘(𝐺‘𝑛)) < 1 → (1st
‘(𝐺‘𝑛)) ≤ 1)) |
40 | 33, 39 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(1st ‘(𝐺‘𝑛)) ≤ 1) |
41 | 20, 40 | eqbrtrd 4605 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((1st ∘ 𝐺)‘𝑛) ≤ 1) |
42 | 41 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ((1st
∘ 𝐺)‘𝑛) ≤ 1) |
43 | | ffn 5958 |
. . . . 5
⊢
((1st ∘ 𝐺):ℕ0⟶ℝ →
(1st ∘ 𝐺)
Fn ℕ0) |
44 | 7, 43 | syl 17 |
. . . 4
⊢ (𝜑 → (1st ∘
𝐺) Fn
ℕ0) |
45 | | breq1 4586 |
. . . . 5
⊢ (𝑧 = ((1st ∘
𝐺)‘𝑛) → (𝑧 ≤ 1 ↔ ((1st ∘ 𝐺)‘𝑛) ≤ 1)) |
46 | 45 | ralrn 6270 |
. . . 4
⊢
((1st ∘ 𝐺) Fn ℕ0 →
(∀𝑧 ∈ ran
(1st ∘ 𝐺)𝑧 ≤ 1 ↔ ∀𝑛 ∈ ℕ0 ((1st
∘ 𝐺)‘𝑛) ≤ 1)) |
47 | 44, 46 | syl 17 |
. . 3
⊢ (𝜑 → (∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ 1 ↔ ∀𝑛 ∈ ℕ0
((1st ∘ 𝐺)‘𝑛) ≤ 1)) |
48 | 42, 47 | mpbird 246 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ 1) |
49 | 9, 18, 48 | 3jca 1235 |
1
⊢ (𝜑 → (ran (1st
∘ 𝐺) ⊆ ℝ
∧ ran (1st ∘ 𝐺) ≠ ∅ ∧ ∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ 1)) |