Metamath Proof Explorer


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 φ M
fzadd2d.2 φ N
fzadd2d.3 φ O
fzadd2d.4 φ P
fzadd2d.5 φ J M N
fzadd2d.6 φ K O P
fzadd2d.7 φ Q = M + O
fzadd2d.8 φ R = N + P
Assertion fzadd2d φ J + K Q R

Proof

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