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

Metamath Proof Explorer

Theorem mulmod0

Description: The product of an integer and a positive real number is 0 modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018) (Revised by AV, 5-Jul-2020)

		Ref	Expression
	Assertion	mulmod0	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( 𝐴 · 𝑀 ) mod 𝑀 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → 𝐴 ∈ ℂ )
3		rpcn	⊢ ( 𝑀 ∈ ℝ⁺ → 𝑀 ∈ ℂ )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → 𝑀 ∈ ℂ )
5		rpne0	⊢ ( 𝑀 ∈ ℝ⁺ → 𝑀 ≠ 0 )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → 𝑀 ≠ 0 )
7	2 4 6	divcan4d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( 𝐴 · 𝑀 ) / 𝑀 ) = 𝐴 )
8		simpl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → 𝐴 ∈ ℤ )
9	7 8	eqeltrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( 𝐴 · 𝑀 ) / 𝑀 ) ∈ ℤ )
10		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
11		rpre	⊢ ( 𝑀 ∈ ℝ⁺ → 𝑀 ∈ ℝ )
12		remulcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝐴 · 𝑀 ) ∈ ℝ )
13	10 11 12	syl2an	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → ( 𝐴 · 𝑀 ) ∈ ℝ )
14		mod0	⊢ ( ( ( 𝐴 · 𝑀 ) ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( ( 𝐴 · 𝑀 ) mod 𝑀 ) = 0 ↔ ( ( 𝐴 · 𝑀 ) / 𝑀 ) ∈ ℤ ) )
15	13 14	sylancom	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( ( 𝐴 · 𝑀 ) mod 𝑀 ) = 0 ↔ ( ( 𝐴 · 𝑀 ) / 𝑀 ) ∈ ℤ ) )
16	9 15	mpbird	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( 𝐴 · 𝑀 ) mod 𝑀 ) = 0 )