This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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