fzadd2d

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

Step	Hyp	Ref	Expression
1		fzadd2d.1	$⊢ φ \to M \in ℤ$
2		fzadd2d.2	$⊢ φ \to N \in ℤ$
3		fzadd2d.3	$⊢ φ \to O \in ℤ$
4		fzadd2d.4	$⊢ φ \to P \in ℤ$
5		fzadd2d.5	$⊢ φ \to J \in (M \dots N)$
6		fzadd2d.6	$⊢ φ \to K \in (O \dots P)$
7		fzadd2d.7	$⊢ φ \to Q = M + O$
8		fzadd2d.8	$⊢ φ \to R = N + P$
9	5 6	jca	$⊢ φ \to (J \in (M \dots N) \land K \in (O \dots P))$
10	1 2	jca	$⊢ φ \to (M \in ℤ \land N \in ℤ)$
11	3 4	jca	$⊢ φ \to (O \in ℤ \land P \in ℤ)$
12	10 11	jca	$⊢ φ \to ((M \in ℤ \land N \in ℤ) \land (O \in ℤ \land P \in ℤ))$
13		fzadd2	$⊢ ((M \in ℤ \land N \in ℤ) \land (O \in ℤ \land P \in ℤ)) \to ((J \in (M \dots N) \land K \in (O \dots P)) \to J + K \in (M + O \dots N + P))$
14	12 13	syl	$⊢ φ \to ((J \in (M \dots N) \land K \in (O \dots P)) \to J + K \in (M + O \dots N + P))$
15	9 14	mpd	$⊢ φ \to J + K \in (M + O \dots N + P)$
16	7 8	oveq12d	$⊢ φ \to (Q \dots R) = (M + O \dots N + P)$
17	15 16	eleqtrrd	$⊢ φ \to J + K \in (Q \dots R)$

Metamath Proof Explorer