irrapxlem3

Description: Lemma for irrapx1 . By subtraction, there is a multiple very close to an integer. (Contributed by Stefan O'Rear, 13-Sep-2014)

		Ref	Expression
	Assertion	irrapxlem3	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to \exists x \in (1 \dots B) \exists y \in ℕ_{0} \|A x - y\| < \frac{1}{B}$

Proof

Step	Hyp	Ref	Expression
1		irrapxlem2	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to \exists a \in (0 \dots B) \exists b \in (0 \dots B) (a < b \land \|(A a \mod 1) - (A b \mod 1)\| < \frac{1}{B})$
2		1m1e0	$⊢ 1 - 1 = 0$
3		elfzelz	$⊢ a \in (0 \dots B) \to a \in ℤ$
4	3	ad2antrl	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \to a \in ℤ$
5	4	zred	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \to a \in ℝ$
6		elfzelz	$⊢ b \in (0 \dots B) \to b \in ℤ$
7	6	ad2antll	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \to b \in ℤ$
8	7	zred	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \to b \in ℝ$
9	5 8	posdifd	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \to (a < b \leftrightarrow 0 < b - a)$
10	9	biimpa	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 0 < b - a$
11	2 10	eqbrtrid	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 1 - 1 < b - a$
12		1z	$⊢ 1 \in ℤ$
13		simplrr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b \in (0 \dots B)$
14	13 6	syl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b \in ℤ$
15		simplrl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to a \in (0 \dots B)$
16	15 3	syl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to a \in ℤ$
17	14 16	zsubcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b - a \in ℤ$
18		zlem1lt	$⊢ (1 \in ℤ \land b - a \in ℤ) \to (1 \leq b - a \leftrightarrow 1 - 1 < b - a)$
19	12 17 18	sylancr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to (1 \leq b - a \leftrightarrow 1 - 1 < b - a)$
20	11 19	mpbird	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 1 \leq b - a$
21	14	zred	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b \in ℝ$
22	16	zred	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to a \in ℝ$
23	21 22	resubcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b - a \in ℝ$
24		0red	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 0 \in ℝ$
25	21 24	resubcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b - 0 \in ℝ$
26		simpllr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to B \in ℕ$
27	26	nnred	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to B \in ℝ$
28		elfzle1	$⊢ a \in (0 \dots B) \to 0 \leq a$
29	15 28	syl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 0 \leq a$
30	24 22 21 29	lesub2dd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b - a \leq b - 0$
31	21	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b \in ℂ$
32	31	subid1d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b - 0 = b$
33		elfzle2	$⊢ b \in (0 \dots B) \to b \leq B$
34	13 33	syl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b \leq B$
35	32 34	eqbrtrd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b - 0 \leq B$
36	23 25 27 30 35	letrd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b - a \leq B$
37	12	a1i	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 1 \in ℤ$
38	26	nnzd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to B \in ℤ$
39		elfz	$⊢ (b - a \in ℤ \land 1 \in ℤ \land B \in ℤ) \to (b - a \in (1 \dots B) \leftrightarrow (1 \leq b - a \land b - a \leq B))$
40	17 37 38 39	syl3anc	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to (b - a \in (1 \dots B) \leftrightarrow (1 \leq b - a \land b - a \leq B))$
41	20 36 40	mpbir2and	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b - a \in (1 \dots B)$
42	41	adantrr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land (a < b \land \|(A a \mod 1) - (A b \mod 1)\| < \frac{1}{B})) \to b - a \in (1 \dots B)$
43		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
44	43	ad3antrrr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A \in ℝ$
45	44 22	remulcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A a \in ℝ$
46	44 21	remulcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A b \in ℝ$
47		simpr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to a < b$
48	22 21 47	ltled	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to a \leq b$
49		rpgt0	$⊢ A \in ℝ^{+} \to 0 < A$
50	49	ad3antrrr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 0 < A$
51		lemul2	$⊢ (a \in ℝ \land b \in ℝ \land (A \in ℝ \land 0 < A)) \to (a \leq b \leftrightarrow A a \leq A b)$
52	22 21 44 50 51	syl112anc	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to (a \leq b \leftrightarrow A a \leq A b)$
53	48 52	mpbid	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A a \leq A b$
54		flword2	$⊢ (A a \in ℝ \land A b \in ℝ \land A a \leq A b) \to ⌊A b⌋ \in ℤ_{\geq ⌊A a⌋}$
55	45 46 53 54	syl3anc	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to ⌊A b⌋ \in ℤ_{\geq ⌊A a⌋}$
56		uznn0sub	$⊢ ⌊A b⌋ \in ℤ_{\geq ⌊A a⌋} \to ⌊A b⌋ - ⌊A a⌋ \in ℕ_{0}$
57	55 56	syl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to ⌊A b⌋ - ⌊A a⌋ \in ℕ_{0}$
58	57	adantrr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land (a < b \land \|(A a \mod 1) - (A b \mod 1)\| < \frac{1}{B})) \to ⌊A b⌋ - ⌊A a⌋ \in ℕ_{0}$
59	44	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A \in ℂ$
60	22	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to a \in ℂ$
61	59 31 60	subdid	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A (b - a) = A b - A a$
62	61	oveq1d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A (b - a) - (⌊A b⌋ - ⌊A a⌋) = A b - A a - (⌊A b⌋ - ⌊A a⌋)$
63	46	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A b \in ℂ$
64	45	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A a \in ℂ$
65	46	flcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to ⌊A b⌋ \in ℤ$
66	65	zcnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to ⌊A b⌋ \in ℂ$
67	45	flcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to ⌊A a⌋ \in ℤ$
68	67	zcnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to ⌊A a⌋ \in ℂ$
69	63 64 66 68	sub4d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A b - A a - (⌊A b⌋ - ⌊A a⌋) = A b - ⌊A b⌋ - (A a - ⌊A a⌋)$
70		modfrac	$⊢ A b \in ℝ \to A b \mod 1 = A b - ⌊A b⌋$
71	46 70	syl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A b \mod 1 = A b - ⌊A b⌋$
72	71	eqcomd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A b - ⌊A b⌋ = A b \mod 1$
73		modfrac	$⊢ A a \in ℝ \to A a \mod 1 = A a - ⌊A a⌋$
74	45 73	syl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A a \mod 1 = A a - ⌊A a⌋$
75	74	eqcomd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A a - ⌊A a⌋ = A a \mod 1$
76	72 75	oveq12d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A b - ⌊A b⌋ - (A a - ⌊A a⌋) = (A b \mod 1) - (A a \mod 1)$
77	62 69 76	3eqtrd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A (b - a) - (⌊A b⌋ - ⌊A a⌋) = (A b \mod 1) - (A a \mod 1)$
78	77	fveq2d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to \|A (b - a) - (⌊A b⌋ - ⌊A a⌋)\| = \|(A b \mod 1) - (A a \mod 1)\|$
79		1rp	$⊢ 1 \in ℝ^{+}$
80	79	a1i	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 1 \in ℝ^{+}$
81	46 80	modcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A b \mod 1 \in ℝ$
82	81	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A b \mod 1 \in ℂ$
83	45 80	modcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A a \mod 1 \in ℝ$
84	83	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A a \mod 1 \in ℂ$
85	82 84	abssubd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to \|(A b \mod 1) - (A a \mod 1)\| = \|(A a \mod 1) - (A b \mod 1)\|$
86	78 85	eqtr2d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to \|(A a \mod 1) - (A b \mod 1)\| = \|A (b - a) - (⌊A b⌋ - ⌊A a⌋)\|$
87	86	breq1d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to (\|(A a \mod 1) - (A b \mod 1)\| < \frac{1}{B} \leftrightarrow \|A (b - a) - (⌊A b⌋ - ⌊A a⌋)\| < \frac{1}{B})$
88	87	biimpd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to (\|(A a \mod 1) - (A b \mod 1)\| < \frac{1}{B} \to \|A (b - a) - (⌊A b⌋ - ⌊A a⌋)\| < \frac{1}{B})$
89	88	impr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land (a < b \land \|(A a \mod 1) - (A b \mod 1)\| < \frac{1}{B})) \to \|A (b - a) - (⌊A b⌋ - ⌊A a⌋)\| < \frac{1}{B}$
90		oveq2	$⊢ x = b - a \to A x = A (b - a)$
91	90	fvoveq1d	$⊢ x = b - a \to \|A x - y\| = \|A (b - a) - y\|$
92	91	breq1d	$⊢ x = b - a \to (\|A x - y\| < \frac{1}{B} \leftrightarrow \|A (b - a) - y\| < \frac{1}{B})$
93		oveq2	$⊢ y = ⌊A b⌋ - ⌊A a⌋ \to A (b - a) - y = A (b - a) - (⌊A b⌋ - ⌊A a⌋)$
94	93	fveq2d	$⊢ y = ⌊A b⌋ - ⌊A a⌋ \to \|A (b - a) - y\| = \|A (b - a) - (⌊A b⌋ - ⌊A a⌋)\|$
95	94	breq1d	$⊢ y = ⌊A b⌋ - ⌊A a⌋ \to (\|A (b - a) - y\| < \frac{1}{B} \leftrightarrow \|A (b - a) - (⌊A b⌋ - ⌊A a⌋)\| < \frac{1}{B})$
96	92 95	rspc2ev	$⊢ (b - a \in (1 \dots B) \land ⌊A b⌋ - ⌊A a⌋ \in ℕ_{0} \land \|A (b - a) - (⌊A b⌋ - ⌊A a⌋)\| < \frac{1}{B}) \to \exists x \in (1 \dots B) \exists y \in ℕ_{0} \|A x - y\| < \frac{1}{B}$
97	42 58 89 96	syl3anc	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land (a < b \land \|(A a \mod 1) - (A b \mod 1)\| < \frac{1}{B})) \to \exists x \in (1 \dots B) \exists y \in ℕ_{0} \|A x - y\| < \frac{1}{B}$
98	97	ex	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \to ((a < b \land \|(A a \mod 1) - (A b \mod 1)\| < \frac{1}{B}) \to \exists x \in (1 \dots B) \exists y \in ℕ_{0} \|A x - y\| < \frac{1}{B})$
99	98	rexlimdvva	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to (\exists a \in (0 \dots B) \exists b \in (0 \dots B) (a < b \land \|(A a \mod 1) - (A b \mod 1)\| < \frac{1}{B}) \to \exists x \in (1 \dots B) \exists y \in ℕ_{0} \|A x - y\| < \frac{1}{B})$
100	1 99	mpd	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to \exists x \in (1 \dots B) \exists y \in ℕ_{0} \|A x - y\| < \frac{1}{B}$

Metamath Proof Explorer

Theorem irrapxlem3

Proof