modid2

		Ref	Expression
	Assertion	modid2	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B = A \leftrightarrow (0 \leq A \land A < B))$

Step	Hyp	Ref	Expression
1		modge0	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to 0 \leq A \mod B$
2		modlt	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B < B$
3	1 2	jca	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (0 \leq A \mod B \land A \mod B < B)$
4		breq2	$⊢ A \mod B = A \to (0 \leq A \mod B \leftrightarrow 0 \leq A)$
5		breq1	$⊢ A \mod B = A \to (A \mod B < B \leftrightarrow A < B)$
6	4 5	anbi12d	$⊢ A \mod B = A \to ((0 \leq A \mod B \land A \mod B < B) \leftrightarrow (0 \leq A \land A < B))$
7	3 6	syl5ibcom	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B = A \to (0 \leq A \land A < B))$
8		modid	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to A \mod B = A$
9	8	ex	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ((0 \leq A \land A < B) \to A \mod B = A)$
10	7 9	impbid	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B = A \leftrightarrow (0 \leq A \land A < B))$

Metamath Proof Explorer