This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itg2add

Description: The S.2 integral is linear. (Measurability is an essential component of this theorem; otherwise consider the characteristic function of a nonmeasurable set and its complement.) (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itg2add.f1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
itg2add.f2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2add.f3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
itg2add.g1 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
itg2add.g2 ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2add.g3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ∈ ℝ )
Assertion itg2add ( 𝜑 → ( ∫2 ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 itg2add.f1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 itg2add.f2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
3 itg2add.f3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
4 itg2add.g1 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
5 itg2add.g2 ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ( 0 [,) +∞ ) )
6 itg2add.g3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ∈ ℝ )
7 1 2 mbfi1fseq ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )
8 4 5 mbfi1fseq ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) )
9 exdistrv ⊢ ( ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) )
10 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → 𝐹 ∈ MblFn )
11 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
12 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
13 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → 𝐺 ∈ MblFn )
14 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → 𝐺 : ℝ ⟶ ( 0 [,) +∞ ) )
15 6 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → ( ∫2 ‘ 𝐺 ) ∈ ℝ )
16 simprl1 ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → 𝑓 : ℕ ⟶ dom ∫1 )
17 simprl2 ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) )
18 simprl3 ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) )
19 simprr1 ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → 𝑔 : ℕ ⟶ dom ∫1 )
20 simprr2 ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) )
21 simprr3 ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) )
22 10 11 12 13 14 15 16 17 18 19 20 21 itg2addlem ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) ) → ( ∫2 ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) )
23 22 ex ⊢ ( 𝜑 → ( ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) → ( ∫2 ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ) )
24 23 exlimdvv ⊢ ( 𝜑 → ( ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) → ( ∫2 ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ) )
25 9 24 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ∧ ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) ) → ( ∫2 ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ) )
26 7 8 25 mp2and ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) )