Theorem fzadd2d

Description: Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024)

	Ref	Expression
Hypotheses	fzadd2d.1	|- ( ph -> M e. ZZ )
	fzadd2d.2	|- ( ph -> N e. ZZ )
	fzadd2d.3	|- ( ph -> O e. ZZ )
	fzadd2d.4	|- ( ph -> P e. ZZ )
	fzadd2d.5	|- ( ph -> J e. ( M ... N ) )
	fzadd2d.6	|- ( ph -> K e. ( O ... P ) )
	fzadd2d.7	|- ( ph -> Q = ( M + O ) )
	fzadd2d.8	|- ( ph -> R = ( N + P ) )
Assertion	fzadd2d	|- ( ph -> ( J + K ) e. ( Q ... R ) )

Proof

Step	Hyp	Ref	Expression
1		fzadd2d.1	|- ( ph -> M e. ZZ )
2		fzadd2d.2	|- ( ph -> N e. ZZ )
3		fzadd2d.3	|- ( ph -> O e. ZZ )
4		fzadd2d.4	|- ( ph -> P e. ZZ )
5		fzadd2d.5	|- ( ph -> J e. ( M ... N ) )
6		fzadd2d.6	|- ( ph -> K e. ( O ... P ) )
7		fzadd2d.7	|- ( ph -> Q = ( M + O ) )
8		fzadd2d.8	|- ( ph -> R = ( N + P ) )
9	5 6	jca	|- ( ph -> ( J e. ( M ... N ) /\ K e. ( O ... P ) ) )
10	1 2	jca	|- ( ph -> ( M e. ZZ /\ N e. ZZ ) )
11	3 4	jca	|- ( ph -> ( O e. ZZ /\ P e. ZZ ) )
12	10 11	jca	|- ( ph -> ( ( M e. ZZ /\ N e. ZZ ) /\ ( O e. ZZ /\ P e. ZZ ) ) )
13		fzadd2	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( O e. ZZ /\ P e. ZZ ) ) -> ( ( J e. ( M ... N ) /\ K e. ( O ... P ) ) -> ( J + K ) e. ( ( M + O ) ... ( N + P ) ) ) )
14	12 13	syl	|- ( ph -> ( ( J e. ( M ... N ) /\ K e. ( O ... P ) ) -> ( J + K ) e. ( ( M + O ) ... ( N + P ) ) ) )
15	9 14	mpd	|- ( ph -> ( J + K ) e. ( ( M + O ) ... ( N + P ) ) )
16	7 8	oveq12d	|- ( ph -> ( Q ... R ) = ( ( M + O ) ... ( N + P ) ) )
17	15 16	eleqtrrd	|- ( ph -> ( J + K ) e. ( Q ... R ) )