Theorem crctcshwlkn0lem1

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

	Ref	Expression
Assertion	crctcshwlkn0lem1	|- ( ( A e. RR /\ B e. NN ) -> ( ( A - B ) + 1 ) <_ A )

Proof

Step	Hyp	Ref	Expression
1		recn	|- ( A e. RR -> A e. CC )
2	1	adantr	|- ( ( A e. RR /\ B e. NN ) -> A e. CC )
3		nncn	|- ( B e. NN -> B e. CC )
4	3	adantl	|- ( ( A e. RR /\ B e. NN ) -> B e. CC )
5		1cnd	|- ( ( A e. RR /\ B e. NN ) -> 1 e. CC )
6		subsub	|- ( ( A e. CC /\ B e. CC /\ 1 e. CC ) -> ( A - ( B - 1 ) ) = ( ( A - B ) + 1 ) )
7	6	eqcomd	|- ( ( A e. CC /\ B e. CC /\ 1 e. CC ) -> ( ( A - B ) + 1 ) = ( A - ( B - 1 ) ) )
8	2 4 5 7	syl3anc	|- ( ( A e. RR /\ B e. NN ) -> ( ( A - B ) + 1 ) = ( A - ( B - 1 ) ) )
9		nnm1ge0	|- ( B e. NN -> 0 <_ ( B - 1 ) )
10	9	adantl	|- ( ( A e. RR /\ B e. NN ) -> 0 <_ ( B - 1 ) )
11		nnre	|- ( B e. NN -> B e. RR )
12		peano2rem	|- ( B e. RR -> ( B - 1 ) e. RR )
13	11 12	syl	|- ( B e. NN -> ( B - 1 ) e. RR )
14		subge02	|- ( ( A e. RR /\ ( B - 1 ) e. RR ) -> ( 0 <_ ( B - 1 ) <-> ( A - ( B - 1 ) ) <_ A ) )
15	14	bicomd	|- ( ( A e. RR /\ ( B - 1 ) e. RR ) -> ( ( A - ( B - 1 ) ) <_ A <-> 0 <_ ( B - 1 ) ) )
16	13 15	sylan2	|- ( ( A e. RR /\ B e. NN ) -> ( ( A - ( B - 1 ) ) <_ A <-> 0 <_ ( B - 1 ) ) )
17	10 16	mpbird	|- ( ( A e. RR /\ B e. NN ) -> ( A - ( B - 1 ) ) <_ A )
18	8 17	eqbrtrd	|- ( ( A e. RR /\ B e. NN ) -> ( ( A - B ) + 1 ) <_ A )