irrapxlem4

Description: Lemma for irrapx1 . Eliminate ranges, use positivity of the input to force positivity of the output by increasing B as needed. (Contributed by Stefan O'Rear, 13-Sep-2014)

		Ref	Expression
	Assertion	irrapxlem4	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to \exists x \in ℕ \exists y \in ℕ \|A x - y\| < \frac{1}{if (x \leq B, B, x)}$

Proof

Step	Hyp	Ref	Expression
1		elfznn	$⊢ a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)) \to a \in ℕ$
2	1	ad3antlr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to a \in ℕ$
3		nn0z	$⊢ b \in ℕ_{0} \to b \in ℤ$
4	3	ad2antlr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to b \in ℤ$
5		simpl	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to A \in ℝ^{+}$
6	5	ad3antrrr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A \in ℝ^{+}$
7	6	rpred	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A \in ℝ$
8	2	nnred	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to a \in ℝ$
9	7 8	remulcld	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A a \in ℝ$
10		nn0re	$⊢ b \in ℕ_{0} \to b \in ℝ$
11	10	ad2antlr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to b \in ℝ$
12	9 11	resubcld	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A a - b \in ℝ$
13	12	recnd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A a - b \in ℂ$
14	13	abscld	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \|A a - b\| \in ℝ$
15	5	rpreccld	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to \frac{1}{A} \in ℝ^{+}$
16	15	rprege0d	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to (\frac{1}{A} \in ℝ \land 0 \leq \frac{1}{A})$
17		flge0nn0	$⊢ (\frac{1}{A} \in ℝ \land 0 \leq \frac{1}{A}) \to ⌊\frac{1}{A}⌋ \in ℕ_{0}$
18		nn0p1nn	$⊢ ⌊\frac{1}{A}⌋ \in ℕ_{0} \to ⌊\frac{1}{A}⌋ + 1 \in ℕ$
19	16 17 18	3syl	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to ⌊\frac{1}{A}⌋ + 1 \in ℕ$
20	19	ad3antrrr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to ⌊\frac{1}{A}⌋ + 1 \in ℕ$
21		simpr	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to B \in ℕ$
22	21	ad3antrrr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to B \in ℕ$
23	20 22	ifcld	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \in ℕ$
24	23	nnrecred	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)} \in ℝ$
25		0red	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to 0 \in ℝ$
26	9 25	resubcld	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A a - 0 \in ℝ$
27		simpr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}$
28	20	nnrecred	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{⌊\frac{1}{A}⌋ + 1} \in ℝ$
29	22	nnred	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to B \in ℝ$
30	6	rprecred	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{A} \in ℝ$
31	30	flcld	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to ⌊\frac{1}{A}⌋ \in ℤ$
32	31	zred	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to ⌊\frac{1}{A}⌋ \in ℝ$
33		peano2re	$⊢ ⌊\frac{1}{A}⌋ \in ℝ \to ⌊\frac{1}{A}⌋ + 1 \in ℝ$
34	32 33	syl	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to ⌊\frac{1}{A}⌋ + 1 \in ℝ$
35		max2	$⊢ (B \in ℝ \land ⌊\frac{1}{A}⌋ + 1 \in ℝ) \to ⌊\frac{1}{A}⌋ + 1 \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)$
36	29 34 35	syl2anc	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to ⌊\frac{1}{A}⌋ + 1 \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)$
37	20	nngt0d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to 0 < ⌊\frac{1}{A}⌋ + 1$
38	23	nnred	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \in ℝ$
39	23	nngt0d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to 0 < if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)$
40		lerec	$⊢ ((⌊\frac{1}{A}⌋ + 1 \in ℝ \land 0 < ⌊\frac{1}{A}⌋ + 1) \land (if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \in ℝ \land 0 < if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \to (⌊\frac{1}{A}⌋ + 1 \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \leftrightarrow \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)} \leq \frac{1}{⌊\frac{1}{A}⌋ + 1})$
41	34 37 38 39 40	syl22anc	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to (⌊\frac{1}{A}⌋ + 1 \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \leftrightarrow \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)} \leq \frac{1}{⌊\frac{1}{A}⌋ + 1})$
42	36 41	mpbid	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)} \leq \frac{1}{⌊\frac{1}{A}⌋ + 1}$
43		fllep1	$⊢ \frac{1}{A} \in ℝ \to \frac{1}{A} \leq ⌊\frac{1}{A}⌋ + 1$
44	30 43	syl	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{A} \leq ⌊\frac{1}{A}⌋ + 1$
45	20	nncnd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to ⌊\frac{1}{A}⌋ + 1 \in ℂ$
46	20	nnne0d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to ⌊\frac{1}{A}⌋ + 1 \neq 0$
47	45 46	recrecd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{\frac{1}{⌊\frac{1}{A}⌋ + 1}} = ⌊\frac{1}{A}⌋ + 1$
48	44 47	breqtrrd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{A} \leq \frac{1}{\frac{1}{⌊\frac{1}{A}⌋ + 1}}$
49	34 37	recgt0d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to 0 < \frac{1}{⌊\frac{1}{A}⌋ + 1}$
50	6	rpgt0d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to 0 < A$
51		lerec	$⊢ ((\frac{1}{⌊\frac{1}{A}⌋ + 1} \in ℝ \land 0 < \frac{1}{⌊\frac{1}{A}⌋ + 1}) \land (A \in ℝ \land 0 < A)) \to (\frac{1}{⌊\frac{1}{A}⌋ + 1} \leq A \leftrightarrow \frac{1}{A} \leq \frac{1}{\frac{1}{⌊\frac{1}{A}⌋ + 1}})$
52	28 49 7 50 51	syl22anc	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to (\frac{1}{⌊\frac{1}{A}⌋ + 1} \leq A \leftrightarrow \frac{1}{A} \leq \frac{1}{\frac{1}{⌊\frac{1}{A}⌋ + 1}})$
53	48 52	mpbird	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{⌊\frac{1}{A}⌋ + 1} \leq A$
54	24 28 7 42 53	letrd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)} \leq A$
55	7	recnd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A \in ℂ$
56	55	mulridd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A \cdot 1 = A$
57	2	nnge1d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to 1 \leq a$
58		1red	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to 1 \in ℝ$
59	58 8 6	lemul2d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to (1 \leq a \leftrightarrow A \cdot 1 \leq A a)$
60	57 59	mpbid	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A \cdot 1 \leq A a$
61	56 60	eqbrtrrd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A \leq A a$
62	9	recnd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A a \in ℂ$
63	62	subid1d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A a - 0 = A a$
64	61 63	breqtrrd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A \leq A a - 0$
65	24 7 26 54 64	letrd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)} \leq A a - 0$
66	14 24 26 27 65	ltletrd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \|A a - b\| < A a - 0$
67	12 26	absltd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to (\|A a - b\| < A a - 0 \leftrightarrow (- (A a - 0) < A a - b \land A a - b < A a - 0))$
68	66 67	mpbid	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to (- (A a - 0) < A a - b \land A a - b < A a - 0)$
69	68	simprd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to A a - b < A a - 0$
70	25 11 9	ltsub2d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to (0 < b \leftrightarrow A a - b < A a - 0)$
71	69 70	mpbird	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to 0 < b$
72		elnnz	$⊢ b \in ℕ \leftrightarrow (b \in ℤ \land 0 < b)$
73	4 71 72	sylanbrc	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to b \in ℕ$
74	22 2	ifcld	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to if (a \leq B, B, a) \in ℕ$
75	74	nnrecred	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{if (a \leq B, B, a)} \in ℝ$
76		elfzle2	$⊢ a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)) \to a \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)$
77	76	ad3antlr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to a \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)$
78		max1	$⊢ (B \in ℝ \land ⌊\frac{1}{A}⌋ + 1 \in ℝ) \to B \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)$
79	29 34 78	syl2anc	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to B \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)$
80		maxle	$⊢ (a \in ℝ \land B \in ℝ \land if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \in ℝ) \to (if (a \leq B, B, a) \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \leftrightarrow (a \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \land B \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)))$
81	8 29 38 80	syl3anc	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to (if (a \leq B, B, a) \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \leftrightarrow (a \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \land B \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)))$
82	77 79 81	mpbir2and	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to if (a \leq B, B, a) \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)$
83	29 8	ifcld	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to if (a \leq B, B, a) \in ℝ$
84	22	nngt0d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to 0 < B$
85		max2	$⊢ (a \in ℝ \land B \in ℝ) \to B \leq if (a \leq B, B, a)$
86	8 29 85	syl2anc	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to B \leq if (a \leq B, B, a)$
87	25 29 83 84 86	ltletrd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to 0 < if (a \leq B, B, a)$
88		lerec	$⊢ ((if (a \leq B, B, a) \in ℝ \land 0 < if (a \leq B, B, a)) \land (if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \in ℝ \land 0 < if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \to (if (a \leq B, B, a) \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \leftrightarrow \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)} \leq \frac{1}{if (a \leq B, B, a)})$
89	83 87 38 39 88	syl22anc	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to (if (a \leq B, B, a) \leq if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \leftrightarrow \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)} \leq \frac{1}{if (a \leq B, B, a)})$
90	82 89	mpbid	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)} \leq \frac{1}{if (a \leq B, B, a)}$
91	14 24 75 27 90	ltletrd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \|A a - b\| < \frac{1}{if (a \leq B, B, a)}$
92		oveq2	$⊢ x = a \to A x = A a$
93	92	fvoveq1d	$⊢ x = a \to \|A x - y\| = \|A a - y\|$
94		breq1	$⊢ x = a \to (x \leq B \leftrightarrow a \leq B)$
95		id	$⊢ x = a \to x = a$
96	94 95	ifbieq2d	$⊢ x = a \to if (x \leq B, B, x) = if (a \leq B, B, a)$
97	96	oveq2d	$⊢ x = a \to \frac{1}{if (x \leq B, B, x)} = \frac{1}{if (a \leq B, B, a)}$
98	93 97	breq12d	$⊢ x = a \to (\|A x - y\| < \frac{1}{if (x \leq B, B, x)} \leftrightarrow \|A a - y\| < \frac{1}{if (a \leq B, B, a)})$
99		oveq2	$⊢ y = b \to A a - y = A a - b$
100	99	fveq2d	$⊢ y = b \to \|A a - y\| = \|A a - b\|$
101	100	breq1d	$⊢ y = b \to (\|A a - y\| < \frac{1}{if (a \leq B, B, a)} \leftrightarrow \|A a - b\| < \frac{1}{if (a \leq B, B, a)})$
102	98 101	rspc2ev	$⊢ (a \in ℕ \land b \in ℕ \land \|A a - b\| < \frac{1}{if (a \leq B, B, a)}) \to \exists x \in ℕ \exists y \in ℕ \|A x - y\| < \frac{1}{if (x \leq B, B, x)}$
103	2 73 91 102	syl3anc	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B))) \land b \in ℕ_{0}) \land \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}) \to \exists x \in ℕ \exists y \in ℕ \|A x - y\| < \frac{1}{if (x \leq B, B, x)}$
104	19 21	ifcld	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \in ℕ$
105		irrapxlem3	$⊢ (A \in ℝ^{+} \land if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B) \in ℕ) \to \exists a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)) \exists b \in ℕ_{0} \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}$
106	5 104 105	syl2anc	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to \exists a \in (1 \dots if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)) \exists b \in ℕ_{0} \|A a - b\| < \frac{1}{if (B \leq ⌊\frac{1}{A}⌋ + 1, ⌊\frac{1}{A}⌋ + 1, B)}$
107	103 106	r19.29vva	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to \exists x \in ℕ \exists y \in ℕ \|A x - y\| < \frac{1}{if (x \leq B, B, x)}$

Metamath Proof Explorer

Theorem irrapxlem4

Proof