Theorem modid0

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

	Ref	Expression
Assertion	modid0	$$⊢N\in {ℝ}^{+}\to N\mathrm{mod}N=0$$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$$⊢N\in {ℝ}^{+}\to N\in ℂ$$
2		rpne0	$$⊢N\in {ℝ}^{+}\to N\ne 0$$
3	1 2	dividd	$$⊢N\in {ℝ}^{+}\to \frac{N}{N}=1$$
4		1z	$$⊢1\in \mathbb{Z}$$
5	3 4	eqeltrdi	$$⊢N\in {ℝ}^{+}\to \frac{N}{N}\in \mathbb{Z}$$
6		rpre	$$⊢N\in {ℝ}^{+}\to N\in ℝ$$
7		mod0	$$⊢\left(N\in ℝ\wedge N\in {ℝ}^{+}\right)\to \left(N\mathrm{mod}N=0\leftrightarrow \frac{N}{N}\in \mathbb{Z}\right)$$
8	6 7	mpancom	$$⊢N\in {ℝ}^{+}\to \left(N\mathrm{mod}N=0\leftrightarrow \frac{N}{N}\in \mathbb{Z}\right)$$
9	5 8	mpbird	$$⊢N\in {ℝ}^{+}\to N\mathrm{mod}N=0$$