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 = TopOpen 𝑠 * 𝑠 0 +∞
lmxrge0.6 φ F : 0 +∞
lmxrge0.7 φ k F k = A
Assertion lmxrge0 φ F t J +∞ x j k j x < A

Proof

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