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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | odd2np1 | |
|
2 | 0xr | |
|
3 | 1xr | |
|
4 | halfre | |
|
5 | 4 | rexri | |
6 | 2 3 5 | 3pm3.2i | |
7 | halfgt0 | |
|
8 | halflt1 | |
|
9 | 7 8 | pm3.2i | |
10 | elioo3g | |
|
11 | 6 9 10 | mpbir2an | |
12 | zltaddlt1le | |
|
13 | 11 12 | mp3an3 | |
14 | zcn | |
|
15 | 14 | adantr | |
16 | 1cnd | |
|
17 | 2cnne0 | |
|
18 | 17 | a1i | |
19 | muldivdir | |
|
20 | 15 16 18 19 | syl3anc | |
21 | 20 | breq1d | |
22 | 20 | breq1d | |
23 | 13 21 22 | 3bitr4rd | |
24 | oveq1 | |
|
25 | 24 | breq1d | |
26 | 24 | breq1d | |
27 | 25 26 | bibi12d | |
28 | 23 27 | syl5ibcom | |
29 | 28 | ex | |
30 | 29 | adantl | |
31 | 30 | com23 | |
32 | 31 | rexlimdva | |
33 | 1 32 | sylbid | |
34 | 33 | 3imp | |