aalioulem6

	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	aalioulem6	$⊢ φ \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (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	aalioulem2	$⊢ φ \to \exists a \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
7	1 2 3 4 5	aalioulem5	$⊢ φ \to \exists b \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
8		reeanv	$⊢ \exists a \in ℝ^{+} \exists b \in ℝ^{+} (\forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|))) \leftrightarrow (\exists a \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land \exists b \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
9	6 7 8	sylanbrc	$⊢ φ \to \exists a \in ℝ^{+} \exists b \in ℝ^{+} (\forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
10		r19.26-2	$⊢ \forall p \in ℤ \forall q \in ℕ ((F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|))) \leftrightarrow (\forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
11		ifcl	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to if (a \leq b, a, b) \in ℝ^{+}$
12	11	adantl	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to if (a \leq b, a, b) \in ℝ^{+}$
13		simpr	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land F (\frac{p}{q}) = 0) \to F (\frac{p}{q}) = 0$
14	11	ad2antlr	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to if (a \leq b, a, b) \in ℝ^{+}$
15		nnrp	$⊢ q \in ℕ \to q \in ℝ^{+}$
16	15	ad2antll	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to q \in ℝ^{+}$
17	3	ad2antrr	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to N \in ℕ$
18	17	nnzd	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to N \in ℤ$
19	16 18	rpexpcld	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to q^{N} \in ℝ^{+}$
20	14 19	rpdivcld	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to \frac{if (a \leq b, a, b)}{q^{N}} \in ℝ^{+}$
21	20	rpred	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to \frac{if (a \leq b, a, b)}{q^{N}} \in ℝ$
22		simplrl	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to a \in ℝ^{+}$
23	22 19	rpdivcld	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to \frac{a}{q^{N}} \in ℝ^{+}$
24	23	rpred	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to \frac{a}{q^{N}} \in ℝ$
25	4	ad2antrr	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to A \in ℝ$
26		znq	$⊢ (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	$⊢ (p \in ℤ \land q \in ℕ) \to \frac{p}{q} \in ℝ$
29	28	adantl	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to \frac{p}{q} \in ℝ$
30	25 29	resubcld	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to A - (\frac{p}{q}) \in ℝ$
31	30	recnd	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to A - (\frac{p}{q}) \in ℂ$
32	31	abscld	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to \|A - (\frac{p}{q})\| \in ℝ$
33	21 24 32	3jca	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to (\frac{if (a \leq b, a, b)}{q^{N}} \in ℝ \land \frac{a}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ)$
34	33	adantr	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to (\frac{if (a \leq b, a, b)}{q^{N}} \in ℝ \land \frac{a}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ)$
35	14	rpred	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to if (a \leq b, a, b) \in ℝ$
36	22	rpred	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to a \in ℝ$
37		simplrr	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to b \in ℝ^{+}$
38	37	rpred	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to b \in ℝ$
39		min1	$⊢ (a \in ℝ \land b \in ℝ) \to if (a \leq b, a, b) \leq a$
40	36 38 39	syl2anc	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to if (a \leq b, a, b) \leq a$
41	35 36 19 40	lediv1dd	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to \frac{if (a \leq b, a, b)}{q^{N}} \leq \frac{a}{q^{N}}$
42	41	anim1i	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to (\frac{if (a \leq b, a, b)}{q^{N}} \leq \frac{a}{q^{N}} \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
43		letr	$⊢ (\frac{if (a \leq b, a, b)}{q^{N}} \in ℝ \land \frac{a}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ) \to ((\frac{if (a \leq b, a, b)}{q^{N}} \leq \frac{a}{q^{N}} \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
44	34 42 43	sylc	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|$
45	44	ex	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to (\frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\| \to \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
46	45	adantr	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land F (\frac{p}{q}) = 0) \to (\frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\| \to \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
47	46	orim2d	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land F (\frac{p}{q}) = 0) \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 b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
48	13 47	embantd	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land F (\frac{p}{q}) = 0) \to ((F (\frac{p}{q}) = 0 \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 b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
49	48	adantrd	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land F (\frac{p}{q}) = 0) \to (((F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|))) \to (A = \frac{p}{q} \lor \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
50		simpr	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land F (\frac{p}{q}) \neq 0) \to F (\frac{p}{q}) \neq 0$
51	37 19	rpdivcld	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to \frac{b}{q^{N}} \in ℝ^{+}$
52	51	rpred	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to \frac{b}{q^{N}} \in ℝ$
53	21 52 32	3jca	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to (\frac{if (a \leq b, a, b)}{q^{N}} \in ℝ \land \frac{b}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ)$
54	53	adantr	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to (\frac{if (a \leq b, a, b)}{q^{N}} \in ℝ \land \frac{b}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ)$
55		min2	$⊢ (a \in ℝ \land b \in ℝ) \to if (a \leq b, a, b) \leq b$
56	36 38 55	syl2anc	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to if (a \leq b, a, b) \leq b$
57	35 38 19 56	lediv1dd	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to \frac{if (a \leq b, a, b)}{q^{N}} \leq \frac{b}{q^{N}}$
58	57	anim1i	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to (\frac{if (a \leq b, a, b)}{q^{N}} \leq \frac{b}{q^{N}} \land \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
59		letr	$⊢ (\frac{if (a \leq b, a, b)}{q^{N}} \in ℝ \land \frac{b}{q^{N}} \in ℝ \land \|A - (\frac{p}{q})\| \in ℝ) \to ((\frac{if (a \leq b, a, b)}{q^{N}} \leq \frac{b}{q^{N}} \land \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
60	54 58 59	sylc	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|$
61	60	ex	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to (\frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\| \to \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
62	61	adantr	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land F (\frac{p}{q}) \neq 0) \to (\frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\| \to \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
63	62	orim2d	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land F (\frac{p}{q}) \neq 0) \to ((A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|) \to (A = \frac{p}{q} \lor \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
64	50 63	embantd	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land F (\frac{p}{q}) \neq 0) \to ((F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \to (A = \frac{p}{q} \lor \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
65	64	adantld	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \land F (\frac{p}{q}) \neq 0) \to (((F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|))) \to (A = \frac{p}{q} \lor \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
66	49 65	pm2.61dane	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (p \in ℤ \land q \in ℕ)) \to (((F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|))) \to (A = \frac{p}{q} \lor \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
67	66	ralimdvva	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to (\forall p \in ℤ \forall q \in ℕ ((F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{q^{N}} \leq \|A - (\frac{p}{q})\|))) \to \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
68		oveq1	$⊢ x = if (a \leq b, a, b) \to \frac{x}{q^{N}} = \frac{if (a \leq b, a, b)}{q^{N}}$
69	68	breq1d	$⊢ x = if (a \leq b, a, b) \to (\frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\| \leftrightarrow \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
70	69	orbi2d	$⊢ x = if (a \leq b, a, b) \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 b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
71	70	2ralbidv	$⊢ x = if (a \leq b, a, b) \to (\forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|) \leftrightarrow \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{if (a \leq b, a, b)}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
72	71	rspcev	$⊢ (if (a \leq b, a, b) \in ℝ^{+} \land \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{if (a \leq b, a, b)}{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}} \leq \|A - (\frac{p}{q})\|)$
73	12 67 72	syl6an	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to (\forall p \in ℤ \forall q \in ℕ ((F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{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}} \leq \|A - (\frac{p}{q})\|))$
74	10 73	biimtrrid	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to ((\forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{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}} \leq \|A - (\frac{p}{q})\|))$
75	74	rexlimdvva	$⊢ φ \to (\exists a \in ℝ^{+} \exists b \in ℝ^{+} (\forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{a}{q^{N}} \leq \|A - (\frac{p}{q})\|)) \land \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) \neq 0 \to (A = \frac{p}{q} \lor \frac{b}{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}} \leq \|A - (\frac{p}{q})\|))$
76	9 75	mpd	$⊢ φ \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)$

Metamath Proof Explorer

Theorem aalioulem6

Proof