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 9869 |
. . 3
⊢ (𝜑 → 𝐺:ℕ⟶ℝ) |
8 | 1, 2, 3, 4, 5, 6 | cvg1nlemcau 9870 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐺‘𝑛) < ((𝐺‘𝑘) + (1 / 𝑛)) ∧ (𝐺‘𝑘) < ((𝐺‘𝑛) + (1 / 𝑛)))) |
9 | 7, 8 | caucvgre 9867 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑐 ∈ ℝ+ ∃𝑎 ∈ ℕ ∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) |
10 | | fveq2 5198 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑤 → (ℤ≥‘𝑎) =
(ℤ≥‘𝑤)) |
11 | 10 | raleqdv 2555 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑤 → (∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)))) |
12 | 11 | cbvrexv 2578 |
. . . . . . . . 9
⊢
(∃𝑎 ∈
ℕ ∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) |
13 | 12 | ralbii 2372 |
. . . . . . . 8
⊢
(∀𝑐 ∈
ℝ+ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∀𝑐 ∈ ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) |
14 | 13 | anbi2i 444 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ↔ ((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)))) |
15 | 14 | anbi1i 445 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ↔ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈
ℝ+)) |
16 | | simpr 108 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
17 | 16 | rphalfcld 8786 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
18 | | simplr 496 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) →
∀𝑐 ∈
ℝ+ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) |
19 | | oveq2 5540 |
. . . . . . . . . . . . 13
⊢ (𝑐 = (𝑥 / 2) → (𝑦 + 𝑐) = (𝑦 + (𝑥 / 2))) |
20 | 19 | breq2d 3797 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝑥 / 2) → ((𝐺‘𝑏) < (𝑦 + 𝑐) ↔ (𝐺‘𝑏) < (𝑦 + (𝑥 / 2)))) |
21 | | oveq2 5540 |
. . . . . . . . . . . . 13
⊢ (𝑐 = (𝑥 / 2) → ((𝐺‘𝑏) + 𝑐) = ((𝐺‘𝑏) + (𝑥 / 2))) |
22 | 21 | breq2d 3797 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝑥 / 2) → (𝑦 < ((𝐺‘𝑏) + 𝑐) ↔ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))) |
23 | 20, 22 | anbi12d 456 |
. . . . . . . . . . 11
⊢ (𝑐 = (𝑥 / 2) → (((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) |
24 | 23 | rexralbidv 2392 |
. . . . . . . . . 10
⊢ (𝑐 = (𝑥 / 2) → (∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) |
25 | 24 | rspcv 2697 |
. . . . . . . . 9
⊢ ((𝑥 / 2) ∈ ℝ+
→ (∀𝑐 ∈
ℝ+ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) → ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) |
26 | 17, 18, 25 | sylc 61 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) →
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))) |
27 | 15, 26 | sylbir 133 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) →
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))) |
28 | 2 | rpred 8773 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ ℝ) |
29 | 28 | ad4antr 477 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝐶 ∈ ℝ) |
30 | | 2re 8109 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
31 | 30 | a1i 9 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 2 ∈
ℝ) |
32 | 29, 31 | remulcld 7149 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → (𝐶 · 2) ∈
ℝ) |
33 | | simplr 496 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑥 ∈ ℝ+) |
34 | 32, 33 | rerpdivcld 8805 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ((𝐶 · 2) / 𝑥) ∈ ℝ) |
35 | 5 | ad4antr 477 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑍 ∈ ℕ) |
36 | 34, 35 | nndivred 8088 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → (((𝐶 · 2) / 𝑥) / 𝑍) ∈ ℝ) |
37 | | simprl 497 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑎 ∈ ℕ) |
38 | 37 | nnred 8052 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑎 ∈ ℝ) |
39 | 36, 38 | readdcld 7148 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) ∈ ℝ) |
40 | | arch 8285 |
. . . . . . . . 9
⊢
(((((𝐶 · 2) /
𝑥) / 𝑍) + 𝑎) ∈ ℝ → ∃𝑒 ∈ ℕ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒) |
41 | 39, 40 | syl 14 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ∃𝑒 ∈ ℕ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒) |
42 | | simprl 497 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → 𝑒 ∈ ℕ) |
43 | 35 | adantr 270 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → 𝑍 ∈ ℕ) |
44 | 42, 43 | nnmulcld 8087 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → (𝑒 · 𝑍) ∈ ℕ) |
45 | 1 | ad6antr 481 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝐹:ℕ⟶ℝ) |
46 | | simplrl 501 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑒 ∈ ℕ) |
47 | 5 | ad6antr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑍 ∈ ℕ) |
48 | 46, 47 | nnmulcld 8087 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑒 · 𝑍) ∈ ℕ) |
49 | | eluznn 8687 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 · 𝑍) ∈ ℕ ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑖 ∈ ℕ) |
50 | 48, 49 | sylancom 411 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑖 ∈ ℕ) |
51 | 45, 50 | ffvelrnd 5324 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) ∈ ℝ) |
52 | 45, 48 | ffvelrnd 5324 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) ∈ ℝ) |
53 | 33 | ad2antrr 471 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ+) |
54 | 53 | rpred 8773 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ) |
55 | 54 | rehalfcld 8277 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑥 / 2) ∈ ℝ) |
56 | 52, 55 | readdcld 7148 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)) ∈ ℝ) |
57 | | simpllr 500 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) → 𝑦 ∈
ℝ) |
58 | 57 | ad3antrrr 475 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 ∈ ℝ) |
59 | 58, 55 | readdcld 7148 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑦 + (𝑥 / 2)) ∈ ℝ) |
60 | 59, 55 | readdcld 7148 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝑦 + (𝑥 / 2)) + (𝑥 / 2)) ∈ ℝ) |
61 | 28 | ad6antr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝐶 ∈ ℝ) |
62 | 61, 48 | nndivred 8088 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐶 / (𝑒 · 𝑍)) ∈ ℝ) |
63 | 52, 62 | readdcld 7148 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))) ∈ ℝ) |
64 | | simpr 108 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) |
65 | 3 | ad6antr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)))) |
66 | | fveq2 5198 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑒 · 𝑍) → (ℤ≥‘𝑛) =
(ℤ≥‘(𝑒 · 𝑍))) |
67 | | fveq2 5198 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (𝑒 · 𝑍) → (𝐹‘𝑛) = (𝐹‘(𝑒 · 𝑍))) |
68 | | oveq2 5540 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = (𝑒 · 𝑍) → (𝐶 / 𝑛) = (𝐶 / (𝑒 · 𝑍))) |
69 | 68 | oveq2d 5548 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑘) + (𝐶 / 𝑛)) = ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍)))) |
70 | 67, 69 | breq12d 3798 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ↔ (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))))) |
71 | 67, 68 | oveq12d 5550 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑛) + (𝐶 / 𝑛)) = ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))) |
72 | 71 | breq2d 3797 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)) ↔ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))) |
73 | 70, 72 | anbi12d 456 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑒 · 𝑍) → (((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))) ↔ ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))) |
74 | 66, 73 | raleqbidv 2561 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (𝑒 · 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))) ↔ ∀𝑘 ∈ (ℤ≥‘(𝑒 · 𝑍))((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))) |
75 | 74 | rspcv 2697 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 · 𝑍) ∈ ℕ → (∀𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))) → ∀𝑘 ∈ (ℤ≥‘(𝑒 · 𝑍))((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))) |
76 | 48, 65, 75 | sylc 61 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ∀𝑘 ∈ (ℤ≥‘(𝑒 · 𝑍))((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))) |
77 | | fveq2 5198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖)) |
78 | 77 | oveq1d 5547 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) = ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍)))) |
79 | 78 | breq2d 3797 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑖 → ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ↔ (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))))) |
80 | 77 | breq1d 3795 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))) ↔ (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))) |
81 | 79, 80 | anbi12d 456 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑖 → (((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))) ↔ ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))) |
82 | 81 | rspcv 2697 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈
(ℤ≥‘(𝑒 · 𝑍)) → (∀𝑘 ∈ (ℤ≥‘(𝑒 · 𝑍))((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))) → ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))) |
83 | 64, 76, 82 | sylc 61 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))) |
84 | 83 | simprd 112 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))) |
85 | | simpr 108 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
86 | 85 | ad3antrrr 475 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ+) |
87 | 86 | rpred 8773 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ) |
88 | 87 | rehalfcld 8277 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑥 / 2) ∈ ℝ) |
89 | 2 | ad6antr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝐶 ∈
ℝ+) |
90 | 37 | ad2antrr 471 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 ∈ ℕ) |
91 | | simplrr 502 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒) |
92 | 89, 86, 47, 46, 90, 91 | cvg1nlemcxze 9868 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐶 / (𝑒 · 𝑍)) < (𝑥 / 2)) |
93 | 62, 88, 92 | ltled 7228 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐶 / (𝑒 · 𝑍)) ≤ (𝑥 / 2)) |
94 | 62, 55, 52, 93 | leadd2dd 7660 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))) ≤ ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))) |
95 | 51, 63, 56, 84, 94 | ltletrd 7527 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))) |
96 | 90 | nnred 8052 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 ∈ ℝ) |
97 | 46 | nnred 8052 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑒 ∈ ℝ) |
98 | | 2rp 8739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℝ+ |
99 | 98 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 2 ∈
ℝ+) |
100 | 89, 99 | rpmulcld 8790 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐶 · 2) ∈
ℝ+) |
101 | 100, 86 | rpdivcld 8791 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐶 · 2) / 𝑥) ∈
ℝ+) |
102 | 47 | nnrpd 8772 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑍 ∈
ℝ+) |
103 | 101, 102 | rpdivcld 8791 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (((𝐶 · 2) / 𝑥) / 𝑍) ∈
ℝ+) |
104 | 103 | rpred 8773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (((𝐶 · 2) / 𝑥) / 𝑍) ∈ ℝ) |
105 | 104, 96 | readdcld 7148 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) ∈ ℝ) |
106 | 96, 103 | ltaddrp2d 8808 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 < ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎)) |
107 | 96, 105, 97, 106, 91 | lttrd 7235 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 < 𝑒) |
108 | 96, 97, 107 | ltled 7228 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 ≤ 𝑒) |
109 | 90 | nnzd 8468 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑎 ∈ ℤ) |
110 | 46 | nnzd 8468 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑒 ∈ ℤ) |
111 | | eluz 8632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℤ ∧ 𝑒 ∈ ℤ) → (𝑒 ∈
(ℤ≥‘𝑎) ↔ 𝑎 ≤ 𝑒)) |
112 | 109, 110,
111 | syl2anc 403 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑒 ∈ (ℤ≥‘𝑎) ↔ 𝑎 ≤ 𝑒)) |
113 | 108, 112 | mpbird 165 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑒 ∈ (ℤ≥‘𝑎)) |
114 | | simprr 498 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))) |
115 | 114 | ad2antrr 471 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))) |
116 | | fveq2 5198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = 𝑒 → (𝐺‘𝑏) = (𝐺‘𝑒)) |
117 | 116 | breq1d 3795 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑒 → ((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ↔ (𝐺‘𝑒) < (𝑦 + (𝑥 / 2)))) |
118 | 116 | oveq1d 5547 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = 𝑒 → ((𝐺‘𝑏) + (𝑥 / 2)) = ((𝐺‘𝑒) + (𝑥 / 2))) |
119 | 118 | breq2d 3797 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑒 → (𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)) ↔ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2)))) |
120 | 117, 119 | anbi12d 456 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑒 → (((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))) ↔ ((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2))))) |
121 | 120 | rspcv 2697 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 ∈
(ℤ≥‘𝑎) → (∀𝑏 ∈ (ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))) → ((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2))))) |
122 | 113, 115,
121 | sylc 61 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2)))) |
123 | | oveq1 5539 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑒 → (𝑗 · 𝑍) = (𝑒 · 𝑍)) |
124 | 123 | fveq2d 5202 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑒 → (𝐹‘(𝑗 · 𝑍)) = (𝐹‘(𝑒 · 𝑍))) |
125 | 124, 4 | fvmptg 5269 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 ∈ ℕ ∧ (𝐹‘(𝑒 · 𝑍)) ∈ ℝ) → (𝐺‘𝑒) = (𝐹‘(𝑒 · 𝑍))) |
126 | 46, 52, 125 | syl2anc 403 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐺‘𝑒) = (𝐹‘(𝑒 · 𝑍))) |
127 | 126 | breq1d 3795 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ↔ (𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2)))) |
128 | 126 | oveq1d 5547 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐺‘𝑒) + (𝑥 / 2)) = ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))) |
129 | 128 | breq2d 3797 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑦 < ((𝐺‘𝑒) + (𝑥 / 2)) ↔ 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)))) |
130 | 127, 129 | anbi12d 456 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2))) ↔ ((𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))))) |
131 | 122, 130 | mpbid 145 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)))) |
132 | 131 | simpld 110 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2))) |
133 | 52, 59, 55, 132 | ltadd1dd 7656 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)) < ((𝑦 + (𝑥 / 2)) + (𝑥 / 2))) |
134 | 51, 56, 60, 95, 133 | lttrd 7235 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < ((𝑦 + (𝑥 / 2)) + (𝑥 / 2))) |
135 | 58 | recnd 7147 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 ∈ ℂ) |
136 | 55 | recnd 7147 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑥 / 2) ∈ ℂ) |
137 | 135, 136,
136 | addassd 7141 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝑦 + (𝑥 / 2)) + (𝑥 / 2)) = (𝑦 + ((𝑥 / 2) + (𝑥 / 2)))) |
138 | 134, 137 | breqtrd 3809 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < (𝑦 + ((𝑥 / 2) + (𝑥 / 2)))) |
139 | 53 | rpcnd 8775 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℂ) |
140 | 139 | 2halvesd 8276 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥) |
141 | 140 | oveq2d 5548 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝑦 + ((𝑥 / 2) + (𝑥 / 2))) = (𝑦 + 𝑥)) |
142 | 138, 141 | breqtrd 3809 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < (𝑦 + 𝑥)) |
143 | 51, 55 | readdcld 7148 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + (𝑥 / 2)) ∈ ℝ) |
144 | 143, 55 | readdcld 7148 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2)) ∈ ℝ) |
145 | 131 | simprd 112 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))) |
146 | 51, 62 | readdcld 7148 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ∈ ℝ) |
147 | 83 | simpld 110 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍)))) |
148 | 62, 55, 51, 93 | leadd2dd 7660 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ≤ ((𝐹‘𝑖) + (𝑥 / 2))) |
149 | 52, 146, 143, 147, 148 | ltletrd 7527 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝑥 / 2))) |
150 | 52, 143, 55, 149 | ltadd1dd 7656 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)) < (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2))) |
151 | 58, 56, 144, 145, 150 | lttrd 7235 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 < (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2))) |
152 | 51 | recnd 7147 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) ∈ ℂ) |
153 | 152, 136,
136 | addassd 7141 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2)) = ((𝐹‘𝑖) + ((𝑥 / 2) + (𝑥 / 2)))) |
154 | 151, 153 | breqtrd 3809 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 < ((𝐹‘𝑖) + ((𝑥 / 2) + (𝑥 / 2)))) |
155 | 140 | oveq2d 5548 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + ((𝑥 / 2) + (𝑥 / 2))) = ((𝐹‘𝑖) + 𝑥)) |
156 | 154, 155 | breqtrd 3809 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → 𝑦 < ((𝐹‘𝑖) + 𝑥)) |
157 | 142, 156 | jca 300 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
158 | 157 | ralrimiva 2434 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → ∀𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
159 | | fveq2 5198 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑒 · 𝑍) → (ℤ≥‘𝑗) =
(ℤ≥‘(𝑒 · 𝑍))) |
160 | 159 | raleqdv 2555 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑒 · 𝑍) → (∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)) ↔ ∀𝑖 ∈ (ℤ≥‘(𝑒 · 𝑍))((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))) |
161 | 160 | rspcev 2701 |
. . . . . . . . 9
⊢ (((𝑒 · 𝑍) ∈ ℕ ∧ ∀𝑖 ∈
(ℤ≥‘(𝑒 · 𝑍))((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
162 | 44, 158, 161 | syl2anc 403 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
163 | 41, 162 | rexlimddv 2481 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧
∀𝑐 ∈
ℝ+ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
164 | 27, 163 | rexlimddv 2481 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑤 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
165 | 15, 164 | sylbi 119 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
166 | 165 | ralrimiva 2434 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |
167 | 166 | ex 113 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑐 ∈ ℝ+
∃𝑎 ∈ ℕ
∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))) |
168 | 167 | reximdva 2463 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑐 ∈ ℝ+ ∃𝑎 ∈ ℕ ∀𝑏 ∈
(ℤ≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))) |
169 | 9, 168 | mpd 13 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) |