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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 − 𝐵 ) + 1 ) ≤ 𝐴 )

Proof

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