Description: If an even number is greater than another even number, then it is greater than or equal to the other even number plus 2. (Contributed by AV, 25-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | evenltle | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | evenz | |
|
2 | evenz | |
|
3 | zltp1le | |
|
4 | 1 2 3 | syl2anr | |
5 | 1 | zred | |
6 | peano2re | |
|
7 | 5 6 | syl | |
8 | 2 | zred | |
9 | leloe | |
|
10 | 7 8 9 | syl2anr | |
11 | 1 | peano2zd | |
12 | zltp1le | |
|
13 | 11 2 12 | syl2anr | |
14 | 1 | zcnd | |
15 | 14 | adantl | |
16 | add1p1 | |
|
17 | 15 16 | syl | |
18 | 17 | breq1d | |
19 | 18 | biimpd | |
20 | 13 19 | sylbid | |
21 | evenp1odd | |
|
22 | zneoALTV | |
|
23 | eqneqall | |
|
24 | 23 | eqcoms | |
25 | 22 24 | syl5com | |
26 | 21 25 | sylan2 | |
27 | 20 26 | jaod | |
28 | 10 27 | sylbid | |
29 | 4 28 | sylbid | |
30 | 29 | 3impia | |