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

Metamath Proof Explorer

Theorem itg2addlem

Description: Lemma for itg2add . (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itg2add.f1 
|- ( ph -> F e. MblFn )
itg2add.f2 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2add.f3 
|- ( ph -> ( S.2 ` F ) e. RR )
itg2add.g1 
|- ( ph -> G e. MblFn )
itg2add.g2 
|- ( ph -> G : RR --> ( 0 [,) +oo ) )
itg2add.g3 
|- ( ph -> ( S.2 ` G ) e. RR )
itg2add.p1 
|- ( ph -> P : NN --> dom S.1 )
itg2add.p2 
|- ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )
itg2add.p3 
|- ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )
itg2add.q1 
|- ( ph -> Q : NN --> dom S.1 )
itg2add.q2 
|- ( ph -> A. n e. NN ( 0p oR <_ ( Q ` n ) /\ ( Q ` n ) oR <_ ( Q ` ( n + 1 ) ) ) )
itg2add.q3 
|- ( ph -> A. x e. RR ( n e. NN |-> ( ( Q ` n ) ` x ) ) ~~> ( G ` x ) )
Assertion itg2addlem 
|- ( ph -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )

Proof

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