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

Metamath Proof Explorer

Theorem intfrac

Description: Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008)

		Ref	Expression
	Assertion	intfrac	$⊢ A \in ℝ \to A = ⌊A⌋ + (A \mod 1)$

Step	Hyp	Ref	Expression
1		modfrac	$⊢ A \in ℝ \to A \mod 1 = A - ⌊A⌋$
2	1	oveq2d	$⊢ A \in ℝ \to ⌊A⌋ + (A \mod 1) = ⌊A⌋ + A - ⌊A⌋$
3		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
4	3	recnd	$⊢ A \in ℝ \to ⌊A⌋ \in ℂ$
5		recn	$⊢ A \in ℝ \to A \in ℂ$
6	4 5	pncan3d	$⊢ A \in ℝ \to ⌊A⌋ + A - ⌊A⌋ = A$
7	2 6	eqtr2d	$⊢ A \in ℝ \to A = ⌊A⌋ + (A \mod 1)$