Metamath Proof Explorer


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 )