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	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ( 1 ... 𝐵 ) ∃ 𝑦 ∈ ℕ₀ ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		irrapxlem2	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑎 ∈ ( 0 ... 𝐵 ) ∃ 𝑏 ∈ ( 0 ... 𝐵 ) ( 𝑎 < 𝑏 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) )
2		1z	⊢ 1 ∈ ℤ
3	2	a1i	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 1 ∈ ℤ )
4		simpllr	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝐵 ∈ ℕ )
5	4	nnzd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝐵 ∈ ℤ )
6		simplrr	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑏 ∈ ( 0 ... 𝐵 ) )
7	6	elfzelzd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑏 ∈ ℤ )
8		simplrl	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 ∈ ( 0 ... 𝐵 ) )
9	8	elfzelzd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 ∈ ℤ )
10	7 9	zsubcld	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑏 − 𝑎 ) ∈ ℤ )
11		1m1e0	⊢ ( 1 − 1 ) = 0
12		elfzelz	⊢ ( 𝑎 ∈ ( 0 ... 𝐵 ) → 𝑎 ∈ ℤ )
13	12	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) → 𝑎 ∈ ℤ )
14	13	zred	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) → 𝑎 ∈ ℝ )
15		elfzelz	⊢ ( 𝑏 ∈ ( 0 ... 𝐵 ) → 𝑏 ∈ ℤ )
16	15	ad2antll	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) → 𝑏 ∈ ℤ )
17	16	zred	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) → 𝑏 ∈ ℝ )
18	14 17	posdifd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) → ( 𝑎 < 𝑏 ↔ 0 < ( 𝑏 − 𝑎 ) ) )
19	18	biimpa	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 0 < ( 𝑏 − 𝑎 ) )
20	11 19	eqbrtrid	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 1 − 1 ) < ( 𝑏 − 𝑎 ) )
21		zlem1lt	⊢ ( ( 1 ∈ ℤ ∧ ( 𝑏 − 𝑎 ) ∈ ℤ ) → ( 1 ≤ ( 𝑏 − 𝑎 ) ↔ ( 1 − 1 ) < ( 𝑏 − 𝑎 ) ) )
22	2 10 21	sylancr	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 1 ≤ ( 𝑏 − 𝑎 ) ↔ ( 1 − 1 ) < ( 𝑏 − 𝑎 ) ) )
23	20 22	mpbird	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 1 ≤ ( 𝑏 − 𝑎 ) )
24	7	zred	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑏 ∈ ℝ )
25	9	zred	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 ∈ ℝ )
26	24 25	resubcld	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑏 − 𝑎 ) ∈ ℝ )
27		0red	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 0 ∈ ℝ )
28	24 27	resubcld	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑏 − 0 ) ∈ ℝ )
29	4	nnred	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝐵 ∈ ℝ )
30		elfzle1	⊢ ( 𝑎 ∈ ( 0 ... 𝐵 ) → 0 ≤ 𝑎 )
31	8 30	syl	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 0 ≤ 𝑎 )
32	27 25 24 31	lesub2dd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑏 − 𝑎 ) ≤ ( 𝑏 − 0 ) )
33	24	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑏 ∈ ℂ )
34	33	subid1d	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑏 − 0 ) = 𝑏 )
35		elfzle2	⊢ ( 𝑏 ∈ ( 0 ... 𝐵 ) → 𝑏 ≤ 𝐵 )
36	6 35	syl	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑏 ≤ 𝐵 )
37	34 36	eqbrtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑏 − 0 ) ≤ 𝐵 )
38	26 28 29 32 37	letrd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑏 − 𝑎 ) ≤ 𝐵 )
39	3 5 10 23 38	elfzd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑏 − 𝑎 ) ∈ ( 1 ... 𝐵 ) )
40	39	adantrr	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) ) → ( 𝑏 − 𝑎 ) ∈ ( 1 ... 𝐵 ) )
41		rpre	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ )
42	41	ad3antrrr	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝐴 ∈ ℝ )
43	42 25	remulcld	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝐴 · 𝑎 ) ∈ ℝ )
44	42 24	remulcld	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝐴 · 𝑏 ) ∈ ℝ )
45		simpr	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 < 𝑏 )
46	25 24 45	ltled	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 ≤ 𝑏 )
47		rpgt0	⊢ ( 𝐴 ∈ ℝ⁺ → 0 < 𝐴 )
48	47	ad3antrrr	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 0 < 𝐴 )
49		lemul2	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝐴 · 𝑎 ) ≤ ( 𝐴 · 𝑏 ) ) )
50	25 24 42 48 49	syl112anc	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝐴 · 𝑎 ) ≤ ( 𝐴 · 𝑏 ) ) )
51	46 50	mpbid	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝐴 · 𝑎 ) ≤ ( 𝐴 · 𝑏 ) )
52		flword2	⊢ ( ( ( 𝐴 · 𝑎 ) ∈ ℝ ∧ ( 𝐴 · 𝑏 ) ∈ ℝ ∧ ( 𝐴 · 𝑎 ) ≤ ( 𝐴 · 𝑏 ) ) → ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) ∈ ( ℤ_≥ ‘ ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) )
53	43 44 51 52	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) ∈ ( ℤ_≥ ‘ ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) )
54		uznn0sub	⊢ ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) ∈ ( ℤ_≥ ‘ ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) → ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ∈ ℕ₀ )
55	53 54	syl	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ∈ ℕ₀ )
56	55	adantrr	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) ) → ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ∈ ℕ₀ )
57	42	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝐴 ∈ ℂ )
58	25	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 ∈ ℂ )
59	57 33 58	subdid	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝐴 · ( 𝑏 − 𝑎 ) ) = ( ( 𝐴 · 𝑏 ) − ( 𝐴 · 𝑎 ) ) )
60	59	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) = ( ( ( 𝐴 · 𝑏 ) − ( 𝐴 · 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) )
61	44	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝐴 · 𝑏 ) ∈ ℂ )
62	43	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝐴 · 𝑎 ) ∈ ℂ )
63	44	flcld	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) ∈ ℤ )
64	63	zcnd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) ∈ ℂ )
65	43	flcld	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ∈ ℤ )
66	65	zcnd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ∈ ℂ )
67	61 62 64 66	sub4d	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( ( 𝐴 · 𝑏 ) − ( 𝐴 · 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) = ( ( ( 𝐴 · 𝑏 ) − ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) ) − ( ( 𝐴 · 𝑎 ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) )
68		modfrac	⊢ ( ( 𝐴 · 𝑏 ) ∈ ℝ → ( ( 𝐴 · 𝑏 ) mod 1 ) = ( ( 𝐴 · 𝑏 ) − ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) ) )
69	44 68	syl	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝐴 · 𝑏 ) mod 1 ) = ( ( 𝐴 · 𝑏 ) − ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) ) )
70	69	eqcomd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝐴 · 𝑏 ) − ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) ) = ( ( 𝐴 · 𝑏 ) mod 1 ) )
71		modfrac	⊢ ( ( 𝐴 · 𝑎 ) ∈ ℝ → ( ( 𝐴 · 𝑎 ) mod 1 ) = ( ( 𝐴 · 𝑎 ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) )
72	43 71	syl	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝐴 · 𝑎 ) mod 1 ) = ( ( 𝐴 · 𝑎 ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) )
73	72	eqcomd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝐴 · 𝑎 ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) = ( ( 𝐴 · 𝑎 ) mod 1 ) )
74	70 73	oveq12d	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( ( 𝐴 · 𝑏 ) − ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) ) − ( ( 𝐴 · 𝑎 ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) = ( ( ( 𝐴 · 𝑏 ) mod 1 ) − ( ( 𝐴 · 𝑎 ) mod 1 ) ) )
75	60 67 74	3eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) = ( ( ( 𝐴 · 𝑏 ) mod 1 ) − ( ( 𝐴 · 𝑎 ) mod 1 ) ) )
76	75	fveq2d	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) ) = ( abs ‘ ( ( ( 𝐴 · 𝑏 ) mod 1 ) − ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) )
77		1rp	⊢ 1 ∈ ℝ⁺
78	77	a1i	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → 1 ∈ ℝ⁺ )
79	44 78	modcld	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝐴 · 𝑏 ) mod 1 ) ∈ ℝ )
80	79	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝐴 · 𝑏 ) mod 1 ) ∈ ℂ )
81	43 78	modcld	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝐴 · 𝑎 ) mod 1 ) ∈ ℝ )
82	81	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝐴 · 𝑎 ) mod 1 ) ∈ ℂ )
83	80 82	abssubd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( abs ‘ ( ( ( 𝐴 · 𝑏 ) mod 1 ) − ( ( 𝐴 · 𝑎 ) mod 1 ) ) ) = ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) )
84	76 83	eqtr2d	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) = ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) ) )
85	84	breq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ↔ ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) ) < ( 1 / 𝐵 ) ) )
86	85	biimpd	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ 𝑎 < 𝑏 ) → ( ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) < ( 1 / 𝐵 ) → ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) ) < ( 1 / 𝐵 ) ) )
87	86	impr	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) ) → ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) ) < ( 1 / 𝐵 ) )
88		oveq2	⊢ ( 𝑥 = ( 𝑏 − 𝑎 ) → ( 𝐴 · 𝑥 ) = ( 𝐴 · ( 𝑏 − 𝑎 ) ) )
89	88	fvoveq1d	⊢ ( 𝑥 = ( 𝑏 − 𝑎 ) → ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) = ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − 𝑦 ) ) )
90	89	breq1d	⊢ ( 𝑥 = ( 𝑏 − 𝑎 ) → ( ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / 𝐵 ) ↔ ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − 𝑦 ) ) < ( 1 / 𝐵 ) ) )
91		oveq2	⊢ ( 𝑦 = ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) → ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − 𝑦 ) = ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) )
92	91	fveq2d	⊢ ( 𝑦 = ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) → ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − 𝑦 ) ) = ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) ) )
93	92	breq1d	⊢ ( 𝑦 = ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) → ( ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − 𝑦 ) ) < ( 1 / 𝐵 ) ↔ ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) ) < ( 1 / 𝐵 ) ) )
94	90 93	rspc2ev	⊢ ( ( ( 𝑏 − 𝑎 ) ∈ ( 1 ... 𝐵 ) ∧ ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ∈ ℕ₀ ∧ ( abs ‘ ( ( 𝐴 · ( 𝑏 − 𝑎 ) ) − ( ( ⌊ ‘ ( 𝐴 · 𝑏 ) ) − ( ⌊ ‘ ( 𝐴 · 𝑎 ) ) ) ) ) < ( 1 / 𝐵 ) ) → ∃ 𝑥 ∈ ( 1 ... 𝐵 ) ∃ 𝑦 ∈ ℕ₀ ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / 𝐵 ) )
95	40 56 87 94	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) ) → ∃ 𝑥 ∈ ( 1 ... 𝐵 ) ∃ 𝑦 ∈ ℕ₀ ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / 𝐵 ) )
96	95	ex	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐵 ) ∧ 𝑏 ∈ ( 0 ... 𝐵 ) ) ) → ( ( 𝑎 < 𝑏 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) → ∃ 𝑥 ∈ ( 1 ... 𝐵 ) ∃ 𝑦 ∈ ℕ₀ ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / 𝐵 ) ) )
97	96	rexlimdvva	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑎 ∈ ( 0 ... 𝐵 ) ∃ 𝑏 ∈ ( 0 ... 𝐵 ) ( 𝑎 < 𝑏 ∧ ( abs ‘ ( ( ( 𝐴 · 𝑎 ) mod 1 ) − ( ( 𝐴 · 𝑏 ) mod 1 ) ) ) < ( 1 / 𝐵 ) ) → ∃ 𝑥 ∈ ( 1 ... 𝐵 ) ∃ 𝑦 ∈ ℕ₀ ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / 𝐵 ) ) )
98	1 97	mpd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ( 1 ... 𝐵 ) ∃ 𝑦 ∈ ℕ₀ ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / 𝐵 ) )

Metamath Proof Explorer

Theorem irrapxlem3

Proof