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 NEvenMEvenM<NM+2N

Proof

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