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 ℕ \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{k}} < \|A - (\frac{p}{q})\|)$

Proof

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

Metamath Proof Explorer

Theorem aaliou2b

Proof