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

Theorem iseralt 15248
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 15221.) (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 13576 . . 3 seq𝑀( + , 𝐹) ∈ V
32a1i 11 . 2 (𝜑 → seq𝑀( + , 𝐹) ∈ V)
4 iseralt.5 . . . 4 (𝜑𝐺 ⇝ 0)
5 iseralt.2 . . . . 5 (𝜑𝑀 ∈ ℤ)
6 climrel 15053 . . . . . . 7 Rel ⇝
76brrelex1i 5605 . . . . . 6 (𝐺 ⇝ 0 → 𝐺 ∈ V)
84, 7syl 17 . . . . 5 (𝜑𝐺 ∈ V)
9 eqidd 2738 . . . . 5 ((𝜑𝑛𝑍) → (𝐺𝑛) = (𝐺𝑛))
10 iseralt.3 . . . . . . 7 (𝜑𝐺:𝑍⟶ℝ)
1110ffvelrnda 6904 . . . . . 6 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ ℝ)
1211recnd 10861 . . . . 5 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ ℂ)
131, 5, 8, 9, 12clim0c 15068 . . . 4 (𝜑 → (𝐺 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥))
144, 13mpbid 235 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥)
15 simpr 488 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗𝑍)
1615, 1eleqtrdi 2848 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
17 eluzelz 12448 . . . . . . . 8 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
18 uzid 12453 . . . . . . . 8 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
1916, 17, 183syl 18 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑗))
20 peano2uz 12497 . . . . . . 7 (𝑗 ∈ (ℤ𝑗) → (𝑗 + 1) ∈ (ℤ𝑗))
21 2fveq3 6722 . . . . . . . . 9 (𝑛 = (𝑗 + 1) → (abs‘(𝐺𝑛)) = (abs‘(𝐺‘(𝑗 + 1))))
2221breq1d 5063 . . . . . . . 8 (𝑛 = (𝑗 + 1) → ((abs‘(𝐺𝑛)) < 𝑥 ↔ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
2322rspcv 3532 . . . . . . 7 ((𝑗 + 1) ∈ (ℤ𝑗) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
2419, 20, 233syl 18 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
25 eluzelz 12448 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ𝑗) → 𝑛 ∈ ℤ)
2625ad2antll 729 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℤ)
2726zcnd 12283 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℂ)
2817, 1eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗𝑍𝑗 ∈ ℤ)
2928ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℤ)
3029zcnd 12283 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℂ)
3127, 30subcld 11189 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℂ)
32 2cnd 11908 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ∈ ℂ)
33 2ne0 11934 . . . . . . . . . . . . . . . . . . . . 21 2 ≠ 0
3433a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ≠ 0)
3531, 32, 34divcan2d 11610 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((𝑛𝑗) / 2)) = (𝑛𝑗))
3635oveq2d 7229 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((𝑛𝑗) / 2))) = (𝑗 + (𝑛𝑗)))
3730, 27pncan3d 11192 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (𝑛𝑗)) = 𝑛)
3836, 37eqtr2d 2778 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 = (𝑗 + (2 · ((𝑛𝑗) / 2))))
3938adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝑛 = (𝑗 + (2 · ((𝑛𝑗) / 2))))
4039fveq2d 6721 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))))
4140fvoveq1d 7235 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))))
42 simpll 767 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝜑)
43 simpl 486 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → 𝑗𝑍)
4443ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝑗𝑍)
45 simpr 488 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → ((𝑛𝑗) / 2) ∈ ℤ)
4626, 29zsubcld 12287 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℤ)
4746zred 12282 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℝ)
48 2rp 12591 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ+
4948a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ∈ ℝ+)
50 eluzle 12451 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ𝑗) → 𝑗𝑛)
5150ad2antll 729 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗𝑛)
5226zred 12282 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℝ)
5329zred 12282 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℝ)
5452, 53subge0d 11422 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (0 ≤ (𝑛𝑗) ↔ 𝑗𝑛))
5551, 54mpbird 260 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ (𝑛𝑗))
5647, 49, 55divge0d 12668 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ ((𝑛𝑗) / 2))
5756adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 0 ≤ ((𝑛𝑗) / 2))
58 elnn0z 12189 . . . . . . . . . . . . . . . 16 (((𝑛𝑗) / 2) ∈ ℕ0 ↔ (((𝑛𝑗) / 2) ∈ ℤ ∧ 0 ≤ ((𝑛𝑗) / 2)))
5945, 57, 58sylanbrc 586 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → ((𝑛𝑗) / 2) ∈ ℕ0)
60 iseralt.4 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
61 iseralt.6 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
621, 5, 10, 60, 4, 61iseraltlem3 15247 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑍 ∧ ((𝑛𝑗) / 2) ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((𝑛𝑗) / 2))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))))
6362simpld 498 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍 ∧ ((𝑛𝑗) / 2) ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
6442, 44, 59, 63syl3anc 1373 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
6541, 64eqbrtrd 5075 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
66 2div2e1 11971 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 / 2) = 1
6766oveq2i 7224 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑛𝑗) + 1) / 2) − (2 / 2)) = ((((𝑛𝑗) + 1) / 2) − 1)
68 peano2cn 11004 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛𝑗) ∈ ℂ → ((𝑛𝑗) + 1) ∈ ℂ)
6931, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℂ)
7069, 32, 32, 34divsubdird 11647 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) − 2) / 2) = ((((𝑛𝑗) + 1) / 2) − (2 / 2)))
71 df-2 11893 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 = (1 + 1)
7271oveq2i 7224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑛𝑗) + 1) − 2) = (((𝑛𝑗) + 1) − (1 + 1))
73 ax-1cn 10787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
7473a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 1 ∈ ℂ)
7531, 74, 74pnpcan2d 11227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) − (1 + 1)) = ((𝑛𝑗) − 1))
7672, 75syl5eq 2790 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) − 2) = ((𝑛𝑗) − 1))
7776oveq1d 7228 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) − 2) / 2) = (((𝑛𝑗) − 1) / 2))
7870, 77eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) / 2) − (2 / 2)) = (((𝑛𝑗) − 1) / 2))
7967, 78eqtr3id 2792 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) / 2) − 1) = (((𝑛𝑗) − 1) / 2))
8079oveq2d 7229 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((((𝑛𝑗) + 1) / 2) − 1)) = (2 · (((𝑛𝑗) − 1) / 2)))
81 subcl 11077 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛𝑗) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛𝑗) − 1) ∈ ℂ)
8231, 73, 81sylancl 589 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) − 1) ∈ ℂ)
8382, 32, 34divcan2d 11610 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · (((𝑛𝑗) − 1) / 2)) = ((𝑛𝑗) − 1))
8427, 30, 74sub32d 11221 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) − 1) = ((𝑛 − 1) − 𝑗))
8580, 83, 843eqtrd 2781 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((((𝑛𝑗) + 1) / 2) − 1)) = ((𝑛 − 1) − 𝑗))
8685oveq2d 7229 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) = (𝑗 + ((𝑛 − 1) − 𝑗)))
87 subcl 11077 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑛 − 1) ∈ ℂ)
8827, 73, 87sylancl 589 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛 − 1) ∈ ℂ)
8930, 88pncan3d 11192 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + ((𝑛 − 1) − 𝑗)) = (𝑛 − 1))
9086, 89eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) = (𝑛 − 1))
9190oveq1d 7228 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1) = ((𝑛 − 1) + 1))
92 npcan 11087 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
9327, 73, 92sylancl 589 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛 − 1) + 1) = 𝑛)
9491, 93eqtr2d 2778 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 = ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1))
9594adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝑛 = ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1))
9695fveq2d 6721 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)))
9796fvoveq1d 7235 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))))
98 simpll 767 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝜑)
9943ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝑗𝑍)
100 simpr 488 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (((𝑛𝑗) + 1) / 2) ∈ ℤ)
101 uznn0sub 12473 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ𝑗) → (𝑛𝑗) ∈ ℕ0)
102101ad2antll 729 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℕ0)
103 nn0p1nn 12129 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛𝑗) ∈ ℕ0 → ((𝑛𝑗) + 1) ∈ ℕ)
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℕ)
105104nnrpd 12626 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℝ+)
106105rphalfcld 12640 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) / 2) ∈ ℝ+)
107106rpgt0d 12631 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 < (((𝑛𝑗) + 1) / 2))
108107adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 0 < (((𝑛𝑗) + 1) / 2))
109 elnnz 12186 . . . . . . . . . . . . . . . . 17 ((((𝑛𝑗) + 1) / 2) ∈ ℕ ↔ ((((𝑛𝑗) + 1) / 2) ∈ ℤ ∧ 0 < (((𝑛𝑗) + 1) / 2)))
110100, 108, 109sylanbrc 586 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (((𝑛𝑗) + 1) / 2) ∈ ℕ)
111 nnm1nn0 12131 . . . . . . . . . . . . . . . 16 ((((𝑛𝑗) + 1) / 2) ∈ ℕ → ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0)
112110, 111syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0)
1131, 5, 10, 60, 4, 61iseraltlem3 15247 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑍 ∧ ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))))
114113simprd 499 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍 ∧ ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
11598, 99, 112, 114syl3anc 1373 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
11697, 115eqbrtrd 5075 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
117 zeo 12263 . . . . . . . . . . . . . 14 ((𝑛𝑗) ∈ ℤ → (((𝑛𝑗) / 2) ∈ ℤ ∨ (((𝑛𝑗) + 1) / 2) ∈ ℤ))
11846, 117syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) / 2) ∈ ℤ ∨ (((𝑛𝑗) + 1) / 2) ∈ ℤ))
11965, 116, 118mpjaodan 959 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
1201peano2uzs 12498 . . . . . . . . . . . . . . 15 (𝑗𝑍 → (𝑗 + 1) ∈ 𝑍)
121120adantr 484 . . . . . . . . . . . . . 14 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → (𝑗 + 1) ∈ 𝑍)
122 ffvelrn 6902 . . . . . . . . . . . . . 14 ((𝐺:𝑍⟶ℝ ∧ (𝑗 + 1) ∈ 𝑍) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
12310, 121, 122syl2an 599 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
1241, 5, 10, 60, 4iseraltlem1 15245 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑗 + 1)))
125121, 124sylan2 596 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ (𝐺‘(𝑗 + 1)))
126123, 125absidd 14986 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) = (𝐺‘(𝑗 + 1)))
127119, 126breqtrrd 5081 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))))
128127adantlr 715 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))))
129 neg1rr 11945 . . . . . . . . . . . . . . . . . . . . 21 -1 ∈ ℝ
130129a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → -1 ∈ ℝ)
131 neg1ne0 11946 . . . . . . . . . . . . . . . . . . . . 21 -1 ≠ 0
132131a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → -1 ≠ 0)
133 eluzelz 12448 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
134133, 1eleq2s 2856 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑍𝑘 ∈ ℤ)
135134adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
136130, 132, 135reexpclzd 13816 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
13710ffvelrnda 6904 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
138136, 137remulcld 10863 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
13961, 138eqeltrd 2838 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
1401, 5, 139serfre 13605 . . . . . . . . . . . . . . . 16 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
1411uztrn2 12457 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → 𝑛𝑍)
142 ffvelrn 6902 . . . . . . . . . . . . . . . 16 ((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑛𝑍) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
143140, 141, 142syl2an 599 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
144 ffvelrn 6902 . . . . . . . . . . . . . . . 16 ((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑗𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
145140, 43, 144syl2an 599 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
146143, 145resubcld 11260 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℝ)
147146recnd 10861 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℂ)
148147abscld 15000 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ)
149148adantlr 715 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ)
150126, 123eqeltrd 2838 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ)
151150adantlr 715 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ)
152 rpre 12594 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
153152ad2antlr 727 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑥 ∈ ℝ)
154 lelttr 10923 . . . . . . . . . . 11 (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ ∧ (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
155149, 151, 153, 154syl3anc 1373 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
156128, 155mpand 695 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
157140adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
158157, 141, 142syl2an 599 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
159156, 158jctild 529 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
160159anassrs 471 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑛 ∈ (ℤ𝑗)) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
161160ralrimdva 3110 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
16224, 161syld 47 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
163162reximdva 3193 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∃𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
164163ralimdva 3100 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
16514, 164mpd 15 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
1661, 3, 165caurcvg2 15241 1 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wo 847  w3a 1089   = wceq 1543  wcel 2110  wne 2940  wral 3061  wrex 3062  Vcvv 3408   class class class wbr 5053  dom cdm 5551  wf 6376  cfv 6380  (class class class)co 7213  cc 10727  cr 10728  0cc0 10729  1c1 10730   + caddc 10732   · cmul 10734   < clt 10867  cle 10868  cmin 11062  -cneg 11063   / cdiv 11489  cn 11830  2c2 11885  0cn0 12090  cz 12176  cuz 12438  +crp 12586  seqcseq 13574  cexp 13635  abscabs 14797  cli 15045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-er 8391  df-pm 8511  df-en 8627  df-dom 8628  df-sdom 8629  df-sup 9058  df-inf 9059  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-n0 12091  df-z 12177  df-uz 12439  df-rp 12587  df-ico 12941  df-fz 13096  df-fl 13367  df-seq 13575  df-exp 13636  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-limsup 15032  df-clim 15049  df-rlim 15050
This theorem is referenced by:  leibpi  25825
  Copyright terms: Public domain W3C validator