modfrac

Description: The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008)

		Ref	Expression
	Assertion	modfrac	$⊢ A \in ℝ \to A \mod 1 = A - ⌊A⌋$

Step	Hyp	Ref	Expression
1		1rp	$⊢ 1 \in ℝ^{+}$
2		modval	$⊢ (A \in ℝ \land 1 \in ℝ^{+}) \to A \mod 1 = A - 1 ⌊\frac{A}{1}⌋$
3	1 2	mpan2	$⊢ A \in ℝ \to A \mod 1 = A - 1 ⌊\frac{A}{1}⌋$
4		recn	$⊢ A \in ℝ \to A \in ℂ$
5	4	div1d	$⊢ A \in ℝ \to \frac{A}{1} = A$
6	5	fveq2d	$⊢ A \in ℝ \to ⌊\frac{A}{1}⌋ = ⌊A⌋$
7	6	oveq2d	$⊢ A \in ℝ \to 1 ⌊\frac{A}{1}⌋ = 1 ⌊A⌋$
8		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
9	8	recnd	$⊢ A \in ℝ \to ⌊A⌋ \in ℂ$
10	9	mullidd	$⊢ A \in ℝ \to 1 ⌊A⌋ = ⌊A⌋$
11	7 10	eqtrd	$⊢ A \in ℝ \to 1 ⌊\frac{A}{1}⌋ = ⌊A⌋$
12	11	oveq2d	$⊢ A \in ℝ \to A - 1 ⌊\frac{A}{1}⌋ = A - ⌊A⌋$
13	3 12	eqtrd	$⊢ A \in ℝ \to A \mod 1 = A - ⌊A⌋$

Metamath Proof Explorer