# Metamath Proof Explorer

## Theorem aaliou2b

Description: Liouville's approximation theorem extended to complex A . (Contributed by Stefan O'Rear, 20-Nov-2014)

Ref Expression
Assertion aaliou2b ${⊢}{A}\in 𝔸\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{k}}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$

### Proof

Step Hyp Ref Expression
1 elin ${⊢}{A}\in \left(𝔸\cap ℝ\right)↔\left({A}\in 𝔸\wedge {A}\in ℝ\right)$
2 aaliou2 ${⊢}{A}\in \left(𝔸\cap ℝ\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{k}}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$
3 1 2 sylbir ${⊢}\left({A}\in 𝔸\wedge {A}\in ℝ\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{k}}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$
4 1nn ${⊢}1\in ℕ$
5 aacn ${⊢}{A}\in 𝔸\to {A}\in ℂ$
6 5 adantr ${⊢}\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\to {A}\in ℂ$
7 6 imcld ${⊢}\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\to \Im \left({A}\right)\in ℝ$
8 7 recnd ${⊢}\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\to \Im \left({A}\right)\in ℂ$
9 reim0b ${⊢}{A}\in ℂ\to \left({A}\in ℝ↔\Im \left({A}\right)=0\right)$
10 5 9 syl ${⊢}{A}\in 𝔸\to \left({A}\in ℝ↔\Im \left({A}\right)=0\right)$
11 10 necon3bbid ${⊢}{A}\in 𝔸\to \left(¬{A}\in ℝ↔\Im \left({A}\right)\ne 0\right)$
12 11 biimpa ${⊢}\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\to \Im \left({A}\right)\ne 0$
13 8 12 absrpcld ${⊢}\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\to \left|\Im \left({A}\right)\right|\in {ℝ}^{+}$
14 13 rphalfcld ${⊢}\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\to \frac{\left|\Im \left({A}\right)\right|}{2}\in {ℝ}^{+}$
15 14 adantr ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\left|\Im \left({A}\right)\right|}{2}\in {ℝ}^{+}$
16 1nn0 ${⊢}1\in {ℕ}_{0}$
17 nnexpcl ${⊢}\left({q}\in ℕ\wedge 1\in {ℕ}_{0}\right)\to {{q}}^{1}\in ℕ$
18 16 17 mpan2 ${⊢}{q}\in ℕ\to {{q}}^{1}\in ℕ$
19 18 ad2antll ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {{q}}^{1}\in ℕ$
20 19 nnrpd ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {{q}}^{1}\in {ℝ}^{+}$
21 15 20 rpdivcld ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}\in {ℝ}^{+}$
22 21 rpred ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}\in ℝ$
23 15 rpred ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\left|\Im \left({A}\right)\right|}{2}\in ℝ$
24 6 adantr ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {A}\in ℂ$
25 znq ${⊢}\left({p}\in ℤ\wedge {q}\in ℕ\right)\to \frac{{p}}{{q}}\in ℚ$
26 25 adantl ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{{p}}{{q}}\in ℚ$
27 qre ${⊢}\frac{{p}}{{q}}\in ℚ\to \frac{{p}}{{q}}\in ℝ$
28 26 27 syl ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{{p}}{{q}}\in ℝ$
29 28 recnd ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{{p}}{{q}}\in ℂ$
30 24 29 subcld ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {A}-\left(\frac{{p}}{{q}}\right)\in ℂ$
31 30 abscld ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\in ℝ$
32 19 nnge1d ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to 1\le {{q}}^{1}$
33 1rp ${⊢}1\in {ℝ}^{+}$
34 rpregt0 ${⊢}1\in {ℝ}^{+}\to \left(1\in ℝ\wedge 0<1\right)$
35 33 34 mp1i ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left(1\in ℝ\wedge 0<1\right)$
36 20 rpregt0d ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left({{q}}^{1}\in ℝ\wedge 0<{{q}}^{1}\right)$
37 15 rpregt0d ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left(\frac{\left|\Im \left({A}\right)\right|}{2}\in ℝ\wedge 0<\frac{\left|\Im \left({A}\right)\right|}{2}\right)$
38 lediv2 ${⊢}\left(\left(1\in ℝ\wedge 0<1\right)\wedge \left({{q}}^{1}\in ℝ\wedge 0<{{q}}^{1}\right)\wedge \left(\frac{\left|\Im \left({A}\right)\right|}{2}\in ℝ\wedge 0<\frac{\left|\Im \left({A}\right)\right|}{2}\right)\right)\to \left(1\le {{q}}^{1}↔\frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}\le \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{1}\right)$
39 35 36 37 38 syl3anc ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left(1\le {{q}}^{1}↔\frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}\le \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{1}\right)$
40 32 39 mpbid ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}\le \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{1}$
41 15 rpcnd ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\left|\Im \left({A}\right)\right|}{2}\in ℂ$
42 41 div1d ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{1}=\frac{\left|\Im \left({A}\right)\right|}{2}$
43 40 42 breqtrd ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}\le \frac{\left|\Im \left({A}\right)\right|}{2}$
44 13 adantr ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left|\Im \left({A}\right)\right|\in {ℝ}^{+}$
45 44 rpred ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left|\Im \left({A}\right)\right|\in ℝ$
46 rphalflt ${⊢}\left|\Im \left({A}\right)\right|\in {ℝ}^{+}\to \frac{\left|\Im \left({A}\right)\right|}{2}<\left|\Im \left({A}\right)\right|$
47 44 46 syl ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\left|\Im \left({A}\right)\right|}{2}<\left|\Im \left({A}\right)\right|$
48 24 29 imsubd ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \Im \left({A}-\left(\frac{{p}}{{q}}\right)\right)=\Im \left({A}\right)-\Im \left(\frac{{p}}{{q}}\right)$
49 28 reim0d ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \Im \left(\frac{{p}}{{q}}\right)=0$
50 49 oveq2d ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \Im \left({A}\right)-\Im \left(\frac{{p}}{{q}}\right)=\Im \left({A}\right)-0$
51 8 adantr ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \Im \left({A}\right)\in ℂ$
52 51 subid1d ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \Im \left({A}\right)-0=\Im \left({A}\right)$
53 48 50 52 3eqtrd ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \Im \left({A}-\left(\frac{{p}}{{q}}\right)\right)=\Im \left({A}\right)$
54 53 fveq2d ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left|\Im \left({A}-\left(\frac{{p}}{{q}}\right)\right)\right|=\left|\Im \left({A}\right)\right|$
55 absimle ${⊢}{A}-\left(\frac{{p}}{{q}}\right)\in ℂ\to \left|\Im \left({A}-\left(\frac{{p}}{{q}}\right)\right)\right|\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|$
56 30 55 syl ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left|\Im \left({A}-\left(\frac{{p}}{{q}}\right)\right)\right|\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|$
57 54 56 eqbrtrrd ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left|\Im \left({A}\right)\right|\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|$
58 23 45 31 47 57 ltletrd ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\left|\Im \left({A}\right)\right|}{2}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|$
59 22 23 31 43 58 lelttrd ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|$
60 59 olcd ${⊢}\left(\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left({A}=\frac{{p}}{{q}}\vee \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$
61 60 ralrimivva ${⊢}\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\to \forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$
62 oveq2 ${⊢}{k}=1\to {{q}}^{{k}}={{q}}^{1}$
63 62 oveq2d ${⊢}{k}=1\to \frac{{x}}{{{q}}^{{k}}}=\frac{{x}}{{{q}}^{1}}$
64 63 breq1d ${⊢}{k}=1\to \left(\frac{{x}}{{{q}}^{{k}}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|↔\frac{{x}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$
65 64 orbi2d ${⊢}{k}=1\to \left(\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{k}}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)↔\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)$
66 65 2ralbidv ${⊢}{k}=1\to \left(\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{k}}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)↔\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)$
67 oveq1 ${⊢}{x}=\frac{\left|\Im \left({A}\right)\right|}{2}\to \frac{{x}}{{{q}}^{1}}=\frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}$
68 67 breq1d ${⊢}{x}=\frac{\left|\Im \left({A}\right)\right|}{2}\to \left(\frac{{x}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|↔\frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$
69 68 orbi2d ${⊢}{x}=\frac{\left|\Im \left({A}\right)\right|}{2}\to \left(\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)↔\left({A}=\frac{{p}}{{q}}\vee \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)$
70 69 2ralbidv ${⊢}{x}=\frac{\left|\Im \left({A}\right)\right|}{2}\to \left(\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)↔\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)$
71 66 70 rspc2ev ${⊢}\left(1\in ℕ\wedge \frac{\left|\Im \left({A}\right)\right|}{2}\in {ℝ}^{+}\wedge \forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{\frac{\left|\Im \left({A}\right)\right|}{2}}{{{q}}^{1}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{k}}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$
72 4 14 61 71 mp3an2i ${⊢}\left({A}\in 𝔸\wedge ¬{A}\in ℝ\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{k}}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$
73 3 72 pm2.61dan ${⊢}{A}\in 𝔸\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{k}}}<\left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$