Step | Hyp | Ref
| Expression |
1 | | xlimmnfv.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | 1 | ad2antrr 725 |
. . . 4
⊢ (((𝜑 ∧ 𝐹~~>*-∞) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℤ) |
3 | | xlimmnfv.z |
. . . 4
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | | xlimmnfv.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
5 | 4 | ad2antrr 725 |
. . . 4
⊢ (((𝜑 ∧ 𝐹~~>*-∞) ∧ 𝑥 ∈ ℝ) → 𝐹:𝑍⟶ℝ*) |
6 | | simplr 768 |
. . . 4
⊢ (((𝜑 ∧ 𝐹~~>*-∞) ∧ 𝑥 ∈ ℝ) → 𝐹~~>*-∞) |
7 | | simpr 488 |
. . . 4
⊢ (((𝜑 ∧ 𝐹~~>*-∞) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
8 | 2, 3, 5, 6, 7 | xlimmnfvlem1 42474 |
. . 3
⊢ (((𝜑 ∧ 𝐹~~>*-∞) ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) |
9 | 8 | ralrimiva 3149 |
. 2
⊢ ((𝜑 ∧ 𝐹~~>*-∞) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) |
10 | | nfv 1915 |
. . . 4
⊢
Ⅎ𝑘𝜑 |
11 | | nfcv 2955 |
. . . . 5
⊢
Ⅎ𝑘ℝ |
12 | | nfcv 2955 |
. . . . . 6
⊢
Ⅎ𝑘𝑍 |
13 | | nfra1 3183 |
. . . . . 6
⊢
Ⅎ𝑘∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥 |
14 | 12, 13 | nfrex 3268 |
. . . . 5
⊢
Ⅎ𝑘∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥 |
15 | 11, 14 | nfralw 3189 |
. . . 4
⊢
Ⅎ𝑘∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥 |
16 | 10, 15 | nfan 1900 |
. . 3
⊢
Ⅎ𝑘(𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) |
17 | | nfv 1915 |
. . . 4
⊢
Ⅎ𝑗𝜑 |
18 | | nfcv 2955 |
. . . . 5
⊢
Ⅎ𝑗ℝ |
19 | | nfre1 3265 |
. . . . 5
⊢
Ⅎ𝑗∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥 |
20 | 18, 19 | nfralw 3189 |
. . . 4
⊢
Ⅎ𝑗∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥 |
21 | 17, 20 | nfan 1900 |
. . 3
⊢
Ⅎ𝑗(𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) |
22 | 1 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) → 𝑀 ∈ ℤ) |
23 | 4 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) → 𝐹:𝑍⟶ℝ*) |
24 | | nfv 1915 |
. . . . . 6
⊢
Ⅎ𝑗 𝑦 ∈ ℝ |
25 | 21, 24 | nfan 1900 |
. . . . 5
⊢
Ⅎ𝑗((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∧ 𝑦 ∈ ℝ) |
26 | 4 | 3ad2ant1 1130 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐹:𝑍⟶ℝ*) |
27 | 3 | uztrn2 12250 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
28 | 27 | 3adant1 1127 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
29 | 26, 28 | ffvelrnd 6829 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈
ℝ*) |
30 | 29 | ad5ant134 1364 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) ≤ (𝑦 − 1)) → (𝐹‘𝑘) ∈
ℝ*) |
31 | | simp-4r 783 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) ≤ (𝑦 − 1)) → 𝑦 ∈ ℝ) |
32 | | peano2rem 10942 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → (𝑦 − 1) ∈
ℝ) |
33 | 32 | rexrd 10680 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → (𝑦 − 1) ∈
ℝ*) |
34 | 31, 33 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) ≤ (𝑦 − 1)) → (𝑦 − 1) ∈
ℝ*) |
35 | | rexr 10676 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ*) |
36 | 35 | ad4antlr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) ≤ (𝑦 − 1)) → 𝑦 ∈ ℝ*) |
37 | | simpr 488 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) ≤ (𝑦 − 1)) → (𝐹‘𝑘) ≤ (𝑦 − 1)) |
38 | 31 | ltm1d 11561 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) ≤ (𝑦 − 1)) → (𝑦 − 1) < 𝑦) |
39 | 30, 34, 36, 37, 38 | xrlelttrd 12541 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) ≤ (𝑦 − 1)) → (𝐹‘𝑘) < 𝑦) |
40 | 39 | ex 416 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘) ≤ (𝑦 − 1) → (𝐹‘𝑘) < 𝑦)) |
41 | 40 | ralimdva 3144 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ (𝑦 − 1) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑦)) |
42 | 41 | imp 410 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ (𝑦 − 1)) → ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑦) |
43 | 42 | adantl3r 749 |
. . . . . 6
⊢
(((((𝜑 ∧
∀𝑥 ∈ ℝ
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ (𝑦 − 1)) → ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑦) |
44 | 43 | 3impa 1107 |
. . . . 5
⊢ ((((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ (𝑦 − 1)) → ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑦) |
45 | 32 | adantl 485 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℝ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥 ∧ 𝑦 ∈ ℝ) → (𝑦 − 1) ∈ ℝ) |
46 | | simpl 486 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℝ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥 ∧ 𝑦 ∈ ℝ) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) |
47 | | breq2 5034 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 − 1) → ((𝐹‘𝑘) ≤ 𝑥 ↔ (𝐹‘𝑘) ≤ (𝑦 − 1))) |
48 | 47 | ralbidv 3162 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 − 1) → (∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ (𝑦 − 1))) |
49 | 48 | rexbidv 3256 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 − 1) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ (𝑦 − 1))) |
50 | 49 | rspcva 3569 |
. . . . . . 7
⊢ (((𝑦 − 1) ∈ ℝ ∧
∀𝑥 ∈ ℝ
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ (𝑦 − 1)) |
51 | 45, 46, 50 | syl2anc 587 |
. . . . . 6
⊢
((∀𝑥 ∈
ℝ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥 ∧ 𝑦 ∈ ℝ) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ (𝑦 − 1)) |
52 | 51 | adantll 713 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ (𝑦 − 1)) |
53 | 25, 44, 52 | reximdd 41789 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑦) |
54 | 53 | ralrimiva 3149 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) → ∀𝑦 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑦) |
55 | 16, 21, 22, 3, 23, 54 | xlimmnfvlem2 42475 |
. 2
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) → 𝐹~~>*-∞) |
56 | 9, 55 | impbida 800 |
1
⊢ (𝜑 → (𝐹~~>*-∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥)) |