Metamath Proof Explorer

Theorem fldivp1

Description: The difference between the floors of adjacent fractions is either 1 or 0. (Contributed by Mario Carneiro, 8-Mar-2014)

Ref Expression
Assertion fldivp1 
|- ( ( M e. ZZ /\ N e. NN ) -> ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = if ( N || ( M + 1 ) , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( N e. NN -> N e. ZZ )
2 nnne0 
 |-  ( N e. NN -> N =/= 0 )
3 peano2z 
 |-  ( M e. ZZ -> ( M + 1 ) e. ZZ )
4 3 adantr 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M + 1 ) e. ZZ )
5 dvdsval2 
 |-  ( ( N e. ZZ /\ N =/= 0 /\ ( M + 1 ) e. ZZ ) -> ( N || ( M + 1 ) <-> ( ( M + 1 ) / N ) e. ZZ ) )
6 1 2 4 5 syl2an23an 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N || ( M + 1 ) <-> ( ( M + 1 ) / N ) e. ZZ ) )
7 6 biimpa 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( ( M + 1 ) / N ) e. ZZ )
8 flid 
 |-  ( ( ( M + 1 ) / N ) e. ZZ -> ( |_ ` ( ( M + 1 ) / N ) ) = ( ( M + 1 ) / N ) )
9 7 8 syl 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( |_ ` ( ( M + 1 ) / N ) ) = ( ( M + 1 ) / N ) )
10 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
11 10 nn0red 
 |-  ( N e. NN -> ( N - 1 ) e. RR )
12 10 nn0ge0d 
 |-  ( N e. NN -> 0 <_ ( N - 1 ) )
13 nnre 
 |-  ( N e. NN -> N e. RR )
14 nngt0 
 |-  ( N e. NN -> 0 < N )
15 divge0 
 |-  ( ( ( ( N - 1 ) e. RR /\ 0 <_ ( N - 1 ) ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( ( N - 1 ) / N ) )
16 11 12 13 14 15 syl22anc 
 |-  ( N e. NN -> 0 <_ ( ( N - 1 ) / N ) )
17 16 ad2antlr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> 0 <_ ( ( N - 1 ) / N ) )
18 13 ltm1d 
 |-  ( N e. NN -> ( N - 1 ) < N )
19 nncn 
 |-  ( N e. NN -> N e. CC )
20 19 mulid1d 
 |-  ( N e. NN -> ( N x. 1 ) = N )
21 18 20 breqtrrd 
 |-  ( N e. NN -> ( N - 1 ) < ( N x. 1 ) )
22 1re 
 |-  1 e. RR
23 22 a1i 
 |-  ( N e. NN -> 1 e. RR )
24 ltdivmul 
 |-  ( ( ( N - 1 ) e. RR /\ 1 e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( ( N - 1 ) / N ) < 1 <-> ( N - 1 ) < ( N x. 1 ) ) )
25 11 23 13 14 24 syl112anc 
 |-  ( N e. NN -> ( ( ( N - 1 ) / N ) < 1 <-> ( N - 1 ) < ( N x. 1 ) ) )
26 21 25 mpbird 
 |-  ( N e. NN -> ( ( N - 1 ) / N ) < 1 )
27 26 ad2antlr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( ( N - 1 ) / N ) < 1 )
28 nndivre 
 |-  ( ( ( N - 1 ) e. RR /\ N e. NN ) -> ( ( N - 1 ) / N ) e. RR )
29 11 28 mpancom 
 |-  ( N e. NN -> ( ( N - 1 ) / N ) e. RR )
