Metamath Proof Explorer


Theorem evenltle

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 N Even M Even M < N M + 2 N

Proof

Step Hyp Ref Expression
1 evenz M Even M
2 evenz N Even N
3 zltp1le M N M < N M + 1 N
4 1 2 3 syl2anr N Even M Even M < N M + 1 N
5 1 zred M Even M
6 peano2re M M + 1
7 5 6 syl M Even M + 1
8 2 zred N Even N
9 leloe M + 1 N M + 1 N M + 1 < N M + 1 = N
10 7 8 9 syl2anr N Even M Even M + 1 N M + 1 < N M + 1 = N
11 1 peano2zd M Even M + 1
12 zltp1le M + 1 N M + 1 < N M + 1 + 1 N
13 11 2 12 syl2anr N Even M Even M + 1 < N M + 1 + 1 N
14 1 zcnd M Even M
15 14 adantl N Even M Even M
16 add1p1 M M + 1 + 1 = M + 2
17 15 16 syl N Even M Even M + 1 + 1 = M + 2
18 17 breq1d N Even M Even M + 1 + 1 N M + 2 N
19 18 biimpd N Even M Even M + 1 + 1 N M + 2 N
20 13 19 sylbid N Even M Even M + 1 < N M + 2 N
21 evenp1odd M Even M + 1 Odd
22 zneoALTV N Even M + 1 Odd N M + 1
23 eqneqall N = M + 1 N M + 1 M + 2 N
24 23 eqcoms M + 1 = N N M + 1 M + 2 N
25 22 24 syl5com N Even M + 1 Odd M + 1 = N M + 2 N
26 21 25 sylan2 N Even M Even M + 1 = N M + 2 N
27 20 26 jaod N Even M Even M + 1 < N M + 1 = N M + 2 N
28 10 27 sylbid N Even M Even M + 1 N M + 2 N
29 4 28 sylbid N Even M Even M < N M + 2 N
30 29 3impia N Even M Even M < N M + 2 N