Metamath Proof Explorer

Theorem flmrecm1

Description: The floor of an integer minus the reciprocal of a positive integer is the integer minus 1. (Contributed by AV, 10-Apr-2026)

Ref Expression
Assertion flmrecm1 
|- ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( M - ( 1 / N ) ) ) = ( M - 1 ) )

Proof

Step Hyp Ref Expression
1 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
2 1 zcnd 
 |-  ( M e. ZZ -> ( M - 1 ) e. CC )
3 2 adantr 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M - 1 ) e. CC )
4 1cnd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> 1 e. CC )
5 nnrecre 
 |-  ( N e. NN -> ( 1 / N ) e. RR )
6 5 recnd 
 |-  ( N e. NN -> ( 1 / N ) e. CC )
7 6 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( 1 / N ) e. CC )
8 zcn 
 |-  ( M e. ZZ -> M e. CC )
9 npcan1 
 |-  ( M e. CC -> ( ( M - 1 ) + 1 ) = M )
10 9 eqcomd 
 |-  ( M e. CC -> M = ( ( M - 1 ) + 1 ) )
11 8 10 syl 
 |-  ( M e. ZZ -> M = ( ( M - 1 ) + 1 ) )
12 11 adantr 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M = ( ( M - 1 ) + 1 ) )
13 12 oveq1d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M - ( 1 / N ) ) = ( ( ( M - 1 ) + 1 ) - ( 1 / N ) ) )
14 3 4 7 13 assraddsubd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M - ( 1 / N ) ) = ( ( M - 1 ) + ( 1 - ( 1 / N ) ) ) )
15 14 fveq2d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( M - ( 1 / N ) ) ) = ( |_ ` ( ( M - 1 ) + ( 1 - ( 1 / N ) ) ) ) )
16 1red 
 |-  ( N e. NN -> 1 e. RR )
17 16 5 resubcld 
 |-  ( N e. NN -> ( 1 - ( 1 / N ) ) e. RR )
18 flzadd 
 |-  ( ( ( M - 1 ) e. ZZ /\ ( 1 - ( 1 / N ) ) e. RR ) -> ( |_ ` ( ( M - 1 ) + ( 1 - ( 1 / N ) ) ) ) = ( ( M - 1 ) + ( |_ ` ( 1 - ( 1 / N ) ) ) ) )
19 1 17 18 syl2an 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( ( M - 1 ) + ( 1 - ( 1 / N ) ) ) ) = ( ( M - 1 ) + ( |_ ` ( 1 - ( 1 / N ) ) ) ) )
20 nnge1 
 |-  ( N e. NN -> 1 <_ N )
21 nnrp 
 |-  ( N e. NN -> N e. RR+ )
22 divle1le 
 |-  ( ( 1 e. RR /\ N e. RR+ ) -> ( ( 1 / N ) <_ 1 <-> 1 <_ N ) )
23 16 21 22 syl2anc 
 |-  ( N e. NN -> ( ( 1 / N ) <_ 1 <-> 1 <_ N ) )
24 20 23 mpbird 
 |-  ( N e. NN -> ( 1 / N ) <_ 1 )
25 16 5 subge0d 
 |-  ( N e. NN -> ( 0 <_ ( 1 - ( 1 / N ) ) <-> ( 1 / N ) <_ 1 ) )
26 24 25 mpbird 
 |-  ( N e. NN -> 0 <_ ( 1 - ( 1 / N ) ) )
27 nnrecgt0 
 |-  ( N e. NN -> 0 < ( 1 / N ) )
28 5 16 ltsubposd 
 |-  ( N e. NN -> ( 0 < ( 1 / N ) <-> ( 1 - ( 1 / N ) ) < 1 ) )
29 27 28 mpbid 
 |-  ( N e. NN -> ( 1 - ( 1 / N ) ) < 1 )
30 0re 
 |-  0 e. RR
31 1xr 
 |-  1 e. RR*
32 30 31 pm3.2i 
 |-  ( 0 e. RR /\ 1 e. RR* )
33 elico2 
 |-  ( ( 0 e. RR /\ 1 e. RR* ) -> ( ( 1 - ( 1 / N ) ) e. ( 0 [,) 1 ) <-> ( ( 1 - ( 1 / N ) ) e. RR /\ 0 <_ ( 1 - ( 1 / N ) ) /\ ( 1 - ( 1 / N ) ) < 1 ) ) )
34 32 33 mp1i 
 |-  ( N e. NN -> ( ( 1 - ( 1 / N ) ) e. ( 0 [,) 1 ) <-> ( ( 1 - ( 1 / N ) ) e. RR /\ 0 <_ ( 1 - ( 1 / N ) ) /\ ( 1 - ( 1 / N ) ) < 1 ) ) )
35 17 26 29 34 mpbir3and 
 |-  ( N e. NN -> ( 1 - ( 1 / N ) ) e. ( 0 [,) 1 ) )
36 ico01fl0 
 |-  ( ( 1 - ( 1 / N ) ) e. ( 0 [,) 1 ) -> ( |_ ` ( 1 - ( 1 / N ) ) ) = 0 )
37 35 36 syl 
 |-  ( N e. NN -> ( |_ ` ( 1 - ( 1 / N ) ) ) = 0 )
38 37 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( 1 - ( 1 / N ) ) ) = 0 )
39 38 oveq2d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M - 1 ) + ( |_ ` ( 1 - ( 1 / N ) ) ) ) = ( ( M - 1 ) + 0 ) )
40 3 addridd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M - 1 ) + 0 ) = ( M - 1 ) )
41 39 40 eqtrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M - 1 ) + ( |_ ` ( 1 - ( 1 / N ) ) ) ) = ( M - 1 ) )
42 15 19 41 3eqtrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( M - ( 1 / N ) ) ) = ( M - 1 ) )