aalioulem4

	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	aalioulem4	$⊢ φ \to \exists x \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{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	aalioulem3	$⊢ φ \to \exists x \in ℝ^{+} \forall a \in ℝ (\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|)$
7		simp2l	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to p \in ℤ$
8		simp2r	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q \in ℕ$
9		znq	$⊢ (p \in ℤ \land q \in ℕ) \to \frac{p}{q} \in ℚ$
10	7 8 9	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \frac{p}{q} \in ℚ$
11		qre	$⊢ \frac{p}{q} \in ℚ \to \frac{p}{q} \in ℝ$
12	10 11	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \frac{p}{q} \in ℝ$
13		simp3r	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \|A - (\frac{p}{q})\| \leq 1$
14		oveq2	$⊢ a = \frac{p}{q} \to A - a = A - (\frac{p}{q})$
15	14	fveq2d	$⊢ a = \frac{p}{q} \to \|A - a\| = \|A - (\frac{p}{q})\|$
16	15	breq1d	$⊢ a = \frac{p}{q} \to (\|A - a\| \leq 1 \leftrightarrow \|A - (\frac{p}{q})\| \leq 1)$
17		2fveq3	$⊢ a = \frac{p}{q} \to \|F (a)\| = \|F (\frac{p}{q})\|$
18	17	oveq2d	$⊢ a = \frac{p}{q} \to x \|F (a)\| = x \|F (\frac{p}{q})\|$
19	18 15	breq12d	$⊢ a = \frac{p}{q} \to (x \|F (a)\| \leq \|A - a\| \leftrightarrow x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|)$
20	16 19	imbi12d	$⊢ a = \frac{p}{q} \to ((\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|) \leftrightarrow (\|A - (\frac{p}{q})\| \leq 1 \to x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|))$
21	20	rspcv	$⊢ \frac{p}{q} \in ℝ \to (\forall a \in ℝ (\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|) \to (\|A - (\frac{p}{q})\| \leq 1 \to x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|))$
22	21	com23	$⊢ \frac{p}{q} \in ℝ \to (\|A - (\frac{p}{q})\| \leq 1 \to (\forall a \in ℝ (\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|) \to x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|))$
23	12 13 22	sylc	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to (\forall a \in ℝ (\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|) \to x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|)$
24		simp1r	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to x \in ℝ^{+}$
25	8	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q \in ℝ^{+}$
26		simp1l	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to φ$
27	26 3	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to N \in ℕ$
28	27	nnzd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to N \in ℤ$
29	25 28	rpexpcld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q^{N} \in ℝ^{+}$
30	24 29	rpdivcld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \frac{x}{q^{N}} \in ℝ^{+}$
31	30	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \frac{x}{q^{N}} \in ℝ$
32	31	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \land x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|) \to \frac{x}{q^{N}} \in ℝ$
33	24	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to x \in ℝ$
34	26 2	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to F \in Poly (ℤ)$
35		plyf	$⊢ F \in Poly (ℤ) \to F : ℂ ⟶ ℂ$
36	34 35	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to F : ℂ ⟶ ℂ$
37	12	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \frac{p}{q} \in ℂ$
38	36 37	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to F (\frac{p}{q}) \in ℂ$
39	38	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \|F (\frac{p}{q})\| \in ℝ$
40	33 39	remulcld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to x \|F (\frac{p}{q})\| \in ℝ$
41	40	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \land x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|) \to x \|F (\frac{p}{q})\| \in ℝ$
42	26 4	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to A \in ℝ$
43	42 12	resubcld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to A - (\frac{p}{q}) \in ℝ$
44	43	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to A - (\frac{p}{q}) \in ℂ$
45	44	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \|A - (\frac{p}{q})\| \in ℝ$
46	45	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \land x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|) \to \|A - (\frac{p}{q})\| \in ℝ$
47	24	rpcnd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to x \in ℂ$
48	29	rpcnd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q^{N} \in ℂ$
49	29	rpne0d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q^{N} \neq 0$
50	47 48 49	divrecd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \frac{x}{q^{N}} = x (\frac{1}{q^{N}})$
51	48 38	absmuld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \|q^{N} F (\frac{p}{q})\| = \|q^{N}\| \|F (\frac{p}{q})\|$
52	29	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q^{N} \in ℝ$
53	29	rpge0d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to 0 \leq q^{N}$
54	52 53	absidd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \|q^{N}\| = q^{N}$
55	54	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \|q^{N}\| \|F (\frac{p}{q})\| = q^{N} \|F (\frac{p}{q})\|$
56	51 55	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \|q^{N} F (\frac{p}{q})\| = q^{N} \|F (\frac{p}{q})\|$
57	48 38	mulcomd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q^{N} F (\frac{p}{q}) = F (\frac{p}{q}) q^{N}$
58	1	oveq2i	$⊢ q^{N} = q^{\deg (F)}$
59	58	oveq2i	$⊢ F (\frac{p}{q}) q^{N} = F (\frac{p}{q}) q^{\deg (F)}$
60	57 59	eqtrdi	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q^{N} F (\frac{p}{q}) = F (\frac{p}{q}) q^{\deg (F)}$
61	34 7 8	aalioulem1	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to F (\frac{p}{q}) q^{\deg (F)} \in ℤ$
62	60 61	eqeltrd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q^{N} F (\frac{p}{q}) \in ℤ$
63		simp3l	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to F (\frac{p}{q}) \neq 0$
64	48 38 49 63	mulne0d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q^{N} F (\frac{p}{q}) \neq 0$
65		nnabscl	$⊢ (q^{N} F (\frac{p}{q}) \in ℤ \land q^{N} F (\frac{p}{q}) \neq 0) \to \|q^{N} F (\frac{p}{q})\| \in ℕ$
66	62 64 65	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \|q^{N} F (\frac{p}{q})\| \in ℕ$
67	56 66	eqeltrrd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to q^{N} \|F (\frac{p}{q})\| \in ℕ$
68	67	nnge1d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to 1 \leq q^{N} \|F (\frac{p}{q})\|$
69		1red	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to 1 \in ℝ$
70	69 39 29	ledivmuld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to (\frac{1}{q^{N}} \leq \|F (\frac{p}{q})\| \leftrightarrow 1 \leq q^{N} \|F (\frac{p}{q})\|)$
71	68 70	mpbird	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \frac{1}{q^{N}} \leq \|F (\frac{p}{q})\|$
72	29	rprecred	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \frac{1}{q^{N}} \in ℝ$
73	72 39 24	lemul2d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to (\frac{1}{q^{N}} \leq \|F (\frac{p}{q})\| \leftrightarrow x (\frac{1}{q^{N}}) \leq x \|F (\frac{p}{q})\|)$
74	71 73	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to x (\frac{1}{q^{N}}) \leq x \|F (\frac{p}{q})\|$
75	50 74	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to \frac{x}{q^{N}} \leq x \|F (\frac{p}{q})\|$
76	75	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \land x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|) \to \frac{x}{q^{N}} \leq x \|F (\frac{p}{q})\|$
77		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \land x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|) \to x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|$
78	32 41 46 76 77	letrd	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \land x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|) \to \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|$
79	78	olcd	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \land x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\|) \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
80	79	ex	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to (x \|F (\frac{p}{q})\| \leq \|A - (\frac{p}{q})\| \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
81	23 80	syld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ) \land (F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1)) \to (\forall a \in ℝ (\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|) \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
82	81	3exp	$⊢ (φ \land x \in ℝ^{+}) \to ((p \in ℤ \land q \in ℕ) \to ((F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1) \to (\forall a \in ℝ (\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|) \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|))))$
83	82	com34	$⊢ (φ \land x \in ℝ^{+}) \to ((p \in ℤ \land q \in ℕ) \to (\forall a \in ℝ (\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|) \to ((F (\frac{p}{q}) \neq 0 \land \|A - (\frac{p}{q})\| \leq 1) \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|))))$
84	83	com23	$⊢ (φ \land x \in ℝ^{+}) \to (\forall a \in ℝ (\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|) \to ((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{x}{q^{N}} \leq \|A - (\frac{p}{q})\|))))$
85	84	ralrimdvv	$⊢ (φ \land x \in ℝ^{+}) \to (\forall a \in ℝ (\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|) \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{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
86	85	reximdva	$⊢ φ \to (\exists x \in ℝ^{+} \forall a \in ℝ (\|A - a\| \leq 1 \to x \|F (a)\| \leq \|A - a\|) \to \exists x \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{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
87	6 86	mpd	$⊢ φ \to \exists x \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{x}{q^{N}} \leq \|A - (\frac{p}{q})\|))$

Metamath Proof Explorer

Theorem aalioulem4

Proof