aalioulem5

	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	aalioulem5	$⊢ φ \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|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	aalioulem4	$⊢ φ \to \exists a \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ ((F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1) \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
7		simpr	$⊢ (φ \land a \in ℝ^{+}) \to a \in ℝ^{+}$
8		1rp	$⊢ 1 \in ℝ^{+}$
9		ifcl	$⊢ (a \in ℝ^{+} \land 1 \in ℝ^{+}) \to if (a \leq 1, a, 1) \in ℝ^{+}$
10	7 8 9	sylancl	$⊢ (φ \land a \in ℝ^{+}) \to if (a \leq 1, a, 1) \in ℝ^{+}$
11	10	adantr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to if (a \leq 1, a, 1) \in ℝ^{+}$
12		simprr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to q \in ℕ$
13	12	nnrpd	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to q \in ℝ^{+}$
14	3	ad2antrr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to N \in ℕ$
15	14	nnzd	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to N \in ℤ$
16	13 15	rpexpcld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to q^{N} \in ℝ^{+}$
17	11 16	rpdivcld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{if (a \leq 1, a, 1)}{q^{N}} \in ℝ^{+}$
18	17	rpred	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{if (a \leq 1, a, 1)}{q^{N}} \in ℝ$
19		1re	$⊢ 1 \in ℝ$
20	19	a1i	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to 1 \in ℝ$
21	4	ad2antrr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to A \in ℝ$
22		znq	$⊢ (p \in ℤ \land q \in ℕ) \to \frac{p}{q} \in ℚ$
23		qre	$⊢ \frac{p}{q} \in ℚ \to \frac{p}{q} \in ℝ$
24	22 23	syl	$⊢ (p \in ℤ \land q \in ℕ) \to \frac{p}{q} \in ℝ$
25	24	adantl	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{p}{q} \in ℝ$
26	21 25	resubcld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to A - (\frac{p}{q}) \in ℝ$
27	26	recnd	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to A - (\frac{p}{q}) \in ℂ$
28	27	abscld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \|A - (\frac{p}{q})\| \in ℝ$
29	18 20 28	3jca	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (\frac{if (a \leq 1, a, 1)}{q^{N}} \in ℝ \land 1 \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ)$
30	29	adantr	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land 1 < \|A - (\frac{p}{q})\|) \to (\frac{if (a \leq 1, a, 1)}{q^{N}} \in ℝ \land 1 \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ)$
31	16	rprecred	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{1}{q^{N}} \in ℝ$
32	11	rpred	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to if (a \leq 1, a, 1) \in ℝ$
33		simplr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to a \in ℝ^{+}$
34	33	rpred	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to a \in ℝ$
35		min2	$⊢ (a \in ℝ \land 1 \in ℝ) \to if (a \leq 1, a, 1) \leq 1$
36	34 19 35	sylancl	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to if (a \leq 1, a, 1) \leq 1$
37	32 20 16 36	lediv1dd	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \frac{1}{q^{N}}$
38	14	nnnn0d	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to N \in ℕ_{0}$
39	12 38	nnexpcld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to q^{N} \in ℕ$
40		1nn	$⊢ 1 \in ℕ$
41	40	a1i	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to 1 \in ℕ$
42	39 41	nnmulcld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to q^{N} \cdot 1 \in ℕ$
43	42	nnge1d	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to 1 \leq q^{N} \cdot 1$
44	20 20 16	ledivmuld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (\frac{1}{q^{N}} \leq 1 \leftrightarrow 1 \leq q^{N} \cdot 1)$
45	43 44	mpbird	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{1}{q^{N}} \leq 1$
46	18 31 20 37 45	letrd	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{if (a \leq 1, a, 1)}{q^{N}} \leq 1$
47	46	adantr	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land 1 < \|A - (\frac{p}{q})\|) \to \frac{if (a \leq 1, a, 1)}{q^{N}} \leq 1$
48		ltle	$⊢ (1 \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ) \to (1 < \|A - (\frac{p}{q})\| \to 1 \leq \|A - (\frac{p}{q})\|)$
49	19 28 48	sylancr	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (1 < \|A - (\frac{p}{q})\| \to 1 \leq \|A - (\frac{p}{q})\|)$
50	49	imp	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land 1 < \|A - (\frac{p}{q})\|) \to 1 \leq \|A - (\frac{p}{q})\|$
51	47 50	jca	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land 1 < \|A - (\frac{p}{q})\|) \to (\frac{if (a \leq 1, a, 1)}{q^{N}} \leq 1 \land 1 \leq \|A - (\frac{p}{q})\|)$
52		letr	$⊢ (\frac{if (a \leq 1, a, 1)}{q^{N}} \in ℝ \land 1 \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ) \to ((\frac{if (a \leq 1, a, 1)}{q^{N}} \leq 1 \land 1 \leq \|A - (\frac{p}{q})\|) \to \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
53	30 51 52	sylc	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land 1 < \|A - (\frac{p}{q})\|) \to \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|$
54	53	olcd	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land 1 < \|A - (\frac{p}{q})\|) \to (A = \frac{p}{q} \lor \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
55	54	2a1d	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land 1 < \|A - (\frac{p}{q})\|) \to (((F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1) \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \to (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
56		pm3.21	$⊢ \|A - (\frac{p}{q})\| \leq 1 \to (F (\frac{p}{q}) \neq 0 \to (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1))$
57	56	adantl	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land \|A - (\frac{p}{q})\| \leq 1) \to (F (\frac{p}{q}) \neq 0 \to (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1))$
58	33 16	rpdivcld	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{a}{q^{N}} \in ℝ^{+}$
59	58	rpred	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{a}{q^{N}} \in ℝ$
60	18 59 28	3jca	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (\frac{if (a \leq 1, a, 1)}{q^{N}} \in ℝ \land \frac{a}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ)$
61	60	adantr	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to (\frac{if (a \leq 1, a, 1)}{q^{N}} \in ℝ \land \frac{a}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ)$
62		min1	$⊢ (a \in ℝ \land 1 \in ℝ) \to if (a \leq 1, a, 1) \leq a$
63	34 19 62	sylancl	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to if (a \leq 1, a, 1) \leq a$
64	32 34 16 63	lediv1dd	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \frac{a}{q^{N}}$
65	64	anim1i	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to (\frac{if (a \leq 1, a, 1)}{q^{N}} \leq \frac{a}{q^{N}} \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
66		letr	$⊢ (\frac{if (a \leq 1, a, 1)}{q^{N}} \in ℝ \land \frac{a}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ) \to ((\frac{if (a \leq 1, a, 1)}{q^{N}} \leq \frac{a}{q^{N}} \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
67	61 65 66	sylc	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|$
68	67	ex	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (\frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\| \to \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
69	68	adantr	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land \|A - (\frac{p}{q})\| \leq 1) \to (\frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\| \to \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
70	69	orim2d	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land \|A - (\frac{p}{q})\| \leq 1) \to ((A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to (A = \frac{p}{q} \lor \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
71	57 70	imim12d	$⊢ (((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land \|A - (\frac{p}{q})\| \leq 1) \to (((F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1) \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \to (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
72	55 71 20 28	ltlecasei	$⊢ ((φ \land a \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (((F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1) \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \to (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
73	72	ralimdvva	$⊢ (φ \land a \in ℝ^{+}) \to (\forall p \in ℤ \forall q \in ℕ ((F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1) \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \to \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
74		oveq1	$⊢ x = if (a \leq 1, a, 1) \to \frac{x}{q^{N}} = \frac{if (a \leq 1, a, 1)}{q^{N}}$
75	74	breq1d	$⊢ x = if (a \leq 1, a, 1) \to (\frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\| \leftrightarrow \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
76	75	orbi2d	$⊢ x = if (a \leq 1, a, 1) \to ((A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|) \leftrightarrow (A = \frac{p}{q} \lor \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
77	76	imbi2d	$⊢ x = if (a \leq 1, a, 1) \to ((F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \leftrightarrow (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
78	77	2ralbidv	$⊢ x = if (a \leq 1, a, 1) \to (\forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \leftrightarrow \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
79	78	rspcev	$⊢ (if (a \leq 1, a, 1) \in ℝ^{+} \land \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{if (a \leq 1, a, 1)}{q^{N}} \leq \|A - (\frac{p}{q})\|))) \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
80	10 73 79	syl6an	$⊢ (φ \land a \in ℝ^{+}) \to (\forall p \in ℤ \forall q \in ℕ ((F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1) \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
81	80	rexlimdva	$⊢ φ \to (\exists a \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ ((F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1) \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
82	6 81	mpd	$⊢ φ \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|))$

Metamath Proof Explorer

Theorem aalioulem5

Proof