Theorem mod0

Description: A mod B is zero iff A is evenly divisible by B . (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Fan Zheng, 7-Jun-2016)

	Ref	Expression
Assertion	mod0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( 𝐴 / 𝐵 ) ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		modval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
2	1	eqeq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) = 0 ) )
3		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
5		rpre	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
7		refldivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℝ )
8	6 7	remulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ∈ ℝ )
9	8	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ∈ ℂ )
10	4 9	subeq0ad	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) = 0 ↔ 𝐴 = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
11	2 10	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ 𝐴 = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
12	7	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
13		rpcnne0	⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
14	13	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
15		divmul2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ↔ 𝐴 = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
16	4 12 14 15	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ↔ 𝐴 = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
17		eqcom	⊢ ( ( 𝐴 / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ↔ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) )
18	16 17	bitr3di	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ↔ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) ) )
19	11 18	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) ) )
20		rerpdivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
21		flidz	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) ↔ ( 𝐴 / 𝐵 ) ∈ ℤ ) )
22	20 21	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) ↔ ( 𝐴 / 𝐵 ) ∈ ℤ ) )
23	19 22	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( 𝐴 / 𝐵 ) ∈ ℤ ) )