ballotlem1c - Mathbox for Thierry Arnoux

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

Theorem ballotlem1c 35244

Description: If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017.)

**Hypotheses**
Ref	Expression
ballotth.m	⊢ 𝑀 ∈ ℕ
ballotth.n	⊢ 𝑁 ∈ ℕ
ballotth.o	⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}
ballotth.p	⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
ballotth.f	⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))
ballotth.e	⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}
ballotth.mgtn	⊢ 𝑁 < 𝑀
ballotth.i	⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))

**Assertion**
Ref	Expression
ballotlem1c	⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ¬ (𝐼‘𝐶) ∈ 𝐶)

Distinct variable groups: 𝑀,𝑐 𝑁,𝑐 𝑂,𝑐 𝑖,𝑀 𝑖,𝑁 𝑖,𝑂 𝑘,𝑀 𝑘,𝑁 𝑘,𝑂 𝑖,𝑐,𝐹,𝑘 𝐶,𝑖,𝑘 𝑖,𝐸,𝑘 𝐶,𝑘 𝑘,𝐼 𝑘,𝑐,𝐸 𝑖,𝐼 Allowed substitution hints: 𝐶(𝑥, 𝑐) 𝑃(𝑥, 𝑖, 𝑘, 𝑐) 𝐸(𝑥) 𝐹(𝑥) 𝐼(𝑥, 𝑐) 𝑀(𝑥) 𝑁(𝑥) 𝑂(𝑥)

