irrapxlem2

Description: Lemma for irrapx1 . Two multiples in the same bucket means they are very close mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		irrapxlem1	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to \exists x \in (0 \dots B) \exists y \in (0 \dots B) (x < y \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋)$
2		nnre	$⊢ B \in ℕ \to B \in ℝ$
3	2	ad3antlr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B \in ℝ$
4		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
5	4	ad3antrrr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to A \in ℝ$
6		elfzelz	$⊢ x \in (0 \dots B) \to x \in ℤ$
7	6	zred	$⊢ x \in (0 \dots B) \to x \in ℝ$
8	7	ad2antlr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to x \in ℝ$
9	5 8	remulcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to A x \in ℝ$
10		1rp	$⊢ 1 \in ℝ^{+}$
11	10	a1i	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to 1 \in ℝ^{+}$
12	9 11	modcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to A x \mod 1 \in ℝ$
13	3 12	remulcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A x \mod 1) \in ℝ$
14		intfrac	$⊢ B (A x \mod 1) \in ℝ \to B (A x \mod 1) = ⌊B (A x \mod 1)⌋ + (B (A x \mod 1) \mod 1)$
15	13 14	syl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A x \mod 1) = ⌊B (A x \mod 1)⌋ + (B (A x \mod 1) \mod 1)$
16		elfzelz	$⊢ y \in (0 \dots B) \to y \in ℤ$
17	16	zred	$⊢ y \in (0 \dots B) \to y \in ℝ$
18	17	adantl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to y \in ℝ$
19	5 18	remulcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to A y \in ℝ$
20	19 11	modcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to A y \mod 1 \in ℝ$
21	3 20	remulcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A y \mod 1) \in ℝ$
22		intfrac	$⊢ B (A y \mod 1) \in ℝ \to B (A y \mod 1) = ⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1)$
23	21 22	syl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A y \mod 1) = ⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1)$
24	15 23	oveq12d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A x \mod 1) - B (A y \mod 1) = ⌊B (A x \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1))$
25	24	fveq2d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to \|B (A x \mod 1) - B (A y \mod 1)\| = \|⌊B (A x \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1))\|$
26	25	adantr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to \|B (A x \mod 1) - B (A y \mod 1)\| = \|⌊B (A x \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1))\|$
27		simpr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋$
28	27	oveq1d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to ⌊B (A x \mod 1)⌋ + (B (A x \mod 1) \mod 1) = ⌊B (A y \mod 1)⌋ + (B (A x \mod 1) \mod 1)$
29	28	oveq1d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to ⌊B (A x \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1)) = ⌊B (A y \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1))$
30	29	fveq2d	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to \|⌊B (A x \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1))\| = \|⌊B (A y \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1))\|$
31	21	flcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to ⌊B (A y \mod 1)⌋ \in ℤ$
32	31	zcnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to ⌊B (A y \mod 1)⌋ \in ℂ$
33	13 11	modcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A x \mod 1) \mod 1 \in ℝ$
34	33	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A x \mod 1) \mod 1 \in ℂ$
35	21 11	modcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A y \mod 1) \mod 1 \in ℝ$
36	35	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A y \mod 1) \mod 1 \in ℂ$
37	32 34 36	pnpcand	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to ⌊B (A y \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1)) = (B (A x \mod 1) \mod 1) - (B (A y \mod 1) \mod 1)$
38	37	fveq2d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to \|⌊B (A y \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1))\| = \|(B (A x \mod 1) \mod 1) - (B (A y \mod 1) \mod 1)\|$
39		0red	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to 0 \in ℝ$
40		1red	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to 1 \in ℝ$
41		modelico	$⊢ (B (A x \mod 1) \in ℝ \land 1 \in ℝ^{+}) \to B (A x \mod 1) \mod 1 \in [0, 1)$
42	13 10 41	sylancl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A x \mod 1) \mod 1 \in [0, 1)$
43		modelico	$⊢ (B (A y \mod 1) \in ℝ \land 1 \in ℝ^{+}) \to B (A y \mod 1) \mod 1 \in [0, 1)$
44	21 10 43	sylancl	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (A y \mod 1) \mod 1 \in [0, 1)$
45		icodiamlt	$⊢ ((0 \in ℝ \land 1 \in ℝ) \land (B (A x \mod 1) \mod 1 \in [0, 1) \land B (A y \mod 1) \mod 1 \in [0, 1))) \to \|(B (A x \mod 1) \mod 1) - (B (A y \mod 1) \mod 1)\| < 1 - 0$
46	39 40 42 44 45	syl22anc	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to \|(B (A x \mod 1) \mod 1) - (B (A y \mod 1) \mod 1)\| < 1 - 0$
47		1m0e1	$⊢ 1 - 0 = 1$
48	46 47	breqtrdi	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to \|(B (A x \mod 1) \mod 1) - (B (A y \mod 1) \mod 1)\| < 1$
49	38 48	eqbrtrd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to \|⌊B (A y \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1))\| < 1$
50	49	adantr	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to \|⌊B (A y \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1))\| < 1$
51	30 50	eqbrtrd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to \|⌊B (A x \mod 1)⌋ + (B (A x \mod 1) \mod 1) - (⌊B (A y \mod 1)⌋ + (B (A y \mod 1) \mod 1))\| < 1$
52	26 51	eqbrtrd	$⊢ ((((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to \|B (A x \mod 1) - B (A y \mod 1)\| < 1$
53	52	ex	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to (⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋ \to \|B (A x \mod 1) - B (A y \mod 1)\| < 1)$
54	12 20	resubcld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to (A x \mod 1) - (A y \mod 1) \in ℝ$
55	54	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to (A x \mod 1) - (A y \mod 1) \in ℂ$
56	55	abscld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to \|(A x \mod 1) - (A y \mod 1)\| \in ℝ$
57		nngt0	$⊢ B \in ℕ \to 0 < B$
58	57	ad3antlr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to 0 < B$
59	58	gt0ne0d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B \neq 0$
60	3 59	rereccld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to \frac{1}{B} \in ℝ$
61		ltmul2	$⊢ (\|(A x \mod 1) - (A y \mod 1)\| \in ℝ \land \frac{1}{B} \in ℝ \land (B \in ℝ \land 0 < B)) \to (\|(A x \mod 1) - (A y \mod 1)\| < \frac{1}{B} \leftrightarrow B \|(A x \mod 1) - (A y \mod 1)\| < B (\frac{1}{B}))$
62	56 60 3 58 61	syl112anc	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to (\|(A x \mod 1) - (A y \mod 1)\| < \frac{1}{B} \leftrightarrow B \|(A x \mod 1) - (A y \mod 1)\| < B (\frac{1}{B}))$
63		nnnn0	$⊢ B \in ℕ \to B \in ℕ_{0}$
64	63	nn0ge0d	$⊢ B \in ℕ \to 0 \leq B$
65	64	ad3antlr	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to 0 \leq B$
66	3 65	absidd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to \|B\| = B$
67	66	eqcomd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B = \|B\|$
68	67	oveq1d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B \|(A x \mod 1) - (A y \mod 1)\| = \|B\| \|(A x \mod 1) - (A y \mod 1)\|$
69	3	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B \in ℂ$
70	69 55	absmuld	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to \|B ((A x \mod 1) - (A y \mod 1))\| = \|B\| \|(A x \mod 1) - (A y \mod 1)\|$
71	12	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to A x \mod 1 \in ℂ$
72	20	recnd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to A y \mod 1 \in ℂ$
73	69 71 72	subdid	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B ((A x \mod 1) - (A y \mod 1)) = B (A x \mod 1) - B (A y \mod 1)$
74	73	fveq2d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to \|B ((A x \mod 1) - (A y \mod 1))\| = \|B (A x \mod 1) - B (A y \mod 1)\|$
75	68 70 74	3eqtr2d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B \|(A x \mod 1) - (A y \mod 1)\| = \|B (A x \mod 1) - B (A y \mod 1)\|$
76	69 59	recidd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to B (\frac{1}{B}) = 1$
77	75 76	breq12d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to (B \|(A x \mod 1) - (A y \mod 1)\| < B (\frac{1}{B}) \leftrightarrow \|B (A x \mod 1) - B (A y \mod 1)\| < 1)$
78	62 77	bitrd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to (\|(A x \mod 1) - (A y \mod 1)\| < \frac{1}{B} \leftrightarrow \|B (A x \mod 1) - B (A y \mod 1)\| < 1)$
79	53 78	sylibrd	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to (⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋ \to \|(A x \mod 1) - (A y \mod 1)\| < \frac{1}{B})$
80	79	anim2d	$⊢ (((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \land y \in (0 \dots B)) \to ((x < y \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to (x < y \land \|(A x \mod 1) - (A y \mod 1)\| < \frac{1}{B}))$
81	80	reximdva	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land x \in (0 \dots B)) \to (\exists y \in (0 \dots B) (x < y \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to \exists y \in (0 \dots B) (x < y \land \|(A x \mod 1) - (A y \mod 1)\| < \frac{1}{B}))$
82	81	reximdva	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to (\exists x \in (0 \dots B) \exists y \in (0 \dots B) (x < y \land ⌊B (A x \mod 1)⌋ = ⌊B (A y \mod 1)⌋) \to \exists x \in (0 \dots B) \exists y \in (0 \dots B) (x < y \land \|(A x \mod 1) - (A y \mod 1)\| < \frac{1}{B}))$
83	1 82	mpd	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to \exists x \in (0 \dots B) \exists y \in (0 \dots B) (x < y \land \|(A x \mod 1) - (A y \mod 1)\| < \frac{1}{B})$

Metamath Proof Explorer

Theorem irrapxlem2

Proof