Theorem 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	⊢ 𝑍 = ( ⌊ ‘ ( 𝑀 / 𝑁 ) )
	intfracq.2	⊢ 𝐹 = ( ( 𝑀 / 𝑁 ) − 𝑍 )
Assertion	intfracq	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 0 ≤ 𝐹 ∧ 𝐹 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ∧ ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		intfracq.1	⊢ 𝑍 = ( ⌊ ‘ ( 𝑀 / 𝑁 ) )
2		intfracq.2	⊢ 𝐹 = ( ( 𝑀 / 𝑁 ) − 𝑍 )
3		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
4	3	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℝ )
5		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
6	5	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
7		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
8	7	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
9	4 6 8	redivcld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) ∈ ℝ )
10	1 2	intfrac2	⊢ ( ( 𝑀 / 𝑁 ) ∈ ℝ → ( 0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) ) )
11	9 10	syl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) ) )
12	11	simp1d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 0 ≤ 𝐹 )
13		fraclt1	⊢ ( ( 𝑀 / 𝑁 ) ∈ ℝ → ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) < 1 )
14	9 13	syl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) < 1 )
15	1	oveq2i	⊢ ( ( 𝑀 / 𝑁 ) − 𝑍 ) = ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) )
16	2 15	eqtri	⊢ 𝐹 = ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) )
17	16	a1i	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐹 = ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) )
18		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
19	18 7	dividd	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / 𝑁 ) = 1 )
20	19	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 / 𝑁 ) = 1 )
21	14 17 20	3brtr4d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐹 < ( 𝑁 / 𝑁 ) )
22		reflcl	⊢ ( ( 𝑀 / 𝑁 ) ∈ ℝ → ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℝ )
23	9 22	syl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℝ )
24	1 23	eqeltrid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑍 ∈ ℝ )
25	9 24	resubcld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 / 𝑁 ) − 𝑍 ) ∈ ℝ )
26	2 25	eqeltrid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐹 ∈ ℝ )
27		nngt0	⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
28	5 27	jca	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
29	28	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
30		ltmuldiv2	⊢ ( ( 𝐹 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑁 · 𝐹 ) < 𝑁 ↔ 𝐹 < ( 𝑁 / 𝑁 ) ) )
31	26 6 29 30	syl3anc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · 𝐹 ) < 𝑁 ↔ 𝐹 < ( 𝑁 / 𝑁 ) ) )
32	21 31	mpbird	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝐹 ) < 𝑁 )
33	2	oveq2i	⊢ ( 𝑁 · 𝐹 ) = ( 𝑁 · ( ( 𝑀 / 𝑁 ) − 𝑍 ) )
34	18	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
35	9	recnd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) ∈ ℂ )
36	9	flcld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℤ )
37	1 36	eqeltrid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑍 ∈ ℤ )
38	37	zcnd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑍 ∈ ℂ )
39	34 35 38	subdid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · ( ( 𝑀 / 𝑁 ) − 𝑍 ) ) = ( ( 𝑁 · ( 𝑀 / 𝑁 ) ) − ( 𝑁 · 𝑍 ) ) )
40	33 39	syl5eq	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝐹 ) = ( ( 𝑁 · ( 𝑀 / 𝑁 ) ) − ( 𝑁 · 𝑍 ) ) )
41		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
42	41	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℂ )
43	42 34 8	divcan2d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · ( 𝑀 / 𝑁 ) ) = 𝑀 )
44		simpl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℤ )
45	43 44	eqeltrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · ( 𝑀 / 𝑁 ) ) ∈ ℤ )
46		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
47	46	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
48	47 37	zmulcld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝑍 ) ∈ ℤ )
49	45 48	zsubcld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · ( 𝑀 / 𝑁 ) ) − ( 𝑁 · 𝑍 ) ) ∈ ℤ )
50	40 49	eqeltrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝐹 ) ∈ ℤ )
51		zltlem1	⊢ ( ( ( 𝑁 · 𝐹 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 · 𝐹 ) < 𝑁 ↔ ( 𝑁 · 𝐹 ) ≤ ( 𝑁 − 1 ) ) )
52	50 47 51	syl2anc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · 𝐹 ) < 𝑁 ↔ ( 𝑁 · 𝐹 ) ≤ ( 𝑁 − 1 ) ) )
53	32 52	mpbid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝐹 ) ≤ ( 𝑁 − 1 ) )
54		peano2rem	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
55	5 54	syl	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℝ )
56	55	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ℝ )
57		lemuldiv2	⊢ ( ( 𝐹 ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑁 · 𝐹 ) ≤ ( 𝑁 − 1 ) ↔ 𝐹 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ) )
58	26 56 29 57	syl3anc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · 𝐹 ) ≤ ( 𝑁 − 1 ) ↔ 𝐹 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ) )
59	53 58	mpbid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐹 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) )
60	11	simp3d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) )
61	12 59 60	3jca	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 0 ≤ 𝐹 ∧ 𝐹 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ∧ ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) ) )