Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  etransclem41 Structured version   Visualization version   GIF version

Theorem etransclem41 45476
Description: ๐‘ƒ does not divide the P-1 -th derivative of ๐น applied to 0. This is the first part of case 2: proven in in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
etransclem41.m (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0)
etransclem41.p (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™)
etransclem41.mp (๐œ‘ โ†’ (!โ€˜๐‘€) < ๐‘ƒ)
etransclem41.f ๐น = (๐‘ฅ โˆˆ โ„ โ†ฆ ((๐‘ฅโ†‘(๐‘ƒ โˆ’ 1)) ยท โˆ๐‘— โˆˆ (1...๐‘€)((๐‘ฅ โˆ’ ๐‘—)โ†‘๐‘ƒ)))
Assertion
Ref Expression
etransclem41 (๐œ‘ โ†’ ยฌ ๐‘ƒ โˆฅ ((((โ„ D๐‘› ๐น)โ€˜(๐‘ƒ โˆ’ 1))โ€˜0) / (!โ€˜(๐‘ƒ โˆ’ 1))))
Distinct variable groups:   ๐‘—,๐‘€,๐‘ฅ   ๐‘ƒ,๐‘—,๐‘ฅ   ๐œ‘,๐‘—,๐‘ฅ
Allowed substitution hints:   ๐น(๐‘ฅ,๐‘—)

