Theorem 0mod

Description: Special case: 0 modulo a positive real number is 0. (Contributed by Mario Carneiro, 22-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2	1	jctl	$$⊢N\in {ℝ}^{+}\to \left(0\in ℝ\wedge N\in {ℝ}^{+}\right)$$
3		rpgt0	$$⊢N\in {ℝ}^{+}\to 0<N$$
4		0le0	$$⊢0\le 0$$
5	3 4	jctil	$$⊢N\in {ℝ}^{+}\to \left(0\le 0\wedge 0<N\right)$$
6		modid	$$⊢\left(\left(0\in ℝ\wedge N\in {ℝ}^{+}\right)\wedge \left(0\le 0\wedge 0<N\right)\right)\to 0\mathrm{mod}N=0$$
7	2 5 6	syl2anc	$$⊢N\in {ℝ}^{+}\to 0\mathrm{mod}N=0$$