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 ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ∧ 𝑀 < 𝑁 ) → ( 𝑀 + 2 ) ≤ 𝑁 )

Proof

Step Hyp Ref Expression
1 evenz ⊢ ( 𝑀 ∈ Even → 𝑀 ∈ ℤ )
2 evenz ⊢ ( 𝑁 ∈ Even → 𝑁 ∈ ℤ )
3 zltp1le ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )
4 1 2 3 syl2anr ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )
5 1 zred ⊢ ( 𝑀 ∈ Even → 𝑀 ∈ ℝ )
6 peano2re ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 + 1 ) ∈ ℝ )
7 5 6 syl ⊢ ( 𝑀 ∈ Even → ( 𝑀 + 1 ) ∈ ℝ )
8 2 zred ⊢ ( 𝑁 ∈ Even → 𝑁 ∈ ℝ )
9 leloe ⊢ ( ( ( 𝑀 + 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 + 1 ) ≤ 𝑁 ↔ ( ( 𝑀 + 1 ) < 𝑁 ∨ ( 𝑀 + 1 ) = 𝑁 ) ) )
10 7 8 9 syl2anr ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( ( 𝑀 + 1 ) ≤ 𝑁 ↔ ( ( 𝑀 + 1 ) < 𝑁 ∨ ( 𝑀 + 1 ) = 𝑁 ) ) )
11 1 peano2zd ⊢ ( 𝑀 ∈ Even → ( 𝑀 + 1 ) ∈ ℤ )
12 zltp1le ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 1 ) < 𝑁 ↔ ( ( 𝑀 + 1 ) + 1 ) ≤ 𝑁 ) )
13 11 2 12 syl2anr ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( ( 𝑀 + 1 ) < 𝑁 ↔ ( ( 𝑀 + 1 ) + 1 ) ≤ 𝑁 ) )
14 1 zcnd ⊢ ( 𝑀 ∈ Even → 𝑀 ∈ ℂ )
15 14 adantl ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → 𝑀 ∈ ℂ )
16 add1p1 ⊢ ( 𝑀 ∈ ℂ → ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + 2 ) )
17 15 16 syl ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + 2 ) )
18 17 breq1d ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( ( ( 𝑀 + 1 ) + 1 ) ≤ 𝑁 ↔ ( 𝑀 + 2 ) ≤ 𝑁 ) )
19 18 biimpd ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( ( ( 𝑀 + 1 ) + 1 ) ≤ 𝑁 → ( 𝑀 + 2 ) ≤ 𝑁 ) )
20 13 19 sylbid ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( ( 𝑀 + 1 ) < 𝑁 → ( 𝑀 + 2 ) ≤ 𝑁 ) )
21 evenp1odd ⊢ ( 𝑀 ∈ Even → ( 𝑀 + 1 ) ∈ Odd )
22 zneoALTV ⊢ ( ( 𝑁 ∈ Even ∧ ( 𝑀 + 1 ) ∈ Odd ) → 𝑁 ≠ ( 𝑀 + 1 ) )
23 eqneqall ⊢ ( 𝑁 = ( 𝑀 + 1 ) → ( 𝑁 ≠ ( 𝑀 + 1 ) → ( 𝑀 + 2 ) ≤ 𝑁 ) )
24 23 eqcoms ⊢ ( ( 𝑀 + 1 ) = 𝑁 → ( 𝑁 ≠ ( 𝑀 + 1 ) → ( 𝑀 + 2 ) ≤ 𝑁 ) )
25 22 24 syl5com ⊢ ( ( 𝑁 ∈ Even ∧ ( 𝑀 + 1 ) ∈ Odd ) → ( ( 𝑀 + 1 ) = 𝑁 → ( 𝑀 + 2 ) ≤ 𝑁 ) )
26 21 25 sylan2 ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( ( 𝑀 + 1 ) = 𝑁 → ( 𝑀 + 2 ) ≤ 𝑁 ) )
27 20 26 jaod ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( ( ( 𝑀 + 1 ) < 𝑁 ∨ ( 𝑀 + 1 ) = 𝑁 ) → ( 𝑀 + 2 ) ≤ 𝑁 ) )
28 10 27 sylbid ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( ( 𝑀 + 1 ) ≤ 𝑁 → ( 𝑀 + 2 ) ≤ 𝑁 ) )
29 4 28 sylbid ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ) → ( 𝑀 < 𝑁 → ( 𝑀 + 2 ) ≤ 𝑁 ) )
30 29 3impia ⊢ ( ( 𝑁 ∈ Even ∧ 𝑀 ∈ Even ∧ 𝑀 < 𝑁 ) → ( 𝑀 + 2 ) ≤ 𝑁 )