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

Theorem iseralt 15495
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 15468.) (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 13824 . . 3 seq𝑀( + , 𝐹) ∈ V
32a1i 11 . 2 (𝜑 → seq𝑀( + , 𝐹) ∈ V)
4 iseralt.5 . . . 4 (𝜑𝐺 ⇝ 0)
5 iseralt.2 . . . . 5 (𝜑𝑀 ∈ ℤ)
6 climrel 15300 . . . . . . 7 Rel ⇝
76brrelex1i 5674 . . . . . 6 (𝐺 ⇝ 0 → 𝐺 ∈ V)
84, 7syl 17 . . . . 5 (𝜑𝐺 ∈ V)
9 eqidd 2737 . . . . 5 ((𝜑𝑛𝑍) → (𝐺𝑛) = (𝐺𝑛))
10 iseralt.3 . . . . . . 7 (𝜑𝐺:𝑍⟶ℝ)
1110ffvelcdmda 7017 . . . . . 6 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ ℝ)
1211recnd 11104 . . . . 5 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ ℂ)
131, 5, 8, 9, 12clim0c 15315 . . . 4 (𝜑 → (𝐺 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥))
144, 13mpbid 231 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥)
15 simpr 485 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗𝑍)
1615, 1eleqtrdi 2847 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
17 eluzelz 12693 . . . . . . . 8 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
18 uzid 12698 . . . . . . . 8 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
1916, 17, 183syl 18 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑗))
20 peano2uz 12742 . . . . . . 7 (𝑗 ∈ (ℤ𝑗) → (𝑗 + 1) ∈ (ℤ𝑗))
21 2fveq3 6830 . . . . . . . . 9 (𝑛 = (𝑗 + 1) → (abs‘(𝐺𝑛)) = (abs‘(𝐺‘(𝑗 + 1))))
2221breq1d 5102 . . . . . . . 8 (𝑛 = (𝑗 + 1) → ((abs‘(𝐺𝑛)) < 𝑥 ↔ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
2322rspcv 3566 . . . . . . 7 ((𝑗 + 1) ∈ (ℤ𝑗) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
2419, 20, 233syl 18 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
25 eluzelz 12693 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ𝑗) → 𝑛 ∈ ℤ)
2625ad2antll 726 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℤ)
2726zcnd 12528 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℂ)
2817, 1eleq2s 2855 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗𝑍𝑗 ∈ ℤ)
2928ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℤ)
3029zcnd 12528 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℂ)
3127, 30subcld 11433 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℂ)
32 2cnd 12152 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ∈ ℂ)
33 2ne0 12178 . . . . . . . . . . . . . . . . . . . . 21 2 ≠ 0
3433a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ≠ 0)
3531, 32, 34divcan2d 11854 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((𝑛𝑗) / 2)) = (𝑛𝑗))
3635oveq2d 7353 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((𝑛𝑗) / 2))) = (𝑗 + (𝑛𝑗)))
3730, 27pncan3d 11436 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (𝑛𝑗)) = 𝑛)
3836, 37eqtr2d 2777 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 = (𝑗 + (2 · ((𝑛𝑗) / 2))))
3938adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝑛 = (𝑗 + (2 · ((𝑛𝑗) / 2))))
4039fveq2d 6829 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))))
4140fvoveq1d 7359 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))))
42 simpll 764 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝜑)
43 simpl 483 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → 𝑗𝑍)
4443ad2antlr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝑗𝑍)
45 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → ((𝑛𝑗) / 2) ∈ ℤ)
4626, 29zsubcld 12532 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℤ)
4746zred 12527 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℝ)
48 2rp 12836 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ+
4948a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ∈ ℝ+)
50 eluzle 12696 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ𝑗) → 𝑗𝑛)
5150ad2antll 726 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗𝑛)
5226zred 12527 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℝ)
5329zred 12527 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℝ)
5452, 53subge0d 11666 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (0 ≤ (𝑛𝑗) ↔ 𝑗𝑛))
5551, 54mpbird 256 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ (𝑛𝑗))
5647, 49, 55divge0d 12913 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ ((𝑛𝑗) / 2))
5756adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 0 ≤ ((𝑛𝑗) / 2))
58 elnn0z 12433 . . . . . . . . . . . . . . . 16 (((𝑛𝑗) / 2) ∈ ℕ0 ↔ (((𝑛𝑗) / 2) ∈ ℤ ∧ 0 ≤ ((𝑛𝑗) / 2)))
5945, 57, 58sylanbrc 583 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → ((𝑛𝑗) / 2) ∈ ℕ0)
60 iseralt.4 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
61 iseralt.6 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
621, 5, 10, 60, 4, 61iseraltlem3 15494 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑍 ∧ ((𝑛𝑗) / 2) ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((𝑛𝑗) / 2))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))))
6362simpld 495 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍 ∧ ((𝑛𝑗) / 2) ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
6442, 44, 59, 63syl3anc 1370 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
6541, 64eqbrtrd 5114 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
66 2div2e1 12215 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 / 2) = 1
6766oveq2i 7348 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑛𝑗) + 1) / 2) − (2 / 2)) = ((((𝑛𝑗) + 1) / 2) − 1)
68 peano2cn 11248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛𝑗) ∈ ℂ → ((𝑛𝑗) + 1) ∈ ℂ)
6931, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℂ)
7069, 32, 32, 34divsubdird 11891 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) − 2) / 2) = ((((𝑛𝑗) + 1) / 2) − (2 / 2)))
71 df-2 12137 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 = (1 + 1)
7271oveq2i 7348 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑛𝑗) + 1) − 2) = (((𝑛𝑗) + 1) − (1 + 1))
73 ax-1cn 11030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
7473a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 1 ∈ ℂ)
7531, 74, 74pnpcan2d 11471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) − (1 + 1)) = ((𝑛𝑗) − 1))
7672, 75eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) − 2) = ((𝑛𝑗) − 1))
7776oveq1d 7352 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) − 2) / 2) = (((𝑛𝑗) − 1) / 2))
7870, 77eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) / 2) − (2 / 2)) = (((𝑛𝑗) − 1) / 2))
7967, 78eqtr3id 2790 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) / 2) − 1) = (((𝑛𝑗) − 1) / 2))
8079oveq2d 7353 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((((𝑛𝑗) + 1) / 2) − 1)) = (2 · (((𝑛𝑗) − 1) / 2)))
81 subcl 11321 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛𝑗) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛𝑗) − 1) ∈ ℂ)
8231, 73, 81sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) − 1) ∈ ℂ)
8382, 32, 34divcan2d 11854 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · (((𝑛𝑗) − 1) / 2)) = ((𝑛𝑗) − 1))
8427, 30, 74sub32d 11465 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) − 1) = ((𝑛 − 1) − 𝑗))
8580, 83, 843eqtrd 2780 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((((𝑛𝑗) + 1) / 2) − 1)) = ((𝑛 − 1) − 𝑗))
8685oveq2d 7353 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) = (𝑗 + ((𝑛 − 1) − 𝑗)))
87 subcl 11321 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑛 − 1) ∈ ℂ)
8827, 73, 87sylancl 586 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛 − 1) ∈ ℂ)
8930, 88pncan3d 11436 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + ((𝑛 − 1) − 𝑗)) = (𝑛 − 1))
9086, 89eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) = (𝑛 − 1))
9190oveq1d 7352 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1) = ((𝑛 − 1) + 1))
92 npcan 11331 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
9327, 73, 92sylancl 586 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛 − 1) + 1) = 𝑛)
9491, 93eqtr2d 2777 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 = ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1))
9594adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝑛 = ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1))
9695fveq2d 6829 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)))
9796fvoveq1d 7359 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))))
98 simpll 764 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝜑)
9943ad2antlr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝑗𝑍)
100 simpr 485 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (((𝑛𝑗) + 1) / 2) ∈ ℤ)
101 uznn0sub 12718 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ𝑗) → (𝑛𝑗) ∈ ℕ0)
102101ad2antll 726 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℕ0)
103 nn0p1nn 12373 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛𝑗) ∈ ℕ0 → ((𝑛𝑗) + 1) ∈ ℕ)
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℕ)
105104nnrpd 12871 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℝ+)
106105rphalfcld 12885 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) / 2) ∈ ℝ+)
107106rpgt0d 12876 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 < (((𝑛𝑗) + 1) / 2))
108107adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 0 < (((𝑛𝑗) + 1) / 2))
109 elnnz 12430 . . . . . . . . . . . . . . . . 17 ((((𝑛𝑗) + 1) / 2) ∈ ℕ ↔ ((((𝑛𝑗) + 1) / 2) ∈ ℤ ∧ 0 < (((𝑛𝑗) + 1) / 2)))
110100, 108, 109sylanbrc 583 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (((𝑛𝑗) + 1) / 2) ∈ ℕ)
111 nnm1nn0 12375 . . . . . . . . . . . . . . . 16 ((((𝑛𝑗) + 1) / 2) ∈ ℕ → ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0)
112110, 111syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0)
1131, 5, 10, 60, 4, 61iseraltlem3 15494 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑍 ∧ ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))))
114113simprd 496 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍 ∧ ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
11598, 99, 112, 114syl3anc 1370 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
11697, 115eqbrtrd 5114 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
117 zeo 12507 . . . . . . . . . . . . . 14 ((𝑛𝑗) ∈ ℤ → (((𝑛𝑗) / 2) ∈ ℤ ∨ (((𝑛𝑗) + 1) / 2) ∈ ℤ))
11846, 117syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) / 2) ∈ ℤ ∨ (((𝑛𝑗) + 1) / 2) ∈ ℤ))
11965, 116, 118mpjaodan 956 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
1201peano2uzs 12743 . . . . . . . . . . . . . . 15 (𝑗𝑍 → (𝑗 + 1) ∈ 𝑍)
121120adantr 481 . . . . . . . . . . . . . 14 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → (𝑗 + 1) ∈ 𝑍)
122 ffvelcdm 7015 . . . . . . . . . . . . . 14 ((𝐺:𝑍⟶ℝ ∧ (𝑗 + 1) ∈ 𝑍) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
12310, 121, 122syl2an 596 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
1241, 5, 10, 60, 4iseraltlem1 15492 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑗 + 1)))
125121, 124sylan2 593 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ (𝐺‘(𝑗 + 1)))
126123, 125absidd 15233 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) = (𝐺‘(𝑗 + 1)))
127119, 126breqtrrd 5120 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))))
128127adantlr 712 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))))
129 neg1rr 12189 . . . . . . . . . . . . . . . . . . . . 21 -1 ∈ ℝ
130129a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → -1 ∈ ℝ)
131 neg1ne0 12190 . . . . . . . . . . . . . . . . . . . . 21 -1 ≠ 0
132131a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → -1 ≠ 0)
133 eluzelz 12693 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
134133, 1eleq2s 2855 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑍𝑘 ∈ ℤ)
135134adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
136130, 132, 135reexpclzd 14065 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
13710ffvelcdmda 7017 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
138136, 137remulcld 11106 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
13961, 138eqeltrd 2837 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
1401, 5, 139serfre 13853 . . . . . . . . . . . . . . . 16 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
1411uztrn2 12702 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → 𝑛𝑍)
142 ffvelcdm 7015 . . . . . . . . . . . . . . . 16 ((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑛𝑍) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
143140, 141, 142syl2an 596 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
144 ffvelcdm 7015 . . . . . . . . . . . . . . . 16 ((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑗𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
145140, 43, 144syl2an 596 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
146143, 145resubcld 11504 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℝ)
147146recnd 11104 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℂ)
148147abscld 15247 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ)
149148adantlr 712 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ)
150126, 123eqeltrd 2837 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ)
151150adantlr 712 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ)
152 rpre 12839 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
153152ad2antlr 724 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑥 ∈ ℝ)
154 lelttr 11166 . . . . . . . . . . 11 (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ ∧ (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
155149, 151, 153, 154syl3anc 1370 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
156128, 155mpand 692 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
157140adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
158157, 141, 142syl2an 596 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
159156, 158jctild 526 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
160159anassrs 468 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑛 ∈ (ℤ𝑗)) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
161160ralrimdva 3147 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
16224, 161syld 47 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
163162reximdva 3161 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∃𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
164163ralimdva 3160 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
16514, 164mpd 15 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
1661, 3, 165caurcvg2 15488 1 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 844  w3a 1086   = wceq 1540  wcel 2105  wne 2940  wral 3061  wrex 3070  Vcvv 3441   class class class wbr 5092  dom cdm 5620  wf 6475  cfv 6479  (class class class)co 7337  cc 10970  cr 10971  0cc0 10972  1c1 10973   + caddc 10975   · cmul 10977   < clt 11110  cle 11111  cmin 11306  -cneg 11307   / cdiv 11733  cn 12074  2c2 12129  0cn0 12334  cz 12420  cuz 12683  +crp 12831  seqcseq 13822  cexp 13883  abscabs 15044  cli 15292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-om 7781  df-1st 7899  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-er 8569  df-pm 8689  df-en 8805  df-dom 8806  df-sdom 8807  df-sup 9299  df-inf 9300  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-n0 12335  df-z 12421  df-uz 12684  df-rp 12832  df-ico 13186  df-fz 13341  df-fl 13613  df-seq 13823  df-exp 13884  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-limsup 15279  df-clim 15296  df-rlim 15297
This theorem is referenced by:  leibpi  26198
  Copyright terms: Public domain W3C validator