itg2addlem

	Ref	Expression
Hypotheses	itg2add.f1	$⊢ φ \to F \in MblFn$
	itg2add.f2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	itg2add.f3	$⊢ φ \to \int^{2} (F) \in ℝ$
	itg2add.g1	$⊢ φ \to G \in MblFn$
	itg2add.g2	$⊢ φ \to G : ℝ ⟶ [0, +∞)$
	itg2add.g3	$⊢ φ \to \int^{2} (G) \in ℝ$
	itg2add.p1	$⊢ φ \to P : ℕ ⟶ dom \int^{1}$
	itg2add.p2	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1))$
	itg2add.p3	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x)$
	itg2add.q1	$⊢ φ \to Q : ℕ ⟶ dom \int^{1}$
	itg2add.q2	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} Q (n) \land Q (n) \leq_{f} Q (n + 1))$
	itg2add.q3	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ Q (n) (x)) ⇝ G (x)$
Assertion	itg2addlem	$⊢ φ \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G)$

Proof

Step	Hyp	Ref	Expression
1		itg2add.f1	$⊢ φ \to F \in MblFn$
2		itg2add.f2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
3		itg2add.f3	$⊢ φ \to \int^{2} (F) \in ℝ$
4		itg2add.g1	$⊢ φ \to G \in MblFn$
5		itg2add.g2	$⊢ φ \to G : ℝ ⟶ [0, +∞)$
6		itg2add.g3	$⊢ φ \to \int^{2} (G) \in ℝ$
7		itg2add.p1	$⊢ φ \to P : ℕ ⟶ dom \int^{1}$
8		itg2add.p2	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1))$
9		itg2add.p3	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x)$
10		itg2add.q1	$⊢ φ \to Q : ℕ ⟶ dom \int^{1}$
11		itg2add.q2	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} Q (n) \land Q (n) \leq_{f} Q (n + 1))$
12		itg2add.q3	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ Q (n) (x)) ⇝ G (x)$
13	1 4	mbfadd	$⊢ φ \to F +_{f} G \in MblFn$
14		ge0addcl	$⊢ (y \in [0, +∞) \land z \in [0, +∞)) \to y + z \in [0, +∞)$
15	14	adantl	$⊢ (φ \land (y \in [0, +∞) \land z \in [0, +∞))) \to y + z \in [0, +∞)$
16		reex	$⊢ ℝ \in V$
17	16	a1i	$⊢ φ \to ℝ \in V$
18		inidm	$⊢ ℝ \cap ℝ = ℝ$
19	15 2 5 17 17 18	off	$⊢ φ \to (F +_{f} G) : ℝ ⟶ [0, +∞)$
20		simpl	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f \in dom \int^{1}$
21		simpr	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to g \in dom \int^{1}$
22	20 21	i1fadd	$⊢ (f \in dom \int^{1} \land g \in dom \int^{1}) \to f +_{f} g \in dom \int^{1}$
23	22	adantl	$⊢ (φ \land (f \in dom \int^{1} \land g \in dom \int^{1})) \to f +_{f} g \in dom \int^{1}$
24		nnex	$⊢ ℕ \in V$
25	24	a1i	$⊢ φ \to ℕ \in V$
26		inidm	$⊢ ℕ \cap ℕ = ℕ$
27	23 7 10 25 25 26	off	$⊢ φ \to (P {\circ_{f} +}_{f} Q) : ℕ ⟶ dom \int^{1}$
28		ge0addcl	$⊢ (f \in [0, +∞) \land g \in [0, +∞)) \to f + g \in [0, +∞)$
29	28	adantl	$⊢ ((φ \land m \in ℕ) \land (f \in [0, +∞) \land g \in [0, +∞))) \to f + g \in [0, +∞)$
30	7	ffvelcdmda	$⊢ (φ \land m \in ℕ) \to P (m) \in dom \int^{1}$
31		fveq2	$⊢ n = m \to P (n) = P (m)$
32	31	breq2d	$⊢ n = m \to (0_{𝑝} \leq_{f} P (n) \leftrightarrow 0_{𝑝} \leq_{f} P (m))$
33		fvoveq1	$⊢ n = m \to P (n + 1) = P (m + 1)$
34	31 33	breq12d	$⊢ n = m \to (P (n) \leq_{f} P (n + 1) \leftrightarrow P (m) \leq_{f} P (m + 1))$
35	32 34	anbi12d	$⊢ n = m \to ((0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1)) \leftrightarrow (0_{𝑝} \leq_{f} P (m) \land P (m) \leq_{f} P (m + 1)))$
36	35	rspccva	$⊢ (\forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1)) \land m \in ℕ) \to (0_{𝑝} \leq_{f} P (m) \land P (m) \leq_{f} P (m + 1))$
37	8 36	sylan	$⊢ (φ \land m \in ℕ) \to (0_{𝑝} \leq_{f} P (m) \land P (m) \leq_{f} P (m + 1))$
38	37	simpld	$⊢ (φ \land m \in ℕ) \to 0_{𝑝} \leq_{f} P (m)$
39		breq2	$⊢ f = P (m) \to (0_{𝑝} \leq_{f} f \leftrightarrow 0_{𝑝} \leq_{f} P (m))$
40		feq1	$⊢ f = P (m) \to (f : ℝ ⟶ [0, +∞) \leftrightarrow P (m) : ℝ ⟶ [0, +∞))$
41	39 40	imbi12d	$⊢ f = P (m) \to ((0_{𝑝} \leq_{f} f \to f : ℝ ⟶ [0, +∞)) \leftrightarrow (0_{𝑝} \leq_{f} P (m) \to P (m) : ℝ ⟶ [0, +∞)))$
42		i1ff	$⊢ f \in dom \int^{1} \to f : ℝ ⟶ ℝ$
43	42	ffnd	$⊢ f \in dom \int^{1} \to f Fn ℝ$
44	43	adantr	$⊢ (f \in dom \int^{1} \land 0_{𝑝} \leq_{f} f) \to f Fn ℝ$
45		0cn	$⊢ 0 \in ℂ$
46		fnconstg	$⊢ 0 \in ℂ \to (ℂ \times \{0\}) Fn ℂ$
47	45 46	ax-mp	$⊢ (ℂ \times \{0\}) Fn ℂ$
48		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
49	48	fneq1i	$⊢ 0_{𝑝} Fn ℂ \leftrightarrow (ℂ \times \{0\}) Fn ℂ$
50	47 49	mpbir	$⊢ 0_{𝑝} Fn ℂ$
51	50	a1i	$⊢ f \in dom \int^{1} \to 0_{𝑝} Fn ℂ$
52		cnex	$⊢ ℂ \in V$
53	52	a1i	$⊢ f \in dom \int^{1} \to ℂ \in V$
54	16	a1i	$⊢ f \in dom \int^{1} \to ℝ \in V$
55		ax-resscn	$⊢ ℝ \subseteq ℂ$
56		sseqin2	$⊢ ℝ \subseteq ℂ \leftrightarrow ℂ \cap ℝ = ℝ$
57	55 56	mpbi	$⊢ ℂ \cap ℝ = ℝ$
58		0pval	$⊢ x \in ℂ \to 0_{𝑝} (x) = 0$
59	58	adantl	$⊢ (f \in dom \int^{1} \land x \in ℂ) \to 0_{𝑝} (x) = 0$
60		eqidd	$⊢ (f \in dom \int^{1} \land x \in ℝ) \to f (x) = f (x)$
61	51 43 53 54 57 59 60	ofrfval	$⊢ f \in dom \int^{1} \to (0_{𝑝} \leq_{f} f \leftrightarrow \forall x \in ℝ 0 \leq f (x))$
62	61	biimpa	$⊢ (f \in dom \int^{1} \land 0_{𝑝} \leq_{f} f) \to \forall x \in ℝ 0 \leq f (x)$
63	42	ffvelcdmda	$⊢ (f \in dom \int^{1} \land x \in ℝ) \to f (x) \in ℝ$
64		elrege0	$⊢ f (x) \in [0, +∞) \leftrightarrow (f (x) \in ℝ \land 0 \leq f (x))$
65	64	simplbi2	$⊢ f (x) \in ℝ \to (0 \leq f (x) \to f (x) \in [0, +∞))$
66	63 65	syl	$⊢ (f \in dom \int^{1} \land x \in ℝ) \to (0 \leq f (x) \to f (x) \in [0, +∞))$
67	66	ralimdva	$⊢ f \in dom \int^{1} \to (\forall x \in ℝ 0 \leq f (x) \to \forall x \in ℝ f (x) \in [0, +∞))$
68	67	imp	$⊢ (f \in dom \int^{1} \land \forall x \in ℝ 0 \leq f (x)) \to \forall x \in ℝ f (x) \in [0, +∞)$
69	62 68	syldan	$⊢ (f \in dom \int^{1} \land 0_{𝑝} \leq_{f} f) \to \forall x \in ℝ f (x) \in [0, +∞)$
70		ffnfv	$⊢ f : ℝ ⟶ [0, +∞) \leftrightarrow (f Fn ℝ \land \forall x \in ℝ f (x) \in [0, +∞))$
71	44 69 70	sylanbrc	$⊢ (f \in dom \int^{1} \land 0_{𝑝} \leq_{f} f) \to f : ℝ ⟶ [0, +∞)$
72	71	ex	$⊢ f \in dom \int^{1} \to (0_{𝑝} \leq_{f} f \to f : ℝ ⟶ [0, +∞))$
73	41 72	vtoclga	$⊢ P (m) \in dom \int^{1} \to (0_{𝑝} \leq_{f} P (m) \to P (m) : ℝ ⟶ [0, +∞))$
74	30 38 73	sylc	$⊢ (φ \land m \in ℕ) \to P (m) : ℝ ⟶ [0, +∞)$
75	10	ffvelcdmda	$⊢ (φ \land m \in ℕ) \to Q (m) \in dom \int^{1}$
76		fveq2	$⊢ n = m \to Q (n) = Q (m)$
77	76	breq2d	$⊢ n = m \to (0_{𝑝} \leq_{f} Q (n) \leftrightarrow 0_{𝑝} \leq_{f} Q (m))$
78		fvoveq1	$⊢ n = m \to Q (n + 1) = Q (m + 1)$
79	76 78	breq12d	$⊢ n = m \to (Q (n) \leq_{f} Q (n + 1) \leftrightarrow Q (m) \leq_{f} Q (m + 1))$
80	77 79	anbi12d	$⊢ n = m \to ((0_{𝑝} \leq_{f} Q (n) \land Q (n) \leq_{f} Q (n + 1)) \leftrightarrow (0_{𝑝} \leq_{f} Q (m) \land Q (m) \leq_{f} Q (m + 1)))$
81	80	rspccva	$⊢ (\forall n \in ℕ (0_{𝑝} \leq_{f} Q (n) \land Q (n) \leq_{f} Q (n + 1)) \land m \in ℕ) \to (0_{𝑝} \leq_{f} Q (m) \land Q (m) \leq_{f} Q (m + 1))$
82	11 81	sylan	$⊢ (φ \land m \in ℕ) \to (0_{𝑝} \leq_{f} Q (m) \land Q (m) \leq_{f} Q (m + 1))$
83	82	simpld	$⊢ (φ \land m \in ℕ) \to 0_{𝑝} \leq_{f} Q (m)$
84		breq2	$⊢ f = Q (m) \to (0_{𝑝} \leq_{f} f \leftrightarrow 0_{𝑝} \leq_{f} Q (m))$
85		feq1	$⊢ f = Q (m) \to (f : ℝ ⟶ [0, +∞) \leftrightarrow Q (m) : ℝ ⟶ [0, +∞))$
86	84 85	imbi12d	$⊢ f = Q (m) \to ((0_{𝑝} \leq_{f} f \to f : ℝ ⟶ [0, +∞)) \leftrightarrow (0_{𝑝} \leq_{f} Q (m) \to Q (m) : ℝ ⟶ [0, +∞)))$
87	86 72	vtoclga	$⊢ Q (m) \in dom \int^{1} \to (0_{𝑝} \leq_{f} Q (m) \to Q (m) : ℝ ⟶ [0, +∞))$
88	75 83 87	sylc	$⊢ (φ \land m \in ℕ) \to Q (m) : ℝ ⟶ [0, +∞)$
89	16	a1i	$⊢ (φ \land m \in ℕ) \to ℝ \in V$
90	29 74 88 89 89 18	off	$⊢ (φ \land m \in ℕ) \to (P (m) +_{f} Q (m)) : ℝ ⟶ [0, +∞)$
91		0plef	$⊢ (P (m) +_{f} Q (m)) : ℝ ⟶ [0, +∞) \leftrightarrow ((P (m) +_{f} Q (m)) : ℝ ⟶ ℝ \land 0_{𝑝} \leq_{f} (P (m) +_{f} Q (m)))$
92	90 91	sylib	$⊢ (φ \land m \in ℕ) \to ((P (m) +_{f} Q (m)) : ℝ ⟶ ℝ \land 0_{𝑝} \leq_{f} (P (m) +_{f} Q (m)))$
93	92	simprd	$⊢ (φ \land m \in ℕ) \to 0_{𝑝} \leq_{f} (P (m) +_{f} Q (m))$
94	7	ffnd	$⊢ φ \to P Fn ℕ$
95	10	ffnd	$⊢ φ \to Q Fn ℕ$
96		eqidd	$⊢ (φ \land m \in ℕ) \to P (m) = P (m)$
97		eqidd	$⊢ (φ \land m \in ℕ) \to Q (m) = Q (m)$
98	94 95 25 25 26 96 97	ofval	$⊢ (φ \land m \in ℕ) \to (P {\circ_{f} +}_{f} Q) (m) = P (m) +_{f} Q (m)$
99	93 98	breqtrrd	$⊢ (φ \land m \in ℕ) \to 0_{𝑝} \leq_{f} (P {\circ_{f} +}_{f} Q) (m)$
100		i1ff	$⊢ P (m) \in dom \int^{1} \to P (m) : ℝ ⟶ ℝ$
101	30 100	syl	$⊢ (φ \land m \in ℕ) \to P (m) : ℝ ⟶ ℝ$
102	101	ffvelcdmda	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m) (y) \in ℝ$
103		i1ff	$⊢ Q (m) \in dom \int^{1} \to Q (m) : ℝ ⟶ ℝ$
104	75 103	syl	$⊢ (φ \land m \in ℕ) \to Q (m) : ℝ ⟶ ℝ$
105	104	ffvelcdmda	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to Q (m) (y) \in ℝ$
106		peano2nn	$⊢ m \in ℕ \to m + 1 \in ℕ$
107		ffvelcdm	$⊢ (P : ℕ ⟶ dom \int^{1} \land m + 1 \in ℕ) \to P (m + 1) \in dom \int^{1}$
108	7 106 107	syl2an	$⊢ (φ \land m \in ℕ) \to P (m + 1) \in dom \int^{1}$
109		i1ff	$⊢ P (m + 1) \in dom \int^{1} \to P (m + 1) : ℝ ⟶ ℝ$
110	108 109	syl	$⊢ (φ \land m \in ℕ) \to P (m + 1) : ℝ ⟶ ℝ$
111	110	ffvelcdmda	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m + 1) (y) \in ℝ$
112		ffvelcdm	$⊢ (Q : ℕ ⟶ dom \int^{1} \land m + 1 \in ℕ) \to Q (m + 1) \in dom \int^{1}$
113	10 106 112	syl2an	$⊢ (φ \land m \in ℕ) \to Q (m + 1) \in dom \int^{1}$
114		i1ff	$⊢ Q (m + 1) \in dom \int^{1} \to Q (m + 1) : ℝ ⟶ ℝ$
115	113 114	syl	$⊢ (φ \land m \in ℕ) \to Q (m + 1) : ℝ ⟶ ℝ$
116	115	ffvelcdmda	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to Q (m + 1) (y) \in ℝ$
117	37	simprd	$⊢ (φ \land m \in ℕ) \to P (m) \leq_{f} P (m + 1)$
118	101	ffnd	$⊢ (φ \land m \in ℕ) \to P (m) Fn ℝ$
119	110	ffnd	$⊢ (φ \land m \in ℕ) \to P (m + 1) Fn ℝ$
120		eqidd	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m) (y) = P (m) (y)$
121		eqidd	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m + 1) (y) = P (m + 1) (y)$
122	118 119 89 89 18 120 121	ofrfval	$⊢ (φ \land m \in ℕ) \to (P (m) \leq_{f} P (m + 1) \leftrightarrow \forall y \in ℝ P (m) (y) \leq P (m + 1) (y))$
123	117 122	mpbid	$⊢ (φ \land m \in ℕ) \to \forall y \in ℝ P (m) (y) \leq P (m + 1) (y)$
124	123	r19.21bi	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m) (y) \leq P (m + 1) (y)$
125	82	simprd	$⊢ (φ \land m \in ℕ) \to Q (m) \leq_{f} Q (m + 1)$
126	104	ffnd	$⊢ (φ \land m \in ℕ) \to Q (m) Fn ℝ$
127	115	ffnd	$⊢ (φ \land m \in ℕ) \to Q (m + 1) Fn ℝ$
128		eqidd	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to Q (m) (y) = Q (m) (y)$
129		eqidd	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to Q (m + 1) (y) = Q (m + 1) (y)$
130	126 127 89 89 18 128 129	ofrfval	$⊢ (φ \land m \in ℕ) \to (Q (m) \leq_{f} Q (m + 1) \leftrightarrow \forall y \in ℝ Q (m) (y) \leq Q (m + 1) (y))$
131	125 130	mpbid	$⊢ (φ \land m \in ℕ) \to \forall y \in ℝ Q (m) (y) \leq Q (m + 1) (y)$
132	131	r19.21bi	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to Q (m) (y) \leq Q (m + 1) (y)$
133	102 105 111 116 124 132	le2addd	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m) (y) + Q (m) (y) \leq P (m + 1) (y) + Q (m + 1) (y)$
134	133	ralrimiva	$⊢ (φ \land m \in ℕ) \to \forall y \in ℝ P (m) (y) + Q (m) (y) \leq P (m + 1) (y) + Q (m + 1) (y)$
135	30 75	i1fadd	$⊢ (φ \land m \in ℕ) \to P (m) +_{f} Q (m) \in dom \int^{1}$
136		i1ff	$⊢ P (m) +_{f} Q (m) \in dom \int^{1} \to (P (m) +_{f} Q (m)) : ℝ ⟶ ℝ$
137		ffn	$⊢ (P (m) +_{f} Q (m)) : ℝ ⟶ ℝ \to (P (m) +_{f} Q (m)) Fn ℝ$
138	135 136 137	3syl	$⊢ (φ \land m \in ℕ) \to (P (m) +_{f} Q (m)) Fn ℝ$
139	108 113	i1fadd	$⊢ (φ \land m \in ℕ) \to P (m + 1) +_{f} Q (m + 1) \in dom \int^{1}$
140		i1ff	$⊢ P (m + 1) +_{f} Q (m + 1) \in dom \int^{1} \to (P (m + 1) +_{f} Q (m + 1)) : ℝ ⟶ ℝ$
141	139 140	syl	$⊢ (φ \land m \in ℕ) \to (P (m + 1) +_{f} Q (m + 1)) : ℝ ⟶ ℝ$
142	141	ffnd	$⊢ (φ \land m \in ℕ) \to (P (m + 1) +_{f} Q (m + 1)) Fn ℝ$
143	118 126 89 89 18 120 128	ofval	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to (P (m) +_{f} Q (m)) (y) = P (m) (y) + Q (m) (y)$
144	119 127 89 89 18 121 129	ofval	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to (P (m + 1) +_{f} Q (m + 1)) (y) = P (m + 1) (y) + Q (m + 1) (y)$
145	138 142 89 89 18 143 144	ofrfval	$⊢ (φ \land m \in ℕ) \to ((P (m) +_{f} Q (m)) \leq_{f} (P (m + 1) +_{f} Q (m + 1)) \leftrightarrow \forall y \in ℝ P (m) (y) + Q (m) (y) \leq P (m + 1) (y) + Q (m + 1) (y))$
146	134 145	mpbird	$⊢ (φ \land m \in ℕ) \to (P (m) +_{f} Q (m)) \leq_{f} (P (m + 1) +_{f} Q (m + 1))$
147		eqidd	$⊢ (φ \land m + 1 \in ℕ) \to P (m + 1) = P (m + 1)$
148		eqidd	$⊢ (φ \land m + 1 \in ℕ) \to Q (m + 1) = Q (m + 1)$
149	94 95 25 25 26 147 148	ofval	$⊢ (φ \land m + 1 \in ℕ) \to (P {\circ_{f} +}_{f} Q) (m + 1) = P (m + 1) +_{f} Q (m + 1)$
150	106 149	sylan2	$⊢ (φ \land m \in ℕ) \to (P {\circ_{f} +}_{f} Q) (m + 1) = P (m + 1) +_{f} Q (m + 1)$
151	146 98 150	3brtr4d	$⊢ (φ \land m \in ℕ) \to (P {\circ_{f} +}_{f} Q) (m) \leq_{f} (P {\circ_{f} +}_{f} Q) (m + 1)$
152	99 151	jca	$⊢ (φ \land m \in ℕ) \to (0_{𝑝} \leq_{f} (P {\circ_{f} +}_{f} Q) (m) \land (P {\circ_{f} +}_{f} Q) (m) \leq_{f} (P {\circ_{f} +}_{f} Q) (m + 1))$
153	152	ralrimiva	$⊢ φ \to \forall m \in ℕ (0_{𝑝} \leq_{f} (P {\circ_{f} +}_{f} Q) (m) \land (P {\circ_{f} +}_{f} Q) (m) \leq_{f} (P {\circ_{f} +}_{f} Q) (m + 1))$
154		fveq2	$⊢ n = m \to (P {\circ_{f} +}_{f} Q) (n) = (P {\circ_{f} +}_{f} Q) (m)$
155	154	fveq1d	$⊢ n = m \to (P {\circ_{f} +}_{f} Q) (n) (y) = (P {\circ_{f} +}_{f} Q) (m) (y)$
156	155	cbvmptv	$⊢ (n \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (n) (y)) = (m \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (m) (y))$
157		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
158		1zzd	$⊢ (φ \land y \in ℝ) \to 1 \in ℤ$
159		fveq2	$⊢ x = y \to P (n) (x) = P (n) (y)$
160	159	mpteq2dv	$⊢ x = y \to (n \in ℕ ⟼ P (n) (x)) = (n \in ℕ ⟼ P (n) (y))$
161		fveq2	$⊢ x = y \to F (x) = F (y)$
162	160 161	breq12d	$⊢ x = y \to ((n \in ℕ ⟼ P (n) (x)) ⇝ F (x) \leftrightarrow (n \in ℕ ⟼ P (n) (y)) ⇝ F (y))$
163	162	rspccva	$⊢ (\forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x) \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) ⇝ F (y)$
164	9 163	sylan	$⊢ (φ \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) ⇝ F (y)$
165	24	mptex	$⊢ (n \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (n) (y)) \in V$
166	165	a1i	$⊢ (φ \land y \in ℝ) \to (n \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (n) (y)) \in V$
167		fveq2	$⊢ x = y \to Q (n) (x) = Q (n) (y)$
168	167	mpteq2dv	$⊢ x = y \to (n \in ℕ ⟼ Q (n) (x)) = (n \in ℕ ⟼ Q (n) (y))$
169		fveq2	$⊢ x = y \to G (x) = G (y)$
170	168 169	breq12d	$⊢ x = y \to ((n \in ℕ ⟼ Q (n) (x)) ⇝ G (x) \leftrightarrow (n \in ℕ ⟼ Q (n) (y)) ⇝ G (y))$
171	170	rspccva	$⊢ (\forall x \in ℝ (n \in ℕ ⟼ Q (n) (x)) ⇝ G (x) \land y \in ℝ) \to (n \in ℕ ⟼ Q (n) (y)) ⇝ G (y)$
172	12 171	sylan	$⊢ (φ \land y \in ℝ) \to (n \in ℕ ⟼ Q (n) (y)) ⇝ G (y)$
173	31	fveq1d	$⊢ n = m \to P (n) (y) = P (m) (y)$
174		eqid	$⊢ (n \in ℕ ⟼ P (n) (y)) = (n \in ℕ ⟼ P (n) (y))$
175		fvex	$⊢ P (m) (y) \in V$
176	173 174 175	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ P (n) (y)) (m) = P (m) (y)$
177	176	adantl	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (m) = P (m) (y)$
178	102	an32s	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to P (m) (y) \in ℝ$
179	177 178	eqeltrd	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (m) \in ℝ$
180	179	recnd	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (m) \in ℂ$
181	76	fveq1d	$⊢ n = m \to Q (n) (y) = Q (m) (y)$
182		eqid	$⊢ (n \in ℕ ⟼ Q (n) (y)) = (n \in ℕ ⟼ Q (n) (y))$
183		fvex	$⊢ Q (m) (y) \in V$
184	181 182 183	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ Q (n) (y)) (m) = Q (m) (y)$
185	184	adantl	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ Q (n) (y)) (m) = Q (m) (y)$
186	105	an32s	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to Q (m) (y) \in ℝ$
187	185 186	eqeltrd	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ Q (n) (y)) (m) \in ℝ$
188	187	recnd	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ Q (n) (y)) (m) \in ℂ$
189	98	fveq1d	$⊢ (φ \land m \in ℕ) \to (P {\circ_{f} +}_{f} Q) (m) (y) = (P (m) +_{f} Q (m)) (y)$
190	189	adantr	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to (P {\circ_{f} +}_{f} Q) (m) (y) = (P (m) +_{f} Q (m)) (y)$
191	190 143	eqtrd	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to (P {\circ_{f} +}_{f} Q) (m) (y) = P (m) (y) + Q (m) (y)$
192	191	an32s	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (P {\circ_{f} +}_{f} Q) (m) (y) = P (m) (y) + Q (m) (y)$
193		eqid	$⊢ (n \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (n) (y)) = (n \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (n) (y))$
194		fvex	$⊢ (P {\circ_{f} +}_{f} Q) (m) (y) \in V$
195	155 193 194	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (n) (y)) (m) = (P {\circ_{f} +}_{f} Q) (m) (y)$
196	195	adantl	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (n) (y)) (m) = (P {\circ_{f} +}_{f} Q) (m) (y)$
197	177 185	oveq12d	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (m) + (n \in ℕ ⟼ Q (n) (y)) (m) = P (m) (y) + Q (m) (y)$
198	192 196 197	3eqtr4d	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (n) (y)) (m) = (n \in ℕ ⟼ P (n) (y)) (m) + (n \in ℕ ⟼ Q (n) (y)) (m)$
199	157 158 164 166 172 180 188 198	climadd	$⊢ (φ \land y \in ℝ) \to (n \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (n) (y)) ⇝ (F (y) + G (y))$
200	156 199	eqbrtrrid	$⊢ (φ \land y \in ℝ) \to (m \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (m) (y)) ⇝ (F (y) + G (y))$
201	2	ffnd	$⊢ φ \to F Fn ℝ$
202	5	ffnd	$⊢ φ \to G Fn ℝ$
203		eqidd	$⊢ (φ \land y \in ℝ) \to F (y) = F (y)$
204		eqidd	$⊢ (φ \land y \in ℝ) \to G (y) = G (y)$
205	201 202 17 17 18 203 204	ofval	$⊢ (φ \land y \in ℝ) \to (F +_{f} G) (y) = F (y) + G (y)$
206	200 205	breqtrrd	$⊢ (φ \land y \in ℝ) \to (m \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (m) (y)) ⇝ (F +_{f} G) (y)$
207	206	ralrimiva	$⊢ φ \to \forall y \in ℝ (m \in ℕ ⟼ (P {\circ_{f} +}_{f} Q) (m) (y)) ⇝ (F +_{f} G) (y)$
208		2fveq3	$⊢ n = j \to \int^{1} ((P {\circ_{f} +}_{f} Q) (n)) = \int^{1} ((P {\circ_{f} +}_{f} Q) (j))$
209	208	cbvmptv	$⊢ (n \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (n))) = (j \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (j)))$
210	3 6	readdcld	$⊢ φ \to \int^{2} (F) + \int^{2} (G) \in ℝ$
211	98	fveq2d	$⊢ (φ \land m \in ℕ) \to \int^{1} ((P {\circ_{f} +}_{f} Q) (m)) = \int^{1} (P (m) +_{f} Q (m))$
212	30 75	itg1add	$⊢ (φ \land m \in ℕ) \to \int^{1} (P (m) +_{f} Q (m)) = \int^{1} (P (m)) + \int^{1} (Q (m))$
213	211 212	eqtrd	$⊢ (φ \land m \in ℕ) \to \int^{1} ((P {\circ_{f} +}_{f} Q) (m)) = \int^{1} (P (m)) + \int^{1} (Q (m))$
214		itg1cl	$⊢ P (m) \in dom \int^{1} \to \int^{1} (P (m)) \in ℝ$
215	30 214	syl	$⊢ (φ \land m \in ℕ) \to \int^{1} (P (m)) \in ℝ$
216		itg1cl	$⊢ Q (m) \in dom \int^{1} \to \int^{1} (Q (m)) \in ℝ$
217	75 216	syl	$⊢ (φ \land m \in ℕ) \to \int^{1} (Q (m)) \in ℝ$
218	3	adantr	$⊢ (φ \land m \in ℕ) \to \int^{2} (F) \in ℝ$
219	6	adantr	$⊢ (φ \land m \in ℕ) \to \int^{2} (G) \in ℝ$
220	2	adantr	$⊢ (φ \land m \in ℕ) \to F : ℝ ⟶ [0, +∞)$
221		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
222		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F : ℝ ⟶ [0, +∞]$
223	220 221 222	sylancl	$⊢ (φ \land m \in ℕ) \to F : ℝ ⟶ [0, +∞]$
224	1 2 7 8 9	itg2i1fseqle	$⊢ (φ \land m \in ℕ) \to P (m) \leq_{f} F$
225		itg2ub	$⊢ (F : ℝ ⟶ [0, +∞] \land P (m) \in dom \int^{1} \land P (m) \leq_{f} F) \to \int^{1} (P (m)) \leq \int^{2} (F)$
226	223 30 224 225	syl3anc	$⊢ (φ \land m \in ℕ) \to \int^{1} (P (m)) \leq \int^{2} (F)$
227	5	adantr	$⊢ (φ \land m \in ℕ) \to G : ℝ ⟶ [0, +∞)$
228		fss	$⊢ (G : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to G : ℝ ⟶ [0, +∞]$
229	227 221 228	sylancl	$⊢ (φ \land m \in ℕ) \to G : ℝ ⟶ [0, +∞]$
230	4 5 10 11 12	itg2i1fseqle	$⊢ (φ \land m \in ℕ) \to Q (m) \leq_{f} G$
231		itg2ub	$⊢ (G : ℝ ⟶ [0, +∞] \land Q (m) \in dom \int^{1} \land Q (m) \leq_{f} G) \to \int^{1} (Q (m)) \leq \int^{2} (G)$
232	229 75 230 231	syl3anc	$⊢ (φ \land m \in ℕ) \to \int^{1} (Q (m)) \leq \int^{2} (G)$
233	215 217 218 219 226 232	le2addd	$⊢ (φ \land m \in ℕ) \to \int^{1} (P (m)) + \int^{1} (Q (m)) \leq \int^{2} (F) + \int^{2} (G)$
234	213 233	eqbrtrd	$⊢ (φ \land m \in ℕ) \to \int^{1} ((P {\circ_{f} +}_{f} Q) (m)) \leq \int^{2} (F) + \int^{2} (G)$
235	234	ralrimiva	$⊢ φ \to \forall m \in ℕ \int^{1} ((P {\circ_{f} +}_{f} Q) (m)) \leq \int^{2} (F) + \int^{2} (G)$
236		2fveq3	$⊢ m = k \to \int^{1} ((P {\circ_{f} +}_{f} Q) (m)) = \int^{1} ((P {\circ_{f} +}_{f} Q) (k))$
237	236	breq1d	$⊢ m = k \to (\int^{1} ((P {\circ_{f} +}_{f} Q) (m)) \leq \int^{2} (F) + \int^{2} (G) \leftrightarrow \int^{1} ((P {\circ_{f} +}_{f} Q) (k)) \leq \int^{2} (F) + \int^{2} (G))$
238	237	rspccva	$⊢ (\forall m \in ℕ \int^{1} ((P {\circ_{f} +}_{f} Q) (m)) \leq \int^{2} (F) + \int^{2} (G) \land k \in ℕ) \to \int^{1} ((P {\circ_{f} +}_{f} Q) (k)) \leq \int^{2} (F) + \int^{2} (G)$
239	235 238	sylan	$⊢ (φ \land k \in ℕ) \to \int^{1} ((P {\circ_{f} +}_{f} Q) (k)) \leq \int^{2} (F) + \int^{2} (G)$
240	13 19 27 153 207 209 210 239	itg2i1fseq2	$⊢ φ \to (n \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (n))) ⇝ \int^{2} (F +_{f} G)$
241		1zzd	$⊢ φ \to 1 \in ℤ$
242		eqid	$⊢ (k \in ℕ ⟼ \int^{1} (P (k))) = (k \in ℕ ⟼ \int^{1} (P (k)))$
243	1 2 7 8 9 242 3	itg2i1fseq3	$⊢ φ \to (k \in ℕ ⟼ \int^{1} (P (k))) ⇝ \int^{2} (F)$
244	24	mptex	$⊢ (n \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (n))) \in V$
245	244	a1i	$⊢ φ \to (n \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (n))) \in V$
246		eqid	$⊢ (k \in ℕ ⟼ \int^{1} (Q (k))) = (k \in ℕ ⟼ \int^{1} (Q (k)))$
247	4 5 10 11 12 246 6	itg2i1fseq3	$⊢ φ \to (k \in ℕ ⟼ \int^{1} (Q (k))) ⇝ \int^{2} (G)$
248		2fveq3	$⊢ k = m \to \int^{1} (P (k)) = \int^{1} (P (m))$
249		fvex	$⊢ \int^{1} (P (m)) \in V$
250	248 242 249	fvmpt	$⊢ m \in ℕ \to (k \in ℕ ⟼ \int^{1} (P (k))) (m) = \int^{1} (P (m))$
251	250	adantl	$⊢ (φ \land m \in ℕ) \to (k \in ℕ ⟼ \int^{1} (P (k))) (m) = \int^{1} (P (m))$
252	215	recnd	$⊢ (φ \land m \in ℕ) \to \int^{1} (P (m)) \in ℂ$
253	251 252	eqeltrd	$⊢ (φ \land m \in ℕ) \to (k \in ℕ ⟼ \int^{1} (P (k))) (m) \in ℂ$
254		2fveq3	$⊢ k = m \to \int^{1} (Q (k)) = \int^{1} (Q (m))$
255		fvex	$⊢ \int^{1} (Q (m)) \in V$
256	254 246 255	fvmpt	$⊢ m \in ℕ \to (k \in ℕ ⟼ \int^{1} (Q (k))) (m) = \int^{1} (Q (m))$
257	256	adantl	$⊢ (φ \land m \in ℕ) \to (k \in ℕ ⟼ \int^{1} (Q (k))) (m) = \int^{1} (Q (m))$
258	217	recnd	$⊢ (φ \land m \in ℕ) \to \int^{1} (Q (m)) \in ℂ$
259	257 258	eqeltrd	$⊢ (φ \land m \in ℕ) \to (k \in ℕ ⟼ \int^{1} (Q (k))) (m) \in ℂ$
260		2fveq3	$⊢ j = m \to \int^{1} ((P {\circ_{f} +}_{f} Q) (j)) = \int^{1} ((P {\circ_{f} +}_{f} Q) (m))$
261		fvex	$⊢ \int^{1} ((P {\circ_{f} +}_{f} Q) (m)) \in V$
262	260 209 261	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (n))) (m) = \int^{1} ((P {\circ_{f} +}_{f} Q) (m))$
263	262	adantl	$⊢ (φ \land m \in ℕ) \to (n \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (n))) (m) = \int^{1} ((P {\circ_{f} +}_{f} Q) (m))$
264	251 257	oveq12d	$⊢ (φ \land m \in ℕ) \to (k \in ℕ ⟼ \int^{1} (P (k))) (m) + (k \in ℕ ⟼ \int^{1} (Q (k))) (m) = \int^{1} (P (m)) + \int^{1} (Q (m))$
265	213 263 264	3eqtr4d	$⊢ (φ \land m \in ℕ) \to (n \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (n))) (m) = (k \in ℕ ⟼ \int^{1} (P (k))) (m) + (k \in ℕ ⟼ \int^{1} (Q (k))) (m)$
266	157 241 243 245 247 253 259 265	climadd	$⊢ φ \to (n \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (n))) ⇝ (\int^{2} (F) + \int^{2} (G))$
267		climuni	$⊢ ((n \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (n))) ⇝ \int^{2} (F +_{f} G) \land (n \in ℕ ⟼ \int^{1} ((P {\circ_{f} +}_{f} Q) (n))) ⇝ (\int^{2} (F) + \int^{2} (G))) \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G)$
268	240 266 267	syl2anc	$⊢ φ \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G)$

Metamath Proof Explorer

Theorem itg2addlem

Proof