Theorem modid0

Description: A positive real number modulo itself is 0. (Contributed by Alexander van der Vekens, 15-May-2018)

	Ref	Expression
Assertion	modid0	⊢ ( 𝑁 ∈ ℝ+ → ( 𝑁 mod 𝑁 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝑁 ∈ ℝ+ → 𝑁 ∈ ℂ )
2		rpne0	⊢ ( 𝑁 ∈ ℝ+ → 𝑁 ≠ 0 )
3	1 2	dividd	⊢ ( 𝑁 ∈ ℝ+ → ( 𝑁 / 𝑁 ) = 1 )
4		1z	⊢ 1 ∈ ℤ
5	3 4	eqeltrdi	⊢ ( 𝑁 ∈ ℝ+ → ( 𝑁 / 𝑁 ) ∈ ℤ )
6		rpre	⊢ ( 𝑁 ∈ ℝ+ → 𝑁 ∈ ℝ )
7		mod0	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝑁 mod 𝑁 ) = 0 ↔ ( 𝑁 / 𝑁 ) ∈ ℤ ) )
8	6 7	mpancom	⊢ ( 𝑁 ∈ ℝ+ → ( ( 𝑁 mod 𝑁 ) = 0 ↔ ( 𝑁 / 𝑁 ) ∈ ℤ ) )
9	5 8	mpbird	⊢ ( 𝑁 ∈ ℝ+ → ( 𝑁 mod 𝑁 ) = 0 )