irrapxlem5

Description: Lemma for irrapx1 . Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014)

		Ref	Expression
	Assertion	irrapxlem5	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \exists x \in ℚ (0 < x \land \|x - A\| < B \land \|x - A\| < {denom (x)}^{- 2})$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to B \in ℝ^{+}$
2	1	rpreccld	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \frac{1}{B} \in ℝ^{+}$
3	2	rprege0d	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to (\frac{1}{B} \in ℝ \land 0 \leq \frac{1}{B})$
4		flge0nn0	$⊢ (\frac{1}{B} \in ℝ \land 0 \leq \frac{1}{B}) \to ⌊\frac{1}{B}⌋ \in ℕ_{0}$
5		nn0p1nn	$⊢ ⌊\frac{1}{B}⌋ \in ℕ_{0} \to ⌊\frac{1}{B}⌋ + 1 \in ℕ$
6	3 4 5	3syl	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to ⌊\frac{1}{B}⌋ + 1 \in ℕ$
7		irrapxlem4	$⊢ (A \in ℝ^{+} \land ⌊\frac{1}{B}⌋ + 1 \in ℕ) \to \exists a \in ℕ \exists b \in ℕ \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}$
8	6 7	syldan	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \exists a \in ℕ \exists b \in ℕ \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}$
9		simplrr	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to b \in ℕ$
10		nnq	$⊢ b \in ℕ \to b \in ℚ$
11	9 10	syl	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to b \in ℚ$
12		simplrl	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \in ℕ$
13		nnq	$⊢ a \in ℕ \to a \in ℚ$
14	12 13	syl	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \in ℚ$
15	12	nnne0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \neq 0$
16		qdivcl	$⊢ (b \in ℚ \land a \in ℚ \land a \neq 0) \to \frac{b}{a} \in ℚ$
17	11 14 15 16	syl3anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{b}{a} \in ℚ$
18	9	nnrpd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to b \in ℝ^{+}$
19	12	nnrpd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \in ℝ^{+}$
20	18 19	rpdivcld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{b}{a} \in ℝ^{+}$
21	20	rpgt0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 0 < \frac{b}{a}$
22	12	nnred	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \in ℝ$
23	12	nnnn0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \in ℕ_{0}$
24	23	nn0ge0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 0 \leq a$
25	22 24	absidd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|a\| = a$
26	25	eqcomd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a = \|a\|$
27	26	oveq1d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \|(\frac{b}{a}) - A\| = \|a\| \|(\frac{b}{a}) - A\|$
28	12	nncnd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \in ℂ$
29		qre	$⊢ \frac{b}{a} \in ℚ \to \frac{b}{a} \in ℝ$
30	17 29	syl	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{b}{a} \in ℝ$
31		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
32	31	ad3antrrr	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to A \in ℝ$
33	30 32	resubcld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to (\frac{b}{a}) - A \in ℝ$
34	33	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to (\frac{b}{a}) - A \in ℂ$
35	28 34	absmuld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|a ((\frac{b}{a}) - A)\| = \|a\| \|(\frac{b}{a}) - A\|$
36	27 35	eqtr4d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \|(\frac{b}{a}) - A\| = \|a ((\frac{b}{a}) - A)\|$
37		qcn	$⊢ \frac{b}{a} \in ℚ \to \frac{b}{a} \in ℂ$
38	17 37	syl	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{b}{a} \in ℂ$
39		rpcn	$⊢ A \in ℝ^{+} \to A \in ℂ$
40	39	ad3antrrr	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to A \in ℂ$
41	28 38 40	subdid	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a ((\frac{b}{a}) - A) = a (\frac{b}{a}) - a A$
42	9	nncnd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to b \in ℂ$
43	42 28 15	divcan2d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a (\frac{b}{a}) = b$
44	28 40	mulcomd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a A = A a$
45	43 44	oveq12d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a (\frac{b}{a}) - a A = b - A a$
46	41 45	eqtrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a ((\frac{b}{a}) - A) = b - A a$
47	46	fveq2d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|a ((\frac{b}{a}) - A)\| = \|b - A a\|$
48	32 22	remulcld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to A a \in ℝ$
49	48	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to A a \in ℂ$
50	42 49	abssubd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|b - A a\| = \|A a - b\|$
51	36 47 50	3eqtrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \|(\frac{b}{a}) - A\| = \|A a - b\|$
52	9	nnred	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to b \in ℝ$
53	48 52	resubcld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to A a - b \in ℝ$
54	53	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to A a - b \in ℂ$
55	54	abscld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|A a - b\| \in ℝ$
56		simpllr	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to B \in ℝ^{+}$
57	56	rprecred	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{B} \in ℝ$
58	56	rpreccld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{B} \in ℝ^{+}$
59	58	rpge0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 0 \leq \frac{1}{B}$
60	57 59 4	syl2anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to ⌊\frac{1}{B}⌋ \in ℕ_{0}$
61	60 5	syl	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to ⌊\frac{1}{B}⌋ + 1 \in ℕ$
62	61	nnrpd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to ⌊\frac{1}{B}⌋ + 1 \in ℝ^{+}$
63	62 19	ifcld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a) \in ℝ^{+}$
64	63	rprecred	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)} \in ℝ$
65	56	rpred	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to B \in ℝ$
66	22 65	remulcld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a B \in ℝ$
67		simpr	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}$
68	58	rprecred	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{\frac{1}{B}} \in ℝ$
69	61	nnred	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to ⌊\frac{1}{B}⌋ + 1 \in ℝ$
70	69 22	ifcld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a) \in ℝ$
71		fllep1	$⊢ \frac{1}{B} \in ℝ \to \frac{1}{B} \leq ⌊\frac{1}{B}⌋ + 1$
72	57 71	syl	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{B} \leq ⌊\frac{1}{B}⌋ + 1$
73		max2	$⊢ (a \in ℝ \land ⌊\frac{1}{B}⌋ + 1 \in ℝ) \to ⌊\frac{1}{B}⌋ + 1 \leq if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)$
74	22 69 73	syl2anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to ⌊\frac{1}{B}⌋ + 1 \leq if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)$
75	57 69 70 72 74	letrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{B} \leq if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)$
76	58 63	lerecd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to (\frac{1}{B} \leq if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a) \leftrightarrow \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)} \leq \frac{1}{\frac{1}{B}})$
77	75 76	mpbid	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)} \leq \frac{1}{\frac{1}{B}}$
78	65	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to B \in ℂ$
79	56	rpne0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to B \neq 0$
80	78 79	recrecd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{\frac{1}{B}} = B$
81	78	mulid2d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 1 B = B$
82	80 81	eqtr4d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{\frac{1}{B}} = 1 B$
83	12	nnge1d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 1 \leq a$
84		1red	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 1 \in ℝ$
85	84 22 56	lemul1d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to (1 \leq a \leftrightarrow 1 B \leq a B)$
86	83 85	mpbid	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 1 B \leq a B$
87	82 86	eqbrtrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{\frac{1}{B}} \leq a B$
88	64 68 66 77 87	letrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)} \leq a B$
89	55 64 66 67 88	ltletrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|A a - b\| < a B$
90	51 89	eqbrtrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \|(\frac{b}{a}) - A\| < a B$
91	34	abscld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|(\frac{b}{a}) - A\| \in ℝ$
92	12	nngt0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 0 < a$
93		ltmul2	$⊢ (\|(\frac{b}{a}) - A\| \in ℝ \land B \in ℝ \land (a \in ℝ \land 0 < a)) \to (\|(\frac{b}{a}) - A\| < B \leftrightarrow a \|(\frac{b}{a}) - A\| < a B)$
94	91 65 22 92 93	syl112anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to (\|(\frac{b}{a}) - A\| < B \leftrightarrow a \|(\frac{b}{a}) - A\| < a B)$
95	90 94	mpbird	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|(\frac{b}{a}) - A\| < B$
96	22 22	remulcld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a a \in ℝ$
97	22 15	msqgt0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 0 < a a$
98	97	gt0ne0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a a \neq 0$
99	96 98	rereccld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{a a} \in ℝ$
100		qdencl	$⊢ \frac{b}{a} \in ℚ \to denom (\frac{b}{a}) \in ℕ$
101	17 100	syl	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to denom (\frac{b}{a}) \in ℕ$
102	101	nnred	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to denom (\frac{b}{a}) \in ℝ$
103	102 102	remulcld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to denom (\frac{b}{a}) denom (\frac{b}{a}) \in ℝ$
104	101	nnne0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to denom (\frac{b}{a}) \neq 0$
105	102 104	msqgt0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 0 < denom (\frac{b}{a}) denom (\frac{b}{a})$
106	105	gt0ne0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to denom (\frac{b}{a}) denom (\frac{b}{a}) \neq 0$
107	103 106	rereccld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{denom (\frac{b}{a}) denom (\frac{b}{a})} \in ℝ$
108	22 15	rereccld	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{a} \in ℝ$
109		max1	$⊢ (a \in ℝ \land ⌊\frac{1}{B}⌋ + 1 \in ℝ) \to a \leq if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)$
110	22 69 109	syl2anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \leq if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)$
111	19 63	lerecd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to (a \leq if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a) \leftrightarrow \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)} \leq \frac{1}{a})$
112	110 111	mpbid	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)} \leq \frac{1}{a}$
113	55 64 108 67 112	ltletrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|A a - b\| < \frac{1}{a}$
114	28 28 28 15 15	divdiv1d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{\frac{a}{a}}{a} = \frac{a}{a a}$
115	28 15	dividd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{a}{a} = 1$
116	115	oveq1d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{\frac{a}{a}}{a} = \frac{1}{a}$
117	96	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a a \in ℂ$
118	28 117 98	divrecd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{a}{a a} = a (\frac{1}{a a})$
119	114 116 118	3eqtr3rd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a (\frac{1}{a a}) = \frac{1}{a}$
120	113 51 119	3brtr4d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to a \|(\frac{b}{a}) - A\| < a (\frac{1}{a a})$
121		ltmul2	$⊢ (\|(\frac{b}{a}) - A\| \in ℝ \land \frac{1}{a a} \in ℝ \land (a \in ℝ \land 0 < a)) \to (\|(\frac{b}{a}) - A\| < \frac{1}{a a} \leftrightarrow a \|(\frac{b}{a}) - A\| < a (\frac{1}{a a}))$
122	91 99 22 92 121	syl112anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to (\|(\frac{b}{a}) - A\| < \frac{1}{a a} \leftrightarrow a \|(\frac{b}{a}) - A\| < a (\frac{1}{a a}))$
123	120 122	mpbird	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|(\frac{b}{a}) - A\| < \frac{1}{a a}$
124	9	nnzd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to b \in ℤ$
125		divdenle	$⊢ (b \in ℤ \land a \in ℕ) \to denom (\frac{b}{a}) \leq a$
126	124 12 125	syl2anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to denom (\frac{b}{a}) \leq a$
127	101	nnnn0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to denom (\frac{b}{a}) \in ℕ_{0}$
128	127	nn0ge0d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to 0 \leq denom (\frac{b}{a})$
129		le2msq	$⊢ ((denom (\frac{b}{a}) \in ℝ \land 0 \leq denom (\frac{b}{a})) \land (a \in ℝ \land 0 \leq a)) \to (denom (\frac{b}{a}) \leq a \leftrightarrow denom (\frac{b}{a}) denom (\frac{b}{a}) \leq a a)$
130	102 128 22 24 129	syl22anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to (denom (\frac{b}{a}) \leq a \leftrightarrow denom (\frac{b}{a}) denom (\frac{b}{a}) \leq a a)$
131	126 130	mpbid	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to denom (\frac{b}{a}) denom (\frac{b}{a}) \leq a a$
132		lerec	$⊢ ((denom (\frac{b}{a}) denom (\frac{b}{a}) \in ℝ \land 0 < denom (\frac{b}{a}) denom (\frac{b}{a})) \land (a a \in ℝ \land 0 < a a)) \to (denom (\frac{b}{a}) denom (\frac{b}{a}) \leq a a \leftrightarrow \frac{1}{a a} \leq \frac{1}{denom (\frac{b}{a}) denom (\frac{b}{a})})$
133	103 105 96 97 132	syl22anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to (denom (\frac{b}{a}) denom (\frac{b}{a}) \leq a a \leftrightarrow \frac{1}{a a} \leq \frac{1}{denom (\frac{b}{a}) denom (\frac{b}{a})})$
134	131 133	mpbid	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{a a} \leq \frac{1}{denom (\frac{b}{a}) denom (\frac{b}{a})}$
135	91 99 107 123 134	ltletrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|(\frac{b}{a}) - A\| < \frac{1}{denom (\frac{b}{a}) denom (\frac{b}{a})}$
136	101	nncnd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to denom (\frac{b}{a}) \in ℂ$
137		2nn0	$⊢ 2 \in ℕ_{0}$
138		expneg	$⊢ (denom (\frac{b}{a}) \in ℂ \land 2 \in ℕ_{0}) \to {denom (\frac{b}{a})}^{- 2} = \frac{1}{{denom (\frac{b}{a})}^{2}}$
139	136 137 138	sylancl	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to {denom (\frac{b}{a})}^{- 2} = \frac{1}{{denom (\frac{b}{a})}^{2}}$
140	136	sqvald	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to {denom (\frac{b}{a})}^{2} = denom (\frac{b}{a}) denom (\frac{b}{a})$
141	140	oveq2d	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \frac{1}{{denom (\frac{b}{a})}^{2}} = \frac{1}{denom (\frac{b}{a}) denom (\frac{b}{a})}$
142	139 141	eqtrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to {denom (\frac{b}{a})}^{- 2} = \frac{1}{denom (\frac{b}{a}) denom (\frac{b}{a})}$
143	135 142	breqtrrd	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \|(\frac{b}{a}) - A\| < {denom (\frac{b}{a})}^{- 2}$
144		breq2	$⊢ x = \frac{b}{a} \to (0 < x \leftrightarrow 0 < \frac{b}{a})$
145		fvoveq1	$⊢ x = \frac{b}{a} \to \|x - A\| = \|(\frac{b}{a}) - A\|$
146	145	breq1d	$⊢ x = \frac{b}{a} \to (\|x - A\| < B \leftrightarrow \|(\frac{b}{a}) - A\| < B)$
147		fveq2	$⊢ x = \frac{b}{a} \to denom (x) = denom (\frac{b}{a})$
148	147	oveq1d	$⊢ x = \frac{b}{a} \to {denom (x)}^{- 2} = {denom (\frac{b}{a})}^{- 2}$
149	145 148	breq12d	$⊢ x = \frac{b}{a} \to (\|x - A\| < {denom (x)}^{- 2} \leftrightarrow \|(\frac{b}{a}) - A\| < {denom (\frac{b}{a})}^{- 2})$
150	144 146 149	3anbi123d	$⊢ x = \frac{b}{a} \to ((0 < x \land \|x - A\| < B \land \|x - A\| < {denom (x)}^{- 2}) \leftrightarrow (0 < \frac{b}{a} \land \|(\frac{b}{a}) - A\| < B \land \|(\frac{b}{a}) - A\| < {denom (\frac{b}{a})}^{- 2}))$
151	150	rspcev	$⊢ (\frac{b}{a} \in ℚ \land (0 < \frac{b}{a} \land \|(\frac{b}{a}) - A\| < B \land \|(\frac{b}{a}) - A\| < {denom (\frac{b}{a})}^{- 2})) \to \exists x \in ℚ (0 < x \land \|x - A\| < B \land \|x - A\| < {denom (x)}^{- 2})$
152	17 21 95 143 151	syl13anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \land \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)}) \to \exists x \in ℚ (0 < x \land \|x - A\| < B \land \|x - A\| < {denom (x)}^{- 2})$
153	152	ex	$⊢ ((A \in ℝ^{+} \land B \in ℝ^{+}) \land (a \in ℕ \land b \in ℕ)) \to (\|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)} \to \exists x \in ℚ (0 < x \land \|x - A\| < B \land \|x - A\| < {denom (x)}^{- 2}))$
154	153	rexlimdvva	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to (\exists a \in ℕ \exists b \in ℕ \|A a - b\| < \frac{1}{if (a \leq ⌊\frac{1}{B}⌋ + 1, ⌊\frac{1}{B}⌋ + 1, a)} \to \exists x \in ℚ (0 < x \land \|x - A\| < B \land \|x - A\| < {denom (x)}^{- 2}))$
155	8 154	mpd	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \exists x \in ℚ (0 < x \land \|x - A\| < B \land \|x - A\| < {denom (x)}^{- 2})$

Metamath Proof Explorer

Theorem irrapxlem5

Proof