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

Metamath Proof Explorer

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 ) ) )