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