aaliou2

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

		Ref	Expression
	Assertion	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})\|)$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ A \in (𝔸 \cap ℝ) \leftrightarrow (A \in 𝔸 \land A \in ℝ)$
2		elaa	$⊢ A \in 𝔸 \leftrightarrow (A \in ℂ \land \exists a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) a (A) = 0)$
3		eldifn	$⊢ a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \to \neg a \in \{0_{𝑝}\}$
4	3	3ad2ant1	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to \neg a \in \{0_{𝑝}\}$
5		simpr	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to a = ℂ \times \{a (0)\}$
6		fveq1	$⊢ a = ℂ \times \{a (0)\} \to a (A) = (ℂ \times \{a (0)\}) (A)$
7	6	adantl	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to a (A) = (ℂ \times \{a (0)\}) (A)$
8		simpl2	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to a (A) = 0$
9		simpl3	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to A \in ℝ$
10	9	recnd	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to A \in ℂ$
11		fvex	$⊢ a (0) \in V$
12	11	fvconst2	$⊢ A \in ℂ \to (ℂ \times \{a (0)\}) (A) = a (0)$
13	10 12	syl	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to (ℂ \times \{a (0)\}) (A) = a (0)$
14	7 8 13	3eqtr3rd	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to a (0) = 0$
15	14	sneqd	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to \{a (0)\} = \{0\}$
16	15	xpeq2d	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to ℂ \times \{a (0)\} = ℂ \times \{0\}$
17	5 16	eqtrd	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to a = ℂ \times \{0\}$
18		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
19	17 18	eqtr4di	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to a = 0_{𝑝}$
20		velsn	$⊢ a \in \{0_{𝑝}\} \leftrightarrow a = 0_{𝑝}$
21	19 20	sylibr	$⊢ ((a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \land a = ℂ \times \{a (0)\}) \to a \in \{0_{𝑝}\}$
22	4 21	mtand	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to \neg a = ℂ \times \{a (0)\}$
23		eldifi	$⊢ a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \to a \in Poly (ℤ)$
24	23	3ad2ant1	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to a \in Poly (ℤ)$
25		0dgrb	$⊢ a \in Poly (ℤ) \to (\deg (a) = 0 \leftrightarrow a = ℂ \times \{a (0)\})$
26	24 25	syl	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to (\deg (a) = 0 \leftrightarrow a = ℂ \times \{a (0)\})$
27	22 26	mtbird	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to \neg \deg (a) = 0$
28		dgrcl	$⊢ a \in Poly (ℤ) \to \deg (a) \in ℕ_{0}$
29	24 28	syl	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to \deg (a) \in ℕ_{0}$
30		elnn0	$⊢ \deg (a) \in ℕ_{0} \leftrightarrow (\deg (a) \in ℕ \lor \deg (a) = 0)$
31	29 30	sylib	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to (\deg (a) \in ℕ \lor \deg (a) = 0)$
32		orel2	$⊢ \neg \deg (a) = 0 \to ((\deg (a) \in ℕ \lor \deg (a) = 0) \to \deg (a) \in ℕ)$
33	27 31 32	sylc	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to \deg (a) \in ℕ$
34		eqid	$⊢ \deg (a) = \deg (a)$
35		simp3	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to A \in ℝ$
36		simp2	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to a (A) = 0$
37	34 24 33 35 36	aaliou	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \land A \in ℝ) \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{\deg (a)}} < \|A - (\frac{p}{q})\|)$
38		oveq2	$⊢ k = \deg (a) \to q^{k} = q^{\deg (a)}$
39	38	oveq2d	$⊢ k = \deg (a) \to \frac{x}{q^{k}} = \frac{x}{q^{\deg (a)}}$
40	39	breq1d	$⊢ k = \deg (a) \to (\frac{x}{q^{k}} < \|A - (\frac{p}{q})\| \leftrightarrow \frac{x}{q^{\deg (a)}} < \|A - (\frac{p}{q})\|)$
41	40	orbi2d	$⊢ k = \deg (a) \to ((A = \frac{p}{q} \lor \frac{x}{q^{k}} < \|A - (\frac{p}{q})\|) \leftrightarrow (A = \frac{p}{q} \lor \frac{x}{q^{\deg (a)}} < \|A - (\frac{p}{q})\|))$
42	41	2ralbidv	$⊢ k = \deg (a) \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^{\deg (a)}} < \|A - (\frac{p}{q})\|))$
43	42	rexbidv	$⊢ k = \deg (a) \to (\exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{k}} < \|A - (\frac{p}{q})\|) \leftrightarrow \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{\deg (a)}} < \|A - (\frac{p}{q})\|))$
44	43	rspcev	$⊢ (\deg (a) \in ℕ \land \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{\deg (a)}} < \|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})\|)$
45	33 37 44	syl2anc	$⊢ (a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land a (A) = 0 \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})\|)$
46	45	3exp	$⊢ a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \to (a (A) = 0 \to (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})\|)))$
47	46	rexlimiv	$⊢ \exists a \in (Poly (ℤ) ∖ \{0_{𝑝}\}) a (A) = 0 \to (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})\|))$
48	2 47	simplbiim	$⊢ A \in 𝔸 \to (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})\|))$
49	48	imp	$⊢ (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})\|)$
50	1 49	sylbi	$⊢ 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})\|)$

Metamath Proof Explorer

Theorem aaliou2

Proof