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 ⊢ 𝐽 = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
lmxrge0.6 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
lmxrge0.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
Assertion lmxrge0 ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < 𝐴 ) )

Proof

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