Metamath Proof Explorer

Theorem crctcshwlkn0lem1

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

Ref Expression
Assertion crctcshwlkn0lem1 ⊢A∈ℝ∧B∈ℕ→A-B+1≤A

Proof

Step Hyp Ref Expression
1 recn ⊢A∈ℝ→A∈ℂ
2 1 adantr ⊢A∈ℝ∧B∈ℕ→A∈ℂ
3 nncn ⊢B∈ℕ→B∈ℂ
4 3 adantl ⊢A∈ℝ∧B∈ℕ→B∈ℂ
5 1cnd ⊢A∈ℝ∧B∈ℕ→1∈ℂ
6 subsub ⊢A∈ℂ∧B∈ℂ∧1∈ℂ→A−B−1=A-B+1
7 6 eqcomd ⊢A∈ℂ∧B∈ℂ∧1∈ℂ→A-B+1=A−B−1
8 2 4 5 7 syl3anc ⊢A∈ℝ∧B∈ℕ→A-B+1=A−B−1
9 nnm1ge0 ⊢B∈ℕ→0≤B−1
10 9 adantl ⊢A∈ℝ∧B∈ℕ→0≤B−1
11 nnre ⊢B∈ℕ→B∈ℝ
12 peano2rem ⊢B∈ℝ→B−1∈ℝ
13 11 12 syl ⊢B∈ℕ→B−1∈ℝ
14 subge02 ⊢A∈ℝ∧B−1∈ℝ→0≤B−1↔A−B−1≤A
15 14 bicomd ⊢A∈ℝ∧B−1∈ℝ→A−B−1≤A↔0≤B−1
16 13 15 sylan2 ⊢A∈ℝ∧B∈ℕ→A−B−1≤A↔0≤B−1
17 10 16 mpbird ⊢A∈ℝ∧B∈ℕ→A−B−1≤A
18 8 17 eqbrtrd ⊢A∈ℝ∧B∈ℕ→A-B+1≤A