Metamath Proof Explorer

Theorem ltoddhalfle

Description: An integer is less than half of an odd number iff it is less than or equal to the half of the predecessor of the odd number (which is an even number). (Contributed by AV, 29-Jun-2021)

Ref Expression
Assertion ltoddhalfle 
|- ( ( N e. ZZ /\ -. 2 || N /\ M e. ZZ ) -> ( M < ( N / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 odd2np1 
 |-  ( N e. ZZ -> ( -. 2 || N <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
2 halfre 
 |-  ( 1 / 2 ) e. RR
3 2 a1i 
 |-  ( n e. ZZ -> ( 1 / 2 ) e. RR )
4 1red 
 |-  ( n e. ZZ -> 1 e. RR )
5 zre 
 |-  ( n e. ZZ -> n e. RR )
6 3 4 5 3jca 
 |-  ( n e. ZZ -> ( ( 1 / 2 ) e. RR /\ 1 e. RR /\ n e. RR ) )
7 6 adantr 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( 1 / 2 ) e. RR /\ 1 e. RR /\ n e. RR ) )
8 halflt1 
 |-  ( 1 / 2 ) < 1
9 axltadd 
 |-  ( ( ( 1 / 2 ) e. RR /\ 1 e. RR /\ n e. RR ) -> ( ( 1 / 2 ) < 1 -> ( n + ( 1 / 2 ) ) < ( n + 1 ) ) )
10 7 8 9 mpisyl 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( n + ( 1 / 2 ) ) < ( n + 1 ) )
11 zre 
 |-  ( M e. ZZ -> M e. RR )
12 11 adantl 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> M e. RR )
13 5 3 readdcld 
 |-  ( n e. ZZ -> ( n + ( 1 / 2 ) ) e. RR )
14 13 adantr 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( n + ( 1 / 2 ) ) e. RR )
15 peano2z 
 |-  ( n e. ZZ -> ( n + 1 ) e. ZZ )
16 15 zred 
 |-  ( n e. ZZ -> ( n + 1 ) e. RR )
17 16 adantr 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( n + 1 ) e. RR )
18 lttr 
 |-  ( ( M e. RR /\ ( n + ( 1 / 2 ) ) e. RR /\ ( n + 1 ) e. RR ) -> ( ( M < ( n + ( 1 / 2 ) ) /\ ( n + ( 1 / 2 ) ) < ( n + 1 ) ) -> M < ( n + 1 ) ) )
19 12 14 17 18 syl3anc 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( M < ( n + ( 1 / 2 ) ) /\ ( n + ( 1 / 2 ) ) < ( n + 1 ) ) -> M < ( n + 1 ) ) )
20 10 19 mpan2d 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( M < ( n + ( 1 / 2 ) ) -> M < ( n + 1 ) ) )
21 zleltp1 
 |-  ( ( M e. ZZ /\ n e. ZZ ) -> ( M <_ n <-> M < ( n + 1 ) ) )
22 21 ancoms 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( M <_ n <-> M < ( n + 1 ) ) )
23 20 22 sylibrd 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( M < ( n + ( 1 / 2 ) ) -> M <_ n ) )
24 halfgt0 
 |-  0 < ( 1 / 2 )
25 3 5 jca 
 |-  ( n e. ZZ -> ( ( 1 / 2 ) e. RR /\ n e. RR ) )
26 25 adantr 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( 1 / 2 ) e. RR /\ n e. RR ) )
27 ltaddpos 
 |-  ( ( ( 1 / 2 ) e. RR /\ n e. RR ) -> ( 0 < ( 1 / 2 ) <-> n < ( n + ( 1 / 2 ) ) ) )
28 26 27 syl 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( 0 < ( 1 / 2 ) <-> n < ( n + ( 1 / 2 ) ) ) )
29 24 28 mpbii 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> n < ( n + ( 1 / 2 ) ) )
30 5 adantr 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> n e. RR )
31 lelttr 
 |-  ( ( M e. RR /\ n e. RR /\ ( n + ( 1 / 2 ) ) e. RR ) -> ( ( M <_ n /\ n < ( n + ( 1 / 2 ) ) ) -> M < ( n + ( 1 / 2 ) ) ) )
