Metamath Proof Explorer

Theorem aaliou

Description: Liouville's theorem on diophantine approximation: Any algebraic number, being a root of a polynomial F in integer coefficients, is not approximable beyond order N = deg ( F ) 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
Hypotheses aalioulem2.a ⊢ 𝑁 = ( deg ‘ 𝐹 )
aalioulem2.b ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) )
aalioulem2.c ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aalioulem2.d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
aalioulem3.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
Assertion aaliou ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 aalioulem2.a ⊢ 𝑁 = ( deg ‘ 𝐹 )
2 aalioulem2.b ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) )
3 aalioulem2.c ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 aalioulem2.d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5 aalioulem3.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
6 1 2 3 4 5 aalioulem6 ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
7 rphalfcl ⊢ ( 𝑎 ∈ ℝ+ → ( 𝑎 / 2 ) ∈ ℝ+ )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) → ( 𝑎 / 2 ) ∈ ℝ+ )
9 7 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑎 / 2 ) ∈ ℝ+ )
10 nnrp ⊢ ( 𝑞 ∈ ℕ → 𝑞 ∈ ℝ+ )
11 10 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℝ+ )
12 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℤ )
14 11 13 rpexpcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℝ+ )
15 9 14 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ+ )
16 15 rpred ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
17 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑎 ∈ ℝ+ )
18 17 14 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ+ )
19 18 rpred ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
20 4 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
21 znq ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ℚ )
22 qre ⊢ ( ( 𝑝 / 𝑞 ) ∈ ℚ → ( 𝑝 / 𝑞 ) ∈ ℝ )
23 21 22 syl ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ℝ )
24 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑝 / 𝑞 ) ∈ ℝ ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℝ )
25 20 23 24 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℝ )
26 25 recnd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℂ )
27 26 abscld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ )
28 16 19 27 3jca ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) )
29 9 rpred ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑎 / 2 ) ∈ ℝ )
30 rpre ⊢ ( 𝑎 ∈ ℝ+ → 𝑎 ∈ ℝ )
31 30 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑎 ∈ ℝ )
32 rphalflt ⊢ ( 𝑎 ∈ ℝ+ → ( 𝑎 / 2 ) < 𝑎 )
33 32 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑎 / 2 ) < 𝑎 )
34 29 31 14 33 ltdiv1dd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) )
35 34 anim1i ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
36 35 ex ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → ( ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
37 ltletr ⊢ ( ( ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) → ( ( ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
38 28 36 37 sylsyld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
39 38 orim2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
40 39 ralimdvva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
41 oveq1 ⊢ ( 𝑥 = ( 𝑎 / 2 ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) = ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) )
42 41 breq1d ⊢ ( 𝑥 = ( 𝑎 / 2 ) → ( ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ↔ ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
43 42 orbi2d ⊢ ( 𝑥 = ( 𝑎 / 2 ) → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
44 43 2ralbidv ⊢ ( 𝑥 = ( 𝑎 / 2 ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
45 44 rspcev ⊢ ( ( ( 𝑎 / 2 ) ∈ ℝ+ ∧ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( ( 𝑎 / 2 ) / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
46 8 40 45 syl6an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
47 46 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
48 6 47 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )