Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > aaliou | Structured version Visualization version GIF version | ||
| Description: Liouville's theorem on diophantine approximation: Any algebraic number, being a root of a polynomial 𝐹 in integer coefficients, is not approximable beyond order 𝑁 = deg(𝐹) by rational numbers. In this form, it also applies to rational numbers themselves, which are not well approximable by other rational numbers. This is Metamath 100 proof #18. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
| Ref | Expression |
|---|---|
| aalioulem2.a | ⊢ 𝑁 = (deg‘𝐹) |
| aalioulem2.b | ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ)) |
| aalioulem2.c | ⊢ (𝜑 → 𝑁 ∈ ℕ) |
| aalioulem2.d | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
| aalioulem3.e | ⊢ (𝜑 → (𝐹‘𝐴) = 0) |
| Ref | Expression |
|---|---|
| aaliou | ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aalioulem2.a | . . 3 ⊢ 𝑁 = (deg‘𝐹) | |
| 2 | aalioulem2.b | . . 3 ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ)) | |
| 3 | aalioulem2.c | . . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ) | |
| 4 | aalioulem2.d | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
| 5 | aalioulem3.e | . . 3 ⊢ (𝜑 → (𝐹‘𝐴) = 0) | |
| 6 | 1, 2, 3, 4, 5 | aalioulem6 26657 | . 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) |
| 7 | rphalfcl 13142 | . . . . 5 ⊢ (𝑎 ∈ ℝ+ → (𝑎 / 2) ∈ ℝ+) | |
| 8 | 7 | adantl 487 | . . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ+) → (𝑎 / 2) ∈ ℝ+) |
| 9 | 7 | ad2antlr 740 | . . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑎 / 2) ∈ ℝ+) |
| 10 | nnrp 13125 | . . . . . . . . . . . 12 ⊢ (𝑞 ∈ ℕ → 𝑞 ∈ ℝ+) | |
| 11 | 10 | ad2antll 742 | . . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℝ+) |
| 12 | 3 | nnzd 12712 | . . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 13 | 12 | ad2antrr 739 | . . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℤ) |
| 14 | 11, 13 | rpexpcld 14384 | . . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℝ+) |
| 15 | 9, 14 | rpdivcld 13174 | . . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝑎 / 2) / (𝑞↑𝑁)) ∈ ℝ+) |
| 16 | 15 | rpred 13157 | . . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝑎 / 2) / (𝑞↑𝑁)) ∈ ℝ) |
| 17 | simplr 781 | . . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑎 ∈ ℝ+) | |
| 18 | 17, 14 | rpdivcld 13174 | . . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑎 / (𝑞↑𝑁)) ∈ ℝ+) |
| 19 | 18 | rpred 13157 | . . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑎 / (𝑞↑𝑁)) ∈ ℝ) |
| 20 | 4 | adantr 486 | . . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ+) → 𝐴 ∈ ℝ) |
| 21 | znq 13072 | . . . . . . . . . . . 12 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ) | |
| 22 | qre 13073 | . . . . . . . . . . . 12 ⊢ ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ) | |
| 23 | 21, 22 | syl 18 | . . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ) |
| 24 | resubcl 11615 | . . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝑝 / 𝑞) ∈ ℝ) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ) | |
| 25 | 20, 23, 24 | syl2an 608 | . . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ) |
| 26 | 25 | recnd 11330 | . . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ) |
| 27 | 26 | abscld 15599 | . . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ) |
| 28 | 16, 19, 27 | 3jca 1146 | . . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (((𝑎 / 2) / (𝑞↑𝑁)) ∈ ℝ ∧ (𝑎 / (𝑞↑𝑁)) ∈ ℝ ∧ (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)) |
| 29 | 9 | rpred 13157 | . . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑎 / 2) ∈ ℝ) |
| 30 | rpre 13122 | . . . . . . . . . . 11 ⊢ (𝑎 ∈ ℝ+ → 𝑎 ∈ ℝ) | |
| 31 | 30 | ad2antlr 740 | . . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑎 ∈ ℝ) |
| 32 | rphalflt 13144 | . . . . . . . . . . 11 ⊢ (𝑎 ∈ ℝ+ → (𝑎 / 2) < 𝑎) | |
| 33 | 32 | ad2antlr 740 | . . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑎 / 2) < 𝑎) |
| 34 | 29, 31, 14, 33 | ltdiv1dd 13214 | . . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝑎 / 2) / (𝑞↑𝑁)) < (𝑎 / (𝑞↑𝑁))) |
| 35 | 34 | anim1i 627 | . . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ (𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (((𝑎 / 2) / (𝑞↑𝑁)) < (𝑎 / (𝑞↑𝑁)) ∧ (𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) |
| 36 | 35 | ex 418 | . . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (((𝑎 / 2) / (𝑞↑𝑁)) < (𝑎 / (𝑞↑𝑁)) ∧ (𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 37 | ltletr 11395 | . . . . . . 7 ⊢ ((((𝑎 / 2) / (𝑞↑𝑁)) ∈ ℝ ∧ (𝑎 / (𝑞↑𝑁)) ∈ ℝ ∧ (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ) → ((((𝑎 / 2) / (𝑞↑𝑁)) < (𝑎 / (𝑞↑𝑁)) ∧ (𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → ((𝑎 / 2) / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) | |
| 38 | 28, 36, 37 | sylsyld 62 | . . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → ((𝑎 / 2) / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
| 39 | 38 | orim2d 982 | . . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ (𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ ((𝑎 / 2) / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 40 | 39 | ralimdvva 3210 | . . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ+) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ ((𝑎 / 2) / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 41 | oveq1 7425 | . . . . . . . 8 ⊢ (𝑥 = (𝑎 / 2) → (𝑥 / (𝑞↑𝑁)) = ((𝑎 / 2) / (𝑞↑𝑁))) | |
| 42 | 41 | breq1d 5113 | . . . . . . 7 ⊢ (𝑥 = (𝑎 / 2) → ((𝑥 / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞))) ↔ ((𝑎 / 2) / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
| 43 | 42 | orbi2d 929 | . . . . . 6 ⊢ (𝑥 = (𝑎 / 2) → ((𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞)))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ ((𝑎 / 2) / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 44 | 43 | 2ralbidv 3227 | . . . . 5 ⊢ (𝑥 = (𝑎 / 2) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞)))) ↔ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ ((𝑎 / 2) / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 45 | 44 | rspcev 3577 | . . . 4 ⊢ (((𝑎 / 2) ∈ ℝ+ ∧ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ ((𝑎 / 2) / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
| 46 | 8, 40, 45 | syl6an 697 | . . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ+) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 47 | 46 | rexlimdva 3164 | . 2 ⊢ (𝜑 → (∃𝑎 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑎 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 48 | 6, 47 | mpd 16 | 1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3077 ∃wrex 3087 class class class wbr 5103 ‘cfv 6537 (class class class)co 7418 ℝcr 11192 0cc0 11193 < clt 11336 ≤ cle 11337 − cmin 11534 / cdiv 11966 ℕcn 12328 2c2 12390 ℤcz 12686 ℚcq 13068 ℝ+crp 13113 ↑cexp 14197 abscabs 15394 Polycply 26495 degcdgr 26498 |
| 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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271 ax-addf 11272 |
| 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 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-om 7876 df-1st 7999 df-2nd 8000 df-supp 8171 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-oadd 8473 df-er 8710 df-map 8842 df-pm 8843 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9347 df-fi 9396 df-sup 9427 df-inf 9428 df-oi 9497 df-dju 9975 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-5 12401 df-6 12402 df-7 12403 df-8 12404 df-9 12405 df-n0 12600 df-xnn0 12673 df-z 12687 df-dec 12808 df-uz 12959 df-q 13069 df-rp 13114 df-xneg 13234 df-xadd 13235 df-xmul 13236 df-ioo 13473 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-fl 13925 df-seq 14138 df-exp 14198 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-clim 15648 df-rlim 15649 df-sum 15847 df-struct 17318 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-ress 17402 df-plusg 17434 df-mulr 17435 df-starv 17436 df-sca 17437 df-vsca 17438 df-ip 17439 df-tset 17440 df-ple 17441 df-ds 17443 df-unif 17444 df-hom 17445 df-cco 17446 df-rest 17586 df-topn 17587 df-0g 17605 df-gsum 17606 df-topgen 17607 df-pt 17608 df-prds 17611 df-xrs 17667 df-qtop 17672 df-imas 17673 df-xps 17675 df-mre 17749 df-mrc 17750 df-acs 17752 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-submnd 18972 df-grp 19140 df-minusg 19141 df-mulg 19271 df-subg 19326 df-cntz 19524 df-cmn 19989 df-abl 19990 df-mgp 20354 df-rng 20368 df-ur 20401 df-ring 20454 df-cring 20455 df-subrng 20791 df-subrg 20815 df-psmet 21663 df-xmet 21664 df-met 21665 df-bl 21666 df-mopn 21667 df-fbas 21668 df-fg 21669 df-cnfld 21672 df-top 23205 df-topon 23222 df-topsp 23244 df-bases 23257 df-cld 23330 df-ntr 23331 df-cls 23332 df-nei 23409 df-lp 23447 df-perf 23448 df-cn 23538 df-cnp 23539 df-haus 23626 df-cmp 23698 df-tx 23874 df-hmeo 24067 df-fil 24158 df-fm 24250 df-flim 24251 df-flf 24252 df-xms 24632 df-ms 24633 df-tms 24634 df-cncf 25192 df-0p 25984 df-limc 26179 df-dv 26180 df-dvn 26181 df-cpn 26182 df-ply 26499 df-idp 26500 df-coe 26501 df-dgr 26502 df-quot 26605 |
| This theorem is used by: aaliou2 26660 |
| Copyright terms: Public domain | W3C validator |