30 29 ad2antlr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( ( N - 1 ) / N ) e. RR )
31 flbi2 
 |-  ( ( ( ( M + 1 ) / N ) e. ZZ /\ ( ( N - 1 ) / N ) e. RR ) -> ( ( |_ ` ( ( ( M + 1 ) / N ) + ( ( N - 1 ) / N ) ) ) = ( ( M + 1 ) / N ) <-> ( 0 <_ ( ( N - 1 ) / N ) /\ ( ( N - 1 ) / N ) < 1 ) ) )
32 7 30 31 syl2anc 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( ( |_ ` ( ( ( M + 1 ) / N ) + ( ( N - 1 ) / N ) ) ) = ( ( M + 1 ) / N ) <-> ( 0 <_ ( ( N - 1 ) / N ) /\ ( ( N - 1 ) / N ) < 1 ) ) )
33 17 27 32 mpbir2and 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( |_ ` ( ( ( M + 1 ) / N ) + ( ( N - 1 ) / N ) ) ) = ( ( M + 1 ) / N ) )
34 9 33 eqtr4d 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( |_ ` ( ( M + 1 ) / N ) ) = ( |_ ` ( ( ( M + 1 ) / N ) + ( ( N - 1 ) / N ) ) ) )
35 zcn 
 |-  ( M e. ZZ -> M e. CC )
36 35 adantr 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M e. CC )
37 ax-1cn 
 |-  1 e. CC
38 37 a1i 
 |-  ( ( M e. ZZ /\ N e. NN ) -> 1 e. CC )
39 19 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N e. CC )
40 36 38 39 ppncand 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M + 1 ) + ( N - 1 ) ) = ( M + N ) )
41 40 oveq1d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) + ( N - 1 ) ) / N ) = ( ( M + N ) / N ) )
42 4 zcnd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M + 1 ) e. CC )
43 subcl 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( N - 1 ) e. CC )
44 19 37 43 sylancl 
 |-  ( N e. NN -> ( N - 1 ) e. CC )
45 44 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N - 1 ) e. CC )
46 2 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N =/= 0 )
47 42 45 39 46 divdird 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) + ( N - 1 ) ) / N ) = ( ( ( M + 1 ) / N ) + ( ( N - 1 ) / N ) ) )
48 41 47 eqtr3d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M + N ) / N ) = ( ( ( M + 1 ) / N ) + ( ( N - 1 ) / N ) ) )
49 36 39 39 46 divdird 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M + N ) / N ) = ( ( M / N ) + ( N / N ) ) )
50 48 49 eqtr3d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) / N ) + ( ( N - 1 ) / N ) ) = ( ( M / N ) + ( N / N ) ) )
51 39 46 dividd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N / N ) = 1 )
52 51 oveq2d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M / N ) + ( N / N ) ) = ( ( M / N ) + 1 ) )
53 50 52 eqtrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) / N ) + ( ( N - 1 ) / N ) ) = ( ( M / N ) + 1 ) )
54 53 fveq2d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( ( ( M + 1 ) / N ) + ( ( N - 1 ) / N ) ) ) = ( |_ ` ( ( M / N ) + 1 ) ) )
55 54 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( |_ ` ( ( ( M + 1 ) / N ) + ( ( N - 1 ) / N ) ) ) = ( |_ ` ( ( M / N ) + 1 ) ) )
56 zre 
 |-  ( M e. ZZ -> M e. RR )
57 nndivre 
 |-  ( ( M e. RR /\ N e. NN ) -> ( M / N ) e. RR )
58 56 57 sylan 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M / N ) e. RR )
59 1z 
 |-  1 e. ZZ
60 fladdz 
 |-  ( ( ( M / N ) e. RR /\ 1 e. ZZ ) -> ( |_ ` ( ( M / N ) + 1 ) ) = ( ( |_ ` ( M / N ) ) + 1 ) )
