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 14964 |
. . . 4
⊢ (𝜑 → 𝐺:ℕ0⟶(ℝ ×
ℝ)) |
6 | | 1stcof 7196 |
. . . 4
⊢ (𝐺:ℕ0⟶(ℝ ×
ℝ) → (1st ∘ 𝐺):ℕ0⟶ℝ) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (𝜑 → (1st ∘
𝐺):ℕ0⟶ℝ) |
8 | | frn 6053 |
. . 3
⊢
((1st ∘ 𝐺):ℕ0⟶ℝ →
ran (1st ∘ 𝐺) ⊆ ℝ) |
9 | 7, 8 | syl 17 |
. 2
⊢ (𝜑 → ran (1st
∘ 𝐺) ⊆
ℝ) |
10 | | fdm 6051 |
. . . . 5
⊢
((1st ∘ 𝐺):ℕ0⟶ℝ →
dom (1st ∘ 𝐺) = ℕ0) |
11 | 7, 10 | syl 17 |
. . . 4
⊢ (𝜑 → dom (1st
∘ 𝐺) =
ℕ0) |
12 | | 0nn0 11307 |
. . . . 5
⊢ 0 ∈
ℕ0 |
13 | | ne0i 3921 |
. . . . 5
⊢ (0 ∈
ℕ0 → ℕ0 ≠ ∅) |
14 | 12, 13 | mp1i 13 |
. . . 4
⊢ (𝜑 → ℕ0 ≠
∅) |
15 | 11, 14 | eqnetrd 2861 |
. . 3
⊢ (𝜑 → dom (1st
∘ 𝐺) ≠
∅) |
16 | | dm0rn0 5342 |
. . . 4
⊢ (dom
(1st ∘ 𝐺)
= ∅ ↔ ran (1st ∘ 𝐺) = ∅) |
17 | 16 | necon3bii 2846 |
. . 3
⊢ (dom
(1st ∘ 𝐺)
≠ ∅ ↔ ran (1st ∘ 𝐺) ≠ ∅) |
18 | 15, 17 | sylib 208 |
. 2
⊢ (𝜑 → ran (1st
∘ 𝐺) ≠
∅) |
19 | | fvco3 6275 |
. . . . . 6
⊢ ((𝐺:ℕ0⟶(ℝ ×
ℝ) ∧ 𝑛 ∈
ℕ0) → ((1st ∘ 𝐺)‘𝑛) = (1st ‘(𝐺‘𝑛))) |
20 | 5, 19 | sylan 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((1st ∘ 𝐺)‘𝑛) = (1st ‘(𝐺‘𝑛))) |
21 | 1 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝐹:ℕ⟶ℝ) |
22 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
23 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
24 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ∈
ℕ0) |
25 | 21, 22, 3, 4, 23, 24 | ruclem10 14968 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘0))) |
26 | 1, 2, 3, 4 | ruclem4 14963 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘0) = 〈0,
1〉) |
27 | 26 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘(𝐺‘0)) =
(2nd ‘〈0, 1〉)) |
28 | | c0ex 10034 |
. . . . . . . . . 10
⊢ 0 ∈
V |
29 | | 1ex 10035 |
. . . . . . . . . 10
⊢ 1 ∈
V |
30 | 28, 29 | op2nd 7177 |
. . . . . . . . 9
⊢
(2nd ‘〈0, 1〉) = 1 |
31 | 27, 30 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘(𝐺‘0)) =
1) |
32 | 31 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2nd ‘(𝐺‘0)) = 1) |
33 | 25, 32 | breqtrd 4679 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(1st ‘(𝐺‘𝑛)) < 1) |
34 | 5 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ (ℝ ×
ℝ)) |
35 | | xp1st 7198 |
. . . . . . . 8
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(1st ‘(𝐺‘𝑛)) ∈ ℝ) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(1st ‘(𝐺‘𝑛)) ∈ ℝ) |
37 | | 1re 10039 |
. . . . . . 7
⊢ 1 ∈
ℝ |
38 | | ltle 10126 |
. . . . . . 7
⊢
(((1st ‘(𝐺‘𝑛)) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((1st ‘(𝐺‘𝑛)) < 1 → (1st
‘(𝐺‘𝑛)) ≤ 1)) |
39 | 36, 37, 38 | sylancl 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((1st ‘(𝐺‘𝑛)) < 1 → (1st
‘(𝐺‘𝑛)) ≤ 1)) |
40 | 33, 39 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(1st ‘(𝐺‘𝑛)) ≤ 1) |
41 | 20, 40 | eqbrtrd 4675 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((1st ∘ 𝐺)‘𝑛) ≤ 1) |
42 | 41 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ((1st
∘ 𝐺)‘𝑛) ≤ 1) |
43 | | ffn 6045 |
. . . . 5
⊢
((1st ∘ 𝐺):ℕ0⟶ℝ →
(1st ∘ 𝐺)
Fn ℕ0) |
44 | 7, 43 | syl 17 |
. . . 4
⊢ (𝜑 → (1st ∘
𝐺) Fn
ℕ0) |
45 | | breq1 4656 |
. . . . 5
⊢ (𝑧 = ((1st ∘
𝐺)‘𝑛) → (𝑧 ≤ 1 ↔ ((1st ∘ 𝐺)‘𝑛) ≤ 1)) |
46 | 45 | ralrn 6362 |
. . . 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 247 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ 1) |
49 | 9, 18, 48 | 3jca 1242 |
1
⊢ (𝜑 → (ran (1st
∘ 𝐺) ⊆ ℝ
∧ ran (1st ∘ 𝐺) ≠ ∅ ∧ ∀𝑧 ∈ ran (1st
∘ 𝐺)𝑧 ≤ 1)) |