Proof of Theorem dfxlim2v
| Step | Hyp | Ref
| Expression |
| 1 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 ∈ ℝ) → 𝐹~~>*𝐴) |
| 2 | | dfxlim2v.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 3 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ ℝ) → 𝑀 ∈ ℤ) |
| 4 | | dfxlim2v.2 |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 5 | | dfxlim2v.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
| 6 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ ℝ) → 𝐹:𝑍⟶ℝ*) |
| 7 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ ℝ) → 𝐴 ∈ ℝ) |
| 8 | 3, 4, 6, 7 | xlimclim2 45855 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ ℝ) → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴)) |
| 9 | 8 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 ∈ ℝ) → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴)) |
| 10 | 1, 9 | mpbid 232 |
. . . 4
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 ∈ ℝ) → 𝐹 ⇝ 𝐴) |
| 11 | 10 | 3mix1d 1337 |
. . 3
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 ∈ ℝ) → (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))) |
| 12 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 = -∞) → 𝐴 = -∞) |
| 13 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐹~~>*𝐴 ∧ 𝐴 = -∞) → 𝐹~~>*𝐴) |
| 14 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐹~~>*𝐴 ∧ 𝐴 = -∞) → 𝐴 = -∞) |
| 15 | 13, 14 | breqtrd 5169 |
. . . . . . . 8
⊢ ((𝐹~~>*𝐴 ∧ 𝐴 = -∞) → 𝐹~~>*-∞) |
| 16 | 15 | adantll 714 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 = -∞) → 𝐹~~>*-∞) |
| 17 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝐹 |
| 18 | 17, 2, 4, 5 | xlimmnf 45856 |
. . . . . . . 8
⊢ (𝜑 → (𝐹~~>*-∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥)) |
| 19 | 18 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 = -∞) → (𝐹~~>*-∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥)) |
| 20 | 16, 19 | mpbid 232 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 = -∞) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) |
| 21 | | 3mix2 1332 |
. . . . . 6
⊢ ((𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) → (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))) |
| 22 | 12, 20, 21 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 = -∞) → (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))) |
| 23 | 22 | adantlr 715 |
. . . 4
⊢ ((((𝜑 ∧ 𝐹~~>*𝐴) ∧ ¬ 𝐴 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))) |
| 24 | | simpll 767 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐹~~>*𝐴) ∧ ¬ 𝐴 ∈ ℝ) ∧ ¬ 𝐴 = -∞) → (𝜑 ∧ 𝐹~~>*𝐴)) |
| 25 | | xlimcl 45837 |
. . . . . . 7
⊢ (𝐹~~>*𝐴 → 𝐴 ∈
ℝ*) |
| 26 | 25 | ad3antlr 731 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹~~>*𝐴) ∧ ¬ 𝐴 ∈ ℝ) ∧ ¬ 𝐴 = -∞) → 𝐴 ∈
ℝ*) |
| 27 | | simplr 769 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹~~>*𝐴) ∧ ¬ 𝐴 ∈ ℝ) ∧ ¬ 𝐴 = -∞) → ¬ 𝐴 ∈
ℝ) |
| 28 | | neqne 2948 |
. . . . . . 7
⊢ (¬
𝐴 = -∞ → 𝐴 ≠ -∞) |
| 29 | 28 | adantl 481 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹~~>*𝐴) ∧ ¬ 𝐴 ∈ ℝ) ∧ ¬ 𝐴 = -∞) → 𝐴 ≠ -∞) |
| 30 | 26, 27, 29 | xrnmnfpnf 45088 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐹~~>*𝐴) ∧ ¬ 𝐴 ∈ ℝ) ∧ ¬ 𝐴 = -∞) → 𝐴 = +∞) |
| 31 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
| 32 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐹~~>*𝐴 ∧ 𝐴 = +∞) → 𝐹~~>*𝐴) |
| 33 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐹~~>*𝐴 ∧ 𝐴 = +∞) → 𝐴 = +∞) |
| 34 | 32, 33 | breqtrd 5169 |
. . . . . . . 8
⊢ ((𝐹~~>*𝐴 ∧ 𝐴 = +∞) → 𝐹~~>*+∞) |
| 35 | 34 | adantll 714 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 = +∞) → 𝐹~~>*+∞) |
| 36 | 17, 2, 4, 5 | xlimpnf 45857 |
. . . . . . . 8
⊢ (𝜑 → (𝐹~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘))) |
| 37 | 36 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 = +∞) → (𝐹~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘))) |
| 38 | 35, 37 | mpbid 232 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 = +∞) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)) |
| 39 | | 3mix3 1333 |
. . . . . 6
⊢ ((𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)) → (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))) |
| 40 | 31, 38, 39 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ 𝐴 = +∞) → (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))) |
| 41 | 24, 30, 40 | syl2anc 584 |
. . . 4
⊢ ((((𝜑 ∧ 𝐹~~>*𝐴) ∧ ¬ 𝐴 ∈ ℝ) ∧ ¬ 𝐴 = -∞) → (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))) |
| 42 | 23, 41 | pm2.61dan 813 |
. . 3
⊢ (((𝜑 ∧ 𝐹~~>*𝐴) ∧ ¬ 𝐴 ∈ ℝ) → (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))) |
| 43 | 11, 42 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ 𝐹~~>*𝐴) → (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))) |
| 44 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ⇝ 𝐴) → 𝑀 ∈ ℤ) |
| 45 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ⇝ 𝐴) → 𝐹:𝑍⟶ℝ*) |
| 46 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ⇝ 𝐴) → 𝐹 ⇝ 𝐴) |
| 47 | 44, 4, 45, 46 | climxlim2 45861 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ⇝ 𝐴) → 𝐹~~>*𝐴) |
| 48 | 18 | biimpar 477 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) → 𝐹~~>*-∞) |
| 49 | 48 | adantrl 716 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥)) → 𝐹~~>*-∞) |
| 50 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥)) → 𝐴 = -∞) |
| 51 | 49, 50 | breqtrrd 5171 |
. . 3
⊢ ((𝜑 ∧ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥)) → 𝐹~~>*𝐴) |
| 52 | 36 | biimpar 477 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)) → 𝐹~~>*+∞) |
| 53 | 52 | adantrl 716 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘))) → 𝐹~~>*+∞) |
| 54 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘))) → 𝐴 = +∞) |
| 55 | 53, 54 | breqtrrd 5171 |
. . 3
⊢ ((𝜑 ∧ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘))) → 𝐹~~>*𝐴) |
| 56 | 47, 51, 55 | 3jaodan 1433 |
. 2
⊢ ((𝜑 ∧ (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))) → 𝐹~~>*𝐴) |
| 57 | 43, 56 | impbida 801 |
1
⊢ (𝜑 → (𝐹~~>*𝐴 ↔ (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘))))) |