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 ( 𝜑 → ( 𝑃ff + 𝑄 ) : ℕ ⟶ 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 ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) = ( ( 𝑃𝑚 ) ∘f + ( 𝑄𝑚 ) ) )
99 93 98 breqtrrd ( ( 𝜑𝑚 ∈ ℕ ) → 0𝑝r ≤ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) )
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 ) ∈ ℕ ) → ( ( 𝑃ff + 𝑄 ) ‘ ( 𝑚 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ∘f + ( 𝑄 ‘ ( 𝑚 + 1 ) ) ) )
150 106 149 sylan2 ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑃ff + 𝑄 ) ‘ ( 𝑚 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ∘f + ( 𝑄 ‘ ( 𝑚 + 1 ) ) ) )
151 146 98 150 3brtr4d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ∘r ≤ ( ( 𝑃ff + 𝑄 ) ‘ ( 𝑚 + 1 ) ) )
152 99 151 jca ( ( 𝜑𝑚 ∈ ℕ ) → ( 0𝑝r ≤ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ∧ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ∘r ≤ ( ( 𝑃ff + 𝑄 ) ‘ ( 𝑚 + 1 ) ) ) )
153 152 ralrimiva ( 𝜑 → ∀ 𝑚 ∈ ℕ ( 0𝑝r ≤ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ∧ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ∘r ≤ ( ( 𝑃ff + 𝑄 ) ‘ ( 𝑚 + 1 ) ) ) )
154 fveq2 ( 𝑛 = 𝑚 → ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) = ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) )
155 154 fveq1d ( 𝑛 = 𝑚 → ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ‘ 𝑦 ) = ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) )
156 155 cbvmptv ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ‘ 𝑦 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) )
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 ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ‘ 𝑦 ) ) ∈ V
166 165 a1i ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ‘ 𝑦 ) ) ∈ 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 ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) = ( ( ( 𝑃𝑚 ) ∘f + ( 𝑄𝑚 ) ) ‘ 𝑦 ) )
190 189 adantr ( ( ( 𝜑𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) = ( ( ( 𝑃𝑚 ) ∘f + ( 𝑄𝑚 ) ) ‘ 𝑦 ) )
191 190 143 eqtrd ( ( ( 𝜑𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) = ( ( ( 𝑃𝑚 ) ‘ 𝑦 ) + ( ( 𝑄𝑚 ) ‘ 𝑦 ) ) )
192 191 an32s ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) = ( ( ( 𝑃𝑚 ) ‘ 𝑦 ) + ( ( 𝑄𝑚 ) ‘ 𝑦 ) ) )
193 eqid ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ‘ 𝑦 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ‘ 𝑦 ) )
194 fvex ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) ∈ V
195 155 193 194 fvmpt ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) = ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) )
196 195 adantl ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) = ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) )
197 177 185 oveq12d ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) + ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑄𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ) = ( ( ( 𝑃𝑚 ) ‘ 𝑦 ) + ( ( 𝑄𝑚 ) ‘ 𝑦 ) ) )
198 192 196 197 3eqtr4d ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) + ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑄𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ) )
199 157 158 164 166 172 180 188 198 climadd ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ ( ( 𝐹𝑦 ) + ( 𝐺𝑦 ) ) )
200 156 199 eqbrtrrid ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) ) ⇝ ( ( 𝐹𝑦 ) + ( 𝐺𝑦 ) ) )
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 ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) ) ⇝ ( ( 𝐹f + 𝐺 ) ‘ 𝑦 ) )
207 206 ralrimiva ( 𝜑 → ∀ 𝑦 ∈ ℝ ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ‘ 𝑦 ) ) ⇝ ( ( 𝐹f + 𝐺 ) ‘ 𝑦 ) )
208 2fveq3 ( 𝑛 = 𝑗 → ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) = ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑗 ) ) )
209 208 cbvmptv ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑗 ) ) )
210 3 6 readdcld ( 𝜑 → ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ∈ ℝ )
211 98 fveq2d ( ( 𝜑𝑚 ∈ ℕ ) → ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) = ( ∫1 ‘ ( ( 𝑃𝑚 ) ∘f + ( 𝑄𝑚 ) ) ) )
212 30 75 itg1add ( ( 𝜑𝑚 ∈ ℕ ) → ( ∫1 ‘ ( ( 𝑃𝑚 ) ∘f + ( 𝑄𝑚 ) ) ) = ( ( ∫1 ‘ ( 𝑃𝑚 ) ) + ( ∫1 ‘ ( 𝑄𝑚 ) ) ) )
213 211 212 eqtrd ( ( 𝜑𝑚 ∈ ℕ ) → ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) = ( ( ∫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 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )
235 234 ralrimiva ( 𝜑 → ∀ 𝑚 ∈ ℕ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )
236 2fveq3 ( 𝑚 = 𝑘 → ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) = ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑘 ) ) )
237 236 breq1d ( 𝑚 = 𝑘 → ( ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ↔ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑘 ) ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ) )
238 237 rspccva ( ( ∀ 𝑚 ∈ ℕ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ∧ 𝑘 ∈ ℕ ) → ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑘 ) ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )
239 235 238 sylan ( ( 𝜑𝑘 ∈ ℕ ) → ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑘 ) ) ≤ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )
240 13 19 27 153 207 209 210 239 itg2i1fseq2 ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) ) ⇝ ( ∫2 ‘ ( 𝐹f + 𝐺 ) ) )
241 1zzd ( 𝜑 → 1 ∈ ℤ )
242 eqid ( 𝑘 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃𝑘 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃𝑘 ) ) )
243 1 2 7 8 9 242 3 itg2i1fseq3 ( 𝜑 → ( 𝑘 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃𝑘 ) ) ) ⇝ ( ∫2𝐹 ) )
244 24 mptex ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) ) ∈ V
245 244 a1i ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) ) ∈ 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 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑗 ) ) = ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) )
261 fvex ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) ∈ V
262 260 209 261 fvmpt ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) ) ‘ 𝑚 ) = ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) )
263 262 adantl ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) ) ‘ 𝑚 ) = ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑚 ) ) )
264 251 257 oveq12d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( 𝑘 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃𝑘 ) ) ) ‘ 𝑚 ) + ( ( 𝑘 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑄𝑘 ) ) ) ‘ 𝑚 ) ) = ( ( ∫1 ‘ ( 𝑃𝑚 ) ) + ( ∫1 ‘ ( 𝑄𝑚 ) ) ) )
265 213 263 264 3eqtr4d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) ) ‘ 𝑚 ) = ( ( ( 𝑘 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃𝑘 ) ) ) ‘ 𝑚 ) + ( ( 𝑘 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑄𝑘 ) ) ) ‘ 𝑚 ) ) )
266 157 241 243 245 247 253 259 265 climadd ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) ) ⇝ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )
267 climuni ( ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) ) ⇝ ( ∫2 ‘ ( 𝐹f + 𝐺 ) ) ∧ ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( ( 𝑃ff + 𝑄 ) ‘ 𝑛 ) ) ) ⇝ ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) ) → ( ∫2 ‘ ( 𝐹f + 𝐺 ) ) = ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )
268 240 266 267 syl2anc ( 𝜑 → ( ∫2 ‘ ( 𝐹f + 𝐺 ) ) = ( ( ∫2𝐹 ) + ( ∫2𝐺 ) ) )