Proof of Theorem etransclem41
Dummy variables ๐‘ ๐‘‘ ๐‘˜ ๐‘› ๐‘š are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 etransclem41.mp . . . . . . 7 (๐œ‘ โ†’ (!โ€˜๐‘€) < ๐‘ƒ)
2 etransclem41.m . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0)
32faccld 14241 . . . . . . . . 9 (๐œ‘ โ†’ (!โ€˜๐‘€) โˆˆ โ„•)
43nnred 12224 . . . . . . . 8 (๐œ‘ โ†’ (!โ€˜๐‘€) โˆˆ โ„)
5 etransclem41.p . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™)
6 prmnn 16608 . . . . . . . . . 10 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
75, 6syl 17 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•)
87nnred 12224 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„)
94, 8ltnled 11358 . . . . . . 7 (๐œ‘ โ†’ ((!โ€˜๐‘€) < ๐‘ƒ โ†” ยฌ ๐‘ƒ โ‰ค (!โ€˜๐‘€)))
101, 9mpbid 231 . . . . . 6 (๐œ‘ โ†’ ยฌ ๐‘ƒ โ‰ค (!โ€˜๐‘€))
117nnzd 12582 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„ค)
1211, 3jca 511 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒ โˆˆ โ„ค โˆง (!โ€˜๐‘€) โˆˆ โ„•))
1312adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘ƒ โˆฅ (!โ€˜๐‘€)) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง (!โ€˜๐‘€) โˆˆ โ„•))
14 simpr 484 . . . . . . 7 ((๐œ‘ โˆง ๐‘ƒ โˆฅ (!โ€˜๐‘€)) โ†’ ๐‘ƒ โˆฅ (!โ€˜๐‘€))
15 dvdsle 16250 . . . . . . 7 ((๐‘ƒ โˆˆ โ„ค โˆง (!โ€˜๐‘€) โˆˆ โ„•) โ†’ (๐‘ƒ โˆฅ (!โ€˜๐‘€) โ†’ ๐‘ƒ โ‰ค (!โ€˜๐‘€)))
1613, 14, 15sylc 65 . . . . . 6 ((๐œ‘ โˆง ๐‘ƒ โˆฅ (!โ€˜๐‘€)) โ†’ ๐‘ƒ โ‰ค (!โ€˜๐‘€))
1710, 16mtand 813 . . . . 5 (๐œ‘ โ†’ ยฌ ๐‘ƒ โˆฅ (!โ€˜๐‘€))
18 fzfid 13935 . . . . . . . . . 10 (โŠค โ†’ (1...๐‘€) โˆˆ Fin)
19 elfzelz 13498 . . . . . . . . . . . . 13 (๐‘— โˆˆ (1...๐‘€) โ†’ ๐‘— โˆˆ โ„ค)
2019znegcld 12665 . . . . . . . . . . . 12 (๐‘— โˆˆ (1...๐‘€) โ†’ -๐‘— โˆˆ โ„ค)
2120zcnd 12664 . . . . . . . . . . 11 (๐‘— โˆˆ (1...๐‘€) โ†’ -๐‘— โˆˆ โ„‚)
2221adantl 481 . . . . . . . . . 10 ((โŠค โˆง ๐‘— โˆˆ (1...๐‘€)) โ†’ -๐‘— โˆˆ โ„‚)
2318, 22fprodabs2 44796 . . . . . . . . 9 (โŠค โ†’ (absโ€˜โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—) = โˆ๐‘— โˆˆ (1...๐‘€)(absโ€˜-๐‘—))
2423mptru 1540 . . . . . . . 8 (absโ€˜โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—) = โˆ๐‘— โˆˆ (1...๐‘€)(absโ€˜-๐‘—)
2519zcnd 12664 . . . . . . . . . . 11 (๐‘— โˆˆ (1...๐‘€) โ†’ ๐‘— โˆˆ โ„‚)
2625absnegd 15393 . . . . . . . . . 10 (๐‘— โˆˆ (1...๐‘€) โ†’ (absโ€˜-๐‘—) = (absโ€˜๐‘—))
2719zred 12663 . . . . . . . . . . 11 (๐‘— โˆˆ (1...๐‘€) โ†’ ๐‘— โˆˆ โ„)
28 0red 11214 . . . . . . . . . . . 12 (๐‘— โˆˆ (1...๐‘€) โ†’ 0 โˆˆ โ„)
29 1red 11212 . . . . . . . . . . . . 13 (๐‘— โˆˆ (1...๐‘€) โ†’ 1 โˆˆ โ„)
30 0lt1 11733 . . . . . . . . . . . . . 14 0 < 1
3130a1i 11 . . . . . . . . . . . . 13 (๐‘— โˆˆ (1...๐‘€) โ†’ 0 < 1)
32 elfzle1 13501 . . . . . . . . . . . . 13 (๐‘— โˆˆ (1...๐‘€) โ†’ 1 โ‰ค ๐‘—)
3328, 29, 27, 31, 32ltletrd 11371 . . . . . . . . . . . 12 (๐‘— โˆˆ (1...๐‘€) โ†’ 0 < ๐‘—)
3428, 27, 33ltled 11359 . . . . . . . . . . 11 (๐‘— โˆˆ (1...๐‘€) โ†’ 0 โ‰ค ๐‘—)
3527, 34absidd 15366 . . . . . . . . . 10 (๐‘— โˆˆ (1...๐‘€) โ†’ (absโ€˜๐‘—) = ๐‘—)
3626, 35eqtrd 2764 . . . . . . . . 9 (๐‘— โˆˆ (1...๐‘€) โ†’ (absโ€˜-๐‘—) = ๐‘—)
3736prodeq2i 15860 . . . . . . . 8 โˆ๐‘— โˆˆ (1...๐‘€)(absโ€˜-๐‘—) = โˆ๐‘— โˆˆ (1...๐‘€)๐‘—
3824, 37eqtri 2752 . . . . . . 7 (absโ€˜โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—) = โˆ๐‘— โˆˆ (1...๐‘€)๐‘—
39 fprodfac 15914 . . . . . . . 8 (๐‘€ โˆˆ โ„•0 โ†’ (!โ€˜๐‘€) = โˆ๐‘— โˆˆ (1...๐‘€)๐‘—)
402, 39syl 17 . . . . . . 7 (๐œ‘ โ†’ (!โ€˜๐‘€) = โˆ๐‘— โˆˆ (1...๐‘€)๐‘—)
4138, 40eqtr4id 2783 . . . . . 6 (๐œ‘ โ†’ (absโ€˜โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—) = (!โ€˜๐‘€))
4241breq2d 5150 . . . . 5 (๐œ‘ โ†’ (๐‘ƒ โˆฅ (absโ€˜โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—) โ†” ๐‘ƒ โˆฅ (!โ€˜๐‘€)))
4317, 42mtbird 325 . . . 4 (๐œ‘ โ†’ ยฌ ๐‘ƒ โˆฅ (absโ€˜โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—))
44 fzfid 13935 . . . . . 6 (๐œ‘ โ†’ (1...๐‘€) โˆˆ Fin)
4520adantl 481 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ (1...๐‘€)) โ†’ -๐‘— โˆˆ โ„ค)
4644, 45fprodzcl 15895 . . . . 5 (๐œ‘ โ†’ โˆ๐‘— โˆˆ (1...๐‘€)-๐‘— โˆˆ โ„ค)
47 dvdsabsb 16216 . . . . 5 ((๐‘ƒ โˆˆ โ„ค โˆง โˆ๐‘— โˆˆ (1...๐‘€)-๐‘— โˆˆ โ„ค) โ†’ (๐‘ƒ โˆฅ โˆ๐‘— โˆˆ (1...๐‘€)-๐‘— โ†” ๐‘ƒ โˆฅ (absโ€˜โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—)))
4811, 46, 47syl2anc 583 . . . 4 (๐œ‘ โ†’ (๐‘ƒ โˆฅ โˆ๐‘— โˆˆ (1...๐‘€)-๐‘— โ†” ๐‘ƒ โˆฅ (absโ€˜โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—)))
4943, 48mtbird 325 . . 3 (๐œ‘ โ†’ ยฌ ๐‘ƒ โˆฅ โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—)
50 prmdvdsexp 16649 . . . 4 ((๐‘ƒ โˆˆ โ„™ โˆง โˆ๐‘— โˆˆ (1...๐‘€)-๐‘— โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„•) โ†’ (๐‘ƒ โˆฅ (โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—โ†‘๐‘ƒ) โ†” ๐‘ƒ โˆฅ โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—))
515, 46, 7, 50syl3anc 1368 . . 3 (๐œ‘ โ†’ (๐‘ƒ โˆฅ (โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—โ†‘๐‘ƒ) โ†” ๐‘ƒ โˆฅ โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—))
5249, 51mtbird 325 . 2 (๐œ‘ โ†’ ยฌ ๐‘ƒ โˆฅ (โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—โ†‘๐‘ƒ))
53 etransclem41.f . . . . . 6 ๐น = (๐‘ฅ โˆˆ โ„ โ†ฆ ((๐‘ฅโ†‘(๐‘ƒ โˆ’ 1)) ยท โˆ๐‘— โˆˆ (1...๐‘€)((๐‘ฅ โˆ’ ๐‘—)โ†‘๐‘ƒ)))
54 etransclem11 45446 . . . . . 6 (๐‘š โˆˆ โ„•0 โ†ฆ {๐‘‘ โˆˆ ((0...๐‘š) โ†‘m (0...๐‘€)) โˆฃ ฮฃ๐‘˜ โˆˆ (0...๐‘€)(๐‘‘โ€˜๐‘˜) = ๐‘š}) = (๐‘› โˆˆ โ„•0 โ†ฆ {๐‘ โˆˆ ((0...๐‘›) โ†‘m (0...๐‘€)) โˆฃ ฮฃ๐‘— โˆˆ (0...๐‘€)(๐‘โ€˜๐‘—) = ๐‘›})
55 eqeq1 2728 . . . . . . . 8 (๐‘˜ = ๐‘— โ†’ (๐‘˜ = 0 โ†” ๐‘— = 0))
5655ifbid 4543 . . . . . . 7 (๐‘˜ = ๐‘— โ†’ if(๐‘˜ = 0, (๐‘ƒ โˆ’ 1), 0) = if(๐‘— = 0, (๐‘ƒ โˆ’ 1), 0))
5756cbvmptv 5251 . . . . . 6 (๐‘˜ โˆˆ (0...๐‘€) โ†ฆ if(๐‘˜ = 0, (๐‘ƒ โˆ’ 1), 0)) = (๐‘— โˆˆ (0...๐‘€) โ†ฆ if(๐‘— = 0, (๐‘ƒ โˆ’ 1), 0))
587, 2, 53, 54, 57etransclem35 45470 . . . . 5 (๐œ‘ โ†’ (((โ„ D๐‘› ๐น)โ€˜(๐‘ƒ โˆ’ 1))โ€˜0) = ((!โ€˜(๐‘ƒ โˆ’ 1)) ยท (โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—โ†‘๐‘ƒ)))
5958oveq1d 7416 . . . 4 (๐œ‘ โ†’ ((((โ„ D๐‘› ๐น)โ€˜(๐‘ƒ โˆ’ 1))โ€˜0) / (!โ€˜(๐‘ƒ โˆ’ 1))) = (((!โ€˜(๐‘ƒ โˆ’ 1)) ยท (โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—โ†‘๐‘ƒ)) / (!โ€˜(๐‘ƒ โˆ’ 1))))
6021adantl 481 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ (1...๐‘€)) โ†’ -๐‘— โˆˆ โ„‚)
6144, 60fprodcl 15893 . . . . . 6 (๐œ‘ โ†’ โˆ๐‘— โˆˆ (1...๐‘€)-๐‘— โˆˆ โ„‚)
627nnnn0d 12529 . . . . . 6 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•0)
6361, 62expcld 14108 . . . . 5 (๐œ‘ โ†’ (โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—โ†‘๐‘ƒ) โˆˆ โ„‚)
64 nnm1nn0 12510 . . . . . . . 8 (๐‘ƒ โˆˆ โ„• โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„•0)
657, 64syl 17 . . . . . . 7 (๐œ‘ โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„•0)
6665faccld 14241 . . . . . 6 (๐œ‘ โ†’ (!โ€˜(๐‘ƒ โˆ’ 1)) โˆˆ โ„•)
6766nncnd 12225 . . . . 5 (๐œ‘ โ†’ (!โ€˜(๐‘ƒ โˆ’ 1)) โˆˆ โ„‚)
6866nnne0d 12259 . . . . 5 (๐œ‘ โ†’ (!โ€˜(๐‘ƒ โˆ’ 1)) โ‰  0)
6963, 67, 68divcan3d 11992 . . . 4 (๐œ‘ โ†’ (((!โ€˜(๐‘ƒ โˆ’ 1)) ยท (โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—โ†‘๐‘ƒ)) / (!โ€˜(๐‘ƒ โˆ’ 1))) = (โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—โ†‘๐‘ƒ))
7059, 69eqtrd 2764 . . 3 (๐œ‘ โ†’ ((((โ„ D๐‘› ๐น)โ€˜(๐‘ƒ โˆ’ 1))โ€˜0) / (!โ€˜(๐‘ƒ โˆ’ 1))) = (โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—โ†‘๐‘ƒ))
7170breq2d 5150 . 2 (๐œ‘ โ†’ (๐‘ƒ โˆฅ ((((โ„ D๐‘› ๐น)โ€˜(๐‘ƒ โˆ’ 1))โ€˜0) / (!โ€˜(๐‘ƒ โˆ’ 1))) โ†” ๐‘ƒ โˆฅ (โˆ๐‘— โˆˆ (1...๐‘€)-๐‘—โ†‘๐‘ƒ)))
7252, 71mtbird 325 1 (๐œ‘ โ†’ ยฌ ๐‘ƒ โˆฅ ((((โ„ D๐‘› ๐น)โ€˜(๐‘ƒ โˆ’ 1))โ€˜0) / (!โ€˜(๐‘ƒ โˆ’ 1))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   = wceq 1533  โŠคwtru 1534   โˆˆ wcel 2098  {crab 3424  ifcif 4520   class class class wbr 5138   โ†ฆ cmpt 5221  โ€˜cfv 6533  (class class class)co 7401   โ†‘m cmap 8816  โ„‚cc 11104  โ„cr 11105  0cc0 11106  1c1 11107   ยท cmul 11111   < clt 11245   โ‰ค cle 11246   โˆ’ cmin 11441  -cneg 11442   / cdiv 11868  โ„•cn 12209  โ„•0cn0 12469  โ„คcz 12555  ...cfz 13481  โ†‘cexp 14024  !cfa 14230  abscabs 15178  ฮฃcsu 15629  โˆcprod 15846   โˆฅ cdvds 16194  โ„™cprime 16605   D๐‘› cdvn 25715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-sum 15630  df-prod 15847  df-dvds 16195  df-gcd 16433  df-prm 16606  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-mulg 18986  df-cntz 19223  df-cmn 19692  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-fbas 21225  df-fg 21226  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-nei 22924  df-lp 22962  df-perf 22963  df-cn 23053  df-cnp 23054  df-haus 23141  df-tx 23388  df-hmeo 23581  df-fil 23672  df-fm 23764  df-flim 23765  df-flf 23766  df-xms 24148  df-ms 24149  df-tms 24150  df-cncf 24720  df-limc 25717  df-dv 25718  df-dvn 25719
This theorem is referenced by:  etransclem44  45479
  Copyright terms: Public domain W3C validator