# Metamath Proof Explorer

## Theorem lmxrge0

Description: Express "sequence F converges to plus infinity" (i.e. diverges), for a sequence of nonnegative extended real numbers. (Contributed by Thierry Arnoux, 2-Aug-2017)

Ref Expression
Hypotheses lmxrge0.j ${⊢}{J}=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$
lmxrge0.6 ${⊢}{\phi }\to {F}:ℕ⟶\left[0,\mathrm{+\infty }\right]$
lmxrge0.7 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({k}\right)={A}$
Assertion lmxrge0

### Proof

Step Hyp Ref Expression
1 lmxrge0.j ${⊢}{J}=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$
2 lmxrge0.6 ${⊢}{\phi }\to {F}:ℕ⟶\left[0,\mathrm{+\infty }\right]$
3 lmxrge0.7 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({k}\right)={A}$
4 eqid ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]={ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]$
5 xrstopn ${⊢}\mathrm{ordTop}\left(\le \right)=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}\right)$
6 4 5 resstopn ${⊢}\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$
7 1 6 eqtr4i ${⊢}{J}=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]$
8 letopon ${⊢}\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$
9 iccssxr ${⊢}\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$
10 resttopon ${⊢}\left(\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)\wedge \left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\right)\to \mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{TopOn}\left(\left[0,\mathrm{+\infty }\right]\right)$
11 8 9 10 mp2an ${⊢}\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{TopOn}\left(\left[0,\mathrm{+\infty }\right]\right)$
12 7 11 eqeltri ${⊢}{J}\in \mathrm{TopOn}\left(\left[0,\mathrm{+\infty }\right]\right)$
13 12 a1i ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left(\left[0,\mathrm{+\infty }\right]\right)$
14 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
15 1zzd ${⊢}{\phi }\to 1\in ℤ$
16 13 14 15 2 3 lmbrf
17 0xr ${⊢}0\in {ℝ}^{*}$
18 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
19 0lepnf ${⊢}0\le \mathrm{+\infty }$
20 ubicc2 ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge 0\le \mathrm{+\infty }\right)\to \mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$
21 17 18 19 20 mp3an ${⊢}\mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$
22 21 biantrur ${⊢}\forall {a}\in {J}\phantom{\rule{.4em}{0ex}}\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)↔\left(\mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]\wedge \forall {a}\in {J}\phantom{\rule{.4em}{0ex}}\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)\right)$
23 16 22 syl6bbr
24 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
25 18 a1i ${⊢}{x}\in ℝ\to \mathrm{+\infty }\in {ℝ}^{*}$
26 ltpnf ${⊢}{x}\in ℝ\to {x}<\mathrm{+\infty }$
27 ubioc1 ${⊢}\left({x}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge {x}<\mathrm{+\infty }\right)\to \mathrm{+\infty }\in \left({x},\mathrm{+\infty }\right]$
28 24 25 26 27 syl3anc ${⊢}{x}\in ℝ\to \mathrm{+\infty }\in \left({x},\mathrm{+\infty }\right]$
29 0ltpnf ${⊢}0<\mathrm{+\infty }$
30 ubioc1 ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge 0<\mathrm{+\infty }\right)\to \mathrm{+\infty }\in \left(0,\mathrm{+\infty }\right]$
31 17 18 29 30 mp3an ${⊢}\mathrm{+\infty }\in \left(0,\mathrm{+\infty }\right]$
32 28 31 jctir ${⊢}{x}\in ℝ\to \left(\mathrm{+\infty }\in \left({x},\mathrm{+\infty }\right]\wedge \mathrm{+\infty }\in \left(0,\mathrm{+\infty }\right]\right)$
33 elin ${⊢}\mathrm{+\infty }\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)↔\left(\mathrm{+\infty }\in \left({x},\mathrm{+\infty }\right]\wedge \mathrm{+\infty }\in \left(0,\mathrm{+\infty }\right]\right)$
34 32 33 sylibr ${⊢}{x}\in ℝ\to \mathrm{+\infty }\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)$
35 34 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \forall {a}\in {J}\phantom{\rule{.4em}{0ex}}\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)\right)\to \mathrm{+\infty }\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)$
36 letop ${⊢}\mathrm{ordTop}\left(\le \right)\in \mathrm{Top}$
37 ovex ${⊢}\left[0,\mathrm{+\infty }\right]\in \mathrm{V}$
38 iocpnfordt ${⊢}\left({x},\mathrm{+\infty }\right]\in \mathrm{ordTop}\left(\le \right)$
39 iocpnfordt ${⊢}\left(0,\mathrm{+\infty }\right]\in \mathrm{ordTop}\left(\le \right)$
40 inopn ${⊢}\left(\mathrm{ordTop}\left(\le \right)\in \mathrm{Top}\wedge \left({x},\mathrm{+\infty }\right]\in \mathrm{ordTop}\left(\le \right)\wedge \left(0,\mathrm{+\infty }\right]\in \mathrm{ordTop}\left(\le \right)\right)\to \left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\in \mathrm{ordTop}\left(\le \right)$
41 36 38 39 40 mp3an ${⊢}\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\in \mathrm{ordTop}\left(\le \right)$
42 elrestr ${⊢}\left(\mathrm{ordTop}\left(\le \right)\in \mathrm{Top}\wedge \left[0,\mathrm{+\infty }\right]\in \mathrm{V}\wedge \left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\in \mathrm{ordTop}\left(\le \right)\right)\to \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\cap \left[0,\mathrm{+\infty }\right]\in \left(\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]\right)$
43 36 37 41 42 mp3an ${⊢}\left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\cap \left[0,\mathrm{+\infty }\right]\in \left(\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]\right)$
44 inss2 ${⊢}\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\subseteq \left(0,\mathrm{+\infty }\right]$
45 iocssicc ${⊢}\left(0,\mathrm{+\infty }\right]\subseteq \left[0,\mathrm{+\infty }\right]$
46 44 45 sstri ${⊢}\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\subseteq \left[0,\mathrm{+\infty }\right]$
47 sseqin2 ${⊢}\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\subseteq \left[0,\mathrm{+\infty }\right]↔\left[0,\mathrm{+\infty }\right]\cap \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]$
48 46 47 mpbi ${⊢}\left[0,\mathrm{+\infty }\right]\cap \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]$
49 incom ${⊢}\left[0,\mathrm{+\infty }\right]\cap \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)=\left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\cap \left[0,\mathrm{+\infty }\right]$
50 48 49 eqtr3i ${⊢}\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]=\left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\cap \left[0,\mathrm{+\infty }\right]$
51 43 50 7 3eltr4i ${⊢}\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\in {J}$
52 51 a1i ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\in {J}$
53 eleq2 ${⊢}{a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\to \left(\mathrm{+\infty }\in {a}↔\mathrm{+\infty }\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\right)$
54 53 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\to \left(\mathrm{+\infty }\in {a}↔\mathrm{+\infty }\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\right)$
55 54 biimprd ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\to \left(\mathrm{+\infty }\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\to \mathrm{+\infty }\in {a}\right)$
56 simp-5r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\wedge {A}\in {a}\right)\to {x}\in ℝ$
57 56 rexrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\wedge {A}\in {a}\right)\to {x}\in {ℝ}^{*}$
58 simpr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\wedge {A}\in {a}\right)\to {A}\in {a}$
59 simp-4r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\wedge {A}\in {a}\right)\to {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]$
60 58 59 eleqtrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\wedge {A}\in {a}\right)\to {A}\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)$
61 elin ${⊢}{A}\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)↔\left({A}\in \left({x},\mathrm{+\infty }\right]\wedge {A}\in \left(0,\mathrm{+\infty }\right]\right)$
62 61 simplbi ${⊢}{A}\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\to {A}\in \left({x},\mathrm{+\infty }\right]$
63 60 62 syl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\wedge {A}\in {a}\right)\to {A}\in \left({x},\mathrm{+\infty }\right]$
64 elioc1 ${⊢}\left({x}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({A}\in \left({x},\mathrm{+\infty }\right]↔\left({A}\in {ℝ}^{*}\wedge {x}<{A}\wedge {A}\le \mathrm{+\infty }\right)\right)$
65 18 64 mpan2 ${⊢}{x}\in {ℝ}^{*}\to \left({A}\in \left({x},\mathrm{+\infty }\right]↔\left({A}\in {ℝ}^{*}\wedge {x}<{A}\wedge {A}\le \mathrm{+\infty }\right)\right)$
66 65 biimpa ${⊢}\left({x}\in {ℝ}^{*}\wedge {A}\in \left({x},\mathrm{+\infty }\right]\right)\to \left({A}\in {ℝ}^{*}\wedge {x}<{A}\wedge {A}\le \mathrm{+\infty }\right)$
67 66 simp2d ${⊢}\left({x}\in {ℝ}^{*}\wedge {A}\in \left({x},\mathrm{+\infty }\right]\right)\to {x}<{A}$
68 57 63 67 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\wedge {A}\in {a}\right)\to {x}<{A}$
69 68 ex ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\to \left({A}\in {a}\to {x}<{A}\right)$
70 69 ralimdva ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\wedge {l}\in ℕ\right)\to \left(\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\to \forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)$
71 70 reximdva ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\to \left(\exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)$
72 fveq2 ${⊢}{j}={l}\to {ℤ}_{\ge {j}}={ℤ}_{\ge {l}}$
73 72 raleqdv ${⊢}{j}={l}\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}↔\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)$
74 73 cbvrexv ${⊢}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}↔\exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{x}<{A}$
75 71 74 syl6ibr ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\to \left(\exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)$
76 55 75 imim12d ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {a}=\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\to \left(\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)\to \left(\mathrm{+\infty }\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\right)$
77 52 76 rspcimdv ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left(\forall {a}\in {J}\phantom{\rule{.4em}{0ex}}\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)\to \left(\mathrm{+\infty }\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\right)$
78 77 imp ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \forall {a}\in {J}\phantom{\rule{.4em}{0ex}}\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)\right)\to \left(\mathrm{+\infty }\in \left(\left({x},\mathrm{+\infty }\right]\cap \left(0,\mathrm{+\infty }\right]\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)$
79 35 78 mpd ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \forall {a}\in {J}\phantom{\rule{.4em}{0ex}}\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}$
80 79 ex ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left(\forall {a}\in {J}\phantom{\rule{.4em}{0ex}}\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)$
81 80 ralrimdva ${⊢}{\phi }\to \left(\forall {a}\in {J}\phantom{\rule{.4em}{0ex}}\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)$
82 simplll ${⊢}\left(\left(\left({\phi }\wedge {a}\in {J}\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\wedge \mathrm{+\infty }\in {a}\right)\to {\phi }$
83 simpllr ${⊢}\left(\left(\left({\phi }\wedge {a}\in {J}\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\wedge \mathrm{+\infty }\in {a}\right)\to {a}\in {J}$
84 simpr ${⊢}\left(\left(\left({\phi }\wedge {a}\in {J}\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\wedge \mathrm{+\infty }\in {a}\right)\to \mathrm{+\infty }\in {a}$
85 1 pnfneige0 ${⊢}\left({a}\in {J}\wedge \mathrm{+\infty }\in {a}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x},\mathrm{+\infty }\right]\subseteq {a}$
86 83 84 85 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {a}\in {J}\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\wedge \mathrm{+\infty }\in {a}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x},\mathrm{+\infty }\right]\subseteq {a}$
87 simplr ${⊢}\left(\left(\left({\phi }\wedge {a}\in {J}\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\wedge \mathrm{+\infty }\in {a}\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}$
88 r19.29r ${⊢}\left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x},\mathrm{+\infty }\right]\subseteq {a}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\left({x},\mathrm{+\infty }\right]\subseteq {a}\wedge \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)$
89 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\to {\phi }$
90 uznnssnn ${⊢}{l}\in ℕ\to {ℤ}_{\ge {l}}\subseteq ℕ$
91 90 ad2antlr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\to {ℤ}_{\ge {l}}\subseteq ℕ$
92 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\to {k}\in {ℤ}_{\ge {l}}$
93 91 92 sseldd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\to {k}\in ℕ$
94 89 93 jca ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\to \left({\phi }\wedge {k}\in ℕ\right)$
95 simp-4r ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\to {x}\in ℝ$
96 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\to \left({x},\mathrm{+\infty }\right]\subseteq {a}$
97 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {x}<{A}\right)\to \left({x},\mathrm{+\infty }\right]\subseteq {a}$
98 simplr ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge {x}<{A}\right)\to {x}\in ℝ$
99 98 rexrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge {x}<{A}\right)\to {x}\in {ℝ}^{*}$
100 2 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({k}\right)\in \left[0,\mathrm{+\infty }\right]$
101 3 100 eqeltrrd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in \left[0,\mathrm{+\infty }\right]$
102 9 101 sseldi ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in {ℝ}^{*}$
103 102 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge {x}<{A}\right)\to {A}\in {ℝ}^{*}$
104 simpr ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge {x}<{A}\right)\to {x}<{A}$
105 pnfge ${⊢}{A}\in {ℝ}^{*}\to {A}\le \mathrm{+\infty }$
106 103 105 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge {x}<{A}\right)\to {A}\le \mathrm{+\infty }$
107 65 biimpar ${⊢}\left({x}\in {ℝ}^{*}\wedge \left({A}\in {ℝ}^{*}\wedge {x}<{A}\wedge {A}\le \mathrm{+\infty }\right)\right)\to {A}\in \left({x},\mathrm{+\infty }\right]$
108 99 103 104 106 107 syl13anc ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge {x}<{A}\right)\to {A}\in \left({x},\mathrm{+\infty }\right]$
109 108 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {x}<{A}\right)\to {A}\in \left({x},\mathrm{+\infty }\right]$
110 97 109 sseldd ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {x}<{A}\right)\to {A}\in {a}$
111 110 ex ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\to \left({x}<{A}\to {A}\in {a}\right)$
112 94 95 96 111 syl21anc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {l}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {l}}\right)\to \left({x}<{A}\to {A}\in {a}\right)$
113 112 ralimdva ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\wedge {l}\in ℕ\right)\to \left(\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{x}<{A}\to \forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)$
114 113 reximdva ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\to \left(\exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{x}<{A}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)$
115 74 114 syl5bi ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({x},\mathrm{+\infty }\right]\subseteq {a}\right)\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)$
116 115 expimpd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left(\left(\left({x},\mathrm{+\infty }\right]\subseteq {a}\wedge \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)$
117 116 rexlimdva ${⊢}{\phi }\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\left({x},\mathrm{+\infty }\right]\subseteq {a}\wedge \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)$
118 88 117 syl5 ${⊢}{\phi }\to \left(\left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x},\mathrm{+\infty }\right]\subseteq {a}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)$
119 118 imp ${⊢}\left({\phi }\wedge \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x},\mathrm{+\infty }\right]\subseteq {a}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\right)\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}$
120 82 86 87 119 syl12anc ${⊢}\left(\left(\left({\phi }\wedge {a}\in {J}\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)\wedge \mathrm{+\infty }\in {a}\right)\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}$
121 120 exp31 ${⊢}\left({\phi }\wedge {a}\in {J}\right)\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\to \left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)\right)$
122 121 ralrimdva ${⊢}{\phi }\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\to \forall {a}\in {J}\phantom{\rule{.4em}{0ex}}\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)\right)$
123 81 122 impbid ${⊢}{\phi }\to \left(\forall {a}\in {J}\phantom{\rule{.4em}{0ex}}\left(\mathrm{+\infty }\in {a}\to \exists {l}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}{A}\in {a}\right)↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{A}\right)$
124 23 123 bitrd