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		1z	$⊢ 1 \in ℤ$
3	2	a1i	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 1 \in ℤ$
4		simpllr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to B \in ℕ$
5	4	nnzd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to B \in ℤ$
6		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)$
7	6	elfzelzd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b \in ℤ$
8		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)$
9	8	elfzelzd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to a \in ℤ$
10	7 9	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 ℤ$
11		1m1e0	$⊢ 1 - 1 = 0$
12		elfzelz	$⊢ a \in (0 \dots B) \to a \in ℤ$
13	12	ad2antrl	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \to a \in ℤ$
14	13	zred	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \to a \in ℝ$
15		elfzelz	$⊢ b \in (0 \dots B) \to b \in ℤ$
16	15	ad2antll	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \to b \in ℤ$
17	16	zred	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \to b \in ℝ$
18	14 17	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)$
19	18	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$
20	11 19	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$
21		zlem1lt	$⊢ (1 \in ℤ \land b - a \in ℤ) \to (1 \leq b - a \leftrightarrow 1 - 1 < b - a)$
22	2 10 21	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)$
23	20 22	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$
24	7	zred	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b \in ℝ$
25	9	zred	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to a \in ℝ$
26	24 25	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 ℝ$
27		0red	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 0 \in ℝ$
28	24 27	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 ℝ$
29	4	nnred	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to B \in ℝ$
30		elfzle1	$⊢ a \in (0 \dots B) \to 0 \leq a$
31	8 30	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$
32	27 25 24 31	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$
33	24	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to b \in ℂ$
34	33	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$
35		elfzle2	$⊢ b \in (0 \dots B) \to b \leq B$
36	6 35	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$
37	34 36	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$
38	26 28 29 32 37	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$
39	3 5 10 23 38	elfzd	$⊢ (((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)$
40	39	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)$
41		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
42	41	ad3antrrr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A \in ℝ$
43	42 25	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 ℝ$
44	42 24	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 ℝ$
45		simpr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to a < b$
46	25 24 45	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$
47		rpgt0	$⊢ A \in ℝ^{+} \to 0 < A$
48	47	ad3antrrr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 0 < A$
49		lemul2	$⊢ (a \in ℝ \land b \in ℝ \land (A \in ℝ \land 0 < A)) \to (a \leq b \leftrightarrow A a \leq A b)$
50	25 24 42 48 49	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)$
51	46 50	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$
52		flword2	$⊢ (A a \in ℝ \land A b \in ℝ \land A a \leq A b) \to ⌊A b⌋ \in ℤ_{\geq ⌊A a⌋}$
53	43 44 51 52	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⌋}$
54		uznn0sub	$⊢ ⌊A b⌋ \in ℤ_{\geq ⌊A a⌋} \to ⌊A b⌋ - ⌊A a⌋ \in ℕ_{0}$
55	53 54	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}$
56	55	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}$
57	42	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to A \in ℂ$
58	25	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to a \in ℂ$
59	57 33 58	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$
60	59	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⌋)$
61	44	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 ℂ$
62	43	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 ℂ$
63	44	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 ℤ$
64	63	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 ℂ$
65	43	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 ℤ$
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 a⌋ \in ℂ$
67	61 62 64 66	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⌋)$
68		modfrac	$⊢ A b \in ℝ \to A b \mod 1 = A b - ⌊A b⌋$
69	44 68	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⌋$
70	69	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$
71		modfrac	$⊢ A a \in ℝ \to A a \mod 1 = A a - ⌊A a⌋$
72	43 71	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⌋$
73	72	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$
74	70 73	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)$
75	60 67 74	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)$
76	75	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)\|$
77		1rp	$⊢ 1 \in ℝ^{+}$
78	77	a1i	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land (a \in (0 \dots B) \land b \in (0 \dots B))) \land a < b) \to 1 \in ℝ^{+}$
79	44 78	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 ℝ$
80	79	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 ℂ$
81	43 78	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 ℝ$
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 a \mod 1 \in ℂ$
83	80 82	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)\|$
84	76 83	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⌋)\|$
85	84	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})$
86	85	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})$
87	86	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}$
88		oveq2	$⊢ x = b - a \to A x = A (b - a)$
89	88	fvoveq1d	$⊢ x = b - a \to \|A x - y\| = \|A (b - a) - y\|$
90	89	breq1d	$⊢ x = b - a \to (\|A x - y\| < \frac{1}{B} \leftrightarrow \|A (b - a) - y\| < \frac{1}{B})$
91		oveq2	$⊢ y = ⌊A b⌋ - ⌊A a⌋ \to A (b - a) - y = A (b - a) - (⌊A b⌋ - ⌊A a⌋)$
92	91	fveq2d	$⊢ y = ⌊A b⌋ - ⌊A a⌋ \to \|A (b - a) - y\| = \|A (b - a) - (⌊A b⌋ - ⌊A a⌋)\|$
93	92	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})$
94	90 93	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}$
95	40 56 87 94	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}$
96	95	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})$
97	96	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})$
98	1 97	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