Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  caucvgrlem Structured version   Visualization version   GIF version

Theorem caucvgrlem 15070
 Description: Lemma for caurcvgr 15071. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by AV, 12-Sep-2020.)
Hypotheses
Ref Expression
caurcvgr.1 (𝜑𝐴 ⊆ ℝ)
caurcvgr.2 (𝜑𝐹:𝐴⟶ℝ)
caurcvgr.3 (𝜑 → sup(𝐴, ℝ*, < ) = +∞)
caurcvgr.4 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝐴𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥))
caucvgrlem.4 (𝜑𝑅 ∈ ℝ+)
Assertion
Ref Expression
caucvgrlem (𝜑 → ∃𝑗𝐴 ((lim sup‘𝐹) ∈ ℝ ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (lim sup‘𝐹))) < (3 · 𝑅))))
Distinct variable groups:   𝑗,𝑘,𝑥,𝐴   𝑗,𝐹,𝑘,𝑥   𝜑,𝑗,𝑘,𝑥   𝑅,𝑗,𝑘,𝑥

Proof of Theorem caucvgrlem
Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 caurcvgr.2 . . . . . . 7 (𝜑𝐹:𝐴⟶ℝ)
2 caurcvgr.1 . . . . . . . 8 (𝜑𝐴 ⊆ ℝ)
3 reex 10659 . . . . . . . . 9 ℝ ∈ V
43ssex 5192 . . . . . . . 8 (𝐴 ⊆ ℝ → 𝐴 ∈ V)
52, 4syl 17 . . . . . . 7 (𝜑𝐴 ∈ V)
63a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ V)
7 fex2 7644 . . . . . . 7 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ V ∧ ℝ ∈ V) → 𝐹 ∈ V)
81, 5, 6, 7syl3anc 1369 . . . . . 6 (𝜑𝐹 ∈ V)
9 limsupcl 14871 . . . . . 6 (𝐹 ∈ V → (lim sup‘𝐹) ∈ ℝ*)
108, 9syl 17 . . . . 5 (𝜑 → (lim sup‘𝐹) ∈ ℝ*)
1110adantr 485 . . . 4 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → (lim sup‘𝐹) ∈ ℝ*)
121adantr 485 . . . . . 6 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → 𝐹:𝐴⟶ℝ)
13 simprl 771 . . . . . 6 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → 𝑗𝐴)
1412, 13ffvelrnd 6844 . . . . 5 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → (𝐹𝑗) ∈ ℝ)
15 caucvgrlem.4 . . . . . . 7 (𝜑𝑅 ∈ ℝ+)
1615rpred 12465 . . . . . 6 (𝜑𝑅 ∈ ℝ)
1716adantr 485 . . . . 5 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → 𝑅 ∈ ℝ)
1814, 17readdcld 10701 . . . 4 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ((𝐹𝑗) + 𝑅) ∈ ℝ)
19 mnfxr 10729 . . . . . 6 -∞ ∈ ℝ*
2019a1i 11 . . . . 5 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → -∞ ∈ ℝ*)
2114, 17resubcld 11099 . . . . . 6 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ((𝐹𝑗) − 𝑅) ∈ ℝ)
2221rexrd 10722 . . . . 5 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ((𝐹𝑗) − 𝑅) ∈ ℝ*)
2321mnfltd 12553 . . . . 5 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → -∞ < ((𝐹𝑗) − 𝑅))
242adantr 485 . . . . . 6 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → 𝐴 ⊆ ℝ)
25 ressxr 10716 . . . . . . . 8 ℝ ⊆ ℝ*
26 fss 6513 . . . . . . . 8 ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℝ*) → 𝐹:𝐴⟶ℝ*)
271, 25, 26sylancl 590 . . . . . . 7 (𝜑𝐹:𝐴⟶ℝ*)
2827adantr 485 . . . . . 6 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → 𝐹:𝐴⟶ℝ*)
29 caurcvgr.3 . . . . . . 7 (𝜑 → sup(𝐴, ℝ*, < ) = +∞)
3029adantr 485 . . . . . 6 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → sup(𝐴, ℝ*, < ) = +∞)
3124, 13sseldd 3894 . . . . . . 7 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → 𝑗 ∈ ℝ)
32 simprr 773 . . . . . . . . 9 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))
33 breq2 5037 . . . . . . . . . . 11 (𝑘 = 𝑚 → (𝑗𝑘𝑗𝑚))
3433imbrov2fvoveq 7176 . . . . . . . . . 10 (𝑘 = 𝑚 → ((𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅) ↔ (𝑗𝑚 → (abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅)))
3534cbvralvw 3362 . . . . . . . . 9 (∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅) ↔ ∀𝑚𝐴 (𝑗𝑚 → (abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅))
3632, 35sylib 221 . . . . . . . 8 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ∀𝑚𝐴 (𝑗𝑚 → (abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅))
3712ffvelrnda 6843 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → (𝐹𝑚) ∈ ℝ)
3814adantr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → (𝐹𝑗) ∈ ℝ)
3937, 38resubcld 11099 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → ((𝐹𝑚) − (𝐹𝑗)) ∈ ℝ)
4039recnd 10700 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → ((𝐹𝑚) − (𝐹𝑗)) ∈ ℂ)
4140abscld 14837 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → (abs‘((𝐹𝑚) − (𝐹𝑗))) ∈ ℝ)
4217adantr 485 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → 𝑅 ∈ ℝ)
43 ltle 10760 . . . . . . . . . . . . 13 (((abs‘((𝐹𝑚) − (𝐹𝑗))) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅 → (abs‘((𝐹𝑚) − (𝐹𝑗))) ≤ 𝑅))
4441, 42, 43syl2anc 588 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → ((abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅 → (abs‘((𝐹𝑚) − (𝐹𝑗))) ≤ 𝑅))
4537, 38, 42absdifled 14835 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → ((abs‘((𝐹𝑚) − (𝐹𝑗))) ≤ 𝑅 ↔ (((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚) ∧ (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅))))
4644, 45sylibd 242 . . . . . . . . . . 11 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → ((abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅 → (((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚) ∧ (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅))))
47 simpl 487 . . . . . . . . . . 11 ((((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚) ∧ (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅)) → ((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚))
4846, 47syl6 35 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → ((abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅 → ((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚)))
4948imim2d 57 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → ((𝑗𝑚 → (abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅) → (𝑗𝑚 → ((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚))))
5049ralimdva 3109 . . . . . . . 8 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → (∀𝑚𝐴 (𝑗𝑚 → (abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅) → ∀𝑚𝐴 (𝑗𝑚 → ((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚))))
5136, 50mpd 15 . . . . . . 7 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ∀𝑚𝐴 (𝑗𝑚 → ((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚)))
52 breq1 5036 . . . . . . . 8 (𝑛 = 𝑗 → (𝑛𝑚𝑗𝑚))
5352rspceaimv 3547 . . . . . . 7 ((𝑗 ∈ ℝ ∧ ∀𝑚𝐴 (𝑗𝑚 → ((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚))) → ∃𝑛 ∈ ℝ ∀𝑚𝐴 (𝑛𝑚 → ((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚)))
5431, 51, 53syl2anc 588 . . . . . 6 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ∃𝑛 ∈ ℝ ∀𝑚𝐴 (𝑛𝑚 → ((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚)))
5524, 28, 22, 30, 54limsupbnd2 14881 . . . . 5 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ((𝐹𝑗) − 𝑅) ≤ (lim sup‘𝐹))
5620, 22, 11, 23, 55xrltletrd 12588 . . . 4 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → -∞ < (lim sup‘𝐹))
5718rexrd 10722 . . . . 5 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ((𝐹𝑗) + 𝑅) ∈ ℝ*)
5841adantrr 717 . . . . . . . . . . 11 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (abs‘((𝐹𝑚) − (𝐹𝑗))) ∈ ℝ)
5917adantr 485 . . . . . . . . . . 11 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → 𝑅 ∈ ℝ)
60 simprr 773 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → 𝑗𝑚)
61 simplrr 778 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))
62 simprl 771 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → 𝑚𝐴)
6334, 61, 62rspcdva 3544 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (𝑗𝑚 → (abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅))
6460, 63mpd 15 . . . . . . . . . . 11 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (abs‘((𝐹𝑚) − (𝐹𝑗))) < 𝑅)
6558, 59, 64ltled 10819 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (abs‘((𝐹𝑚) − (𝐹𝑗))) ≤ 𝑅)
6637adantrr 717 . . . . . . . . . . 11 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (𝐹𝑚) ∈ ℝ)
6714adantr 485 . . . . . . . . . . 11 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (𝐹𝑗) ∈ ℝ)
6866, 67, 59absdifled 14835 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((abs‘((𝐹𝑚) − (𝐹𝑗))) ≤ 𝑅 ↔ (((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚) ∧ (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅))))
6965, 68mpbid 235 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚) ∧ (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅)))
7069simprd 500 . . . . . . . 8 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅))
7170expr 461 . . . . . . 7 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → (𝑗𝑚 → (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅)))
7271ralrimiva 3114 . . . . . 6 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ∀𝑚𝐴 (𝑗𝑚 → (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅)))
7352rspceaimv 3547 . . . . . 6 ((𝑗 ∈ ℝ ∧ ∀𝑚𝐴 (𝑗𝑚 → (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅))) → ∃𝑛 ∈ ℝ ∀𝑚𝐴 (𝑛𝑚 → (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅)))
7431, 72, 73syl2anc 588 . . . . 5 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ∃𝑛 ∈ ℝ ∀𝑚𝐴 (𝑛𝑚 → (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅)))
7524, 28, 57, 74limsupbnd1 14880 . . . 4 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → (lim sup‘𝐹) ≤ ((𝐹𝑗) + 𝑅))
76 xrre 12596 . . . 4 ((((lim sup‘𝐹) ∈ ℝ* ∧ ((𝐹𝑗) + 𝑅) ∈ ℝ) ∧ (-∞ < (lim sup‘𝐹) ∧ (lim sup‘𝐹) ≤ ((𝐹𝑗) + 𝑅))) → (lim sup‘𝐹) ∈ ℝ)
7711, 18, 56, 75, 76syl22anc 838 . . 3 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → (lim sup‘𝐹) ∈ ℝ)
7877adantr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (lim sup‘𝐹) ∈ ℝ)
7966, 78resubcld 11099 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) − (lim sup‘𝐹)) ∈ ℝ)
8079recnd 10700 . . . . . . . 8 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) − (lim sup‘𝐹)) ∈ ℂ)
8180abscld 14837 . . . . . . 7 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (abs‘((𝐹𝑚) − (lim sup‘𝐹))) ∈ ℝ)
82 2re 11741 . . . . . . . 8 2 ∈ ℝ
83 remulcl 10653 . . . . . . . 8 ((2 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (2 · 𝑅) ∈ ℝ)
8482, 59, 83sylancr 591 . . . . . . 7 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (2 · 𝑅) ∈ ℝ)
85 3re 11747 . . . . . . . 8 3 ∈ ℝ
86 remulcl 10653 . . . . . . . 8 ((3 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (3 · 𝑅) ∈ ℝ)
8785, 59, 86sylancr 591 . . . . . . 7 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (3 · 𝑅) ∈ ℝ)
8866recnd 10700 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (𝐹𝑚) ∈ ℂ)
8978recnd 10700 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (lim sup‘𝐹) ∈ ℂ)
9088, 89abssubd 14854 . . . . . . . 8 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (abs‘((𝐹𝑚) − (lim sup‘𝐹))) = (abs‘((lim sup‘𝐹) − (𝐹𝑚))))
9166, 84resubcld 11099 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) − (2 · 𝑅)) ∈ ℝ)
9221adantr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑗) − 𝑅) ∈ ℝ)
9359recnd 10700 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → 𝑅 ∈ ℂ)
94932timesd 11910 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (2 · 𝑅) = (𝑅 + 𝑅))
9594oveq2d 7167 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) − (2 · 𝑅)) = ((𝐹𝑚) − (𝑅 + 𝑅)))
9688, 93, 93subsub4d 11059 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (((𝐹𝑚) − 𝑅) − 𝑅) = ((𝐹𝑚) − (𝑅 + 𝑅)))
9795, 96eqtr4d 2797 . . . . . . . . . . 11 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) − (2 · 𝑅)) = (((𝐹𝑚) − 𝑅) − 𝑅))
9866, 59resubcld 11099 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) − 𝑅) ∈ ℝ)
9966, 59, 67lesubaddd 11268 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (((𝐹𝑚) − 𝑅) ≤ (𝐹𝑗) ↔ (𝐹𝑚) ≤ ((𝐹𝑗) + 𝑅)))
10070, 99mpbird 260 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) − 𝑅) ≤ (𝐹𝑗))
10198, 67, 59, 100lesub1dd 11287 . . . . . . . . . . 11 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (((𝐹𝑚) − 𝑅) − 𝑅) ≤ ((𝐹𝑗) − 𝑅))
10297, 101eqbrtrd 5055 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) − (2 · 𝑅)) ≤ ((𝐹𝑗) − 𝑅))
10355adantr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑗) − 𝑅) ≤ (lim sup‘𝐹))
10491, 92, 78, 102, 103letrd 10828 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) − (2 · 𝑅)) ≤ (lim sup‘𝐹))
10518adantr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑗) + 𝑅) ∈ ℝ)
10666, 84readdcld 10701 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) + (2 · 𝑅)) ∈ ℝ)
10775adantr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (lim sup‘𝐹) ≤ ((𝐹𝑗) + 𝑅))
10866, 59readdcld 10701 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) + 𝑅) ∈ ℝ)
10969, 47syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚))
11067, 59, 66lesubaddd 11268 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (((𝐹𝑗) − 𝑅) ≤ (𝐹𝑚) ↔ (𝐹𝑗) ≤ ((𝐹𝑚) + 𝑅)))
111109, 110mpbid 235 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (𝐹𝑗) ≤ ((𝐹𝑚) + 𝑅))
11267, 108, 59, 111leadd1dd 11285 . . . . . . . . . . 11 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑗) + 𝑅) ≤ (((𝐹𝑚) + 𝑅) + 𝑅))
11388, 93, 93addassd 10694 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (((𝐹𝑚) + 𝑅) + 𝑅) = ((𝐹𝑚) + (𝑅 + 𝑅)))
11494oveq2d 7167 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑚) + (2 · 𝑅)) = ((𝐹𝑚) + (𝑅 + 𝑅)))
115113, 114eqtr4d 2797 . . . . . . . . . . 11 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (((𝐹𝑚) + 𝑅) + 𝑅) = ((𝐹𝑚) + (2 · 𝑅)))
116112, 115breqtrd 5059 . . . . . . . . . 10 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((𝐹𝑗) + 𝑅) ≤ ((𝐹𝑚) + (2 · 𝑅)))
11778, 105, 106, 107, 116letrd 10828 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (lim sup‘𝐹) ≤ ((𝐹𝑚) + (2 · 𝑅)))
11878, 66, 84absdifled 14835 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → ((abs‘((lim sup‘𝐹) − (𝐹𝑚))) ≤ (2 · 𝑅) ↔ (((𝐹𝑚) − (2 · 𝑅)) ≤ (lim sup‘𝐹) ∧ (lim sup‘𝐹) ≤ ((𝐹𝑚) + (2 · 𝑅)))))
119104, 117, 118mpbir2and 713 . . . . . . . 8 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (abs‘((lim sup‘𝐹) − (𝐹𝑚))) ≤ (2 · 𝑅))
12090, 119eqbrtrd 5055 . . . . . . 7 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (abs‘((𝐹𝑚) − (lim sup‘𝐹))) ≤ (2 · 𝑅))
121 2lt3 11839 . . . . . . . 8 2 < 3
12282a1i 11 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → 2 ∈ ℝ)
12385a1i 11 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → 3 ∈ ℝ)
12415adantr 485 . . . . . . . . . 10 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → 𝑅 ∈ ℝ+)
125124adantr 485 . . . . . . . . 9 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → 𝑅 ∈ ℝ+)
126122, 123, 125ltmul1d 12506 . . . . . . . 8 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (2 < 3 ↔ (2 · 𝑅) < (3 · 𝑅)))
127121, 126mpbii 236 . . . . . . 7 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (2 · 𝑅) < (3 · 𝑅))
12881, 84, 87, 120, 127lelttrd 10829 . . . . . 6 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ (𝑚𝐴𝑗𝑚)) → (abs‘((𝐹𝑚) − (lim sup‘𝐹))) < (3 · 𝑅))
129128expr 461 . . . . 5 (((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) ∧ 𝑚𝐴) → (𝑗𝑚 → (abs‘((𝐹𝑚) − (lim sup‘𝐹))) < (3 · 𝑅)))
130129ralrimiva 3114 . . . 4 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ∀𝑚𝐴 (𝑗𝑚 → (abs‘((𝐹𝑚) − (lim sup‘𝐹))) < (3 · 𝑅)))
13133imbrov2fvoveq 7176 . . . . 5 (𝑘 = 𝑚 → ((𝑗𝑘 → (abs‘((𝐹𝑘) − (lim sup‘𝐹))) < (3 · 𝑅)) ↔ (𝑗𝑚 → (abs‘((𝐹𝑚) − (lim sup‘𝐹))) < (3 · 𝑅))))
132131cbvralvw 3362 . . . 4 (∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (lim sup‘𝐹))) < (3 · 𝑅)) ↔ ∀𝑚𝐴 (𝑗𝑚 → (abs‘((𝐹𝑚) − (lim sup‘𝐹))) < (3 · 𝑅)))
133130, 132sylibr 237 . . 3 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (lim sup‘𝐹))) < (3 · 𝑅)))
13477, 133jca 516 . 2 ((𝜑 ∧ (𝑗𝐴 ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))) → ((lim sup‘𝐹) ∈ ℝ ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (lim sup‘𝐹))) < (3 · 𝑅))))
135 breq2 5037 . . . . 5 (𝑥 = 𝑅 → ((abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥 ↔ (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))
136135imbi2d 345 . . . 4 (𝑥 = 𝑅 → ((𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥) ↔ (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅)))
137136rexralbidv 3226 . . 3 (𝑥 = 𝑅 → (∃𝑗𝐴𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥) ↔ ∃𝑗𝐴𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅)))
138 caurcvgr.4 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝐴𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥))
139137, 138, 15rspcdva 3544 . 2 (𝜑 → ∃𝑗𝐴𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑅))
140134, 139reximddv 3200 1 (𝜑 → ∃𝑗𝐴 ((lim sup‘𝐹) ∈ ℝ ∧ ∀𝑘𝐴 (𝑗𝑘 → (abs‘((𝐹𝑘) − (lim sup‘𝐹))) < (3 · 𝑅))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∀wral 3071  ∃wrex 3072  Vcvv 3410   ⊆ wss 3859   class class class wbr 5033  ⟶wf 6332  ‘cfv 6336  (class class class)co 7151  supcsup 8930  ℝcr 10567   + caddc 10571   · cmul 10573  +∞cpnf 10703  -∞cmnf 10704  ℝ*cxr 10705   < clt 10706   ≤ cle 10707   − cmin 10901  2c2 11722  3c3 11723  ℝ+crp 12423  abscabs 14634  lim supclsp 14868 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10624  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644  ax-pre-mulgt0 10645  ax-pre-sup 10646 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-2nd 7695  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-sup 8932  df-inf 8933  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712  df-sub 10903  df-neg 10904  df-div 11329  df-nn 11668  df-2 11730  df-3 11731  df-n0 11928  df-z 12014  df-uz 12276  df-rp 12424  df-ico 12778  df-seq 13412  df-exp 13473  df-cj 14499  df-re 14500  df-im 14501  df-sqrt 14635  df-abs 14636  df-limsup 14869 This theorem is referenced by:  caurcvgr  15071
 Copyright terms: Public domain W3C validator