Proof of Theorem climleltrp
Step | Hyp | Ref
| Expression |
1 | | climleltrp.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
2 | | climleltrp.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
3 | 1, 2 | eleqtrdi 2843 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
4 | | uzss 12340 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
6 | 5, 2 | sseqtrrdi 3926 |
. 2
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆ 𝑍) |
7 | | climleltrp.k |
. . . 4
⊢
Ⅎ𝑘𝜑 |
8 | | climleltrp.f |
. . . 4
⊢
Ⅎ𝑘𝐹 |
9 | | uzssz 12338 |
. . . . 5
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
10 | 9, 3 | sseldi 3873 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
11 | | eqid 2738 |
. . . 4
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
12 | | climleltrp.a |
. . . 4
⊢ (𝜑 → 𝐹 ⇝ 𝐴) |
13 | | eqidd 2739 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
14 | | climleltrp.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
15 | 7, 8, 10, 11, 12, 13, 14 | clim2d 42740 |
. . 3
⊢ (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑁)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋)) |
16 | | nfv 1920 |
. . . . . 6
⊢
Ⅎ𝑘 𝑗 ∈
(ℤ≥‘𝑁) |
17 | 7, 16 | nfan 1905 |
. . . . 5
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) |
18 | | simplll 775 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝜑) |
19 | | uzss 12340 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑁) → (ℤ≥‘𝑗) ⊆
(ℤ≥‘𝑁)) |
20 | 19 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) →
(ℤ≥‘𝑗) ⊆ (ℤ≥‘𝑁)) |
21 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ (ℤ≥‘𝑗)) |
22 | 20, 21 | sseldd 3876 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ (ℤ≥‘𝑁)) |
23 | 22 | adantr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝑘 ∈ (ℤ≥‘𝑁)) |
24 | | simpr 488 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) |
25 | | climleltrp.r |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ) |
26 | 13, 25 | eqeltrd 2833 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ) |
27 | 26 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) ∈ ℝ) |
28 | | climcl 14939 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ) |
29 | 12, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ ℂ) |
30 | 29 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → 𝐴 ∈ ℂ) |
31 | 26 | recnd 10740 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑘) ∈ ℂ) |
32 | 30, 31 | pncan3d 11071 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) = (𝐹‘𝑘)) |
33 | 32 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑘) = (𝐴 + ((𝐹‘𝑘) − 𝐴))) |
34 | 33 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) = (𝐴 + ((𝐹‘𝑘) − 𝐴))) |
35 | 34, 27 | eqeltrrd 2834 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) ∈ ℝ) |
36 | | climleltrp.c |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℝ) |
37 | 36 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐶 ∈ ℝ) |
38 | 7, 8, 11, 10, 12, 25 | climreclf 42731 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ ℝ) |
39 | 38 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐴 ∈ ℝ) |
40 | 27, 39 | resubcld 11139 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ℝ) |
41 | 37, 40 | readdcld 10741 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐶 + ((𝐹‘𝑘) − 𝐴)) ∈ ℝ) |
42 | 14 | rpred 12507 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ ℝ) |
43 | 42 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝑋 ∈ ℝ) |
44 | 37, 43 | readdcld 10741 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐶 + 𝑋) ∈ ℝ) |
45 | | climleltrp.l |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≤ 𝐶) |
46 | 45 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐴 ≤ 𝐶) |
47 | 39, 37, 40, 46 | leadd1dd 11325 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) ≤ (𝐶 + ((𝐹‘𝑘) − 𝐴))) |
48 | 31 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) ∈ ℂ) |
49 | 30 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐴 ∈ ℂ) |
50 | 48, 49 | subcld 11068 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ℂ) |
51 | 50 | abscld 14879 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (abs‘((𝐹‘𝑘) − 𝐴)) ∈ ℝ) |
52 | 40 | leabsd 14857 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) ≤ (abs‘((𝐹‘𝑘) − 𝐴))) |
53 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) |
54 | 40, 51, 43, 52, 53 | lelttrd 10869 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) < 𝑋) |
55 | 40, 43, 37, 54 | ltadd2dd 10870 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐶 + ((𝐹‘𝑘) − 𝐴)) < (𝐶 + 𝑋)) |
56 | 35, 41, 44, 47, 55 | lelttrd 10869 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) < (𝐶 + 𝑋)) |
57 | 34, 56 | eqbrtrd 5049 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) < (𝐶 + 𝑋)) |
58 | 27, 57 | jca 515 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))) |
59 | 18, 23, 24, 58 | syl21anc 837 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))) |
60 | 59 | adantrl 716 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋)) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))) |
61 | 60 | ex 416 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))) |
62 | 17, 61 | ralimdaa 3128 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) → (∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))) |
63 | 62 | reximdva 3183 |
. . 3
⊢ (𝜑 → (∃𝑗 ∈ (ℤ≥‘𝑁)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ∃𝑗 ∈ (ℤ≥‘𝑁)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))) |
64 | 15, 63 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑁)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))) |
65 | | ssrexv 3942 |
. 2
⊢
((ℤ≥‘𝑁) ⊆ 𝑍 → (∃𝑗 ∈ (ℤ≥‘𝑁)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))) |
66 | 6, 64, 65 | sylc 65 |
1
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))) |