Theorem eluzaddiOLD

Description: Obsolete version of eluzaddi 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	eluzaddiOLD	|- ( N e. ( ZZ>= ` M ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) )

Proof

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