Theorem modirr

Description: A number modulo an irrational multiple of it is nonzero. (Contributed by NM, 11-Nov-2008)

	Ref	Expression
Assertion	modirr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐴 / 𝐵 ) ∈ ( ℝ ∖ ℚ ) ) → ( 𝐴 mod 𝐵 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		eldif	⊢ ( ( 𝐴 / 𝐵 ) ∈ ( ℝ ∖ ℚ ) ↔ ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ ¬ ( 𝐴 / 𝐵 ) ∈ ℚ ) )
2		modval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
3	2	eqeq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) = 0 ) )
4		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
6		rpre	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
7	6	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
8		refldivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℝ )
9	7 8	remulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ∈ ℝ )
10	9	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ∈ ℂ )
11	5 10	subeq0ad	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) = 0 ↔ 𝐴 = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
12		rerpdivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
13		reflcl	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℝ )
14	13	recnd	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
15	12 14	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
16		rpcnne0	⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
17	16	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
18		divmul2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ↔ 𝐴 = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
19	5 15 17 18	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ↔ 𝐴 = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
20		eqcom	⊢ ( ( 𝐴 / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ↔ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) )
21	19 20	bitr3di	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ↔ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) ) )
22	3 11 21	3bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) ) )
23		flidz	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) ↔ ( 𝐴 / 𝐵 ) ∈ ℤ ) )
24		zq	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℤ → ( 𝐴 / 𝐵 ) ∈ ℚ )
25	23 24	syl6bi	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) → ( 𝐴 / 𝐵 ) ∈ ℚ ) )
26	12 25	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) → ( 𝐴 / 𝐵 ) ∈ ℚ ) )
27	22 26	sylbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 → ( 𝐴 / 𝐵 ) ∈ ℚ ) )
28	27	necon3bd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ¬ ( 𝐴 / 𝐵 ) ∈ ℚ → ( 𝐴 mod 𝐵 ) ≠ 0 ) )
29	28	adantld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ ¬ ( 𝐴 / 𝐵 ) ∈ ℚ ) → ( 𝐴 mod 𝐵 ) ≠ 0 ) )
30	1 29	syl5bi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ∈ ( ℝ ∖ ℚ ) → ( 𝐴 mod 𝐵 ) ≠ 0 ) )
31	30	3impia	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐴 / 𝐵 ) ∈ ( ℝ ∖ ℚ ) ) → ( 𝐴 mod 𝐵 ) ≠ 0 )