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 e. Even /\ M e. Even /\ M < N ) -> ( M + 2 ) <_ N )

Proof

Step Hyp Ref Expression
1 evenz
 |-  ( M e. Even -> M e. ZZ )
2 evenz
 |-  ( N e. Even -> N e. ZZ )
3 zltp1le
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )
4 1 2 3 syl2anr
 |-  ( ( N e. Even /\ M e. Even ) -> ( M < N <-> ( M + 1 ) <_ N ) )
5 1 zred
 |-  ( M e. Even -> M e. RR )
6 peano2re
 |-  ( M e. RR -> ( M + 1 ) e. RR )
7 5 6 syl
 |-  ( M e. Even -> ( M + 1 ) e. RR )
8 2 zred
 |-  ( N e. Even -> N e. RR )
9 leloe
 |-  ( ( ( M + 1 ) e. RR /\ N e. RR ) -> ( ( M + 1 ) <_ N <-> ( ( M + 1 ) < N \/ ( M + 1 ) = N ) ) )
10 7 8 9 syl2anr
 |-  ( ( N e. Even /\ M e. Even ) -> ( ( M + 1 ) <_ N <-> ( ( M + 1 ) < N \/ ( M + 1 ) = N ) ) )
11 1 peano2zd
 |-  ( M e. Even -> ( M + 1 ) e. ZZ )
12 zltp1le
 |-  ( ( ( M + 1 ) e. ZZ /\ N e. ZZ ) -> ( ( M + 1 ) < N <-> ( ( M + 1 ) + 1 ) <_ N ) )
13 11 2 12 syl2anr
 |-  ( ( N e. Even /\ M e. Even ) -> ( ( M + 1 ) < N <-> ( ( M + 1 ) + 1 ) <_ N ) )
14 1 zcnd
 |-  ( M e. Even -> M e. CC )
15 14 adantl
 |-  ( ( N e. Even /\ M e. Even ) -> M e. CC )
16 add1p1
 |-  ( M e. CC -> ( ( M + 1 ) + 1 ) = ( M + 2 ) )
17 15 16 syl
 |-  ( ( N e. Even /\ M e. Even ) -> ( ( M + 1 ) + 1 ) = ( M + 2 ) )
18 17 breq1d
 |-  ( ( N e. Even /\ M e. Even ) -> ( ( ( M + 1 ) + 1 ) <_ N <-> ( M + 2 ) <_ N ) )
19 18 biimpd
 |-  ( ( N e. Even /\ M e. Even ) -> ( ( ( M + 1 ) + 1 ) <_ N -> ( M + 2 ) <_ N ) )
20 13 19 sylbid
 |-  ( ( N e. Even /\ M e. Even ) -> ( ( M + 1 ) < N -> ( M + 2 ) <_ N ) )
21 evenp1odd
 |-  ( M e. Even -> ( M + 1 ) e. Odd )
22 zneoALTV
 |-  ( ( N e. Even /\ ( M + 1 ) e. 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 e. Even /\ ( M + 1 ) e. Odd ) -> ( ( M + 1 ) = N -> ( M + 2 ) <_ N ) )
26 21 25 sylan2
 |-  ( ( N e. Even /\ M e. Even ) -> ( ( M + 1 ) = N -> ( M + 2 ) <_ N ) )
27 20 26 jaod
 |-  ( ( N e. Even /\ M e. Even ) -> ( ( ( M + 1 ) < N \/ ( M + 1 ) = N ) -> ( M + 2 ) <_ N ) )
28 10 27 sylbid
 |-  ( ( N e. Even /\ M e. Even ) -> ( ( M + 1 ) <_ N -> ( M + 2 ) <_ N ) )
29 4 28 sylbid
 |-  ( ( N e. Even /\ M e. Even ) -> ( M < N -> ( M + 2 ) <_ N ) )
30 29 3impia
 |-  ( ( N e. Even /\ M e. Even /\ M < N ) -> ( M + 2 ) <_ N )