Theorem fldiv

Description: Cancellation of the embedded floor of a real divided by an integer. (Contributed by NM, 16-Aug-2008)

	Ref	Expression
Assertion	fldiv	|- ( ( A e. RR /\ N e. NN ) -> ( |_ ` ( ( |_ ` A ) / N ) ) = ( |_ ` ( A / N ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( |_ ` A ) = ( |_ ` A )
2		eqid	|- ( A - ( |_ ` A ) ) = ( A - ( |_ ` A ) )
3	1 2	intfrac2	|- ( A e. RR -> ( 0 <_ ( A - ( |_ ` A ) ) /\ ( A - ( |_ ` A ) ) < 1 /\ A = ( ( |_ ` A ) + ( A - ( |_ ` A ) ) ) ) )
4	3	simp3d	|- ( A e. RR -> A = ( ( |_ ` A ) + ( A - ( |_ ` A ) ) ) )
5	4	adantr	|- ( ( A e. RR /\ N e. NN ) -> A = ( ( |_ ` A ) + ( A - ( |_ ` A ) ) ) )
6	5	oveq1d	|- ( ( A e. RR /\ N e. NN ) -> ( A / N ) = ( ( ( |_ ` A ) + ( A - ( |_ ` A ) ) ) / N ) )
7		reflcl	|- ( A e. RR -> ( |_ ` A ) e. RR )
8	7	recnd	|- ( A e. RR -> ( |_ ` A ) e. CC )
9		resubcl	|- ( ( A e. RR /\ ( |_ ` A ) e. RR ) -> ( A - ( |_ ` A ) ) e. RR )
10	7 9	mpdan	|- ( A e. RR -> ( A - ( |_ ` A ) ) e. RR )
11	10	recnd	|- ( A e. RR -> ( A - ( |_ ` A ) ) e. CC )
12		nncn	|- ( N e. NN -> N e. CC )
13		nnne0	|- ( N e. NN -> N =/= 0 )
14	12 13	jca	|- ( N e. NN -> ( N e. CC /\ N =/= 0 ) )
15		divdir	|- ( ( ( |_ ` A ) e. CC /\ ( A - ( |_ ` A ) ) e. CC /\ ( N e. CC /\ N =/= 0 ) ) -> ( ( ( |_ ` A ) + ( A - ( |_ ` A ) ) ) / N ) = ( ( ( |_ ` A ) / N ) + ( ( A - ( |_ ` A ) ) / N ) ) )
16	8 11 14 15	syl2an3an	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( |_ ` A ) + ( A - ( |_ ` A ) ) ) / N ) = ( ( ( |_ ` A ) / N ) + ( ( A - ( |_ ` A ) ) / N ) ) )
17	6 16	eqtrd	|- ( ( A e. RR /\ N e. NN ) -> ( A / N ) = ( ( ( |_ ` A ) / N ) + ( ( A - ( |_ ` A ) ) / N ) ) )
18		flcl	|- ( A e. RR -> ( |_ ` A ) e. ZZ )
19		eqid	|- ( |_ ` ( ( |_ ` A ) / N ) ) = ( |_ ` ( ( |_ ` A ) / N ) )
20		eqid	|- ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) = ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) )
21	19 20	intfracq	|- ( ( ( |_ ` A ) e. ZZ /\ N e. NN ) -> ( 0 <_ ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) /\ ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) <_ ( ( N - 1 ) / N ) /\ ( ( |_ ` A ) / N ) = ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) ) ) )
22	21	simp3d	|- ( ( ( |_ ` A ) e. ZZ /\ N e. NN ) -> ( ( |_ ` A ) / N ) = ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) ) )
23	18 22	sylan	|- ( ( A e. RR /\ N e. NN ) -> ( ( |_ ` A ) / N ) = ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) ) )
24	23	oveq1d	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( |_ ` A ) / N ) + ( ( A - ( |_ ` A ) ) / N ) ) = ( ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) )
25	7	adantr	|- ( ( A e. RR /\ N e. NN ) -> ( |_ ` A ) e. RR )
26		nnre	|- ( N e. NN -> N e. RR )
27	26	adantl	|- ( ( A e. RR /\ N e. NN ) -> N e. RR )
28	13	adantl	|- ( ( A e. RR /\ N e. NN ) -> N =/= 0 )
29	25 27 28	redivcld	|- ( ( A e. RR /\ N e. NN ) -> ( ( |_ ` A ) / N ) e. RR )
30		reflcl	|- ( ( ( |_ ` A ) / N ) e. RR -> ( |_ ` ( ( |_ ` A ) / N ) ) e. RR )
31	29 30	syl	|- ( ( A e. RR /\ N e. NN ) -> ( |_ ` ( ( |_ ` A ) / N ) ) e. RR )
32	31	recnd	|- ( ( A e. RR /\ N e. NN ) -> ( |_ ` ( ( |_ ` A ) / N ) ) e. CC )
33	29 31	resubcld	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) e. RR )
34	33	recnd	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) e. CC )
35	10	adantr	|- ( ( A e. RR /\ N e. NN ) -> ( A - ( |_ ` A ) ) e. RR )
36	35 27 28	redivcld	|- ( ( A e. RR /\ N e. NN ) -> ( ( A - ( |_ ` A ) ) / N ) e. RR )
37	36	recnd	|- ( ( A e. RR /\ N e. NN ) -> ( ( A - ( |_ ` A ) ) / N ) e. CC )
38	32 34 37	addassd	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) = ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) ) )
39	17 24 38	3eqtrd	|- ( ( A e. RR /\ N e. NN ) -> ( A / N ) = ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) ) )
40	39	fveq2d	|- ( ( A e. RR /\ N e. NN ) -> ( |_ ` ( A / N ) ) = ( |_ ` ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) ) ) )
41	21	simp1d	|- ( ( ( |_ ` A ) e. ZZ /\ N e. NN ) -> 0 <_ ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) )
42	18 41	sylan	|- ( ( A e. RR /\ N e. NN ) -> 0 <_ ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) )
43		fracge0	|- ( A e. RR -> 0 <_ ( A - ( |_ ` A ) ) )
44	10 43	jca	|- ( A e. RR -> ( ( A - ( |_ ` A ) ) e. RR /\ 0 <_ ( A - ( |_ ` A ) ) ) )
45		nngt0	|- ( N e. NN -> 0 < N )
46	26 45	jca	|- ( N e. NN -> ( N e. RR /\ 0 < N ) )
47		divge0	|- ( ( ( ( A - ( |_ ` A ) ) e. RR /\ 0 <_ ( A - ( |_ ` A ) ) ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( ( A - ( |_ ` A ) ) / N ) )
48	44 46 47	syl2an	|- ( ( A e. RR /\ N e. NN ) -> 0 <_ ( ( A - ( |_ ` A ) ) / N ) )
49	33 36 42 48	addge0d	|- ( ( A e. RR /\ N e. NN ) -> 0 <_ ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) )
50		peano2rem	|- ( N e. RR -> ( N - 1 ) e. RR )
51	26 50	syl	|- ( N e. NN -> ( N - 1 ) e. RR )
52	51 26 13	redivcld	|- ( N e. NN -> ( ( N - 1 ) / N ) e. RR )
53		nnrecre	|- ( N e. NN -> ( 1 / N ) e. RR )
54	52 53	jca	|- ( N e. NN -> ( ( ( N - 1 ) / N ) e. RR /\ ( 1 / N ) e. RR ) )
55	54	adantl	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( N - 1 ) / N ) e. RR /\ ( 1 / N ) e. RR ) )
56	33 36 55	jca31	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) e. RR /\ ( ( A - ( |_ ` A ) ) / N ) e. RR ) /\ ( ( ( N - 1 ) / N ) e. RR /\ ( 1 / N ) e. RR ) ) )
57	21	simp2d	|- ( ( ( |_ ` A ) e. ZZ /\ N e. NN ) -> ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) <_ ( ( N - 1 ) / N ) )
58	18 57	sylan	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) <_ ( ( N - 1 ) / N ) )
59		fraclt1	|- ( A e. RR -> ( A - ( |_ ` A ) ) < 1 )
60	59	adantr	|- ( ( A e. RR /\ N e. NN ) -> ( A - ( |_ ` A ) ) < 1 )
61		1re	|- 1 e. RR
62		ltdiv1	|- ( ( ( A - ( |_ ` A ) ) e. RR /\ 1 e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( A - ( |_ ` A ) ) < 1 <-> ( ( A - ( |_ ` A ) ) / N ) < ( 1 / N ) ) )
63	61 62	mp3an2	|- ( ( ( A - ( |_ ` A ) ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( A - ( |_ ` A ) ) < 1 <-> ( ( A - ( |_ ` A ) ) / N ) < ( 1 / N ) ) )
64	10 46 63	syl2an	|- ( ( A e. RR /\ N e. NN ) -> ( ( A - ( |_ ` A ) ) < 1 <-> ( ( A - ( |_ ` A ) ) / N ) < ( 1 / N ) ) )
65	60 64	mpbid	|- ( ( A e. RR /\ N e. NN ) -> ( ( A - ( |_ ` A ) ) / N ) < ( 1 / N ) )
66	58 65	jca	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) <_ ( ( N - 1 ) / N ) /\ ( ( A - ( |_ ` A ) ) / N ) < ( 1 / N ) ) )
67		leltadd	|- ( ( ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) e. RR /\ ( ( A - ( |_ ` A ) ) / N ) e. RR ) /\ ( ( ( N - 1 ) / N ) e. RR /\ ( 1 / N ) e. RR ) ) -> ( ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) <_ ( ( N - 1 ) / N ) /\ ( ( A - ( |_ ` A ) ) / N ) < ( 1 / N ) ) -> ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) < ( ( ( N - 1 ) / N ) + ( 1 / N ) ) ) )
68	56 66 67	sylc	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) < ( ( ( N - 1 ) / N ) + ( 1 / N ) ) )
69		ax-1cn	|- 1 e. CC
70		npcan	|- ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
71	12 69 70	sylancl	|- ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
72	71	oveq1d	|- ( N e. NN -> ( ( ( N - 1 ) + 1 ) / N ) = ( N / N ) )
73	51	recnd	|- ( N e. NN -> ( N - 1 ) e. CC )
74		divdir	|- ( ( ( N - 1 ) e. CC /\ 1 e. CC /\ ( N e. CC /\ N =/= 0 ) ) -> ( ( ( N - 1 ) + 1 ) / N ) = ( ( ( N - 1 ) / N ) + ( 1 / N ) ) )
75	69 74	mp3an2	|- ( ( ( N - 1 ) e. CC /\ ( N e. CC /\ N =/= 0 ) ) -> ( ( ( N - 1 ) + 1 ) / N ) = ( ( ( N - 1 ) / N ) + ( 1 / N ) ) )
76	73 12 13 75	syl12anc	|- ( N e. NN -> ( ( ( N - 1 ) + 1 ) / N ) = ( ( ( N - 1 ) / N ) + ( 1 / N ) ) )
77	12 13	dividd	|- ( N e. NN -> ( N / N ) = 1 )
78	72 76 77	3eqtr3d	|- ( N e. NN -> ( ( ( N - 1 ) / N ) + ( 1 / N ) ) = 1 )
79	78	adantl	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( N - 1 ) / N ) + ( 1 / N ) ) = 1 )
80	68 79	breqtrd	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) < 1 )
81	29	flcld	|- ( ( A e. RR /\ N e. NN ) -> ( |_ ` ( ( |_ ` A ) / N ) ) e. ZZ )
82	33 36	readdcld	|- ( ( A e. RR /\ N e. NN ) -> ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) e. RR )
83		flbi2	|- ( ( ( |_ ` ( ( |_ ` A ) / N ) ) e. ZZ /\ ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) e. RR ) -> ( ( |_ ` ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) ) ) = ( |_ ` ( ( |_ ` A ) / N ) ) <-> ( 0 <_ ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) /\ ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) < 1 ) ) )
84	81 82 83	syl2anc	|- ( ( A e. RR /\ N e. NN ) -> ( ( |_ ` ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) ) ) = ( |_ ` ( ( |_ ` A ) / N ) ) <-> ( 0 <_ ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) /\ ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) < 1 ) ) )
85	49 80 84	mpbir2and	|- ( ( A e. RR /\ N e. NN ) -> ( |_ ` ( ( |_ ` ( ( |_ ` A ) / N ) ) + ( ( ( ( |_ ` A ) / N ) - ( |_ ` ( ( |_ ` A ) / N ) ) ) + ( ( A - ( |_ ` A ) ) / N ) ) ) ) = ( |_ ` ( ( |_ ` A ) / N ) ) )
86	40 85	eqtr2d	|- ( ( A e. RR /\ N e. NN ) -> ( |_ ` ( ( |_ ` A ) / N ) ) = ( |_ ` ( A / N ) ) )