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

Metamath Proof Explorer

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 \mod N = 0$

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