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 ) ≤ 𝐴 )