**Proof of Theorem ballotlem1c**
Step	Hyp	Ref	Expression
1		ballotth.m	. . 3 ⊢ 𝑀 ∈ ℕ
2		ballotth.n	. . 3 ⊢ 𝑁 ∈ ℕ
3		ballotth.o	. . 3 ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}
4		ballotth.p	. . 3 ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
5		ballotth.f	. . 3 ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))
6		eldifi 4070	. . . 4 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 𝐶 ∈ 𝑂)
7	6	ad2antrr 739	. . 3 ⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → 𝐶 ∈ 𝑂)
8		ballotth.e	. . . . . . . . . 10 ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}
9		ballotth.mgtn	. . . . . . . . . 10 ⊢ 𝑁 < 𝑀
10		ballotth.i	. . . . . . . . . 10 ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))
11	1, 2, 3, 4, 5, 8, 9, 10	ballotlemiex 35238	. . . . . . . . 9 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0))
12	11	simpld 500	. . . . . . . 8 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)))
13		elfznn 13725	. . . . . . . 8 ⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ∈ ℕ)
14	12, 13	syl 18	. . . . . . 7 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℕ)
15	14	adantr 486	. . . . . 6 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (𝐼‘𝐶) ∈ ℕ)
16	1, 2, 3, 4, 5, 8, 9, 10	ballotlemii 35240	. . . . . 6 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (𝐼‘𝐶) ≠ 1)
17		eluz2b3 13087	. . . . . 6 ⊢ ((𝐼‘𝐶) ∈ (ℤ_≥‘2) ↔ ((𝐼‘𝐶) ∈ ℕ ∧ (𝐼‘𝐶) ≠ 1))
18	15, 16, 17	sylanbrc 595	. . . . 5 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (𝐼‘𝐶) ∈ (ℤ_≥‘2))
19		uz2m1nn 13088	. . . . 5 ⊢ ((𝐼‘𝐶) ∈ (ℤ_≥‘2) → ((𝐼‘𝐶) − 1) ∈ ℕ)
20	18, 19	syl 18	. . . 4 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ((𝐼‘𝐶) − 1) ∈ ℕ)
21	20	adantr 486	. . 3 ⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐼‘𝐶) − 1) ∈ ℕ)
22		fveq2 6914	. . . . 5 ⊢ (𝑖 = 1 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘1))
23	22	breq2d 5118	. . . 4 ⊢ (𝑖 = 1 → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘1)))
24		elnnuz 13043	. . . . . . 7 ⊢ (((𝐼‘𝐶) − 1) ∈ ℕ ↔ ((𝐼‘𝐶) − 1) ∈ (ℤ_≥‘1))
25	24	biimpi 219	. . . . . 6 ⊢ (((𝐼‘𝐶) − 1) ∈ ℕ → ((𝐼‘𝐶) − 1) ∈ (ℤ_≥‘1))
26		eluzfz1 13702	. . . . . 6 ⊢ (((𝐼‘𝐶) − 1) ∈ (ℤ_≥‘1) → 1 ∈ (1...((𝐼‘𝐶) − 1)))
27	20, 25, 26	3syl 19	. . . . 5 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → 1 ∈ (1...((𝐼‘𝐶) − 1)))
28	27	adantr 486	. . . 4 ⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → 1 ∈ (1...((𝐼‘𝐶) − 1)))
29		0le1 11877	. . . . . . 7 ⊢ 0 ≤ 1
30		1e0p1 12899	. . . . . . 7 ⊢ 1 = (0 + 1)
31	29, 30	breqtri 5134	. . . . . 6 ⊢ 0 ≤ (0 + 1)
32		1nn 12384	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
33	32	a1i 11	. . . . . . . . . 10 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 1 ∈ ℕ)
34	1, 2, 3, 4, 5, 6, 33	ballotlemfp1 35228	. . . . . . . . 9 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((¬ 1 ∈ 𝐶 → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) − 1)) ∧ (1 ∈ 𝐶 → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) + 1))))
35	34	simprd 501	. . . . . . . 8 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (1 ∈ 𝐶 → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) + 1)))
36	35	imp 412	. . . . . . 7 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) + 1))
37		1m1e0 12453	. . . . . . . . . 10 ⊢ (1 − 1) = 0
38	37	fveq2i 6917	. . . . . . . . 9 ⊢ ((𝐹‘𝐶)‘(1 − 1)) = ((𝐹‘𝐶)‘0)
39	38	oveq1i 7459	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘(1 − 1)) + 1) = (((𝐹‘𝐶)‘0) + 1)
40	39	a1i 11	. . . . . . 7 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (((𝐹‘𝐶)‘(1 − 1)) + 1) = (((𝐹‘𝐶)‘0) + 1))
41	1, 2, 3, 4, 5	ballotlemfval0 35232	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘0) = 0)
42	6, 41	syl 18	. . . . . . . . 9 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐹‘𝐶)‘0) = 0)
43	42	adantr 486	. . . . . . . 8 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ((𝐹‘𝐶)‘0) = 0)
44	43	oveq1d 7464	. . . . . . 7 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (((𝐹‘𝐶)‘0) + 1) = (0 + 1))
45	36, 40, 44	3eqtrrd 2803	. . . . . 6 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (0 + 1) = ((𝐹‘𝐶)‘1))
46	31, 45	breqtrid 5146	. . . . 5 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘1))
47	46	adantr 486	. . . 4 ⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘1))
48	23, 28, 47	rspcedvdw 3583	. . 3 ⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → ∃𝑖 ∈ (1...((𝐼‘𝐶) − 1))0 ≤ ((𝐹‘𝐶)‘𝑖))
49		df-neg 11581	. . . . . 6 ⊢ -1 = (0 − 1)
50	1, 2, 3, 4, 5, 6, 14	ballotlemfp1 35228	. . . . . . . . . 10 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((¬ (𝐼‘𝐶) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) − 1)) ∧ ((𝐼‘𝐶) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) + 1))))
51	50	simprd 501	. . . . . . . . 9 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) + 1)))
52	51	imp 412	. . . . . . . 8 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) + 1))
53	11	simprd 501	. . . . . . . . 9 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)
54	53	adantr 486	. . . . . . . 8 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)
55	52, 54	eqtr3d 2800	. . . . . . 7 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) + 1) = 0)
56		0cnd 11336	. . . . . . . 8 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → 0 ∈ ℂ)
57		1cnd 11339	. . . . . . . 8 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → 1 ∈ ℂ)
58	6	adantr 486	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → 𝐶 ∈ 𝑂)
59	14	nnzd 12757	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℤ)
60	59	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → (𝐼‘𝐶) ∈ ℤ)
61		1zzd 12765	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → 1 ∈ ℤ)
62	60, 61	zsubcld 12846	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐼‘𝐶) − 1) ∈ ℤ)
63	1, 2, 3, 4, 5, 58, 62	ballotlemfelz 35227	. . . . . . . . 9 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) ∈ ℤ)
64	63	zcnd 12842	. . . . . . . 8 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) ∈ ℂ)
65	56, 57, 64	subadd2d 11725	. . . . . . 7 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((0 − 1) = ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) ↔ (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) + 1) = 0))
66	55, 65	mpbird 260	. . . . . 6 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → (0 − 1) = ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)))
67	49, 66	eqtrid 2810	. . . . 5 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → -1 = ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)))
68		neg1lt0 12346	. . . . 5 ⊢ -1 < 0
69	67, 68	eqbrtrrdi 5149	. . . 4 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) < 0)
70	69	adantlr 728	. . 3 ⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) < 0)
71	1, 2, 3, 4, 5, 7, 21, 48, 70	ballotlemfcc 35230	. 2 ⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0)
72	1, 2, 3, 4, 5, 8, 9, 10	ballotlemimin 35242	. . 3 ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ¬ ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0)
73	72	ad2antrr 739	. 2 ⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → ¬ ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0)
74	71, 73	pm2.65da 829	1 ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ¬ (𝐼‘𝐶) ∈ 𝐶)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 ∖ cdif 4048 ∩ cin 4092 𝒫 cpw 4560 class class class wbr 5106 ↦ cmpt 5190 ‘cfv 6564 (class class class)co 7449 infcinf 9468 ℝcr 11236 0cc0 11237 1c1 11238 + caddc 11240 < clt 11380 ≤ cle 11381 − cmin 11578 -cneg 11579 / cdiv 12011 ℕcn 12373 2c2 12435 ℤcz 12731 ℤ_≥cuz 13003 ...cfz 13677 ♯chash 14513

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-cnex 11293 ax-resscn 11294 ax-1cn 11295 ax-icn 11296 ax-addcl 11297 ax-addrcl 11298 ax-mulcl 11299 ax-mulrcl 11300 ax-mulcom 11301 ax-addass 11302 ax-mulass 11303 ax-distr 11304 ax-i2m1 11305 ax-1ne0 11306 ax-1rid 11307 ax-rnegex 11308 ax-rrecex 11309 ax-cnre 11310 ax-pre-lttri 11311 ax-pre-lttrn 11312 ax-pre-ltadd 11313 ax-pre-mulgt0 11314

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-om 7910 df-1st 8033 df-2nd 8034 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-1o 8512 df-oadd 8516 df-er 8753 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-sup 9469 df-inf 9470 df-dju 10017 df-card 10055 df-pnf 11382 df-mnf 11383 df-xr 11384 df-ltxr 11385 df-le 11386 df-sub 11580 df-neg 11581 df-nn 12374 df-2 12443 df-n0 12645 df-z 12732 df-uz 13004 df-fz 13678 df-hash 14514

This theorem is used by: ballotlem7 35272

W3C validator