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	$⊢ N = \deg (F)$
	aalioulem2.b	$⊢ φ \to F \in Poly (ℤ)$
	aalioulem2.c	$⊢ φ \to N \in ℕ$
	aalioulem2.d	$⊢ φ \to A \in ℝ$
	aalioulem3.e	$⊢ φ \to F (A) = 0$
Assertion	aaliou	$⊢ φ \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{N}} < \|A - (\frac{p}{q})\|)$

Proof

Step	Hyp	Ref	Expression
1		aalioulem2.a	$⊢ N = \deg (F)$
2		aalioulem2.b	$⊢ φ \to F \in Poly (ℤ)$
3		aalioulem2.c	$⊢ φ \to N \in ℕ$
4		aalioulem2.d	$⊢ φ \to A \in ℝ$
5		aalioulem3.e	$⊢ φ \to F (A) = 0$
6	1 2 3 4 5	aalioulem6	$⊢ φ \to \exists a \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
7		rphalfcl	$⊢ a \in ℝ^{+} \to \frac{a}{2} \in ℝ^{+}$
8	7	adantl	$⊢ (φ \land a \in ℝ^{+}) \to \frac{a}{2} \in ℝ^{+}$
9	7	ad2antlr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{a}{2} \in ℝ^{+}$
10		nnrp	$⊢ q \in ℕ \to q \in ℝ^{+}$
11	10	ad2antll	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to q \in ℝ^{+}$
12	3	nnzd	$⊢ φ \to N \in ℤ$
13	12	ad2antrr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to N \in ℤ$
14	11 13	rpexpcld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to q^{N} \in ℝ^{+}$
15	9 14	rpdivcld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{\frac{a}{2}}{q^{N}} \in ℝ^{+}$
16	15	rpred	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{\frac{a}{2}}{q^{N}} \in ℝ$
17		simplr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to a \in ℝ^{+}$
18	17 14	rpdivcld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{a}{q^{N}} \in ℝ^{+}$
19	18	rpred	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{a}{q^{N}} \in ℝ$
20	4	adantr	$⊢ (φ \land a \in ℝ^{+}) \to A \in ℝ$
21		znq	$⊢ (p \in ℤ \land q \in ℕ) \to \frac{p}{q} \in ℚ$
22		qre	$⊢ \frac{p}{q} \in ℚ \to \frac{p}{q} \in ℝ$
23	21 22	syl	$⊢ (p \in ℤ \land q \in ℕ) \to \frac{p}{q} \in ℝ$
24		resubcl	$⊢ (A \in ℝ \land \frac{p}{q} \in ℝ) \to A - (\frac{p}{q}) \in ℝ$
25	20 23 24	syl2an	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to A - (\frac{p}{q}) \in ℝ$
26	25	recnd	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to A - (\frac{p}{q}) \in ℂ$
27	26	abscld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \|A - (\frac{p}{q})\| \in ℝ$
28	16 19 27	3jca	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (\frac{\frac{a}{2}}{q^{N}} \in ℝ \land \frac{a}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ)$
29	9	rpred	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{a}{2} \in ℝ$
30		rpre	$⊢ a \in ℝ^{+} \to a \in ℝ$
31	30	ad2antlr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to a \in ℝ$
32		rphalflt	$⊢ a \in ℝ^{+} \to \frac{a}{2} < a$
33	32	ad2antlr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{a}{2} < a$
34	29 31 14 33	ltdiv1dd	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{\frac{a}{2}}{q^{N}} < \frac{a}{q^{N}}$
35	34	anim1i	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to (\frac{\frac{a}{2}}{q^{N}} < \frac{a}{q^{N}} \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
36	35	ex	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (\frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\| \to (\frac{\frac{a}{2}}{q^{N}} < \frac{a}{q^{N}} \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
37		ltletr	$⊢ (\frac{\frac{a}{2}}{q^{N}} \in ℝ \land \frac{a}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ) \to ((\frac{\frac{a}{2}}{q^{N}} < \frac{a}{q^{N}} \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to \frac{\frac{a}{2}}{q^{N}} < \|A - (\frac{p}{q})\|)$
38	28 36 37	sylsyld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (\frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\| \to \frac{\frac{a}{2}}{q^{N}} < \|A - (\frac{p}{q})\|)$
39	38	orim2d	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to ((A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to (A = \frac{p}{q} \lor \frac{\frac{a}{2}}{q^{N}} < \|A - (\frac{p}{q})\|))$
40	39	ralimdvva	$⊢ (φ \land a \in ℝ^{+}) \to (\forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{\frac{a}{2}}{q^{N}} < \|A - (\frac{p}{q})\|))$
41		oveq1	$⊢ x = \frac{a}{2} \to \frac{x}{q^{N}} = \frac{\frac{a}{2}}{q^{N}}$
42	41	breq1d	$⊢ x = \frac{a}{2} \to (\frac{x}{q^{N}} < \|A - (\frac{p}{q})\| \leftrightarrow \frac{\frac{a}{2}}{q^{N}} < \|A - (\frac{p}{q})\|)$
43	42	orbi2d	$⊢ x = \frac{a}{2} \to ((A = \frac{p}{q} \lor \frac{x}{q^{N}} < \|A - (\frac{p}{q})\|) \leftrightarrow (A = \frac{p}{q} \lor \frac{\frac{a}{2}}{q^{N}} < \|A - (\frac{p}{q})\|))$
44	43	2ralbidv	$⊢ x = \frac{a}{2} \to (\forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{N}} < \|A - (\frac{p}{q})\|) \leftrightarrow \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{\frac{a}{2}}{q^{N}} < \|A - (\frac{p}{q})\|))$
45	44	rspcev	$⊢ (\frac{a}{2} \in ℝ^{+} \land \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{\frac{a}{2}}{q^{N}} < \|A - (\frac{p}{q})\|)) \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{N}} < \|A - (\frac{p}{q})\|)$
46	8 40 45	syl6an	$⊢ (φ \land a \in ℝ^{+}) \to (\forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{N}} < \|A - (\frac{p}{q})\|))$
47	46	rexlimdva	$⊢ φ \to (\exists a \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{N}} < \|A - (\frac{p}{q})\|))$
48	6 47	mpd	$⊢ φ \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{N}} < \|A - (\frac{p}{q})\|)$

Metamath Proof Explorer

Theorem aaliou

Proof