Theorem intfracqOLD 6255

Description: Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfracOLD 6254.

Hypotheses

Ref	Expression
intfracq.1	|- Z = (|_` (M / N))
intfracq.2	|- F = ((M / N) - Z)

Assertion

Ref	Expression
intfracqOLD	|- ((M e. ZZ /\ N e. NN) -> ((Z e. ZZ /\ 0 <_ F) /\ (F <_ ((N - 1) / N) /\ (M / N) = (Z + F))))

Proof of Theorem intfracqOLD

Step	Hyp	Ref	Expression
1		pm3.26 319	. . . . . 6 |- ((F <_ ((N - 1) / N) /\ F < 1) -> F <_ ((N - 1) / N))
2	1	anim1i 334	. . . . 5 |- (((F <_ ((N - 1) / N) /\ F < 1) /\ (M / N) = (Z + F)) -> (F <_ ((N - 1) / N) /\ (M / N) = (Z + F)))
3	2	anasss 440	. . . 4 |- ((F <_ ((N - 1) / N) /\ (F < 1 /\ (M / N) = (Z + F))) -> (F <_ ((N - 1) / N) /\ (M / N) = (Z + F)))
4	3	anim2i 335	. . 3 |- (((Z e. ZZ /\ 0 <_ F) /\ (F <_ ((N - 1) / N) /\ (F < 1 /\ (M / N) = (Z + F)))) -> ((Z e. ZZ /\ 0 <_ F) /\ (F <_ ((N - 1) / N) /\ (M / N) = (Z + F))))
5	4	an1s 486	. 2 |- ((F <_ ((N - 1) / N) /\ ((Z e. ZZ /\ 0 <_ F) /\ (F < 1 /\ (M / N) = (Z + F)))) -> ((Z e. ZZ /\ 0 <_ F) /\ (F <_ ((N - 1) / N) /\ (M / N) = (Z + F))))
6		redivclt 5800	. . . . . . . 8 |- ((M e. RR /\ N e. RR /\ N =/= 0) -> (M / N) e. RR)
7		zret 6139	. . . . . . . . 9 |- (M e. ZZ -> M e. RR)
8	7	adantr 389	. . . . . . . 8 |- ((M e. ZZ /\ N e. NN) -> M e. RR)
9		nnret 5929	. . . . . . . . 9 |- (N e. NN -> N e. RR)
10	9	adantl 388	. . . . . . . 8 |- ((M e. ZZ /\ N e. NN) -> N e. RR)
11		nnne0t 5949	. . . . . . . . 9 |- (N e. NN -> N =/= 0)
12	11	adantl 388	. . . . . . . 8 |- ((M e. ZZ /\ N e. NN) -> N =/= 0)
13	6, 8, 10, 12	syl3anc 858	. . . . . . 7 |- ((M e. ZZ /\ N e. NN) -> (M / N) e. RR)
14		fraclt1t 6231	. . . . . . 7 |- ((M / N) e. RR -> ((M / N) - (|_` (M / N))) < 1)
15	13, 14	syl 10	. . . . . 6 |- ((M e. ZZ /\ N e. NN) -> ((M / N) - (|_` (M / N))) < 1)
16		intfracq.2	. . . . . . . 8 |- F = ((M / N) - Z)
17		intfracq.1	. . . . . . . . 9 |- Z = (|_` (M / N))
18	17	opreq2i 3972	. . . . . . . 8 |- ((M / N) - Z) = ((M / N) - (|_` (M / N)))
19	16, 18	eqtr 1495	. . . . . . 7 |- F = ((M / N) - (|_` (M / N)))
20	19	a1i 8	. . . . . 6 |- ((M e. ZZ /\ N e. NN) -> F = ((M / N) - (|_` (M / N))))
21		dividt 5766	. . . . . . . 8 |- ((N e. CC /\ N =/= 0) -> (N / N) = 1)
22		nncnt 5930	. . . . . . . 8 |- (N e. NN -> N e. CC)
23	21, 22, 11	sylanc 471	. . . . . . 7 |- (N e. NN -> (N / N) = 1)
24	23	adantl 388	. . . . . 6 |- ((M e. ZZ /\ N e. NN) -> (N / N) = 1)
25	15, 20, 24	3brtr4d 2645	. . . . 5 |- ((M e. ZZ /\ N e. NN) -> F < (N / N))
26		ltmuldiv2t 5865	. . . . . 6 |- ((F e. RR /\ N e. RR /\ (N e. RR /\ 0 < N)) -> ((N x. F) < N <-> F < (N / N)))
27		resubclt 5438	. . . . . . . 8 |- (((M / N) e. RR /\ Z e. RR) -> ((M / N) - Z) e. RR)
28		flreclt 6227	. . . . . . . . . 10 |- ((M / N) e. RR -> (|_` (M / N)) e. RR)
29	13, 28	syl 10	. . . . . . . . 9 |- ((M e. ZZ /\ N e. NN) -> (|_` (M / N)) e. RR)
30	29, 17	syl5eqel 1552	. . . . . . . 8 |- ((M e. ZZ /\ N e. NN) -> Z e. RR)
31	27, 13, 30	sylanc 471	. . . . . . 7 |- ((M e. ZZ /\ N e. NN) -> ((M / N) - Z) e. RR)
32	31, 16	syl5eqel 1552	. . . . . 6 |- ((M e. ZZ /\ N e. NN) -> F e. RR)
33		nngt0t 5946	. . . . . . . 8 |- (N e. NN -> 0 < N)
34	9, 33	jca 288	. . . . . . 7 |- (N e. NN -> (N e. RR /\ 0 < N))
35	34	adantl 388	. . . . . 6 |- ((M e. ZZ /\ N e. NN) -> (N e. RR /\ 0 < N))
36	26, 32, 10, 35	syl3anc 858	. . . . 5 |- ((M e. ZZ /\ N e. NN) -> ((N x. F) < N <-> F < (N / N)))
37	25, 36	mpbird 196	. . . 4 |- ((M e. ZZ /\ N e. NN) -> (N x. F) < N)
38		zltlem1t 6184	. . . . 5 |- (((N x. F) e. ZZ /\ N e. ZZ) -> ((N x. F) < N <-> (N x. F) <_ (N - 1)))
39		subdit 5427	. . . . . . . 8 |- ((N e. CC /\ (M / N) e. CC /\ Z e. CC) -> (N x. ((M / N) - Z)) = ((N x. (M / N)) - (N x. Z)))
40	22	adantl 388	. . . . . . . 8 |- ((M e. ZZ /\ N e. NN) -> N e. CC)
41	13	recnd 5315	. . . . . . . 8 |- ((M e. ZZ /\ N e. NN) -> (M / N) e. CC)
42	17, 16	intfracOLD 6254	. . . . . . . . . . . 12 |- ((M / N) e. RR -> ((Z e. ZZ /\ 0 <_ F) /\ (F < 1 /\ (M / N) = (Z + F))))
43	42	pm3.26d 321	. . . . . . . . . . 11 |- ((M / N) e. RR -> (Z e. ZZ /\ 0 <_ F))
44	43	pm3.26d 321	. . . . . . . . . 10 |- ((M / N) e. RR -> Z e. ZZ)
45	13, 44	syl 10	. . . . . . . . 9 |- ((M e. ZZ /\ N e. NN) -> Z e. ZZ)
46		zcnt 6140	. . . . . . . . 9 |- (Z e. ZZ -> Z e. CC)
47	45, 46	syl 10	. . . . . . . 8 |- ((M e. ZZ /\ N e. NN) -> Z e. CC)
48	39, 40, 41, 47	syl3anc 858	. . . . . . 7 |- ((M e. ZZ /\ N e. NN) -> (N x. ((M / N) - Z)) = ((N x. (M / N)) - (N x. Z)))
49	16	opreq2i 3972	. . . . . . 7 |- (N x. F) = (N x. ((M / N) - Z))
50	48, 49	syl5eq 1519	. . . . . 6 |- ((M e. ZZ /\ N e. NN) -> (N x. F) = ((N x. (M / N)) - (N x. Z)))
51		zsubclt 6168	. . . . . . 7 |- (((N x. (M / N)) e. ZZ /\ (N x. Z) e. ZZ) -> ((N x. (M / N)) - (N x. Z)) e. ZZ)
52		divcan2tOLD 5727	. . . . . . . . 9 |- ((N e. CC /\ M e. CC /\ N =/= 0) -> (N x. (M / N)) = M)
53		zcnt 6140	. . . . . . . . . 10 |- (M e. ZZ -> M e. CC)
54	53	adantr 389	. . . . . . . . 9 |- ((M e. ZZ /\ N e. NN) -> M e. CC)
55	52, 40, 54, 12	syl3anc 858	. . . . . . . 8 |- ((M e. ZZ /\ N e. NN) -> (N x. (M / N)) = M)
56		pm3.26 319	. . . . . . . 8 |- ((M e. ZZ /\ N e. NN) -> M e. ZZ)
57	55, 56	eqeltrd 1548	. . . . . . 7 |- ((M e. ZZ /\ N e. NN) -> (N x. (M / N)) e. ZZ)
58		zmulclt 6180	. . . . . . . 8 |- ((N e. ZZ /\ Z e. ZZ) -> (N x. Z) e. ZZ)
59		nnzt 6153	. . . . . . . . 9 |- (N e. NN -> N e. ZZ)
60	59	adantl 388	. . . . . . . 8 |- ((M e. ZZ /\ N e. NN) -> N e. ZZ)
61	58, 60, 45	sylanc 471	. . . . . . 7 |- ((M e. ZZ /\ N e. NN) -> (N x. Z) e. ZZ)
62	51, 57, 61	sylanc 471	. . . . . 6 |- ((M e. ZZ /\ N e. NN) -> ((N x. (M / N)) - (N x. Z)) e. ZZ)
63	50, 62	eqeltrd 1548	. . . . 5 |- ((M e. ZZ /\ N e. NN) -> (N x. F) e. ZZ)
64	38, 63, 60	sylanc 471	. . . 4 |- ((M e. ZZ /\ N e. NN) -> ((N x. F) < N <-> (N x. F) <_ (N - 1)))
65	37, 64	mpbid 195	. . 3 |- ((M e. ZZ /\ N e. NN) -> (N x. F) <_ (N - 1))
66		lemuldiv2t 5876	. . . 4 |- ((F e. RR /\ (N - 1) e. RR /\ (N e. RR /\ 0 < N)) -> ((N x. F) <_ (N - 1) <-> F <_ ((N - 1) / N)))
67		peano2rem 5442	. . . . . 6 |- (N e. RR -> (N - 1) e. RR)
68	9, 67	syl 10	. . . . 5 |- (N e. NN -> (N - 1) e. RR)
69	68	adantl 388	. . . 4 |- ((M e. ZZ /\ N e. NN) -> (N - 1) e. RR)
70	66, 32, 69, 35	syl3anc 858	. . 3 |- ((M e. ZZ /\ N e. NN) -> ((N x. F) <_ (N - 1) <-> F <_ ((N - 1) / N)))
71	65, 70	mpbid 195	. 2 |- ((M e. ZZ /\ N e. NN) -> F <_ ((N - 1) / N))
72	13, 42	syl 10	. 2 |- ((M e. ZZ /\ N e. NN) -> ((Z e. ZZ /\ 0 <_ F) /\ (F < 1 /\ (M / N) = (Z + F))))
73	5, 71, 72	sylanc 471	1 |- ((M e. ZZ /\ N e. NN) -> ((Z e. ZZ /\ 0 <_ F) /\ (F <_ ((N - 1