Step | Hyp | Ref
| Expression |
1 | | resqrexlemex.seq |
. . . . . . 7
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)})) |
2 | | resqrexlemex.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | | resqrexlemex.agt0 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝐴) |
4 | 1, 2, 3 | resqrexlemf 10971 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶ℝ+) |
5 | 4 | ffvelrnda 5631 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈
ℝ+) |
6 | | 2z 9240 |
. . . . . 6
⊢ 2 ∈
ℤ |
7 | 6 | a1i 9 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 2 ∈
ℤ) |
8 | 5, 7 | rpexpcld 10633 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥)↑2) ∈
ℝ+) |
9 | | eqid 2170 |
. . . 4
⊢ (𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2)) = (𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2)) |
10 | 8, 9 | fmptd 5650 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2)):ℕ⟶ℝ+) |
11 | | rpssre 9621 |
. . . 4
⊢
ℝ+ ⊆ ℝ |
12 | 11 | a1i 9 |
. . 3
⊢ (𝜑 → ℝ+
⊆ ℝ) |
13 | 10, 12 | fssd 5360 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2)):ℕ⟶ℝ) |
14 | | resqrexlemgt0.rr |
. . 3
⊢ (𝜑 → 𝐿 ∈ ℝ) |
15 | 14 | resqcld 10635 |
. 2
⊢ (𝜑 → (𝐿↑2) ∈ ℝ) |
16 | | resqrexlemgt0.lim |
. . . 4
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒))) |
17 | | oveq2 5861 |
. . . . . . . . 9
⊢ (𝑒 = 𝑎 → (𝐿 + 𝑒) = (𝐿 + 𝑎)) |
18 | 17 | breq2d 4001 |
. . . . . . . 8
⊢ (𝑒 = 𝑎 → ((𝐹‘𝑖) < (𝐿 + 𝑒) ↔ (𝐹‘𝑖) < (𝐿 + 𝑎))) |
19 | | oveq2 5861 |
. . . . . . . . 9
⊢ (𝑒 = 𝑎 → ((𝐹‘𝑖) + 𝑒) = ((𝐹‘𝑖) + 𝑎)) |
20 | 19 | breq2d 4001 |
. . . . . . . 8
⊢ (𝑒 = 𝑎 → (𝐿 < ((𝐹‘𝑖) + 𝑒) ↔ 𝐿 < ((𝐹‘𝑖) + 𝑎))) |
21 | 18, 20 | anbi12d 470 |
. . . . . . 7
⊢ (𝑒 = 𝑎 → (((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) ↔ ((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎)))) |
22 | 21 | rexralbidv 2496 |
. . . . . 6
⊢ (𝑒 = 𝑎 → (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) ↔ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎)))) |
23 | 22 | cbvralv 2696 |
. . . . 5
⊢
(∀𝑒 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) ↔ ∀𝑎 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎))) |
24 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑗 = 𝑏 → (ℤ≥‘𝑗) =
(ℤ≥‘𝑏)) |
25 | 24 | raleqdv 2671 |
. . . . . . 7
⊢ (𝑗 = 𝑏 → (∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎)) ↔ ∀𝑖 ∈ (ℤ≥‘𝑏)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎)))) |
26 | 25 | cbvrexv 2697 |
. . . . . 6
⊢
(∃𝑗 ∈
ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎)) ↔ ∃𝑏 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑏)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎))) |
27 | 26 | ralbii 2476 |
. . . . 5
⊢
(∀𝑎 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎)) ↔ ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑏)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎))) |
28 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑐 → (𝐹‘𝑖) = (𝐹‘𝑐)) |
29 | 28 | breq1d 3999 |
. . . . . . . . 9
⊢ (𝑖 = 𝑐 → ((𝐹‘𝑖) < (𝐿 + 𝑎) ↔ (𝐹‘𝑐) < (𝐿 + 𝑎))) |
30 | 28 | oveq1d 5868 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑐 → ((𝐹‘𝑖) + 𝑎) = ((𝐹‘𝑐) + 𝑎)) |
31 | 30 | breq2d 4001 |
. . . . . . . . 9
⊢ (𝑖 = 𝑐 → (𝐿 < ((𝐹‘𝑖) + 𝑎) ↔ 𝐿 < ((𝐹‘𝑐) + 𝑎))) |
32 | 29, 31 | anbi12d 470 |
. . . . . . . 8
⊢ (𝑖 = 𝑐 → (((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎)) ↔ ((𝐹‘𝑐) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑐) + 𝑎)))) |
33 | 32 | cbvralv 2696 |
. . . . . . 7
⊢
(∀𝑖 ∈
(ℤ≥‘𝑏)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎)) ↔ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝐹‘𝑐) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑐) + 𝑎))) |
34 | 33 | rexbii 2477 |
. . . . . 6
⊢
(∃𝑏 ∈
ℕ ∀𝑖 ∈
(ℤ≥‘𝑏)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎)) ↔ ∃𝑏 ∈ ℕ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝐹‘𝑐) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑐) + 𝑎))) |
35 | 34 | ralbii 2476 |
. . . . 5
⊢
(∀𝑎 ∈
ℝ+ ∃𝑏 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑏)((𝐹‘𝑖) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑎)) ↔ ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℕ ∀𝑐 ∈
(ℤ≥‘𝑏)((𝐹‘𝑐) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑐) + 𝑎))) |
36 | 23, 27, 35 | 3bitri 205 |
. . . 4
⊢
(∀𝑒 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) ↔ ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℕ ∀𝑐 ∈
(ℤ≥‘𝑏)((𝐹‘𝑐) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑐) + 𝑎))) |
37 | 16, 36 | sylib 121 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℕ ∀𝑐 ∈
(ℤ≥‘𝑏)((𝐹‘𝑐) < (𝐿 + 𝑎) ∧ 𝐿 < ((𝐹‘𝑐) + 𝑎))) |
38 | 1, 2, 3, 14, 37, 9 | resqrexlemglsq 10986 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℕ ∀𝑑 ∈
(ℤ≥‘𝑏)(((𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2))‘𝑑) < ((𝐿↑2) + 𝑎) ∧ (𝐿↑2) < (((𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2))‘𝑑) + 𝑎))) |
39 | 1, 2, 3, 14, 37, 9 | resqrexlemga 10987 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℕ ∀𝑑 ∈
(ℤ≥‘𝑏)(((𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2))‘𝑑) < (𝐴 + 𝑎) ∧ 𝐴 < (((𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2))‘𝑑) + 𝑎))) |
40 | 13, 15, 38, 2, 39 | recvguniq 10959 |
1
⊢ (𝜑 → (𝐿↑2) = 𝐴) |