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 )