Metamath Proof Explorer

Theorem aaliou2

Description: Liouville's approximation theorem for algebraic numbers per se. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion aaliou2 ( 𝐴 ∈ ( 𝔸 ∩ ℝ ) → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝐴 ∈ ( 𝔸 ∩ ℝ ) ↔ ( 𝐴 ∈ 𝔸 ∧ 𝐴 ∈ ℝ ) )
2 elaa ⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑎 ‘ 𝐴 ) = 0 ) )
3 eldifn ⊢ ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → ¬ 𝑎 ∈ { 0𝑝 } )
4 3 3ad2ant1 ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → ¬ 𝑎 ∈ { 0𝑝 } )
5 simpr ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) )
6 fveq1 ⊢ ( 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) → ( 𝑎 ‘ 𝐴 ) = ( ( ℂ × { ( 𝑎 ‘ 0 ) } ) ‘ 𝐴 ) )
7 6 adantl ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → ( 𝑎 ‘ 𝐴 ) = ( ( ℂ × { ( 𝑎 ‘ 0 ) } ) ‘ 𝐴 ) )
8 simpl2 ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → ( 𝑎 ‘ 𝐴 ) = 0 )
9 simpl3 ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → 𝐴 ∈ ℝ )
10 9 recnd ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → 𝐴 ∈ ℂ )
11 fvex ⊢ ( 𝑎 ‘ 0 ) ∈ V
12 11 fvconst2 ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ × { ( 𝑎 ‘ 0 ) } ) ‘ 𝐴 ) = ( 𝑎 ‘ 0 ) )
13 10 12 syl ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → ( ( ℂ × { ( 𝑎 ‘ 0 ) } ) ‘ 𝐴 ) = ( 𝑎 ‘ 0 ) )
14 7 8 13 3eqtr3rd ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → ( 𝑎 ‘ 0 ) = 0 )
15 14 sneqd ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → { ( 𝑎 ‘ 0 ) } = { 0 } )
16 15 xpeq2d ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → ( ℂ × { ( 𝑎 ‘ 0 ) } ) = ( ℂ × { 0 } ) )
17 5 16 eqtrd ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → 𝑎 = ( ℂ × { 0 } ) )
18 df-0p ⊢ 0𝑝 = ( ℂ × { 0 } )
19 17 18 eqtr4di ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → 𝑎 = 0𝑝 )
20 velsn ⊢ ( 𝑎 ∈ { 0𝑝 } ↔ 𝑎 = 0𝑝 )
21 19 20 sylibr ⊢ ( ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) → 𝑎 ∈ { 0𝑝 } )
22 4 21 mtand ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → ¬ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) )
23 eldifi ⊢ ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → 𝑎 ∈ ( Poly ‘ ℤ ) )
24 23 3ad2ant1 ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → 𝑎 ∈ ( Poly ‘ ℤ ) )
25 0dgrb ⊢ ( 𝑎 ∈ ( Poly ‘ ℤ ) → ( ( deg ‘ 𝑎 ) = 0 ↔ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) )
26 24 25 syl ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → ( ( deg ‘ 𝑎 ) = 0 ↔ 𝑎 = ( ℂ × { ( 𝑎 ‘ 0 ) } ) ) )
27 22 26 mtbird ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → ¬ ( deg ‘ 𝑎 ) = 0 )
28 dgrcl ⊢ ( 𝑎 ∈ ( Poly ‘ ℤ ) → ( deg ‘ 𝑎 ) ∈ ℕ0 )
29 24 28 syl ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → ( deg ‘ 𝑎 ) ∈ ℕ0 )
30 elnn0 ⊢ ( ( deg ‘ 𝑎 ) ∈ ℕ0 ↔ ( ( deg ‘ 𝑎 ) ∈ ℕ ∨ ( deg ‘ 𝑎 ) = 0 ) )
31 29 30 sylib ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → ( ( deg ‘ 𝑎 ) ∈ ℕ ∨ ( deg ‘ 𝑎 ) = 0 ) )
32 orel2 ⊢ ( ¬ ( deg ‘ 𝑎 ) = 0 → ( ( ( deg ‘ 𝑎 ) ∈ ℕ ∨ ( deg ‘ 𝑎 ) = 0 ) → ( deg ‘ 𝑎 ) ∈ ℕ ) )
33 27 31 32 sylc ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → ( deg ‘ 𝑎 ) ∈ ℕ )
34 eqid ⊢ ( deg ‘ 𝑎 ) = ( deg ‘ 𝑎 )
35 simp3 ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
36 simp2 ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → ( 𝑎 ‘ 𝐴 ) = 0 )
37 34 24 33 35 36 aaliou ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ ( deg ‘ 𝑎 ) ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
38 oveq2 ⊢ ( 𝑘 = ( deg ‘ 𝑎 ) → ( 𝑞 ↑ 𝑘 ) = ( 𝑞 ↑ ( deg ‘ 𝑎 ) ) )
39 38 oveq2d ⊢ ( 𝑘 = ( deg ‘ 𝑎 ) → ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) = ( 𝑥 / ( 𝑞 ↑ ( deg ‘ 𝑎 ) ) ) )
40 39 breq1d ⊢ ( 𝑘 = ( deg ‘ 𝑎 ) → ( ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ↔ ( 𝑥 / ( 𝑞 ↑ ( deg ‘ 𝑎 ) ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
41 40 orbi2d ⊢ ( 𝑘 = ( deg ‘ 𝑎 ) → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ ( deg ‘ 𝑎 ) ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
42 41 2ralbidv ⊢ ( 𝑘 = ( deg ‘ 𝑎 ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ ( deg ‘ 𝑎 ) ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
43 42 rexbidv ⊢ ( 𝑘 = ( deg ‘ 𝑎 ) → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ ( deg ‘ 𝑎 ) ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
44 43 rspcev ⊢ ( ( ( deg ‘ 𝑎 ) ∈ ℕ ∧ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ ( deg ‘ 𝑎 ) ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
45 33 37 44 syl2anc ⊢ ( ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ∧ 𝐴 ∈ ℝ ) → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
46 45 3exp ⊢ ( 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → ( ( 𝑎 ‘ 𝐴 ) = 0 → ( 𝐴 ∈ ℝ → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
47 46 rexlimiv ⊢ ( ∃ 𝑎 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑎 ‘ 𝐴 ) = 0 → ( 𝐴 ∈ ℝ → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
48 2 47 simplbiim ⊢ ( 𝐴 ∈ 𝔸 → ( 𝐴 ∈ ℝ → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
49 48 imp ⊢ ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ∈ ℝ ) → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
50 1 49 sylbi ⊢ ( 𝐴 ∈ ( 𝔸 ∩ ℝ ) → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )