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¬2NMM<N2MN12

Proof

Step Hyp Ref Expression
1 odd2np1 N¬2Nn2n+1=N
2 halfre 12
3 2 a1i n12
4 1red n1
5 zre nn
6 3 4 5 3jca n121n
7 6 adantr nM121n
8 halflt1 12<1
9 axltadd 121n12<1n+12<n+1
10 7 8 9 mpisyl nMn+12<n+1
11 zre MM
12 11 adantl nMM
13 5 3 readdcld nn+12
14 13 adantr nMn+12
15 peano2z nn+1
16 15 zred nn+1
17 16 adantr nMn+1
18 lttr Mn+12n+1M<n+12n+12<n+1M<n+1
19 12 14 17 18 syl3anc nMM<n+12n+12<n+1M<n+1
20 10 19 mpan2d nMM<n+12M<n+1
21 zleltp1 MnMnM<n+1
22 21 ancoms nMMnM<n+1
23 20 22 sylibrd nMM<n+12Mn
24 halfgt0 0<12
25 3 5 jca n12n
26 25 adantr nM12n
27 ltaddpos 12n0<12n<n+12
28 26 27 syl nM0<12n<n+12
29 24 28 mpbii nMn<n+12
30 5 adantr nMn
31 lelttr Mnn+12Mnn<n+12M<n+12
32 12 30 14 31 syl3anc nMMnn<n+12M<n+12
33 29 32 mpan2d nMMnM<n+12
34 23 33 impbid nMM<n+12Mn
35 zcn nn
36 1cnd n1
37 2cnne0 220
38 37 a1i n220
39 muldivdir n12202n+12=n+12
40 35 36 38 39 syl3anc n2n+12=n+12
41 40 breq2d nM<2n+12M<n+12
42 41 adantr nMM<2n+12M<n+12
43 2z 2
44 43 a1i n2
45 id nn
46 44 45 zmulcld n2n
47 46 zcnd n2n
48 47 adantr nM2n
49 pncan1 2n2n+1-1=2n
50 48 49 syl nM2n+1-1=2n
51 50 oveq1d nM2n+1-12=2n2
52 2cnd n2
53 2ne0 20
54 53 a1i n20
55 35 52 54 divcan3d n2n2=n
56 55 adantr nM2n2=n
57 51 56 eqtrd nM2n+1-12=n
58 57 breq2d nMM2n+1-12Mn
59 34 42 58 3bitr4d nMM<2n+12M2n+1-12
60 oveq1 2n+1=N2n+12=N2
61 60 breq2d 2n+1=NM<2n+12M<N2
62 oveq1 2n+1=N2n+1-1=N1
63 62 oveq1d 2n+1=N2n+1-12=N12
64 63 breq2d 2n+1=NM2n+1-12MN12
65 61 64 bibi12d 2n+1=NM<2n+12M2n+1-12M<N2MN12
66 59 65 syl5ibcom nM2n+1=NM<N2MN12
67 66 ex nM2n+1=NM<N2MN12
68 67 adantl NnM2n+1=NM<N2MN12
69 68 com23 Nn2n+1=NMM<N2MN12
70 69 rexlimdva Nn2n+1=NMM<N2MN12
71 1 70 sylbid N¬2NMM<N2MN12
72 71 3imp N¬2NMM<N2MN12