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	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ( 0 ... 𝐵 ) ∃ 𝑦 ∈ ( 0 ... 𝐵 ) ( 𝑥 < 𝑦 ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fzssuz	⊢ ( 0 ... 𝐵 ) ⊆ ( ℤ_≥ ‘ 0 )
2		uzssz	⊢ ( ℤ_≥ ‘ 0 ) ⊆ ℤ
3		zssre	⊢ ℤ ⊆ ℝ
4	2 3	sstri	⊢ ( ℤ_≥ ‘ 0 ) ⊆ ℝ
5	1 4	sstri	⊢ ( 0 ... 𝐵 ) ⊆ ℝ
6	5	a1i	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ( 0 ... 𝐵 ) ⊆ ℝ )
7		ovexd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ( 0 ... ( 𝐵 − 1 ) ) ∈ V )
8		nnm1nn0	⊢ ( 𝐵 ∈ ℕ → ( 𝐵 − 1 ) ∈ ℕ₀ )
9	8	adantl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 − 1 ) ∈ ℕ₀ )
10		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
11	9 10	eleqtrdi	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 − 1 ) ∈ ( ℤ_≥ ‘ 0 ) )
12		nnz	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
13	12	adantl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℤ )
14		nnre	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
15	14	adantl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℝ )
16	15	ltm1d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 − 1 ) < 𝐵 )
17		fzsdom2	⊢ ( ( ( ( 𝐵 − 1 ) ∈ ( ℤ_≥ ‘ 0 ) ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐵 − 1 ) < 𝐵 ) → ( 0 ... ( 𝐵 − 1 ) ) ≺ ( 0 ... 𝐵 ) )
18	11 13 16 17	syl21anc	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ( 0 ... ( 𝐵 − 1 ) ) ≺ ( 0 ... 𝐵 ) )
19	14	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 𝐵 ∈ ℝ )
20		rpre	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ )
21	20	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 𝐴 ∈ ℝ )
22		elfzelz	⊢ ( 𝑎 ∈ ( 0 ... 𝐵 ) → 𝑎 ∈ ℤ )
23	22	zred	⊢ ( 𝑎 ∈ ( 0 ... 𝐵 ) → 𝑎 ∈ ℝ )
24	23	adantl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 𝑎 ∈ ℝ )
25	21 24	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 𝐴 · 𝑎 ) ∈ ℝ )
26		1rp	⊢ 1 ∈ ℝ⁺
27		modcl	⊢ ( ( ( 𝐴 · 𝑎 ) ∈ ℝ ∧ 1 ∈ ℝ⁺ ) → ( ( 𝐴 · 𝑎 ) mod 1 ) ∈ ℝ )
28	25 26 27	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐴 · 𝑎 ) mod 1 ) ∈ ℝ )
29	19 28	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ∈ ℝ )
30	29	flcld	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ∈ ℤ )
31	19	recnd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 𝐵 ∈ ℂ )
32	31	mul01d	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · 0 ) = 0 )
33		modge0	⊢ ( ( ( 𝐴 · 𝑎 ) ∈ ℝ ∧ 1 ∈ ℝ⁺ ) → 0 ≤ ( ( 𝐴 · 𝑎 ) mod 1 ) )
34	25 26 33	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 0 ≤ ( ( 𝐴 · 𝑎 ) mod 1 ) )
35		0red	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 0 ∈ ℝ )
36		nngt0	⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
37	36	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 0 < 𝐵 )
38		lemul2	⊢ ( ( 0 ∈ ℝ ∧ ( ( 𝐴 · 𝑎 ) mod 1 ) ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 0 ≤ ( ( 𝐴 · 𝑎 ) mod 1 ) ↔ ( 𝐵 · 0 ) ≤ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) )
39	35 28 19 37 38	syl112anc	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 0 ≤ ( ( 𝐴 · 𝑎 ) mod 1 ) ↔ ( 𝐵 · 0 ) ≤ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) )
40	34 39	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · 0 ) ≤ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) )
41	32 40	eqbrtrrd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 0 ≤ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) )
42	35 29	lenltd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 0 ≤ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ↔ ¬ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) < 0 ) )
43	41 42	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ¬ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) < 0 )
44		0z	⊢ 0 ∈ ℤ
45		fllt	⊢ ( ( ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) < 0 ↔ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) < 0 ) )
46	29 44 45	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) < 0 ↔ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) < 0 ) )
47	43 46	mtbid	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ¬ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) < 0 )
48	30	zred	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ∈ ℝ )
49	35 48	lenltd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 0 ≤ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ↔ ¬ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) < 0 ) )
50	47 49	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 0 ≤ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) )
51		elnn0z	⊢ ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ∈ ℕ₀ ↔ ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ) )
52	30 50 51	sylanbrc	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ∈ ℕ₀ )
53	8	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 − 1 ) ∈ ℕ₀ )
54		flle	⊢ ( ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ≤ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) )
55	29 54	syl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ≤ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) )
56		modlt	⊢ ( ( ( 𝐴 · 𝑎 ) ∈ ℝ ∧ 1 ∈ ℝ⁺ ) → ( ( 𝐴 · 𝑎 ) mod 1 ) < 1 )
57	25 26 56	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐴 · 𝑎 ) mod 1 ) < 1 )
58		1red	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 1 ∈ ℝ )
59		ltmul2	⊢ ( ( ( ( 𝐴 · 𝑎 ) mod 1 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( ( 𝐴 · 𝑎 ) mod 1 ) < 1 ↔ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) < ( 𝐵 · 1 ) ) )
60	28 58 19 37 59	syl112anc	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ( ( 𝐴 · 𝑎 ) mod 1 ) < 1 ↔ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) < ( 𝐵 · 1 ) ) )
61	57 60	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) < ( 𝐵 · 1 ) )
62	31	mulid1d	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · 1 ) = 𝐵 )
63	61 62	breqtrd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) < 𝐵 )
64	48 29 19 55 63	lelttrd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) < 𝐵 )
65		nncn	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
66		ax-1cn	⊢ 1 ∈ ℂ
67		npcan	⊢ ( ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐵 − 1 ) + 1 ) = 𝐵 )
68	65 66 67	sylancl	⊢ ( 𝐵 ∈ ℕ → ( ( 𝐵 − 1 ) + 1 ) = 𝐵 )
69	68	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ( 𝐵 − 1 ) + 1 ) = 𝐵 )
70	64 69	breqtrrd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) < ( ( 𝐵 − 1 ) + 1 ) )
71	12	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → 𝐵 ∈ ℤ )
72		1z	⊢ 1 ∈ ℤ
73		zsubcl	⊢ ( ( 𝐵 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝐵 − 1 ) ∈ ℤ )
74	71 72 73	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 − 1 ) ∈ ℤ )
75		zleltp1	⊢ ( ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ∈ ℤ ∧ ( 𝐵 − 1 ) ∈ ℤ ) → ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ≤ ( 𝐵 − 1 ) ↔ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) < ( ( 𝐵 − 1 ) + 1 ) ) )
76	30 74 75	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ≤ ( 𝐵 − 1 ) ↔ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) < ( ( 𝐵 − 1 ) + 1 ) ) )
77	70 76	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ≤ ( 𝐵 − 1 ) )
78		elfz2nn0	⊢ ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ∈ ( 0 ... ( 𝐵 − 1 ) ) ↔ ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ∈ ℕ₀ ∧ ( 𝐵 − 1 ) ∈ ℕ₀ ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ≤ ( 𝐵 − 1 ) ) )
79	52 53 77 78	syl3anbrc	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 0 ... 𝐵 ) ) → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) ∈ ( 0 ... ( 𝐵 − 1 ) ) )
80		oveq2	⊢ ( 𝑎 = 𝑥 → ( 𝐴 · 𝑎 ) = ( 𝐴 · 𝑥 ) )
81	80	oveq1d	⊢ ( 𝑎 = 𝑥 → ( ( 𝐴 · 𝑎 ) mod 1 ) = ( ( 𝐴 · 𝑥 ) mod 1 ) )
82	81	oveq2d	⊢ ( 𝑎 = 𝑥 → ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) = ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) )
83	82	fveq2d	⊢ ( 𝑎 = 𝑥 → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) )
84		oveq2	⊢ ( 𝑎 = 𝑦 → ( 𝐴 · 𝑎 ) = ( 𝐴 · 𝑦 ) )
85	84	oveq1d	⊢ ( 𝑎 = 𝑦 → ( ( 𝐴 · 𝑎 ) mod 1 ) = ( ( 𝐴 · 𝑦 ) mod 1 ) )
86	85	oveq2d	⊢ ( 𝑎 = 𝑦 → ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) = ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) )
87	86	fveq2d	⊢ ( 𝑎 = 𝑦 → ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) )
88	6 7 18 79 83 87	fphpdo	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ( 0 ... 𝐵 ) ∃ 𝑦 ∈ ( 0 ... 𝐵 ) ( 𝑥 < 𝑦 ∧ ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑥 ) mod 1 ) ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐴 · 𝑦 ) mod 1 ) ) ) ) )

Metamath Proof Explorer

Theorem irrapxlem1

Proof