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	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	fzadd2d.2	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	fzadd2d.3	⊢ ( 𝜑 → 𝑂 ∈ ℤ )
	fzadd2d.4	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
	fzadd2d.5	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑀 ... 𝑁 ) )
	fzadd2d.6	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑂 ... 𝑃 ) )
	fzadd2d.7	⊢ ( 𝜑 → 𝑄 = ( 𝑀 + 𝑂 ) )
	fzadd2d.8	⊢ ( 𝜑 → 𝑅 = ( 𝑁 + 𝑃 ) )
Assertion	fzadd2d	⊢ ( 𝜑 → ( 𝐽 + 𝐾 ) ∈ ( 𝑄 ... 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		fzadd2d.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		fzadd2d.2	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
3		fzadd2d.3	⊢ ( 𝜑 → 𝑂 ∈ ℤ )
4		fzadd2d.4	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
5		fzadd2d.5	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑀 ... 𝑁 ) )
6		fzadd2d.6	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑂 ... 𝑃 ) )
7		fzadd2d.7	⊢ ( 𝜑 → 𝑄 = ( 𝑀 + 𝑂 ) )
8		fzadd2d.8	⊢ ( 𝜑 → 𝑅 = ( 𝑁 + 𝑃 ) )
9	5 6	jca	⊢ ( 𝜑 → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑂 ... 𝑃 ) ) )
10	1 2	jca	⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
11	3 4	jca	⊢ ( 𝜑 → ( 𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ ) )
12	10 11	jca	⊢ ( 𝜑 → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) )
13		fzadd2	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) → ( ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑂 ... 𝑃 ) ) → ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ) )
14	12 13	syl	⊢ ( 𝜑 → ( ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑂 ... 𝑃 ) ) → ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) ) )
15	9 14	mpd	⊢ ( 𝜑 → ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) )
16	7 8	oveq12d	⊢ ( 𝜑 → ( 𝑄 ... 𝑅 ) = ( ( 𝑀 + 𝑂 ) ... ( 𝑁 + 𝑃 ) ) )
17	15 16	eleqtrrd	⊢ ( 𝜑 → ( 𝐽 + 𝐾 ) ∈ ( 𝑄 ... 𝑅 ) )