Step | Hyp | Ref
| Expression |
1 | | cvg1n.f |
. . . 4
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
2 | | cvg1n.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
3 | | cvg1n.cau |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)))) |
4 | | cvg1nlem.g |
. . . 4
⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍))) |
5 | | cvg1nlem.z |
. . . 4
⊢ (𝜑 → 𝑍 ∈ ℕ) |
6 | | cvg1nlem.start |
. . . 4
⊢ (𝜑 → 𝐶 < 𝑍) |
7 | 1, 2, 3, 4, 5, 6 | cvg1nlemf 10934 |
. . 3
⊢ (𝜑 → 𝐺:ℕ⟶ℝ) |
8 | 1, 2, 3, 4, 5, 6 | cvg1nlemcau 10935 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐺‘𝑛) < ((𝐺‘𝑘) + (1 / 𝑛)) ∧ (𝐺‘𝑘) < ((𝐺‘𝑛) + (1 / 𝑛)))) |
9 | 7, 8 | caucvgre 10932 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑐 ∈ ℝ+ ∃𝑎 ∈ ℕ ∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) |
10 | | fveq2 5494 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑤 → (ℤ≥‘𝑎) =
(ℤ≥‘𝑤)) |
11 | 10 | raleqdv 2671 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑤 → (∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)))) |
12 | 11 | cbvrexv 2697 |
. . . . . . . . 9
⊢
(∃𝑎 ∈
ℕ ∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) |
13 | 12 | ralbii 2476 |
. . . . . . . 8
⊢
(∀𝑐 ∈
ℝ+ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∀𝑐 ∈ ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) |
14 | 13 | anbi2i 454 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ↔ ((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)))) |
15 | 14 | anbi1i 455 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ↔ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈
ℝ+)) |
16 | | oveq2 5858 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝑥 / 2) → (𝑦 + 𝑐) = (𝑦 + (𝑥 / 2))) |
17 | 16 | breq2d 3999 |
. . . . . . . . . . 11
⊢ (𝑐 = (𝑥 / 2) → ((𝐺‘𝑏) < (𝑦 + 𝑐) ↔ (𝐺‘𝑏) < (𝑦 + (𝑥 / 2)))) |
18 | | oveq2 5858 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝑥 / 2) → ((𝐺‘𝑏) + 𝑐) = ((𝐺‘𝑏) + (𝑥 / 2))) |
19 | 18 | breq2d 3999 |
. . . . . . . . . . 11
⊢ (𝑐 = (𝑥 / 2) → (𝑦 < ((𝐺‘𝑏) + 𝑐) ↔ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))) |
20 | 17, 19 | anbi12d 470 |
. . . . . . . . . 10
⊢ (𝑐 = (𝑥 / 2) → (((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) |
21 | 20 | rexralbidv 2496 |
. . . . . . . . 9
⊢ (𝑐 = (𝑥 / 2) → (∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) |
22 | | simplr 525 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) →
∀𝑐 ∈
ℝ+ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) |
23 | | simpr 109 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
24 | 23 | rphalfcld 9653 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
25 | 21, 22, 24 | rspcdva 2839 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) →
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))) |
26 | 15, 25 | sylbir 134 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) →
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))) |
27 | 2 | rpred 9640 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ ℝ) |
28 | 27 | ad4antr 491 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝐶 ∈ ℝ) |
29 | | 2re 8935 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
30 | 29 | a1i 9 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 2 ∈
ℝ) |
31 | 28, 30 | remulcld 7937 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → (𝐶 · 2) ∈
ℝ) |
32 | | simplr 525 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑥 ∈ ℝ+) |
33 | 31, 32 | rerpdivcld 9672 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ((𝐶 · 2) / 𝑥) ∈ ℝ) |
34 | 5 | ad4antr 491 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑍 ∈ ℕ) |
35 | 33, 34 | nndivred 8915 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → (((𝐶 · 2) / 𝑥) / 𝑍) ∈ ℝ) |
36 | | simprl 526 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑎 ∈ ℕ) |
37 | 36 | nnred 8878 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑎 ∈ ℝ) |
38 | 35, 37 | readdcld 7936 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) ∈ ℝ) |
39 | | arch 9119 |
. . . . . . . . 9
⊢
(((((𝐶 · 2) /
𝑥) / 𝑍) + 𝑎) ∈ ℝ → ∃𝑒 ∈ ℕ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒) |
40 | 38, 39 | syl 14 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ∃𝑒 ∈ ℕ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒) |
41 | | simprl 526 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → 𝑒 ∈ ℕ) |
42 | 34 | adantr 274 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → 𝑍 ∈ ℕ) |
43 | 41, 42 | nnmulcld 8914 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → (𝑒 · 𝑍) ∈ ℕ) |
44 | 1 | ad6antr 495 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝐹:ℕ⟶ℝ) |
45 | | simplrl 530 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑒 ∈ ℕ) |
46 | 5 | ad6antr 495 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑍 ∈ ℕ) |
47 | 45, 46 | nnmulcld 8914 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑒 · 𝑍) ∈ ℕ) |
48 | | eluznn 9546 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 · 𝑍) ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑖 ∈ ℕ) |
49 | 47, 48 | sylancom 418 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑖 ∈ ℕ) |
50 | 44, 49 | ffvelrnd 5629 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) ∈ ℝ) |
51 | 44, 47 | ffvelrnd 5629 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) ∈ ℝ) |
52 | 32 | ad2antrr 485 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ+) |
53 | 52 | rpred 9640 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ) |
54 | 53 | rehalfcld 9111 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑥 / 2) ∈ ℝ) |
55 | 51, 54 | readdcld 7936 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)) ∈ ℝ) |
56 | | simpllr 529 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) → 𝑦 ∈
ℝ) |
57 | 56 | ad3antrrr 489 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 ∈ ℝ) |
58 | 57, 54 | readdcld 7936 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑦 + (𝑥 / 2)) ∈ ℝ) |
59 | 58, 54 | readdcld 7936 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝑦 + (𝑥 / 2)) + (𝑥 / 2)) ∈ ℝ) |
60 | 27 | ad6antr 495 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝐶 ∈ ℝ) |
61 | 60, 47 | nndivred 8915 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐶 / (𝑒 · 𝑍)) ∈ ℝ) |
62 | 51, 61 | readdcld 7936 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))) ∈ ℝ) |
63 | | fveq2 5494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖)) |
64 | 63 | oveq1d 5865 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) = ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍)))) |
65 | 64 | breq2d 3999 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑖 → ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ↔ (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))))) |
66 | 63 | breq1d 3997 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))) ↔ (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))) |
67 | 65, 66 | anbi12d 470 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑖 → (((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))) ↔ ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))) |
68 | | fveq2 5494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (𝑒 · 𝑍) → (ℤ≥‘𝑛) =
(ℤ≥‘(𝑒 · 𝑍))) |
69 | | fveq2 5494 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑒 · 𝑍) → (𝐹‘𝑛) = (𝐹‘(𝑒 · 𝑍))) |
70 | | oveq2 5858 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (𝑒 · 𝑍) → (𝐶 / 𝑛) = (𝐶 / (𝑒 · 𝑍))) |
71 | 70 | oveq2d 5866 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑘) + (𝐶 / 𝑛)) = ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍)))) |
72 | 69, 71 | breq12d 4000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ↔ (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))))) |
73 | 69, 70 | oveq12d 5868 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑛) + (𝐶 / 𝑛)) = ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))) |
74 | 73 | breq2d 3999 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)) ↔ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))) |
75 | 72, 74 | anbi12d 470 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (𝑒 · 𝑍) → (((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))) ↔ ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))) |
76 | 68, 75 | raleqbidv 2677 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑒 · 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))) ↔ ∀𝑘 ∈ (ℤ≥‘(𝑒 · 𝑍))((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))) |
77 | 3 | ad6antr 495 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)))) |
78 | 76, 77, 47 | rspcdva 2839 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ∀𝑘 ∈ (ℤ≥‘(𝑒 · 𝑍))((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))) |
79 | | simpr 109 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) |
80 | 67, 78, 79 | rspcdva 2839 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))) |
81 | 80 | simprd 113 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))) |
82 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
83 | 82 | ad3antrrr 489 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ+) |
84 | 83 | rpred 9640 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ) |
85 | 84 | rehalfcld 9111 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑥 / 2) ∈ ℝ) |
86 | 2 | ad6antr 495 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝐶 ∈
ℝ+) |
87 | 36 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 ∈ ℕ) |
88 | | simplrr 531 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒) |
89 | 86, 83, 46, 45, 87, 88 | cvg1nlemcxze 10933 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐶 / (𝑒 · 𝑍)) < (𝑥 / 2)) |
90 | 61, 85, 89 | ltled 8025 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐶 / (𝑒 · 𝑍)) ≤ (𝑥 / 2)) |
91 | 61, 54, 51, 90 | leadd2dd 8466 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))) ≤ ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))) |
92 | 50, 62, 55, 81, 91 | ltletrd 8329 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))) |
93 | | fveq2 5494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑒 → (𝐺‘𝑏) = (𝐺‘𝑒)) |
94 | 93 | breq1d 3997 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑒 → ((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ↔ (𝐺‘𝑒) < (𝑦 + (𝑥 / 2)))) |
95 | 93 | oveq1d 5865 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑒 → ((𝐺‘𝑏) + (𝑥 / 2)) = ((𝐺‘𝑒) + (𝑥 / 2))) |
96 | 95 | breq2d 3999 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑒 → (𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)) ↔ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2)))) |
97 | 94, 96 | anbi12d 470 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑒 → (((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))) ↔ ((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2))))) |
98 | | simprr 527 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))) |
99 | 98 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))) |
100 | 87 | nnred 8878 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 ∈ ℝ) |
101 | 45 | nnred 8878 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑒 ∈ ℝ) |
102 | | 2rp 9602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℝ+ |
103 | 102 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 2 ∈
ℝ+) |
104 | 86, 103 | rpmulcld 9657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐶 · 2) ∈
ℝ+) |
105 | 104, 83 | rpdivcld 9658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐶 · 2) / 𝑥) ∈
ℝ+) |
106 | 46 | nnrpd 9638 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑍 ∈
ℝ+) |
107 | 105, 106 | rpdivcld 9658 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (((𝐶 · 2) / 𝑥) / 𝑍) ∈
ℝ+) |
108 | 107 | rpred 9640 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (((𝐶 · 2) / 𝑥) / 𝑍) ∈ ℝ) |
109 | 108, 100 | readdcld 7936 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) ∈ ℝ) |
110 | 100, 107 | ltaddrp2d 9675 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 < ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎)) |
111 | 100, 109,
101, 110, 88 | lttrd 8032 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 < 𝑒) |
112 | 100, 101,
111 | ltled 8025 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 ≤ 𝑒) |
113 | 87 | nnzd 9320 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 ∈ ℤ) |
114 | 45 | nnzd 9320 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑒 ∈ ℤ) |
115 | | eluz 9487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℤ ∧ 𝑒 ∈ ℤ) → (𝑒 ∈
(ℤ≥‘𝑎) ↔ 𝑎 ≤ 𝑒)) |
116 | 113, 114,
115 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑒 ∈ (ℤ≥‘𝑎) ↔ 𝑎 ≤ 𝑒)) |
117 | 112, 116 | mpbird 166 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑒 ∈ (ℤ≥‘𝑎)) |
118 | 97, 99, 117 | rspcdva 2839 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2)))) |
119 | | oveq1 5857 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑒 → (𝑗 · 𝑍) = (𝑒 · 𝑍)) |
120 | 119 | fveq2d 5498 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑒 → (𝐹‘(𝑗 · 𝑍)) = (𝐹‘(𝑒 · 𝑍))) |
121 | 120, 4 | fvmptg 5570 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 ∈ ℕ ∧ (𝐹‘(𝑒 · 𝑍)) ∈ ℝ) → (𝐺‘𝑒) = (𝐹‘(𝑒 · 𝑍))) |
122 | 45, 51, 121 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐺‘𝑒) = (𝐹‘(𝑒 · 𝑍))) |
123 | 122 | breq1d 3997 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ↔ (𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2)))) |
124 | 122 | oveq1d 5865 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐺‘𝑒) + (𝑥 / 2)) = ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))) |
125 | 124 | breq2d 3999 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑦 < ((𝐺‘𝑒) + (𝑥 / 2)) ↔ 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)))) |
126 | 123, 125 | anbi12d 470 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2))) ↔ ((𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))))) |
127 | 118, 126 | mpbid 146 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)))) |
128 | 127 | simpld 111 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2))) |
129 | 51, 58, 54, 128 | ltadd1dd 8462 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)) < ((𝑦 + (𝑥 / 2)) + (𝑥 / 2))) |
130 | 50, 55, 59, 92, 129 | lttrd 8032 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < ((𝑦 + (𝑥 / 2)) + (𝑥 / 2))) |
131 | 57 | recnd 7935 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 ∈ ℂ) |
132 | 54 | recnd 7935 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑥 / 2) ∈ ℂ) |
133 | 131, 132,
132 | addassd 7929 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝑦 + (𝑥 / 2)) + (𝑥 / 2)) = (𝑦 + ((𝑥 / 2) + (𝑥 / 2)))) |
134 | 130, 133 | breqtrd 4013 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < (𝑦 + ((𝑥 / 2) + (𝑥 / 2)))) |
135 | 52 | rpcnd 9642 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℂ) |
136 | 135 | 2halvesd 9110 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥) |
137 | 136 | oveq2d 5866 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑦 + ((𝑥 / 2) + (𝑥 / 2))) = (𝑦 + 𝑥)) |
138 | 134, 137 | breqtrd 4013 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < (𝑦 + 𝑥)) |
139 | 50, 54 | readdcld 7936 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + (𝑥 / 2)) ∈ ℝ) |
140 | 139, 54 | readdcld 7936 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2)) ∈ ℝ) |
141 | 127 | simprd 113 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))) |
142 | 50, 61 | readdcld 7936 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ∈ ℝ) |
143 | 80 | simpld 111 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍)))) |
144 | 61, 54, 50, 90 | leadd2dd 8466 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ≤ ((𝐹‘𝑖) + (𝑥 / 2))) |
145 | 51, 142, 139, 143, 144 | ltletrd 8329 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝑥 / 2))) |
146 | 51, 139, 54, 145 | ltadd1dd 8462 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)) < (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2))) |
147 | 57, 55, 140, 141, 146 | lttrd 8032 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 < (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2))) |
148 | 50 | recnd 7935 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) ∈ ℂ) |
149 | 148, 132,
132 | addassd 7929 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2)) = ((𝐹‘𝑖) + ((𝑥 / 2) + (𝑥 / 2)))) |
150 | 147, 149 | breqtrd 4013 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 < ((𝐹‘𝑖) + ((𝑥 / 2) + (𝑥 / 2)))) |
151 | 136 | oveq2d 5866 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + ((𝑥 / 2) + (𝑥 / 2))) = ((𝐹‘𝑖) + 𝑥)) |
152 | 150, 151 | breqtrd 4013 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 < ((𝐹‘𝑖) + 𝑥)) |
153 | 138, 152 | jca 304 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
154 | 153 | ralrimiva 2543 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → ∀𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
155 | | fveq2 5494 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑒 · 𝑍) → (ℤ≥‘𝑗) =
(ℤ≥‘(𝑒 · 𝑍))) |
156 | 155 | raleqdv 2671 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑒 · 𝑍) → (∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)) ↔ ∀𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))) |
157 | 156 | rspcev 2834 |
. . . . . . . . 9
⊢ (((𝑒 · 𝑍) ∈ ℕ ∧ ∀𝑖 ∈
(ℤ≥‘(𝑒 · 𝑍))((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
158 | 43, 154, 157 | syl2anc 409 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
159 | 40, 158 | rexlimddv 2592 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
160 | 26, 159 | rexlimddv 2592 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
161 | 15, 160 | sylbi 120 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
162 | 161 | ralrimiva 2543 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
163 | 162 | ex 114 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))) |
164 | 163 | reximdva 2572 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑐 ∈ ℝ+ ∃𝑎 ∈ ℕ ∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))) |
165 | 9, 164 | mpd 13 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |