# Metamath Proof Explorer

## Theorem crctcshwlkn0lem1

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 13-Mar-2021)

Ref Expression
Assertion crctcshwlkn0lem1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℕ\right)\to {A}-{B}+1\le {A}$

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
2 1 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in ℕ\right)\to {A}\in ℂ$
3 nncn ${⊢}{B}\in ℕ\to {B}\in ℂ$
4 3 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in ℕ\right)\to {B}\in ℂ$
5 1cnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℕ\right)\to 1\in ℂ$
6 subsub ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge 1\in ℂ\right)\to {A}-\left({B}-1\right)={A}-{B}+1$
7 6 eqcomd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge 1\in ℂ\right)\to {A}-{B}+1={A}-\left({B}-1\right)$
8 2 4 5 7 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℕ\right)\to {A}-{B}+1={A}-\left({B}-1\right)$
9 nnm1ge0 ${⊢}{B}\in ℕ\to 0\le {B}-1$
10 9 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in ℕ\right)\to 0\le {B}-1$
11 nnre ${⊢}{B}\in ℕ\to {B}\in ℝ$
12 peano2rem ${⊢}{B}\in ℝ\to {B}-1\in ℝ$
13 11 12 syl ${⊢}{B}\in ℕ\to {B}-1\in ℝ$
14 subge02 ${⊢}\left({A}\in ℝ\wedge {B}-1\in ℝ\right)\to \left(0\le {B}-1↔{A}-\left({B}-1\right)\le {A}\right)$
15 14 bicomd ${⊢}\left({A}\in ℝ\wedge {B}-1\in ℝ\right)\to \left({A}-\left({B}-1\right)\le {A}↔0\le {B}-1\right)$
16 13 15 sylan2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℕ\right)\to \left({A}-\left({B}-1\right)\le {A}↔0\le {B}-1\right)$
17 10 16 mpbird ${⊢}\left({A}\in ℝ\wedge {B}\in ℕ\right)\to {A}-\left({B}-1\right)\le {A}$
18 8 17 eqbrtrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℕ\right)\to {A}-{B}+1\le {A}$