Theorem eluzsubiOLD

Description: Obsolete version of eluzsubi as of 7-Feb-2025. (Contributed by Paul Chapman, 22-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	eluzsubi.1	|- M e. ZZ
	eluzsubi.2	|- K e. ZZ
Assertion	eluzsubiOLD	|- ( N e. ( ZZ>= ` ( M + K ) ) -> ( N - K ) e. ( ZZ>= ` M ) )

Proof

Step	Hyp	Ref	Expression
1		eluzsubi.1	|- M e. ZZ
2		eluzsubi.2	|- K e. ZZ
3		eluzelz	|- ( N e. ( ZZ>= ` ( M + K ) ) -> N e. ZZ )
4		zsubcl	|- ( ( N e. ZZ /\ K e. ZZ ) -> ( N - K ) e. ZZ )
5	3 2 4	sylancl	|- ( N e. ( ZZ>= ` ( M + K ) ) -> ( N - K ) e. ZZ )
6		zaddcl	|- ( ( M e. ZZ /\ K e. ZZ ) -> ( M + K ) e. ZZ )
7	1 2 6	mp2an	|- ( M + K ) e. ZZ
8	7	eluz1i	|- ( N e. ( ZZ>= ` ( M + K ) ) <-> ( N e. ZZ /\ ( M + K ) <_ N ) )
9	1	zrei	|- M e. RR
10	2	zrei	|- K e. RR
11		zre	|- ( N e. ZZ -> N e. RR )
12		leaddsub	|- ( ( M e. RR /\ K e. RR /\ N e. RR ) -> ( ( M + K ) <_ N <-> M <_ ( N - K ) ) )
13	9 10 11 12	mp3an12i	|- ( N e. ZZ -> ( ( M + K ) <_ N <-> M <_ ( N - K ) ) )
14	13	biimpa	|- ( ( N e. ZZ /\ ( M + K ) <_ N ) -> M <_ ( N - K ) )
15	8 14	sylbi	|- ( N e. ( ZZ>= ` ( M + K ) ) -> M <_ ( N - K ) )
16	1	eluz1i	|- ( ( N - K ) e. ( ZZ>= ` M ) <-> ( ( N - K ) e. ZZ /\ M <_ ( N - K ) ) )
17	5 15 16	sylanbrc	|- ( N e. ( ZZ>= ` ( M + K ) ) -> ( N - K ) e. ( ZZ>= ` M ) )