Metamath Proof Explorer

Theorem itg2addlem

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