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¬2NMN2MN2<M

Proof

Step Hyp Ref Expression
1 odd2np1 N¬2Nn2n+1=N
2 0xr 0*
3 1xr 1*
4 halfre 12
5 4 rexri 12*
6 2 3 5 3pm3.2i 0*1*12*
7 halfgt0 0<12
8 halflt1 12<1
9 7 8 pm3.2i 0<1212<1
10 elioo3g 12010*1*12*0<1212<1
11 6 9 10 mpbir2an 1201
12 zltaddlt1le nM1201n+12<Mn+12M
13 11 12 mp3an3 nMn+12<Mn+12M
14 zcn nn
15 14 adantr nMn
16 1cnd nM1
17 2cnne0 220
18 17 a1i nM220
19 muldivdir n12202n+12=n+12
20 15 16 18 19 syl3anc nM2n+12=n+12
21 20 breq1d nM2n+12<Mn+12<M
22 20 breq1d nM2n+12Mn+12M
23 13 21 22 3bitr4rd nM2n+12M2n+12<M
24 oveq1 2n+1=N2n+12=N2
25 24 breq1d 2n+1=N2n+12MN2M
26 24 breq1d 2n+1=N2n+12<MN2<M
27 25 26 bibi12d 2n+1=N2n+12M2n+12<MN2MN2<M
28 23 27 syl5ibcom nM2n+1=NN2MN2<M
29 28 ex nM2n+1=NN2MN2<M
30 29 adantl NnM2n+1=NN2MN2<M
31 30 com23 Nn2n+1=NMN2MN2<M
32 31 rexlimdva Nn2n+1=NMN2MN2<M
33 1 32 sylbid N¬2NMN2MN2<M
34 33 3imp N¬2NMN2MN2<M