aalioulem2

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 15-Nov-2014) (Proof shortened by AV, 28-Sep-2020)

	Ref	Expression
Hypotheses	aalioulem2.a	$⊢ N = \deg (F)$
	aalioulem2.b	$⊢ φ \to F \in Poly (ℤ)$
	aalioulem2.c	$⊢ φ \to N \in ℕ$
	aalioulem2.d	$⊢ φ \to A \in ℝ$
Assertion	aalioulem2	$⊢ φ \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 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		1rp	$⊢ 1 \in ℝ^{+}$
6		snssi	$⊢ 1 \in ℝ^{+} \to \{1\} \subseteq ℝ^{+}$
7	5 6	ax-mp	$⊢ \{1\} \subseteq ℝ^{+}$
8		ssrab2	$⊢ \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \subseteq ℝ^{+}$
9	7 8	unssi	$⊢ \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \subseteq ℝ^{+}$
10		ltso	$⊢ < Or ℝ$
11	10	a1i	$⊢ φ \to < Or ℝ$
12		snfi	$⊢ \{1\} \in Fin$
13	3	nnne0d	$⊢ φ \to N \neq 0$
14	1	eqcomi	$⊢ \deg (F) = N$
15		dgr0	$⊢ \deg (0_{𝑝}) = 0$
16	13 14 15	3netr4g	$⊢ φ \to \deg (F) \neq \deg (0_{𝑝})$
17		fveq2	$⊢ F = 0_{𝑝} \to \deg (F) = \deg (0_{𝑝})$
18	17	necon3i	$⊢ \deg (F) \neq \deg (0_{𝑝}) \to F \neq 0_{𝑝}$
19	16 18	syl	$⊢ φ \to F \neq 0_{𝑝}$
20		eqid	$⊢ F^{-1} [\{0\}] = F^{-1} [\{0\}]$
21	20	fta1	$⊢ (F \in Poly (ℤ) \land F \neq 0_{𝑝}) \to (F^{-1} [\{0\}] \in Fin \land \|F^{-1} [\{0\}]\| \leq \deg (F))$
22	2 19 21	syl2anc	$⊢ φ \to (F^{-1} [\{0\}] \in Fin \land \|F^{-1} [\{0\}]\| \leq \deg (F))$
23	22	simpld	$⊢ φ \to F^{-1} [\{0\}] \in Fin$
24		abrexfi	$⊢ F^{-1} [\{0\}] \in Fin \to \{a \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \in Fin$
25	23 24	syl	$⊢ φ \to \{a \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \in Fin$
26		rabssab	$⊢ \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \subseteq \{a \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\}$
27		ssfi	$⊢ (\{a \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \in Fin \land \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \subseteq \{a \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\}) \to \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \in Fin$
28	25 26 27	sylancl	$⊢ φ \to \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \in Fin$
29		unfi	$⊢ (\{1\} \in Fin \land \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \in Fin) \to \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \in Fin$
30	12 28 29	sylancr	$⊢ φ \to \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \in Fin$
31		1ex	$⊢ 1 \in V$
32	31	snid	$⊢ 1 \in \{1\}$
33		elun1	$⊢ 1 \in \{1\} \to 1 \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\})$
34		ne0i	$⊢ 1 \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\}) \to \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \neq \emptyset$
35	32 33 34	mp2b	$⊢ \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \neq \emptyset$
36	35	a1i	$⊢ φ \to \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \neq \emptyset$
37		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
38	9 37	sstri	$⊢ \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \subseteq ℝ$
39	38	a1i	$⊢ φ \to \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \subseteq ℝ$
40		fiinfcl	$⊢ (< Or ℝ \land (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \in Fin \land \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \neq \emptyset \land \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \subseteq ℝ)) \to inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\})$
41	11 30 36 39 40	syl13anc	$⊢ φ \to inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\})$
42	9 41	sselid	$⊢ φ \to inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \in ℝ^{+}$
43		0re	$⊢ 0 \in ℝ$
44		rpge0	$⊢ d \in ℝ^{+} \to 0 \leq d$
45	44	rgen	$⊢ \forall d \in ℝ^{+} 0 \leq d$
46		breq1	$⊢ c = 0 \to (c \leq d \leftrightarrow 0 \leq d)$
47	46	ralbidv	$⊢ c = 0 \to (\forall d \in ℝ^{+} c \leq d \leftrightarrow \forall d \in ℝ^{+} 0 \leq d)$
48	47	rspcev	$⊢ (0 \in ℝ \land \forall d \in ℝ^{+} 0 \leq d) \to \exists c \in ℝ \forall d \in ℝ^{+} c \leq d$
49	43 45 48	mp2an	$⊢ \exists c \in ℝ \forall d \in ℝ^{+} c \leq d$
50		ssralv	$⊢ \{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \subseteq ℝ^{+} \to (\forall d \in ℝ^{+} c \leq d \to \forall d \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\}) c \leq d)$
51	9 50	ax-mp	$⊢ \forall d \in ℝ^{+} c \leq d \to \forall d \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\}) c \leq d$
52	51	reximi	$⊢ \exists c \in ℝ \forall d \in ℝ^{+} c \leq d \to \exists c \in ℝ \forall d \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\}) c \leq d$
53	49 52	ax-mp	$⊢ \exists c \in ℝ \forall d \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\}) c \leq d$
54		eqeq1	$⊢ a = \|A - r\| \to (a = \|A - b\| \leftrightarrow \|A - r\| = \|A - b\|)$
55	54	rexbidv	$⊢ a = \|A - r\| \to (\exists b \in F^{-1} [\{0\}] a = \|A - b\| \leftrightarrow \exists b \in F^{-1} [\{0\}] \|A - r\| = \|A - b\|)$
56	4	ad2antrr	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to A \in ℝ$
57		simplr	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to r \in ℝ$
58	56 57	resubcld	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to A - r \in ℝ$
59	58	recnd	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to A - r \in ℂ$
60	4	ad2antrr	$⊢ ((φ \land r \in ℝ) \land F (r) = 0) \to A \in ℝ$
61	60	recnd	$⊢ ((φ \land r \in ℝ) \land F (r) = 0) \to A \in ℂ$
62		simplr	$⊢ ((φ \land r \in ℝ) \land F (r) = 0) \to r \in ℝ$
63	62	recnd	$⊢ ((φ \land r \in ℝ) \land F (r) = 0) \to r \in ℂ$
64	61 63	subeq0ad	$⊢ ((φ \land r \in ℝ) \land F (r) = 0) \to (A - r = 0 \leftrightarrow A = r)$
65	64	necon3abid	$⊢ ((φ \land r \in ℝ) \land F (r) = 0) \to (A - r \neq 0 \leftrightarrow \neg A = r)$
66	65	biimprd	$⊢ ((φ \land r \in ℝ) \land F (r) = 0) \to (\neg A = r \to A - r \neq 0)$
67	66	impr	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to A - r \neq 0$
68	59 67	absrpcld	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to \|A - r\| \in ℝ^{+}$
69	57	recnd	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to r \in ℂ$
70		simprl	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to F (r) = 0$
71		plyf	$⊢ F \in Poly (ℤ) \to F : ℂ ⟶ ℂ$
72	2 71	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
73	72	ffnd	$⊢ φ \to F Fn ℂ$
74	73	ad2antrr	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to F Fn ℂ$
75		fniniseg	$⊢ F Fn ℂ \to (r \in F^{-1} [\{0\}] \leftrightarrow (r \in ℂ \land F (r) = 0))$
76	74 75	syl	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to (r \in F^{-1} [\{0\}] \leftrightarrow (r \in ℂ \land F (r) = 0))$
77	69 70 76	mpbir2and	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to r \in F^{-1} [\{0\}]$
78		eqid	$⊢ \|A - r\| = \|A - r\|$
79		oveq2	$⊢ b = r \to A - b = A - r$
80	79	fveq2d	$⊢ b = r \to \|A - b\| = \|A - r\|$
81	80	rspceeqv	$⊢ (r \in F^{-1} [\{0\}] \land \|A - r\| = \|A - r\|) \to \exists b \in F^{-1} [\{0\}] \|A - r\| = \|A - b\|$
82	77 78 81	sylancl	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to \exists b \in F^{-1} [\{0\}] \|A - r\| = \|A - b\|$
83	55 68 82	elrabd	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to \|A - r\| \in \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\}$
84		elun2	$⊢ \|A - r\| \in \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \to \|A - r\| \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\})$
85	83 84	syl	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to \|A - r\| \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\})$
86		infrelb	$⊢ (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} \subseteq ℝ \land \exists c \in ℝ \forall d \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\}) c \leq d \land \|A - r\| \in (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\})) \to inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|$
87	38 53 85 86	mp3an12i	$⊢ ((φ \land r \in ℝ) \land (F (r) = 0 \land \neg A = r)) \to inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|$
88	87	expr	$⊢ ((φ \land r \in ℝ) \land F (r) = 0) \to (\neg A = r \to inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|)$
89	88	orrd	$⊢ ((φ \land r \in ℝ) \land F (r) = 0) \to (A = r \lor inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|)$
90	89	ex	$⊢ (φ \land r \in ℝ) \to (F (r) = 0 \to (A = r \lor inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|))$
91	90	ralrimiva	$⊢ φ \to \forall r \in ℝ (F (r) = 0 \to (A = r \lor inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|))$
92		breq1	$⊢ x = inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \to (x \leq \|A - r\| \leftrightarrow inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|)$
93	92	orbi2d	$⊢ x = inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \to ((A = r \lor x \leq \|A - r\|) \leftrightarrow (A = r \lor inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|))$
94	93	imbi2d	$⊢ x = inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \to ((F (r) = 0 \to (A = r \lor x \leq \|A - r\|)) \leftrightarrow (F (r) = 0 \to (A = r \lor inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|)))$
95	94	ralbidv	$⊢ x = inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \to (\forall r \in ℝ (F (r) = 0 \to (A = r \lor x \leq \|A - r\|)) \leftrightarrow \forall r \in ℝ (F (r) = 0 \to (A = r \lor inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|)))$
96	95	rspcev	$⊢ (inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \in ℝ^{+} \land \forall r \in ℝ (F (r) = 0 \to (A = r \lor inf (\{1\} \cup \{a \in ℝ^{+} \| \exists b \in F^{-1} [\{0\}] a = \|A - b\|\} ℝ <) \leq \|A - r\|))) \to \exists x \in ℝ^{+} \forall r \in ℝ (F (r) = 0 \to (A = r \lor x \leq \|A - r\|))$
97	42 91 96	syl2anc	$⊢ φ \to \exists x \in ℝ^{+} \forall r \in ℝ (F (r) = 0 \to (A = r \lor x \leq \|A - r\|))$
98		fveqeq2	$⊢ r = \frac{p}{q} \to (F (r) = 0 \leftrightarrow F (\frac{p}{q}) = 0)$
99		eqeq2	$⊢ r = \frac{p}{q} \to (A = r \leftrightarrow A = \frac{p}{q})$
100		oveq2	$⊢ r = \frac{p}{q} \to A - r = A - (\frac{p}{q})$
101	100	fveq2d	$⊢ r = \frac{p}{q} \to \|A - r\| = \|A - (\frac{p}{q})\|$
102	101	breq2d	$⊢ r = \frac{p}{q} \to (x \leq \|A - r\| \leftrightarrow x \leq \|A - (\frac{p}{q})\|)$
103	99 102	orbi12d	$⊢ r = \frac{p}{q} \to ((A = r \lor x \leq \|A - r\|) \leftrightarrow (A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|))$
104	98 103	imbi12d	$⊢ r = \frac{p}{q} \to ((F (r) = 0 \to (A = r \lor x \leq \|A - r\|)) \leftrightarrow (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|)))$
105	104	rspcv	$⊢ \frac{p}{q} \in ℝ \to (\forall r \in ℝ (F (r) = 0 \to (A = r \lor x \leq \|A - r\|)) \to (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|)))$
106		znq	$⊢ (p \in ℤ \land q \in ℕ) \to \frac{p}{q} \in ℚ$
107		qre	$⊢ \frac{p}{q} \in ℚ \to \frac{p}{q} \in ℝ$
108	106 107	syl	$⊢ (p \in ℤ \land q \in ℕ) \to \frac{p}{q} \in ℝ$
109	105 108	syl11	$⊢ \forall r \in ℝ (F (r) = 0 \to (A = r \lor x \leq \|A - r\|)) \to ((p \in ℤ \land q \in ℕ) \to (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|)))$
110	109	ralrimivv	$⊢ \forall r \in ℝ (F (r) = 0 \to (A = r \lor x \leq \|A - r\|)) \to \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|))$
111	110	reximi	$⊢ \exists x \in ℝ^{+} \forall r \in ℝ (F (r) = 0 \to (A = r \lor x \leq \|A - r\|)) \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|))$
112	97 111	syl	$⊢ φ \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|))$
113		simplr	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to x \in ℝ^{+}$
114		simprr	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to q \in ℕ$
115	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
116	115	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to N \in ℕ_{0}$
117	114 116	nnexpcld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to q^{N} \in ℕ$
118	117	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to q^{N} \in ℝ^{+}$
119	113 118	rpdivcld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{x}{q^{N}} \in ℝ^{+}$
120	119	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{x}{q^{N}} \in ℝ$
121	120	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land x \leq \|A - (\frac{p}{q})\|) \to \frac{x}{q^{N}} \in ℝ$
122		simpllr	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land x \leq \|A - (\frac{p}{q})\|) \to x \in ℝ^{+}$
123	122	rpred	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land x \leq \|A - (\frac{p}{q})\|) \to x \in ℝ$
124	4	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to A \in ℝ$
125	108	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{p}{q} \in ℝ$
126	124 125	resubcld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to A - (\frac{p}{q}) \in ℝ$
127	126	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to A - (\frac{p}{q}) \in ℂ$
128	127	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \|A - (\frac{p}{q})\| \in ℝ$
129	128	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land x \leq \|A - (\frac{p}{q})\|) \to \|A - (\frac{p}{q})\| \in ℝ$
130		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
131	130	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to x \in ℝ$
132	113	rpcnne0d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (x \in ℂ \land x \neq 0)$
133		divid	$⊢ (x \in ℂ \land x \neq 0) \to \frac{x}{x} = 1$
134	132 133	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{x}{x} = 1$
135	117	nnge1d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to 1 \leq q^{N}$
136	134 135	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{x}{x} \leq q^{N}$
137	131 113 118 136	lediv23d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to \frac{x}{q^{N}} \leq x$
138	137	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land x \leq \|A - (\frac{p}{q})\|) \to \frac{x}{q^{N}} \leq x$
139		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land x \leq \|A - (\frac{p}{q})\|) \to x \leq \|A - (\frac{p}{q})\|$
140	121 123 129 138 139	letrd	$⊢ (((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \land x \leq \|A - (\frac{p}{q})\|) \to \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|$
141	140	ex	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to (x \leq \|A - (\frac{p}{q})\| \to \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)$
142	141	orim2d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to ((A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|) \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|))$
143	142	imim2d	$⊢ ((φ \land x \in ℝ^{+}) \land (p \in ℤ \land q \in ℕ)) \to ((F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|)) \to (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
144	143	ralimdvva	$⊢ (φ \land x \in ℝ^{+}) \to (\forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|)) \to \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
145	144	reximdva	$⊢ φ \to (\exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor x \leq \|A - (\frac{p}{q})\|)) \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|)))$
146	112 145	mpd	$⊢ φ \to \exists x \in ℝ^{+} \forall p \in ℤ \forall q \in ℕ (F (\frac{p}{q}) = 0 \to (A = \frac{p}{q} \lor \frac{x}{q^{N}} \leq \|A - (\frac{p}{q})\|))$

Metamath Proof Explorer

Theorem aalioulem2

Proof