32 12 30 14 31 syl3anc 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( M <_ n /\ n < ( n + ( 1 / 2 ) ) ) -> M < ( n + ( 1 / 2 ) ) ) )
33 29 32 mpan2d 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( M <_ n -> M < ( n + ( 1 / 2 ) ) ) )
34 23 33 impbid 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( M < ( n + ( 1 / 2 ) ) <-> M <_ n ) )
35 zcn 
 |-  ( n e. ZZ -> n e. CC )
36 1cnd 
 |-  ( n e. ZZ -> 1 e. CC )
37 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
38 37 a1i 
 |-  ( n e. ZZ -> ( 2 e. CC /\ 2 =/= 0 ) )
39 muldivdir 
 |-  ( ( n e. CC /\ 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( 2 x. n ) + 1 ) / 2 ) = ( n + ( 1 / 2 ) ) )
40 35 36 38 39 syl3anc 
 |-  ( n e. ZZ -> ( ( ( 2 x. n ) + 1 ) / 2 ) = ( n + ( 1 / 2 ) ) )
41 40 breq2d 
 |-  ( n e. ZZ -> ( M < ( ( ( 2 x. n ) + 1 ) / 2 ) <-> M < ( n + ( 1 / 2 ) ) ) )
42 41 adantr 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( M < ( ( ( 2 x. n ) + 1 ) / 2 ) <-> M < ( n + ( 1 / 2 ) ) ) )
43 2z 
 |-  2 e. ZZ
44 43 a1i 
 |-  ( n e. ZZ -> 2 e. ZZ )
45 id 
 |-  ( n e. ZZ -> n e. ZZ )
46 44 45 zmulcld 
 |-  ( n e. ZZ -> ( 2 x. n ) e. ZZ )
47 46 zcnd 
 |-  ( n e. ZZ -> ( 2 x. n ) e. CC )
48 47 adantr 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( 2 x. n ) e. CC )
49 pncan1 
 |-  ( ( 2 x. n ) e. CC -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
50 48 49 syl 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
51 50 oveq1d 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) = ( ( 2 x. n ) / 2 ) )
52 2cnd 
 |-  ( n e. ZZ -> 2 e. CC )
53 2ne0 
 |-  2 =/= 0
54 53 a1i 
 |-  ( n e. ZZ -> 2 =/= 0 )
55 35 52 54 divcan3d 
 |-  ( n e. ZZ -> ( ( 2 x. n ) / 2 ) = n )
56 55 adantr 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( 2 x. n ) / 2 ) = n )
57 51 56 eqtrd 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) = n )
58 57 breq2d 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( M <_ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) <-> M <_ n ) )
59 34 42 58 3bitr4d 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( M < ( ( ( 2 x. n ) + 1 ) / 2 ) <-> M <_ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) )
60 oveq1 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( ( ( 2 x. n ) + 1 ) / 2 ) = ( N / 2 ) )
61 60 breq2d 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( M < ( ( ( 2 x. n ) + 1 ) / 2 ) <-> M < ( N / 2 ) ) )
62 oveq1 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( N - 1 ) )
63 62 oveq1d 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) = ( ( N - 1 ) / 2 ) )
64 63 breq2d 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( M <_ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) )
65 61 64 bibi12d 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( ( M < ( ( ( 2 x. n ) + 1 ) / 2 ) <-> M <_ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) <-> ( M < ( N / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) ) )
66 59 65 syl5ibcom 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( ( 2 x. n ) + 1 ) = N -> ( M < ( N / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) ) )
67 66 ex 
 |-  ( n e. ZZ -> ( M e. ZZ -> ( ( ( 2 x. n ) + 1 ) = N -> ( M < ( N / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) ) ) )
68 67 adantl 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( M e. ZZ -> ( ( ( 2 x. n ) + 1 ) = N -> ( M < ( N / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) ) ) )
69 68 com23 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( ( ( 2 x. n ) + 1 ) = N -> ( M e. ZZ -> ( M < ( N / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) ) ) )
70 69 rexlimdva 
 |-  ( N e. ZZ -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = N -> ( M e. ZZ -> ( M < ( N / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) ) ) )
71 1 70 sylbid 
 |-  ( N e. ZZ -> ( -. 2 || N -> ( M e. ZZ -> ( M < ( N / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) ) ) )
72 71 3imp 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ M e. ZZ ) -> ( M < ( N / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) )