irrapxlem1

Description: Lemma for irrapx1 . Divides the unit interval into B half-open sections and using the pigeonhole principle fphpdo finds two multiples of A in the same section mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014)

		Ref	Expression
	Assertion	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)⌋)$

Proof

Step	Hyp	Ref	Expression
1		fzssuz	$⊢ (0 \dots B) \subseteq ℤ_{\geq 0}$
2		uzssz	$⊢ ℤ_{\geq 0} \subseteq ℤ$
3		zssre	$⊢ ℤ \subseteq ℝ$
4	2 3	sstri	$⊢ ℤ_{\geq 0} \subseteq ℝ$
5	1 4	sstri	$⊢ (0 \dots B) \subseteq ℝ$
6	5	a1i	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to (0 \dots B) \subseteq ℝ$
7		ovexd	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to (0 \dots B - 1) \in V$
8		nnm1nn0	$⊢ B \in ℕ \to B - 1 \in ℕ_{0}$
9	8	adantl	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to B - 1 \in ℕ_{0}$
10		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
11	9 10	eleqtrdi	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to B - 1 \in ℤ_{\geq 0}$
12		nnz	$⊢ B \in ℕ \to B \in ℤ$
13	12	adantl	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to B \in ℤ$
14		nnre	$⊢ B \in ℕ \to B \in ℝ$
15	14	adantl	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to B \in ℝ$
16	15	ltm1d	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to B - 1 < B$
17		fzsdom2	$⊢ ((B - 1 \in ℤ_{\geq 0} \land B \in ℤ) \land B - 1 < B) \to (0 \dots B - 1) ≺ (0 \dots B)$
18	11 13 16 17	syl21anc	$⊢ (A \in ℝ^{+} \land B \in ℕ) \to (0 \dots B - 1) ≺ (0 \dots B)$
19	14	ad2antlr	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B \in ℝ$
20		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
21	20	ad2antrr	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to A \in ℝ$
22		elfzelz	$⊢ a \in (0 \dots B) \to a \in ℤ$
23	22	zred	$⊢ a \in (0 \dots B) \to a \in ℝ$
24	23	adantl	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to a \in ℝ$
25	21 24	remulcld	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to A a \in ℝ$
26		1rp	$⊢ 1 \in ℝ^{+}$
27		modcl	$⊢ (A a \in ℝ \land 1 \in ℝ^{+}) \to A a \mod 1 \in ℝ$
28	25 26 27	sylancl	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to A a \mod 1 \in ℝ$
29	19 28	remulcld	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B (A a \mod 1) \in ℝ$
30	29	flcld	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to ⌊B (A a \mod 1)⌋ \in ℤ$
31	19	recnd	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B \in ℂ$
32	31	mul01d	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B \cdot 0 = 0$
33		modge0	$⊢ (A a \in ℝ \land 1 \in ℝ^{+}) \to 0 \leq A a \mod 1$
34	25 26 33	sylancl	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to 0 \leq A a \mod 1$
35		0red	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to 0 \in ℝ$
36		nngt0	$⊢ B \in ℕ \to 0 < B$
37	36	ad2antlr	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to 0 < B$
38		lemul2	$⊢ (0 \in ℝ \land A a \mod 1 \in ℝ \land (B \in ℝ \land 0 < B)) \to (0 \leq A a \mod 1 \leftrightarrow B \cdot 0 \leq B (A a \mod 1))$
39	35 28 19 37 38	syl112anc	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to (0 \leq A a \mod 1 \leftrightarrow B \cdot 0 \leq B (A a \mod 1))$
40	34 39	mpbid	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B \cdot 0 \leq B (A a \mod 1)$
41	32 40	eqbrtrrd	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to 0 \leq B (A a \mod 1)$
42	35 29	lenltd	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to (0 \leq B (A a \mod 1) \leftrightarrow \neg B (A a \mod 1) < 0)$
43	41 42	mpbid	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to \neg B (A a \mod 1) < 0$
44		0z	$⊢ 0 \in ℤ$
45		fllt	$⊢ (B (A a \mod 1) \in ℝ \land 0 \in ℤ) \to (B (A a \mod 1) < 0 \leftrightarrow ⌊B (A a \mod 1)⌋ < 0)$
46	29 44 45	sylancl	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to (B (A a \mod 1) < 0 \leftrightarrow ⌊B (A a \mod 1)⌋ < 0)$
47	43 46	mtbid	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to \neg ⌊B (A a \mod 1)⌋ < 0$
48	30	zred	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to ⌊B (A a \mod 1)⌋ \in ℝ$
49	35 48	lenltd	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to (0 \leq ⌊B (A a \mod 1)⌋ \leftrightarrow \neg ⌊B (A a \mod 1)⌋ < 0)$
50	47 49	mpbird	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to 0 \leq ⌊B (A a \mod 1)⌋$
51		elnn0z	$⊢ ⌊B (A a \mod 1)⌋ \in ℕ_{0} \leftrightarrow (⌊B (A a \mod 1)⌋ \in ℤ \land 0 \leq ⌊B (A a \mod 1)⌋)$
52	30 50 51	sylanbrc	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to ⌊B (A a \mod 1)⌋ \in ℕ_{0}$
53	8	ad2antlr	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B - 1 \in ℕ_{0}$
54		flle	$⊢ B (A a \mod 1) \in ℝ \to ⌊B (A a \mod 1)⌋ \leq B (A a \mod 1)$
55	29 54	syl	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to ⌊B (A a \mod 1)⌋ \leq B (A a \mod 1)$
56		modlt	$⊢ (A a \in ℝ \land 1 \in ℝ^{+}) \to A a \mod 1 < 1$
57	25 26 56	sylancl	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to A a \mod 1 < 1$
58		1red	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to 1 \in ℝ$
59		ltmul2	$⊢ (A a \mod 1 \in ℝ \land 1 \in ℝ \land (B \in ℝ \land 0 < B)) \to (A a \mod 1 < 1 \leftrightarrow B (A a \mod 1) < B \cdot 1)$
60	28 58 19 37 59	syl112anc	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to (A a \mod 1 < 1 \leftrightarrow B (A a \mod 1) < B \cdot 1)$
61	57 60	mpbid	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B (A a \mod 1) < B \cdot 1$
62	31	mulid1d	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B \cdot 1 = B$
63	61 62	breqtrd	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B (A a \mod 1) < B$
64	48 29 19 55 63	lelttrd	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to ⌊B (A a \mod 1)⌋ < B$
65		nncn	$⊢ B \in ℕ \to B \in ℂ$
66		ax-1cn	$⊢ 1 \in ℂ$
67		npcan	$⊢ (B \in ℂ \land 1 \in ℂ) \to B - 1 + 1 = B$
68	65 66 67	sylancl	$⊢ B \in ℕ \to B - 1 + 1 = B$
69	68	ad2antlr	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B - 1 + 1 = B$
70	64 69	breqtrrd	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to ⌊B (A a \mod 1)⌋ < B - 1 + 1$
71	12	ad2antlr	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B \in ℤ$
72		1z	$⊢ 1 \in ℤ$
73		zsubcl	$⊢ (B \in ℤ \land 1 \in ℤ) \to B - 1 \in ℤ$
74	71 72 73	sylancl	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to B - 1 \in ℤ$
75		zleltp1	$⊢ (⌊B (A a \mod 1)⌋ \in ℤ \land B - 1 \in ℤ) \to (⌊B (A a \mod 1)⌋ \leq B - 1 \leftrightarrow ⌊B (A a \mod 1)⌋ < B - 1 + 1)$
76	30 74 75	syl2anc	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to (⌊B (A a \mod 1)⌋ \leq B - 1 \leftrightarrow ⌊B (A a \mod 1)⌋ < B - 1 + 1)$
77	70 76	mpbird	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to ⌊B (A a \mod 1)⌋ \leq B - 1$
78		elfz2nn0	$⊢ ⌊B (A a \mod 1)⌋ \in (0 \dots B - 1) \leftrightarrow (⌊B (A a \mod 1)⌋ \in ℕ_{0} \land B - 1 \in ℕ_{0} \land ⌊B (A a \mod 1)⌋ \leq B - 1)$
79	52 53 77 78	syl3anbrc	$⊢ ((A \in ℝ^{+} \land B \in ℕ) \land a \in (0 \dots B)) \to ⌊B (A a \mod 1)⌋ \in (0 \dots B - 1)$
80		oveq2	$⊢ a = x \to A a = A x$
81	80	oveq1d	$⊢ a = x \to A a \mod 1 = A x \mod 1$
82	81	oveq2d	$⊢ a = x \to B (A a \mod 1) = B (A x \mod 1)$
83	82	fveq2d	$⊢ a = x \to ⌊B (A a \mod 1)⌋ = ⌊B (A x \mod 1)⌋$
84		oveq2	$⊢ a = y \to A a = A y$
85	84	oveq1d	$⊢ a = y \to A a \mod 1 = A y \mod 1$
86	85	oveq2d	$⊢ a = y \to B (A a \mod 1) = B (A y \mod 1)$
87	86	fveq2d	$⊢ a = y \to ⌊B (A a \mod 1)⌋ = ⌊B (A y \mod 1)⌋$
88	6 7 18 79 83 87	fphpdo	$⊢ (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)⌋)$

Metamath Proof Explorer

Theorem irrapxlem1

Proof