intfracq

Description: Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfrac2 . (Contributed by NM, 16-Aug-2008)

	Ref	Expression
Hypotheses	intfracq.1	$⊢ Z = ⌊\frac{M}{N}⌋$
	intfracq.2	$⊢ F = (\frac{M}{N}) - Z$
Assertion	intfracq	$⊢ (M \in ℤ \land N \in ℕ) \to (0 \leq F \land F \leq \frac{N - 1}{N} \land \frac{M}{N} = Z + F)$

Proof

Step	Hyp	Ref	Expression
1		intfracq.1	$⊢ Z = ⌊\frac{M}{N}⌋$
2		intfracq.2	$⊢ F = (\frac{M}{N}) - Z$
3		zre	$⊢ M \in ℤ \to M \in ℝ$
4	3	adantr	$⊢ (M \in ℤ \land N \in ℕ) \to M \in ℝ$
5		nnre	$⊢ N \in ℕ \to N \in ℝ$
6	5	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N \in ℝ$
7		nnne0	$⊢ N \in ℕ \to N \neq 0$
8	7	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N \neq 0$
9	4 6 8	redivcld	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M}{N} \in ℝ$
10	1 2	intfrac2	$⊢ \frac{M}{N} \in ℝ \to (0 \leq F \land F < 1 \land \frac{M}{N} = Z + F)$
11	9 10	syl	$⊢ (M \in ℤ \land N \in ℕ) \to (0 \leq F \land F < 1 \land \frac{M}{N} = Z + F)$
12	11	simp1d	$⊢ (M \in ℤ \land N \in ℕ) \to 0 \leq F$
13		fraclt1	$⊢ \frac{M}{N} \in ℝ \to (\frac{M}{N}) - ⌊\frac{M}{N}⌋ < 1$
14	9 13	syl	$⊢ (M \in ℤ \land N \in ℕ) \to (\frac{M}{N}) - ⌊\frac{M}{N}⌋ < 1$
15	1	oveq2i	$⊢ (\frac{M}{N}) - Z = (\frac{M}{N}) - ⌊\frac{M}{N}⌋$
16	2 15	eqtri	$⊢ F = (\frac{M}{N}) - ⌊\frac{M}{N}⌋$
17	16	a1i	$⊢ (M \in ℤ \land N \in ℕ) \to F = (\frac{M}{N}) - ⌊\frac{M}{N}⌋$
18		nncn	$⊢ N \in ℕ \to N \in ℂ$
19	18 7	dividd	$⊢ N \in ℕ \to \frac{N}{N} = 1$
20	19	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{N}{N} = 1$
21	14 17 20	3brtr4d	$⊢ (M \in ℤ \land N \in ℕ) \to F < \frac{N}{N}$
22		reflcl	$⊢ \frac{M}{N} \in ℝ \to ⌊\frac{M}{N}⌋ \in ℝ$
23	9 22	syl	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M}{N}⌋ \in ℝ$
24	1 23	eqeltrid	$⊢ (M \in ℤ \land N \in ℕ) \to Z \in ℝ$
25	9 24	resubcld	$⊢ (M \in ℤ \land N \in ℕ) \to (\frac{M}{N}) - Z \in ℝ$
26	2 25	eqeltrid	$⊢ (M \in ℤ \land N \in ℕ) \to F \in ℝ$
27		nngt0	$⊢ N \in ℕ \to 0 < N$
28	5 27	jca	$⊢ N \in ℕ \to (N \in ℝ \land 0 < N)$
29	28	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to (N \in ℝ \land 0 < N)$
30		ltmuldiv2	$⊢ (F \in ℝ \land N \in ℝ \land (N \in ℝ \land 0 < N)) \to (N F < N \leftrightarrow F < \frac{N}{N})$
31	26 6 29 30	syl3anc	$⊢ (M \in ℤ \land N \in ℕ) \to (N F < N \leftrightarrow F < \frac{N}{N})$
32	21 31	mpbird	$⊢ (M \in ℤ \land N \in ℕ) \to N F < N$
33	2	oveq2i	$⊢ N F = N ((\frac{M}{N}) - Z)$
34	18	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N \in ℂ$
35	9	recnd	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M}{N} \in ℂ$
36	9	flcld	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M}{N}⌋ \in ℤ$
37	1 36	eqeltrid	$⊢ (M \in ℤ \land N \in ℕ) \to Z \in ℤ$
38	37	zcnd	$⊢ (M \in ℤ \land N \in ℕ) \to Z \in ℂ$
39	34 35 38	subdid	$⊢ (M \in ℤ \land N \in ℕ) \to N ((\frac{M}{N}) - Z) = N (\frac{M}{N}) - N Z$
40	33 39	syl5eq	$⊢ (M \in ℤ \land N \in ℕ) \to N F = N (\frac{M}{N}) - N Z$
41		zcn	$⊢ M \in ℤ \to M \in ℂ$
42	41	adantr	$⊢ (M \in ℤ \land N \in ℕ) \to M \in ℂ$
43	42 34 8	divcan2d	$⊢ (M \in ℤ \land N \in ℕ) \to N (\frac{M}{N}) = M$
44		simpl	$⊢ (M \in ℤ \land N \in ℕ) \to M \in ℤ$
45	43 44	eqeltrd	$⊢ (M \in ℤ \land N \in ℕ) \to N (\frac{M}{N}) \in ℤ$
46		nnz	$⊢ N \in ℕ \to N \in ℤ$
47	46	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N \in ℤ$
48	47 37	zmulcld	$⊢ (M \in ℤ \land N \in ℕ) \to N Z \in ℤ$
49	45 48	zsubcld	$⊢ (M \in ℤ \land N \in ℕ) \to N (\frac{M}{N}) - N Z \in ℤ$
50	40 49	eqeltrd	$⊢ (M \in ℤ \land N \in ℕ) \to N F \in ℤ$
51		zltlem1	$⊢ (N F \in ℤ \land N \in ℤ) \to (N F < N \leftrightarrow N F \leq N - 1)$
52	50 47 51	syl2anc	$⊢ (M \in ℤ \land N \in ℕ) \to (N F < N \leftrightarrow N F \leq N - 1)$
53	32 52	mpbid	$⊢ (M \in ℤ \land N \in ℕ) \to N F \leq N - 1$
54		peano2rem	$⊢ N \in ℝ \to N - 1 \in ℝ$
55	5 54	syl	$⊢ N \in ℕ \to N - 1 \in ℝ$
56	55	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N - 1 \in ℝ$
57		lemuldiv2	$⊢ (F \in ℝ \land N - 1 \in ℝ \land (N \in ℝ \land 0 < N)) \to (N F \leq N - 1 \leftrightarrow F \leq \frac{N - 1}{N})$
58	26 56 29 57	syl3anc	$⊢ (M \in ℤ \land N \in ℕ) \to (N F \leq N - 1 \leftrightarrow F \leq \frac{N - 1}{N})$
59	53 58	mpbid	$⊢ (M \in ℤ \land N \in ℕ) \to F \leq \frac{N - 1}{N}$
60	11	simp3d	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M}{N} = Z + F$
61	12 59 60	3jca	$⊢ (M \in ℤ \land N \in ℕ) \to (0 \leq F \land F \leq \frac{N - 1}{N} \land \frac{M}{N} = Z + F)$

Metamath Proof Explorer

Theorem intfracq

Proof