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