61 58 59 60 sylancl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( ( M / N ) + 1 ) ) = ( ( |_ ` ( M / N ) ) + 1 ) )
62 61 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( |_ ` ( ( M / N ) + 1 ) ) = ( ( |_ ` ( M / N ) ) + 1 ) )
63 34 55 62 3eqtrrd 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( ( |_ ` ( M / N ) ) + 1 ) = ( |_ ` ( ( M + 1 ) / N ) ) )
64 zre 
 |-  ( ( M + 1 ) e. ZZ -> ( M + 1 ) e. RR )
65 3 64 syl 
 |-  ( M e. ZZ -> ( M + 1 ) e. RR )
66 nndivre 
 |-  ( ( ( M + 1 ) e. RR /\ N e. NN ) -> ( ( M + 1 ) / N ) e. RR )
67 65 66 sylan 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M + 1 ) / N ) e. RR )
68 67 flcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( ( M + 1 ) / N ) ) e. ZZ )
69 68 zcnd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( ( M + 1 ) / N ) ) e. CC )
70 58 flcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( M / N ) ) e. ZZ )
71 70 zcnd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( M / N ) ) e. CC )
72 69 71 38 subaddd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = 1 <-> ( ( |_ ` ( M / N ) ) + 1 ) = ( |_ ` ( ( M + 1 ) / N ) ) ) )
73 72 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = 1 <-> ( ( |_ ` ( M / N ) ) + 1 ) = ( |_ ` ( ( M + 1 ) / N ) ) ) )
74 63 73 mpbird 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = 1 )
75 iftrue 
 |-  ( N || ( M + 1 ) -> if ( N || ( M + 1 ) , 1 , 0 ) = 1 )
76 75 adantl 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> if ( N || ( M + 1 ) , 1 , 0 ) = 1 )
77 74 76 eqtr4d 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ N || ( M + 1 ) ) -> ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = if ( N || ( M + 1 ) , 1 , 0 ) )
78 zmodcl 
 |-  ( ( ( M + 1 ) e. ZZ /\ N e. NN ) -> ( ( M + 1 ) mod N ) e. NN0 )
79 3 78 sylan 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M + 1 ) mod N ) e. NN0 )
80 79 nn0red 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M + 1 ) mod N ) e. RR )
81 resubcl 
 |-  ( ( ( ( M + 1 ) mod N ) e. RR /\ 1 e. RR ) -> ( ( ( M + 1 ) mod N ) - 1 ) e. RR )
82 80 22 81 sylancl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) mod N ) - 1 ) e. RR )
83 82 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( ( ( M + 1 ) mod N ) - 1 ) e. RR )
84 elnn0 
 |-  ( ( ( M + 1 ) mod N ) e. NN0 <-> ( ( ( M + 1 ) mod N ) e. NN \/ ( ( M + 1 ) mod N ) = 0 ) )
85 79 84 sylib 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) mod N ) e. NN \/ ( ( M + 1 ) mod N ) = 0 ) )
86 85 ord 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( -. ( ( M + 1 ) mod N ) e. NN -> ( ( M + 1 ) mod N ) = 0 ) )
87 id 
 |-  ( N e. NN -> N e. NN )
88 dvdsval3 
 |-  ( ( N e. NN /\ ( M + 1 ) e. ZZ ) -> ( N || ( M + 1 ) <-> ( ( M + 1 ) mod N ) = 0 ) )
89 87 3 88 syl2anr 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N || ( M + 1 ) <-> ( ( M + 1 ) mod N ) = 0 ) )
90 86 89 sylibrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( -. ( ( M + 1 ) mod N ) e. NN -> N || ( M + 1 ) ) )
91 90 con1d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( -. N || ( M + 1 ) -> ( ( M + 1 ) mod N ) e. NN ) )
92 91 imp 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( ( M + 1 ) mod N ) e. NN )
93 nnm1nn0 
 |-  ( ( ( M + 1 ) mod N ) e. NN -> ( ( ( M + 1 ) mod N ) - 1 ) e. NN0 )
94 92 93 syl 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( ( ( M + 1 ) mod N ) - 1 ) e. NN0 )
95 94 nn0ge0d 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> 0 <_ ( ( ( M + 1 ) mod N ) - 1 ) )
96 13 14 jca 
 |-  ( N e. NN -> ( N e. RR /\ 0 < N ) )
97 96 ad2antlr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( N e. RR /\ 0 < N ) )
98 divge0 
 |-  ( ( ( ( ( ( M + 1 ) mod N ) - 1 ) e. RR /\ 0 <_ ( ( ( M + 1 ) mod N ) - 1 ) ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) )
99 83 95 97 98 syl21anc 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> 0 <_ ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) )
100 13 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N e. RR )
101 80 ltm1d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) mod N ) - 1 ) < ( ( M + 1 ) mod N ) )
102 nnrp 
 |-  ( N e. NN -> N e. RR+ )
103 modlt 
 |-  ( ( ( M + 1 ) e. RR /\ N e. RR+ ) -> ( ( M + 1 ) mod N ) < N )
104 65 102 103 syl2an 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M + 1 ) mod N ) < N )
105 82 80 100 101 104 lttrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) mod N ) - 1 ) < N )
106 39 mulid1d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. 1 ) = N )
107 105 106 breqtrrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) mod N ) - 1 ) < ( N x. 1 ) )
108 22 a1i 
 |-  ( ( M e. ZZ /\ N e. NN ) -> 1 e. RR )
109 14 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> 0 < N )
110 ltdivmul 
 |-  ( ( ( ( ( M + 1 ) mod N ) - 1 ) e. RR /\ 1 e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) < 1 <-> ( ( ( M + 1 ) mod N ) - 1 ) < ( N x. 1 ) ) )
111 82 108 100 109 110 syl112anc 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) < 1 <-> ( ( ( M + 1 ) mod N ) - 1 ) < ( N x. 1 ) ) )
112 107 111 mpbird 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) < 1 )
113 112 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) < 1 )
114 nndivre 
 |-  ( ( ( ( ( M + 1 ) mod N ) - 1 ) e. RR /\ N e. NN ) -> ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) e. RR )
115 82 114 sylancom 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) e. RR )
116 flbi2 
 |-  ( ( ( |_ ` ( ( M + 1 ) / N ) ) e. ZZ /\ ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) e. RR ) -> ( ( |_ ` ( ( |_ ` ( ( M + 1 ) / N ) ) + ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) ) ) = ( |_ ` ( ( M + 1 ) / N ) ) <-> ( 0 <_ ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) /\ ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) < 1 ) ) )
117 68 115 116 syl2anc 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( |_ ` ( ( |_ ` ( ( M + 1 ) / N ) ) + ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) ) ) = ( |_ ` ( ( M + 1 ) / N ) ) <-> ( 0 <_ ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) /\ ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) < 1 ) ) )
118 117 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( ( |_ ` ( ( |_ ` ( ( M + 1 ) / N ) ) + ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) ) ) = ( |_ ` ( ( M + 1 ) / N ) ) <-> ( 0 <_ ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) /\ ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) < 1 ) ) )
119 99 113 118 mpbir2and 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( |_ ` ( ( |_ ` ( ( M + 1 ) / N ) ) + ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) ) ) = ( |_ ` ( ( M + 1 ) / N ) ) )
120 modval 
 |-  ( ( ( M + 1 ) e. RR /\ N e. RR+ ) -> ( ( M + 1 ) mod N ) = ( ( M + 1 ) - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) )
121 65 102 120 syl2an 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M + 1 ) mod N ) = ( ( M + 1 ) - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) )
122 121 oveq1d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) mod N ) - 1 ) = ( ( ( M + 1 ) - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) - 1 ) )
123 39 69 mulcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) e. CC )
124 42 38 123 sub32d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) - 1 ) - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) = ( ( ( M + 1 ) - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) - 1 ) )
125 122 124 eqtr4d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) mod N ) - 1 ) = ( ( ( M + 1 ) - 1 ) - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) )
126 pncan 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M + 1 ) - 1 ) = M )
127 36 37 126 sylancl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M + 1 ) - 1 ) = M )
128 127 oveq1d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) - 1 ) - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) = ( M - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) )
129 125 128 eqtrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M + 1 ) mod N ) - 1 ) = ( M - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) )
130 129 oveq1d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) = ( ( M - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) / N ) )
131 36 123 39 46 divsubdird 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M - ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) ) / N ) = ( ( M / N ) - ( ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) / N ) ) )
132 69 39 46 divcan3d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) / N ) = ( |_ ` ( ( M + 1 ) / N ) ) )
133 132 oveq2d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M / N ) - ( ( N x. ( |_ ` ( ( M + 1 ) / N ) ) ) / N ) ) = ( ( M / N ) - ( |_ ` ( ( M + 1 ) / N ) ) ) )
134 130 131 133 3eqtrrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M / N ) - ( |_ ` ( ( M + 1 ) / N ) ) ) = ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) )
135 58 recnd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M / N ) e. CC )
136 115 recnd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) e. CC )
137 135 69 136 subaddd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( M / N ) - ( |_ ` ( ( M + 1 ) / N ) ) ) = ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) <-> ( ( |_ ` ( ( M + 1 ) / N ) ) + ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) ) = ( M / N ) ) )
138 134 137 mpbid 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( |_ ` ( ( M + 1 ) / N ) ) + ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) ) = ( M / N ) )
139 138 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( ( |_ ` ( ( M + 1 ) / N ) ) + ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) ) = ( M / N ) )
140 139 fveq2d 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( |_ ` ( ( |_ ` ( ( M + 1 ) / N ) ) + ( ( ( ( M + 1 ) mod N ) - 1 ) / N ) ) ) = ( |_ ` ( M / N ) ) )
141 119 140 eqtr3d 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( |_ ` ( ( M + 1 ) / N ) ) = ( |_ ` ( M / N ) ) )
142 69 71 subeq0ad 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = 0 <-> ( |_ ` ( ( M + 1 ) / N ) ) = ( |_ ` ( M / N ) ) ) )
143 142 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = 0 <-> ( |_ ` ( ( M + 1 ) / N ) ) = ( |_ ` ( M / N ) ) ) )
144 141 143 mpbird 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = 0 )
145 iffalse 
 |-  ( -. N || ( M + 1 ) -> if ( N || ( M + 1 ) , 1 , 0 ) = 0 )
146 145 adantl 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> if ( N || ( M + 1 ) , 1 , 0 ) = 0 )
147 144 146 eqtr4d 
 |-  ( ( ( M e. ZZ /\ N e. NN ) /\ -. N || ( M + 1 ) ) -> ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = if ( N || ( M + 1 ) , 1 , 0 ) )
148 77 147 pm2.61dan 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = if ( N || ( M + 1 ) , 1 , 0 ) )