modid

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

Proof

Step	Hyp	Ref	Expression
1		modval	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
2	1	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
3		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
4	3	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to \frac{A}{B} \in ℝ$
5	4	recnd	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to \frac{A}{B} \in ℂ$
6		addlid	$⊢ \frac{A}{B} \in ℂ \to 0 + (\frac{A}{B}) = \frac{A}{B}$
7	6	fveq2d	$⊢ \frac{A}{B} \in ℂ \to ⌊0 + (\frac{A}{B})⌋ = ⌊\frac{A}{B}⌋$
8	5 7	syl	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to ⌊0 + (\frac{A}{B})⌋ = ⌊\frac{A}{B}⌋$
9		rpregt0	$⊢ B \in ℝ^{+} \to (B \in ℝ \land 0 < B)$
10		divge0	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 < B)) \to 0 \leq \frac{A}{B}$
11	9 10	sylan2	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to 0 \leq \frac{A}{B}$
12	11	an32s	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land 0 \leq A) \to 0 \leq \frac{A}{B}$
13	12	adantrr	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to 0 \leq \frac{A}{B}$
14		simpr	$⊢ (B \in ℝ^{+} \land A < B) \to A < B$
15		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
16	15	mulridd	$⊢ B \in ℝ^{+} \to B \cdot 1 = B$
17	16	adantr	$⊢ (B \in ℝ^{+} \land A < B) \to B \cdot 1 = B$
18	14 17	breqtrrd	$⊢ (B \in ℝ^{+} \land A < B) \to A < B \cdot 1$
19	18	ad2ant2l	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to A < B \cdot 1$
20		simpll	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to A \in ℝ$
21	9	ad2antlr	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to (B \in ℝ \land 0 < B)$
22		1re	$⊢ 1 \in ℝ$
23		ltdivmul	$⊢ (A \in ℝ \land 1 \in ℝ \land (B \in ℝ \land 0 < B)) \to (\frac{A}{B} < 1 \leftrightarrow A < B \cdot 1)$
24	22 23	mp3an2	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B)) \to (\frac{A}{B} < 1 \leftrightarrow A < B \cdot 1)$
25	20 21 24	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to (\frac{A}{B} < 1 \leftrightarrow A < B \cdot 1)$
26	19 25	mpbird	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to \frac{A}{B} < 1$
27		0z	$⊢ 0 \in ℤ$
28		flbi2	$⊢ (0 \in ℤ \land \frac{A}{B} \in ℝ) \to (⌊0 + (\frac{A}{B})⌋ = 0 \leftrightarrow (0 \leq \frac{A}{B} \land \frac{A}{B} < 1))$
29	27 4 28	sylancr	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to (⌊0 + (\frac{A}{B})⌋ = 0 \leftrightarrow (0 \leq \frac{A}{B} \land \frac{A}{B} < 1))$
30	13 26 29	mpbir2and	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to ⌊0 + (\frac{A}{B})⌋ = 0$
31	8 30	eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to ⌊\frac{A}{B}⌋ = 0$
32	31	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to B ⌊\frac{A}{B}⌋ = B \cdot 0$
33	15	mul01d	$⊢ B \in ℝ^{+} \to B \cdot 0 = 0$
34	33	ad2antlr	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to B \cdot 0 = 0$
35	32 34	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to B ⌊\frac{A}{B}⌋ = 0$
36	35	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to A - B ⌊\frac{A}{B}⌋ = A - 0$
37		recn	$⊢ A \in ℝ \to A \in ℂ$
38	37	subid1d	$⊢ A \in ℝ \to A - 0 = A$
39	38	ad2antrr	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to A - 0 = A$
40	36 39	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to A - B ⌊\frac{A}{B}⌋ = A$
41	2 40	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land (0 \leq A \land A < B)) \to A \mod B = A$

Metamath Proof Explorer

Theorem modid

Proof