Proof of Theorem resqrexlemga
Step | Hyp | Ref
| Expression |
1 | | resqrexlemex.seq |
. . . . . . . . . . 11
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)})) |
2 | | resqrexlemex.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | | resqrexlemex.agt0 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝐴) |
4 | 1, 2, 3 | resqrexlemf 10971 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶ℝ+) |
5 | 4 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝐹:ℕ⟶ℝ+) |
6 | | 1nn 8889 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
7 | 6 | a1i 9 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 1 ∈
ℕ) |
8 | 5, 7 | ffvelrnd 5632 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝐹‘1) ∈
ℝ+) |
9 | | 2z 9240 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
10 | 9 | a1i 9 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 2 ∈
ℤ) |
11 | 8, 10 | rpexpcld 10633 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → ((𝐹‘1)↑2) ∈
ℝ+) |
12 | | simpr 109 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ+) |
13 | 11, 12 | rpdivcld 9671 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (((𝐹‘1)↑2) / 𝑒) ∈
ℝ+) |
14 | 13 | rpred 9653 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (((𝐹‘1)↑2) / 𝑒) ∈
ℝ) |
15 | | 1red 7935 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 1 ∈
ℝ) |
16 | 14, 15 | readdcld 7949 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → ((((𝐹‘1)↑2) / 𝑒) + 1) ∈
ℝ) |
17 | | arch 9132 |
. . . 4
⊢
(((((𝐹‘1)↑2) / 𝑒) + 1) ∈ ℝ → ∃𝑗 ∈ ℕ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) |
18 | 16, 17 | syl 14 |
. . 3
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑗 ∈ ℕ
((((𝐹‘1)↑2) /
𝑒) + 1) < 𝑗) |
19 | | simpllr 529 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑗 ∈ ℕ) |
20 | | simpr 109 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ (ℤ≥‘𝑗)) |
21 | | eluznn 9559 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
22 | 19, 20, 21 | syl2anc 409 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
23 | | simplll 528 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) → 𝜑) |
24 | 23 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝜑) |
25 | 24, 4 | syl 14 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐹:ℕ⟶ℝ+) |
26 | 25, 22 | ffvelrnd 5632 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈
ℝ+) |
27 | 9 | a1i 9 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 2 ∈
ℤ) |
28 | 26, 27 | rpexpcld 10633 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘)↑2) ∈
ℝ+) |
29 | | fveq2 5496 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → (𝐹‘𝑥) = (𝐹‘𝑘)) |
30 | 29 | oveq1d 5868 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → ((𝐹‘𝑥)↑2) = ((𝐹‘𝑘)↑2)) |
31 | | resqrexlemsqa.g |
. . . . . . . . . 10
⊢ 𝐺 = (𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2)) |
32 | 30, 31 | fvmptg 5572 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ ((𝐹‘𝑘)↑2) ∈ ℝ+) →
(𝐺‘𝑘) = ((𝐹‘𝑘)↑2)) |
33 | 22, 28, 32 | syl2anc 409 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐺‘𝑘) = ((𝐹‘𝑘)↑2)) |
34 | 28 | rpred 9653 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘)↑2) ∈ ℝ) |
35 | 24, 2 | syl 14 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐴 ∈ ℝ) |
36 | 34, 35 | resubcld 8300 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)↑2) − 𝐴) ∈ ℝ) |
37 | 11 | ad3antrrr 489 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘1)↑2) ∈
ℝ+) |
38 | 37 | rpred 9653 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘1)↑2) ∈
ℝ) |
39 | | 4re 8955 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℝ |
40 | | 4pos 8975 |
. . . . . . . . . . . . . 14
⊢ 0 <
4 |
41 | 39, 40 | elrpii 9613 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℝ+ |
42 | 41 | a1i 9 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 4 ∈
ℝ+) |
43 | | nnm1nn0 9176 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) |
44 | 22, 43 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝑘 − 1) ∈
ℕ0) |
45 | 44 | nn0zd 9332 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝑘 − 1) ∈ ℤ) |
46 | 42, 45 | rpexpcld 10633 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (4↑(𝑘 − 1)) ∈
ℝ+) |
47 | 38, 46 | rerpdivcld 9685 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘1)↑2) / (4↑(𝑘 − 1))) ∈
ℝ) |
48 | 12 | ad3antrrr 489 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑒 ∈ ℝ+) |
49 | 48 | rpred 9653 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑒 ∈ ℝ) |
50 | 1, 2, 3 | resqrexlemcalc3 10980 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑘)↑2) − 𝐴) ≤ (((𝐹‘1)↑2) / (4↑(𝑘 − 1)))) |
51 | 24, 22, 50 | syl2anc 409 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)↑2) − 𝐴) ≤ (((𝐹‘1)↑2) / (4↑(𝑘 − 1)))) |
52 | 14 | ad3antrrr 489 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘1)↑2) / 𝑒) ∈ ℝ) |
53 | 22 | nnred 8891 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ ℝ) |
54 | | 1red 7935 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 1 ∈
ℝ) |
55 | 53, 54 | resubcld 8300 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝑘 − 1) ∈ ℝ) |
56 | 39 | a1i 9 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 4 ∈
ℝ) |
57 | 56, 44 | reexpcld 10626 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (4↑(𝑘 − 1)) ∈
ℝ) |
58 | 16 | ad3antrrr 489 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((((𝐹‘1)↑2) / 𝑒) + 1) ∈ ℝ) |
59 | 19 | nnred 8891 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑗 ∈ ℝ) |
60 | | simplr 525 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) |
61 | | eluzle 9499 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
(ℤ≥‘𝑗) → 𝑗 ≤ 𝑘) |
62 | 61 | adantl 275 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑗 ≤ 𝑘) |
63 | 58, 59, 53, 60, 62 | ltletrd 8342 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑘) |
64 | 52, 54, 53 | ltaddsubd 8464 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑘 ↔ (((𝐹‘1)↑2) / 𝑒) < (𝑘 − 1))) |
65 | 63, 64 | mpbid 146 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘1)↑2) / 𝑒) < (𝑘 − 1)) |
66 | | 4z 9242 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℤ |
67 | | 2re 8948 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
68 | | 2lt4 9051 |
. . . . . . . . . . . . . . 15
⊢ 2 <
4 |
69 | 67, 39, 68 | ltleii 8022 |
. . . . . . . . . . . . . 14
⊢ 2 ≤
4 |
70 | | eluz2 9493 |
. . . . . . . . . . . . . 14
⊢ (4 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 4 ∈
ℤ ∧ 2 ≤ 4)) |
71 | 9, 66, 69, 70 | mpbir3an 1174 |
. . . . . . . . . . . . 13
⊢ 4 ∈
(ℤ≥‘2) |
72 | | bernneq3 10598 |
. . . . . . . . . . . . 13
⊢ ((4
∈ (ℤ≥‘2) ∧ (𝑘 − 1) ∈ ℕ0)
→ (𝑘 − 1) <
(4↑(𝑘 −
1))) |
73 | 71, 44, 72 | sylancr 412 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝑘 − 1) < (4↑(𝑘 − 1))) |
74 | 52, 55, 57, 65, 73 | lttrd 8045 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘1)↑2) / 𝑒) < (4↑(𝑘 − 1))) |
75 | 38, 48, 46, 74 | ltdiv23d 9714 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘1)↑2) / (4↑(𝑘 − 1))) < 𝑒) |
76 | 36, 47, 49, 51, 75 | lelttrd 8044 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)↑2) − 𝐴) < 𝑒) |
77 | 34, 35, 49 | ltsubadd2d 8462 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((((𝐹‘𝑘)↑2) − 𝐴) < 𝑒 ↔ ((𝐹‘𝑘)↑2) < (𝐴 + 𝑒))) |
78 | 76, 77 | mpbid 146 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘)↑2) < (𝐴 + 𝑒)) |
79 | 33, 78 | eqbrtrd 4011 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐺‘𝑘) < (𝐴 + 𝑒)) |
80 | 33, 28 | eqeltrd 2247 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐺‘𝑘) ∈
ℝ+) |
81 | 80 | rpred 9653 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐺‘𝑘) ∈ ℝ) |
82 | 81, 49 | readdcld 7949 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐺‘𝑘) + 𝑒) ∈ ℝ) |
83 | 1, 2, 3 | resqrexlemover 10974 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 < ((𝐹‘𝑘)↑2)) |
84 | 24, 22, 83 | syl2anc 409 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐴 < ((𝐹‘𝑘)↑2)) |
85 | 84, 33 | breqtrrd 4017 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐴 < (𝐺‘𝑘)) |
86 | 81, 48 | ltaddrpd 9687 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐺‘𝑘) < ((𝐺‘𝑘) + 𝑒)) |
87 | 35, 81, 82, 85, 86 | lttrd 8045 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐴 < ((𝐺‘𝑘) + 𝑒)) |
88 | 79, 87 | jca 304 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑗 ∈ ℕ)
∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐺‘𝑘) < (𝐴 + 𝑒) ∧ 𝐴 < ((𝐺‘𝑘) + 𝑒))) |
89 | 88 | ralrimiva 2543 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ ((((𝐹‘1)↑2) / 𝑒) + 1) < 𝑗) → ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘) < (𝐴 + 𝑒) ∧ 𝐴 < ((𝐺‘𝑘) + 𝑒))) |
90 | 89 | ex 114 |
. . . 4
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(((((𝐹‘1)↑2) /
𝑒) + 1) < 𝑗 → ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘) < (𝐴 + 𝑒) ∧ 𝐴 < ((𝐺‘𝑘) + 𝑒)))) |
91 | 90 | reximdva 2572 |
. . 3
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑗 ∈ ℕ
((((𝐹‘1)↑2) /
𝑒) + 1) < 𝑗 → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘) < (𝐴 + 𝑒) ∧ 𝐴 < ((𝐺‘𝑘) + 𝑒)))) |
92 | 18, 91 | mpd 13 |
. 2
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘) < (𝐴 + 𝑒) ∧ 𝐴 < ((𝐺‘𝑘) + 𝑒))) |
93 | 92 | ralrimiva 2543 |
1
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘) < (𝐴 + 𝑒) ∧ 𝐴 < ((𝐺‘𝑘) + 𝑒))) |