Metamath Proof Explorer

Theorem halfleoddlt

Description: An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 odd2np1 
 |-  ( N e. ZZ -> ( -. 2 || N <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
2 0xr 
 |-  0 e. RR*
3 1xr 
 |-  1 e. RR*
4 halfre 
 |-  ( 1 / 2 ) e. RR
5 4 rexri 
 |-  ( 1 / 2 ) e. RR*
6 2 3 5 3pm3.2i 
 |-  ( 0 e. RR* /\ 1 e. RR* /\ ( 1 / 2 ) e. RR* )
7 halfgt0 
 |-  0 < ( 1 / 2 )
8 halflt1 
 |-  ( 1 / 2 ) < 1
9 7 8 pm3.2i 
 |-  ( 0 < ( 1 / 2 ) /\ ( 1 / 2 ) < 1 )
10 elioo3g 
 |-  ( ( 1 / 2 ) e. ( 0 (,) 1 ) <-> ( ( 0 e. RR* /\ 1 e. RR* /\ ( 1 / 2 ) e. RR* ) /\ ( 0 < ( 1 / 2 ) /\ ( 1 / 2 ) < 1 ) ) )
11 6 9 10 mpbir2an 
 |-  ( 1 / 2 ) e. ( 0 (,) 1 )
12 zltaddlt1le 
 |-  ( ( n e. ZZ /\ M e. ZZ /\ ( 1 / 2 ) e. ( 0 (,) 1 ) ) -> ( ( n + ( 1 / 2 ) ) < M <-> ( n + ( 1 / 2 ) ) <_ M ) )
13 11 12 mp3an3 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( n + ( 1 / 2 ) ) < M <-> ( n + ( 1 / 2 ) ) <_ M ) )
14 zcn 
 |-  ( n e. ZZ -> n e. CC )
15 14 adantr 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> n e. CC )
16 1cnd 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> 1 e. CC )
17 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
18 17 a1i 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( 2 e. CC /\ 2 =/= 0 ) )
19 muldivdir 
 |-  ( ( n e. CC /\ 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( 2 x. n ) + 1 ) / 2 ) = ( n + ( 1 / 2 ) ) )
20 15 16 18 19 syl3anc 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( ( 2 x. n ) + 1 ) / 2 ) = ( n + ( 1 / 2 ) ) )
21 20 breq1d 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( ( ( 2 x. n ) + 1 ) / 2 ) < M <-> ( n + ( 1 / 2 ) ) < M ) )
22 20 breq1d 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( ( ( 2 x. n ) + 1 ) / 2 ) <_ M <-> ( n + ( 1 / 2 ) ) <_ M ) )
23 13 21 22 3bitr4rd 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( ( ( 2 x. n ) + 1 ) / 2 ) <_ M <-> ( ( ( 2 x. n ) + 1 ) / 2 ) < M ) )
24 oveq1 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( ( ( 2 x. n ) + 1 ) / 2 ) = ( N / 2 ) )
25 24 breq1d 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( ( ( ( 2 x. n ) + 1 ) / 2 ) <_ M <-> ( N / 2 ) <_ M ) )
26 24 breq1d 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( ( ( ( 2 x. n ) + 1 ) / 2 ) < M <-> ( N / 2 ) < M ) )
27 25 26 bibi12d 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( ( ( ( ( 2 x. n ) + 1 ) / 2 ) <_ M <-> ( ( ( 2 x. n ) + 1 ) / 2 ) < M ) <-> ( ( N / 2 ) <_ M <-> ( N / 2 ) < M ) ) )
28 23 27 syl5ibcom 
 |-  ( ( n e. ZZ /\ M e. ZZ ) -> ( ( ( 2 x. n ) + 1 ) = N -> ( ( N / 2 ) <_ M <-> ( N / 2 ) < M ) ) )
29 28 ex 
 |-  ( n e. ZZ -> ( M e. ZZ -> ( ( ( 2 x. n ) + 1 ) = N -> ( ( N / 2 ) <_ M <-> ( N / 2 ) < M ) ) ) )
30 29 adantl 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( M e. ZZ -> ( ( ( 2 x. n ) + 1 ) = N -> ( ( N / 2 ) <_ M <-> ( N / 2 ) < M ) ) ) )
31 30 com23 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( ( ( 2 x. n ) + 1 ) = N -> ( M e. ZZ -> ( ( N / 2 ) <_ M <-> ( N / 2 ) < M ) ) ) )
32 31 rexlimdva 
 |-  ( N e. ZZ -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = N -> ( M e. ZZ -> ( ( N / 2 ) <_ M <-> ( N / 2 ) < M ) ) ) )
33 1 32 sylbid 
 |-  ( N e. ZZ -> ( -. 2 || N -> ( M e. ZZ -> ( ( N / 2 ) <_ M <-> ( N / 2 ) < M ) ) ) )
34 33 3imp 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ M e. ZZ ) -> ( ( N / 2 ) <_ M <-> ( N / 2 ) < M ) )