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

Metamath Proof Explorer

Theorem modcld

Description: Closure law for the modulo operation. (Contributed by Mario Carneiro, 28-May-2016)

Step	Hyp	Ref	Expression
1		modcld.1	$⊢ φ \to A \in ℝ$
2		modcld.2	$⊢ φ \to B \in ℝ^{+}$
3		modcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in ℝ$
4	1 2 3	syl2anc	$⊢ φ \to A \mod B \in ℝ$