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

Theorem iseralt 14623
Description: The alternating series test. If 𝐺(𝑘) is a decreasing sequence that converges to 0, then Σ𝑘𝑍(-1↑𝑘) · 𝐺(𝑘) is a convergent series. (Note that the first term is positive if 𝑀 is even, and negative if 𝑀 is odd. If the parity of your series does not match up with this, you will need to post-compose the series with multiplication by -1 using isermulc2 14596.) (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 9-Jul-2022.)
Hypotheses
Ref Expression
iseralt.1 𝑍 = (ℤ𝑀)
iseralt.2 (𝜑𝑀 ∈ ℤ)
iseralt.3 (𝜑𝐺:𝑍⟶ℝ)
iseralt.4 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
iseralt.5 (𝜑𝐺 ⇝ 0)
iseralt.6 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
Assertion
Ref Expression
iseralt (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Distinct variable groups:   𝑘,𝐹   𝑘,𝐺   𝑘,𝑀   𝜑,𝑘   𝑘,𝑍

Proof of Theorem iseralt
Dummy variables 𝑗 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iseralt.1 . 2 𝑍 = (ℤ𝑀)
2 seqex 13010 . . 3 seq𝑀( + , 𝐹) ∈ V
32a1i 11 . 2 (𝜑 → seq𝑀( + , 𝐹) ∈ V)
4 iseralt.5 . . . 4 (𝜑𝐺 ⇝ 0)
5 iseralt.2 . . . . 5 (𝜑𝑀 ∈ ℤ)
6 climrel 14431 . . . . . . 7 Rel ⇝
76brrelexi 5298 . . . . . 6 (𝐺 ⇝ 0 → 𝐺 ∈ V)
84, 7syl 17 . . . . 5 (𝜑𝐺 ∈ V)
9 eqidd 2772 . . . . 5 ((𝜑𝑛𝑍) → (𝐺𝑛) = (𝐺𝑛))
10 iseralt.3 . . . . . . 7 (𝜑𝐺:𝑍⟶ℝ)
1110ffvelrnda 6502 . . . . . 6 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ ℝ)
1211recnd 10270 . . . . 5 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ ℂ)
131, 5, 8, 9, 12clim0c 14446 . . . 4 (𝜑 → (𝐺 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥))
144, 13mpbid 222 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥)
15 simpr 471 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗𝑍)
1615, 1syl6eleq 2860 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
17 eluzelz 11898 . . . . . . . 8 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
18 uzid 11903 . . . . . . . 8 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
1916, 17, 183syl 18 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑗))
20 peano2uz 11943 . . . . . . 7 (𝑗 ∈ (ℤ𝑗) → (𝑗 + 1) ∈ (ℤ𝑗))
21 fveq2 6332 . . . . . . . . . 10 (𝑛 = (𝑗 + 1) → (𝐺𝑛) = (𝐺‘(𝑗 + 1)))
2221fveq2d 6336 . . . . . . . . 9 (𝑛 = (𝑗 + 1) → (abs‘(𝐺𝑛)) = (abs‘(𝐺‘(𝑗 + 1))))
2322breq1d 4796 . . . . . . . 8 (𝑛 = (𝑗 + 1) → ((abs‘(𝐺𝑛)) < 𝑥 ↔ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
2423rspcv 3456 . . . . . . 7 ((𝑗 + 1) ∈ (ℤ𝑗) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
2519, 20, 243syl 18 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
26 eluzelz 11898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ𝑗) → 𝑛 ∈ ℤ)
2726ad2antll 700 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℤ)
2827zcnd 11685 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℂ)
2917, 1eleq2s 2868 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗𝑍𝑗 ∈ ℤ)
3029ad2antrl 699 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℤ)
3130zcnd 11685 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℂ)
3228, 31subcld 10594 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℂ)
33 2cnd 11295 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ∈ ℂ)
34 2ne0 11315 . . . . . . . . . . . . . . . . . . . . 21 2 ≠ 0
3534a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ≠ 0)
3632, 33, 35divcan2d 11005 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((𝑛𝑗) / 2)) = (𝑛𝑗))
3736oveq2d 6809 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((𝑛𝑗) / 2))) = (𝑗 + (𝑛𝑗)))
3831, 28pncan3d 10597 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (𝑛𝑗)) = 𝑛)
3937, 38eqtr2d 2806 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 = (𝑗 + (2 · ((𝑛𝑗) / 2))))
4039adantr 466 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝑛 = (𝑗 + (2 · ((𝑛𝑗) / 2))))
4140fveq2d 6336 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))))
4241fvoveq1d 6815 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))))
43 simpll 742 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝜑)
44 simpl 468 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → 𝑗𝑍)
4544ad2antlr 698 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝑗𝑍)
46 simpr 471 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → ((𝑛𝑗) / 2) ∈ ℤ)
4727, 30zsubcld 11689 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℤ)
4847zred 11684 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℝ)
49 2rp 12040 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ+
5049a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ∈ ℝ+)
51 eluzle 11901 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ𝑗) → 𝑗𝑛)
5251ad2antll 700 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗𝑛)
5327zred 11684 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℝ)
5430zred 11684 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℝ)
5553, 54subge0d 10819 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (0 ≤ (𝑛𝑗) ↔ 𝑗𝑛))
5652, 55mpbird 247 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ (𝑛𝑗))
5748, 50, 56divge0d 12115 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ ((𝑛𝑗) / 2))
5857adantr 466 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 0 ≤ ((𝑛𝑗) / 2))
59 elnn0z 11592 . . . . . . . . . . . . . . . 16 (((𝑛𝑗) / 2) ∈ ℕ0 ↔ (((𝑛𝑗) / 2) ∈ ℤ ∧ 0 ≤ ((𝑛𝑗) / 2)))
6046, 58, 59sylanbrc 564 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → ((𝑛𝑗) / 2) ∈ ℕ0)
61 iseralt.4 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
62 iseralt.6 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
631, 5, 10, 61, 4, 62iseraltlem3 14622 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑍 ∧ ((𝑛𝑗) / 2) ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((𝑛𝑗) / 2))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))))
6463simpld 476 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍 ∧ ((𝑛𝑗) / 2) ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
6543, 45, 60, 64syl3anc 1476 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
6642, 65eqbrtrd 4808 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
67 2div2e1 11352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 / 2) = 1
6867oveq2i 6804 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑛𝑗) + 1) / 2) − (2 / 2)) = ((((𝑛𝑗) + 1) / 2) − 1)
69 peano2cn 10410 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛𝑗) ∈ ℂ → ((𝑛𝑗) + 1) ∈ ℂ)
7032, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℂ)
7170, 33, 33, 35divsubdird 11042 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) − 2) / 2) = ((((𝑛𝑗) + 1) / 2) − (2 / 2)))
72 df-2 11281 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 = (1 + 1)
7372oveq2i 6804 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑛𝑗) + 1) − 2) = (((𝑛𝑗) + 1) − (1 + 1))
74 ax-1cn 10196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
7574a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 1 ∈ ℂ)
7632, 75, 75pnpcan2d 10632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) − (1 + 1)) = ((𝑛𝑗) − 1))
7773, 76syl5eq 2817 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) − 2) = ((𝑛𝑗) − 1))
7877oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) − 2) / 2) = (((𝑛𝑗) − 1) / 2))
7971, 78eqtr3d 2807 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) / 2) − (2 / 2)) = (((𝑛𝑗) − 1) / 2))
8068, 79syl5eqr 2819 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) / 2) − 1) = (((𝑛𝑗) − 1) / 2))
8180oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((((𝑛𝑗) + 1) / 2) − 1)) = (2 · (((𝑛𝑗) − 1) / 2)))
82 subcl 10482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛𝑗) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛𝑗) − 1) ∈ ℂ)
8332, 74, 82sylancl 566 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) − 1) ∈ ℂ)
8483, 33, 35divcan2d 11005 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · (((𝑛𝑗) − 1) / 2)) = ((𝑛𝑗) − 1))
8528, 31, 75sub32d 10626 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) − 1) = ((𝑛 − 1) − 𝑗))
8681, 84, 853eqtrd 2809 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((((𝑛𝑗) + 1) / 2) − 1)) = ((𝑛 − 1) − 𝑗))
8786oveq2d 6809 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) = (𝑗 + ((𝑛 − 1) − 𝑗)))
88 subcl 10482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑛 − 1) ∈ ℂ)
8928, 74, 88sylancl 566 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛 − 1) ∈ ℂ)
9031, 89pncan3d 10597 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + ((𝑛 − 1) − 𝑗)) = (𝑛 − 1))
9187, 90eqtrd 2805 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) = (𝑛 − 1))
9291oveq1d 6808 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1) = ((𝑛 − 1) + 1))
93 npcan 10492 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
9428, 74, 93sylancl 566 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛 − 1) + 1) = 𝑛)
9592, 94eqtr2d 2806 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 = ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1))
9695adantr 466 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝑛 = ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1))
9796fveq2d 6336 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)))
9897fvoveq1d 6815 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))))
99 simpll 742 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝜑)
10044ad2antlr 698 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝑗𝑍)
101 simpr 471 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (((𝑛𝑗) + 1) / 2) ∈ ℤ)
102 uznn0sub 11921 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ𝑗) → (𝑛𝑗) ∈ ℕ0)
103102ad2antll 700 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℕ0)
104 nn0p1nn 11534 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛𝑗) ∈ ℕ0 → ((𝑛𝑗) + 1) ∈ ℕ)
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℕ)
106105nnrpd 12073 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℝ+)
107106rphalfcld 12087 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) / 2) ∈ ℝ+)
108107rpgt0d 12078 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 < (((𝑛𝑗) + 1) / 2))
109108adantr 466 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 0 < (((𝑛𝑗) + 1) / 2))
110 elnnz 11589 . . . . . . . . . . . . . . . . 17 ((((𝑛𝑗) + 1) / 2) ∈ ℕ ↔ ((((𝑛𝑗) + 1) / 2) ∈ ℤ ∧ 0 < (((𝑛𝑗) + 1) / 2)))
111101, 109, 110sylanbrc 564 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (((𝑛𝑗) + 1) / 2) ∈ ℕ)
112 nnm1nn0 11536 . . . . . . . . . . . . . . . 16 ((((𝑛𝑗) + 1) / 2) ∈ ℕ → ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0)
113111, 112syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0)
1141, 5, 10, 61, 4, 62iseraltlem3 14622 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑍 ∧ ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))))
115114simprd 477 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍 ∧ ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
11699, 100, 113, 115syl3anc 1476 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
11798, 116eqbrtrd 4808 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
118 zeo 11665 . . . . . . . . . . . . . 14 ((𝑛𝑗) ∈ ℤ → (((𝑛𝑗) / 2) ∈ ℤ ∨ (((𝑛𝑗) + 1) / 2) ∈ ℤ))
11947, 118syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) / 2) ∈ ℤ ∨ (((𝑛𝑗) + 1) / 2) ∈ ℤ))
12066, 117, 119mpjaodan 962 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
1211peano2uzs 11944 . . . . . . . . . . . . . . 15 (𝑗𝑍 → (𝑗 + 1) ∈ 𝑍)
122121adantr 466 . . . . . . . . . . . . . 14 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → (𝑗 + 1) ∈ 𝑍)
123 ffvelrn 6500 . . . . . . . . . . . . . 14 ((𝐺:𝑍⟶ℝ ∧ (𝑗 + 1) ∈ 𝑍) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
12410, 122, 123syl2an 575 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
1251, 5, 10, 61, 4iseraltlem1 14620 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑗 + 1)))
126122, 125sylan2 572 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ (𝐺‘(𝑗 + 1)))
127124, 126absidd 14369 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) = (𝐺‘(𝑗 + 1)))
128120, 127breqtrrd 4814 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))))
129128adantlr 686 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))))
130 neg1rr 11327 . . . . . . . . . . . . . . . . . . . . 21 -1 ∈ ℝ
131130a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → -1 ∈ ℝ)
132 neg1ne0 11328 . . . . . . . . . . . . . . . . . . . . 21 -1 ≠ 0
133132a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → -1 ≠ 0)
134 eluzelz 11898 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
135134, 1eleq2s 2868 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑍𝑘 ∈ ℤ)
136135adantl 467 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
137131, 133, 136reexpclzd 13241 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
13810ffvelrnda 6502 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
139137, 138remulcld 10272 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
14062, 139eqeltrd 2850 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
1411, 5, 140serfre 13037 . . . . . . . . . . . . . . . 16 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
1421uztrn2 11906 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → 𝑛𝑍)
143 ffvelrn 6500 . . . . . . . . . . . . . . . 16 ((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑛𝑍) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
144141, 142, 143syl2an 575 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
145 ffvelrn 6500 . . . . . . . . . . . . . . . 16 ((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑗𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
146141, 44, 145syl2an 575 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
147144, 146resubcld 10660 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℝ)
148147recnd 10270 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℂ)
149148abscld 14383 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ)
150149adantlr 686 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ)
151127, 124eqeltrd 2850 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ)
152151adantlr 686 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ)
153 rpre 12042 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
154153ad2antlr 698 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑥 ∈ ℝ)
155 lelttr 10330 . . . . . . . . . . 11 (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ ∧ (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
156150, 152, 154, 155syl3anc 1476 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
157129, 156mpand 667 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
158141adantr 466 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
159158, 142, 143syl2an 575 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
160157, 159jctild 509 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
161160anassrs 458 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑛 ∈ (ℤ𝑗)) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
162161ralrimdva 3118 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
16325, 162syld 47 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
164163reximdva 3165 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∃𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
165164ralimdva 3111 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
16614, 165mpd 15 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
1671, 3, 166caurcvg2 14616 1 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wo 826  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  Vcvv 3351   class class class wbr 4786  dom cdm 5249  wf 6027  cfv 6031  (class class class)co 6793  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143   < clt 10276  cle 10277  cmin 10468  -cneg 10469   / cdiv 10886  cn 11222  2c2 11272  0cn0 11494  cz 11579  cuz 11888  +crp 12035  seqcseq 13008  cexp 13067  abscabs 14182  cli 14423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-rp 12036  df-ico 12386  df-fz 12534  df-fl 12801  df-seq 13009  df-exp 13068  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-limsup 14410  df-clim 14427  df-rlim 14428
This theorem is referenced by:  leibpi  24890
  Copyright terms: Public domain W3C validator