This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) → ( 𝐴 / 𝐵 ) ∈ ℚ ) )
26 12 25 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) → ( 𝐴 / 𝐵 ) ∈ ℚ ) )
27 22 26 sylbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 → ( 𝐴 / 𝐵 ) ∈ ℚ ) )
28 27 necon3bd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ¬ ( 𝐴 / 𝐵 ) ∈ ℚ → ( 𝐴 mod 𝐵 ) ≠ 0 ) )
29 28 adantld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ ¬ ( 𝐴 / 𝐵 ) ∈ ℚ ) → ( 𝐴 mod 𝐵 ) ≠ 0 ) )
30 1 29 biimtrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ∈ ( ℝ ∖ ℚ ) → ( 𝐴 mod 𝐵 ) ≠ 0 ) )
31 30 3impia ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐴 / 𝐵 ) ∈ ( ℝ ∖ ℚ ) ) → ( 𝐴 mod 𝐵 ) ≠ 0 )