Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lmxrge0 Structured version   Visualization version   GIF version

Theorem lmxrge0 30445
Description: Express "sequence 𝐹 converges to plus infinity" (i.e. diverges), for a sequence of nonnegative extended real numbers. (Contributed by Thierry Arnoux, 2-Aug-2017.)
Hypotheses
Ref Expression
lmxrge0.j 𝐽 = (TopOpen‘(ℝ*𝑠s (0[,]+∞)))
lmxrge0.6 (𝜑𝐹:ℕ⟶(0[,]+∞))
lmxrge0.7 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) = 𝐴)
Assertion
Ref Expression
lmxrge0 (𝜑 → (𝐹(⇝𝑡𝐽)+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴))
Distinct variable groups:   𝑥,𝑗,𝐴   𝑗,𝑘,𝐹,𝑥   𝑘,𝐽,𝑥   𝜑,𝑘,𝑥
Allowed substitution hints:   𝜑(𝑗)   𝐴(𝑘)   𝐽(𝑗)

Proof of Theorem lmxrge0
Dummy variables 𝑎 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lmxrge0.j . . . . . . 7 𝐽 = (TopOpen‘(ℝ*𝑠s (0[,]+∞)))
2 eqid 2765 . . . . . . . 8 (ℝ*𝑠s (0[,]+∞)) = (ℝ*𝑠s (0[,]+∞))
3 xrstopn 21292 . . . . . . . 8 (ordTop‘ ≤ ) = (TopOpen‘ℝ*𝑠)
42, 3resstopn 21270 . . . . . . 7 ((ordTop‘ ≤ ) ↾t (0[,]+∞)) = (TopOpen‘(ℝ*𝑠s (0[,]+∞)))
51, 4eqtr4i 2790 . . . . . 6 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))
6 letopon 21289 . . . . . . 7 (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
7 iccssxr 12458 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
8 resttopon 21245 . . . . . . 7 (((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧ (0[,]+∞) ⊆ ℝ*) → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ (TopOn‘(0[,]+∞)))
96, 7, 8mp2an 683 . . . . . 6 ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ (TopOn‘(0[,]+∞))
105, 9eqeltri 2840 . . . . 5 𝐽 ∈ (TopOn‘(0[,]+∞))
1110a1i 11 . . . 4 (𝜑𝐽 ∈ (TopOn‘(0[,]+∞)))
12 nnuz 11923 . . . 4 ℕ = (ℤ‘1)
13 1zzd 11655 . . . 4 (𝜑 → 1 ∈ ℤ)
14 lmxrge0.6 . . . 4 (𝜑𝐹:ℕ⟶(0[,]+∞))
15 lmxrge0.7 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) = 𝐴)
1611, 12, 13, 14, 15lmbrf 21344 . . 3 (𝜑 → (𝐹(⇝𝑡𝐽)+∞ ↔ (+∞ ∈ (0[,]+∞) ∧ ∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎))))
17 0xr 10340 . . . . 5 0 ∈ ℝ*
18 pnfxr 10346 . . . . 5 +∞ ∈ ℝ*
19 0lepnf 12166 . . . . 5 0 ≤ +∞
20 ubicc2 12493 . . . . 5 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞) → +∞ ∈ (0[,]+∞))
2117, 18, 19, 20mp3an 1585 . . . 4 +∞ ∈ (0[,]+∞)
2221biantrur 526 . . 3 (∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎) ↔ (+∞ ∈ (0[,]+∞) ∧ ∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎)))
2316, 22syl6bbr 280 . 2 (𝜑 → (𝐹(⇝𝑡𝐽)+∞ ↔ ∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎)))
24 rexr 10339 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
2518a1i 11 . . . . . . . . . 10 (𝑥 ∈ ℝ → +∞ ∈ ℝ*)
26 ltpnf 12154 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 < +∞)
27 ubioc1 12429 . . . . . . . . . 10 ((𝑥 ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 < +∞) → +∞ ∈ (𝑥(,]+∞))
2824, 25, 26, 27syl3anc 1490 . . . . . . . . 9 (𝑥 ∈ ℝ → +∞ ∈ (𝑥(,]+∞))
29 0ltpnf 12156 . . . . . . . . . 10 0 < +∞
30 ubioc1 12429 . . . . . . . . . 10 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → +∞ ∈ (0(,]+∞))
3117, 18, 29, 30mp3an 1585 . . . . . . . . 9 +∞ ∈ (0(,]+∞)
3228, 31jctir 516 . . . . . . . 8 (𝑥 ∈ ℝ → (+∞ ∈ (𝑥(,]+∞) ∧ +∞ ∈ (0(,]+∞)))
33 elin 3958 . . . . . . . 8 (+∞ ∈ ((𝑥(,]+∞) ∩ (0(,]+∞)) ↔ (+∞ ∈ (𝑥(,]+∞) ∧ +∞ ∈ (0(,]+∞)))
3432, 33sylibr 225 . . . . . . 7 (𝑥 ∈ ℝ → +∞ ∈ ((𝑥(,]+∞) ∩ (0(,]+∞)))
3534ad2antlr 718 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎)) → +∞ ∈ ((𝑥(,]+∞) ∩ (0(,]+∞)))
36 letop 21290 . . . . . . . . . . 11 (ordTop‘ ≤ ) ∈ Top
37 ovex 6874 . . . . . . . . . . 11 (0[,]+∞) ∈ V
38 iocpnfordt 21299 . . . . . . . . . . . 12 (𝑥(,]+∞) ∈ (ordTop‘ ≤ )
39 iocpnfordt 21299 . . . . . . . . . . . 12 (0(,]+∞) ∈ (ordTop‘ ≤ )
40 inopn 20983 . . . . . . . . . . . 12 (((ordTop‘ ≤ ) ∈ Top ∧ (𝑥(,]+∞) ∈ (ordTop‘ ≤ ) ∧ (0(,]+∞) ∈ (ordTop‘ ≤ )) → ((𝑥(,]+∞) ∩ (0(,]+∞)) ∈ (ordTop‘ ≤ ))
4136, 38, 39, 40mp3an 1585 . . . . . . . . . . 11 ((𝑥(,]+∞) ∩ (0(,]+∞)) ∈ (ordTop‘ ≤ )
42 elrestr 16355 . . . . . . . . . . 11 (((ordTop‘ ≤ ) ∈ Top ∧ (0[,]+∞) ∈ V ∧ ((𝑥(,]+∞) ∩ (0(,]+∞)) ∈ (ordTop‘ ≤ )) → (((𝑥(,]+∞) ∩ (0(,]+∞)) ∩ (0[,]+∞)) ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞)))
4336, 37, 41, 42mp3an 1585 . . . . . . . . . 10 (((𝑥(,]+∞) ∩ (0(,]+∞)) ∩ (0[,]+∞)) ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞))
44 inss2 3993 . . . . . . . . . . . . 13 ((𝑥(,]+∞) ∩ (0(,]+∞)) ⊆ (0(,]+∞)
45 iocssicc 12464 . . . . . . . . . . . . 13 (0(,]+∞) ⊆ (0[,]+∞)
4644, 45sstri 3770 . . . . . . . . . . . 12 ((𝑥(,]+∞) ∩ (0(,]+∞)) ⊆ (0[,]+∞)
47 sseqin2 3979 . . . . . . . . . . . 12 (((𝑥(,]+∞) ∩ (0(,]+∞)) ⊆ (0[,]+∞) ↔ ((0[,]+∞) ∩ ((𝑥(,]+∞) ∩ (0(,]+∞))) = ((𝑥(,]+∞) ∩ (0(,]+∞)))
4846, 47mpbi 221 . . . . . . . . . . 11 ((0[,]+∞) ∩ ((𝑥(,]+∞) ∩ (0(,]+∞))) = ((𝑥(,]+∞) ∩ (0(,]+∞))
49 incom 3967 . . . . . . . . . . 11 ((0[,]+∞) ∩ ((𝑥(,]+∞) ∩ (0(,]+∞))) = (((𝑥(,]+∞) ∩ (0(,]+∞)) ∩ (0[,]+∞))
5048, 49eqtr3i 2789 . . . . . . . . . 10 ((𝑥(,]+∞) ∩ (0(,]+∞)) = (((𝑥(,]+∞) ∩ (0(,]+∞)) ∩ (0[,]+∞))
5143, 50, 53eltr4i 2857 . . . . . . . . 9 ((𝑥(,]+∞) ∩ (0(,]+∞)) ∈ 𝐽
5251a1i 11 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ((𝑥(,]+∞) ∩ (0(,]+∞)) ∈ 𝐽)
53 eleq2 2833 . . . . . . . . . . 11 (𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞)) → (+∞ ∈ 𝑎 ↔ +∞ ∈ ((𝑥(,]+∞) ∩ (0(,]+∞))))
5453adantl 473 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) → (+∞ ∈ 𝑎 ↔ +∞ ∈ ((𝑥(,]+∞) ∩ (0(,]+∞))))
5554biimprd 239 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) → (+∞ ∈ ((𝑥(,]+∞) ∩ (0(,]+∞)) → +∞ ∈ 𝑎))
56 simp-5r 807 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) ∧ 𝐴𝑎) → 𝑥 ∈ ℝ)
5756rexrd 10343 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) ∧ 𝐴𝑎) → 𝑥 ∈ ℝ*)
58 simpr 477 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) ∧ 𝐴𝑎) → 𝐴𝑎)
59 simp-4r 803 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) ∧ 𝐴𝑎) → 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞)))
6058, 59eleqtrd 2846 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) ∧ 𝐴𝑎) → 𝐴 ∈ ((𝑥(,]+∞) ∩ (0(,]+∞)))
61 elin 3958 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ((𝑥(,]+∞) ∩ (0(,]+∞)) ↔ (𝐴 ∈ (𝑥(,]+∞) ∧ 𝐴 ∈ (0(,]+∞)))
6261simplbi 491 . . . . . . . . . . . . . . 15 (𝐴 ∈ ((𝑥(,]+∞) ∩ (0(,]+∞)) → 𝐴 ∈ (𝑥(,]+∞))
6360, 62syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) ∧ 𝐴𝑎) → 𝐴 ∈ (𝑥(,]+∞))
64 elioc1 12419 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (𝑥(,]+∞) ↔ (𝐴 ∈ ℝ*𝑥 < 𝐴𝐴 ≤ +∞)))
6518, 64mpan2 682 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ* → (𝐴 ∈ (𝑥(,]+∞) ↔ (𝐴 ∈ ℝ*𝑥 < 𝐴𝐴 ≤ +∞)))
6665biimpa 468 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ*𝐴 ∈ (𝑥(,]+∞)) → (𝐴 ∈ ℝ*𝑥 < 𝐴𝐴 ≤ +∞))
6766simp2d 1173 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ*𝐴 ∈ (𝑥(,]+∞)) → 𝑥 < 𝐴)
6857, 63, 67syl2anc 579 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) ∧ 𝐴𝑎) → 𝑥 < 𝐴)
6968ex 401 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) → (𝐴𝑎𝑥 < 𝐴))
7069ralimdva 3109 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) ∧ 𝑙 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑙)𝐴𝑎 → ∀𝑘 ∈ (ℤ𝑙)𝑥 < 𝐴))
7170reximdva 3163 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) → (∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝑥 < 𝐴))
72 fveq2 6375 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (ℤ𝑗) = (ℤ𝑙))
7372raleqdv 3292 . . . . . . . . . . 11 (𝑗 = 𝑙 → (∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴 ↔ ∀𝑘 ∈ (ℤ𝑙)𝑥 < 𝐴))
7473cbvrexv 3320 . . . . . . . . . 10 (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴 ↔ ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝑥 < 𝐴)
7571, 74syl6ibr 243 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) → (∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴))
7655, 75imim12d 81 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ 𝑎 = ((𝑥(,]+∞) ∩ (0(,]+∞))) → ((+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎) → (+∞ ∈ ((𝑥(,]+∞) ∩ (0(,]+∞)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴)))
7752, 76rspcimdv 3462 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎) → (+∞ ∈ ((𝑥(,]+∞) ∩ (0(,]+∞)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴)))
7877imp 395 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎)) → (+∞ ∈ ((𝑥(,]+∞) ∩ (0(,]+∞)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴))
7935, 78mpd 15 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴)
8079ex 401 . . . 4 ((𝜑𝑥 ∈ ℝ) → (∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴))
8180ralrimdva 3116 . . 3 (𝜑 → (∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴))
82 simplll 791 . . . . . 6 ((((𝜑𝑎𝐽) ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴) ∧ +∞ ∈ 𝑎) → 𝜑)
83 simpllr 793 . . . . . . 7 ((((𝜑𝑎𝐽) ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴) ∧ +∞ ∈ 𝑎) → 𝑎𝐽)
84 simpr 477 . . . . . . 7 ((((𝜑𝑎𝐽) ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴) ∧ +∞ ∈ 𝑎) → +∞ ∈ 𝑎)
851pnfneige0 30444 . . . . . . 7 ((𝑎𝐽 ∧ +∞ ∈ 𝑎) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝑎)
8683, 84, 85syl2anc 579 . . . . . 6 ((((𝜑𝑎𝐽) ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴) ∧ +∞ ∈ 𝑎) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝑎)
87 simplr 785 . . . . . 6 ((((𝜑𝑎𝐽) ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴) ∧ +∞ ∈ 𝑎) → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴)
88 r19.29r 3220 . . . . . . . 8 ((∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝑎 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴) → ∃𝑥 ∈ ℝ ((𝑥(,]+∞) ⊆ 𝑎 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴))
89 simp-4l 801 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) → 𝜑)
90 uznnssnn 11935 . . . . . . . . . . . . . . . . 17 (𝑙 ∈ ℕ → (ℤ𝑙) ⊆ ℕ)
9190ad2antlr 718 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) → (ℤ𝑙) ⊆ ℕ)
92 simpr 477 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) → 𝑘 ∈ (ℤ𝑙))
9391, 92sseldd 3762 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) → 𝑘 ∈ ℕ)
9489, 93jca 507 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) → (𝜑𝑘 ∈ ℕ))
95 simp-4r 803 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) → 𝑥 ∈ ℝ)
96 simpllr 793 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) → (𝑥(,]+∞) ⊆ 𝑎)
97 simplr 785 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑥 < 𝐴) → (𝑥(,]+∞) ⊆ 𝑎)
98 simplr 785 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < 𝐴) → 𝑥 ∈ ℝ)
9998rexrd 10343 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < 𝐴) → 𝑥 ∈ ℝ*)
10014ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ (0[,]+∞))
10115, 100eqeltrrd 2845 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))
1027, 101sseldi 3759 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℝ*)
103102ad2antrr 717 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < 𝐴) → 𝐴 ∈ ℝ*)
104 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < 𝐴) → 𝑥 < 𝐴)
105 pnfge 12164 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℝ*𝐴 ≤ +∞)
106103, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < 𝐴) → 𝐴 ≤ +∞)
10765biimpar 469 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ* ∧ (𝐴 ∈ ℝ*𝑥 < 𝐴𝐴 ≤ +∞)) → 𝐴 ∈ (𝑥(,]+∞))
10899, 103, 104, 106, 107syl13anc 1491 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < 𝐴) → 𝐴 ∈ (𝑥(,]+∞))
109108adantlr 706 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑥 < 𝐴) → 𝐴 ∈ (𝑥(,]+∞))
11097, 109sseldd 3762 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑥 < 𝐴) → 𝐴𝑎)
111110ex 401 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) → (𝑥 < 𝐴𝐴𝑎))
11294, 95, 96, 111syl21anc 866 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑙 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑙)) → (𝑥 < 𝐴𝐴𝑎))
113112ralimdva 3109 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) ∧ 𝑙 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑙)𝑥 < 𝐴 → ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎))
114113reximdva 3163 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) → (∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝑥 < 𝐴 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎))
11574, 114syl5bi 233 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑎) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎))
116115expimpd 445 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (((𝑥(,]+∞) ⊆ 𝑎 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴) → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎))
117116rexlimdva 3178 . . . . . . . 8 (𝜑 → (∃𝑥 ∈ ℝ ((𝑥(,]+∞) ⊆ 𝑎 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴) → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎))
11888, 117syl5 34 . . . . . . 7 (𝜑 → ((∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝑎 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴) → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎))
119118imp 395 . . . . . 6 ((𝜑 ∧ (∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝑎 ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴)) → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎)
12082, 86, 87, 119syl12anc 865 . . . . 5 ((((𝜑𝑎𝐽) ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴) ∧ +∞ ∈ 𝑎) → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎)
121120exp31 410 . . . 4 ((𝜑𝑎𝐽) → (∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴 → (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎)))
122121ralrimdva 3116 . . 3 (𝜑 → (∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴 → ∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎)))
12381, 122impbid 203 . 2 (𝜑 → (∀𝑎𝐽 (+∞ ∈ 𝑎 → ∃𝑙 ∈ ℕ ∀𝑘 ∈ (ℤ𝑙)𝐴𝑎) ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴))
12423, 123bitrd 270 1 (𝜑 → (𝐹(⇝𝑡𝐽)+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑥 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  wrex 3056  Vcvv 3350  cin 3731  wss 3732   class class class wbr 4809  wf 6064  cfv 6068  (class class class)co 6842  cr 10188  0cc0 10189  1c1 10190  +∞cpnf 10325  *cxr 10327   < clt 10328  cle 10329  cn 11274  cuz 11886  (,]cioc 12378  [,]cicc 12380  s cress 16131  t crest 16347  TopOpenctopn 16348  ordTopcordt 16425  *𝑠cxrs 16426  Topctop 20977  TopOnctopon 20994  𝑡clm 21310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fi 8524  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-ioo 12381  df-ioc 12382  df-ico 12383  df-icc 12384  df-fz 12534  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-mulr 16228  df-tset 16233  df-ple 16234  df-ds 16236  df-rest 16349  df-topn 16350  df-topgen 16370  df-ordt 16427  df-xrs 16428  df-ps 17466  df-tsr 17467  df-top 20978  df-topon 20995  df-bases 21030  df-lm 21313
This theorem is referenced by:  lmdvglim  30447
  Copyright terms: Public domain W3C validator