Metamath Proof Explorer


Theorem itg2seq

Description: Definitional property of the S.2 integral: for any function F there is a countable sequence g of simple functions less than F whose integrals converge to the integral of F . (This theorem is for the most part unnecessary in lieu of itg2i1fseq , but unlike that theorem this one doesn't require F to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014)

Ref Expression
Assertion itg2seq F : 0 +∞ g g : dom 1 n g n f F 2 F = sup ran n 1 g n * <

Proof

Step Hyp Ref Expression
1 nnre n n
2 1 ad2antlr F : 0 +∞ n 2 F = +∞ n
3 2 ltpnfd F : 0 +∞ n 2 F = +∞ n < +∞
4 iftrue 2 F = +∞ if 2 F = +∞ n 2 F 1 n = n
5 4 adantl F : 0 +∞ n 2 F = +∞ if 2 F = +∞ n 2 F 1 n = n
6 simpr F : 0 +∞ n 2 F = +∞ 2 F = +∞
7 3 5 6 3brtr4d F : 0 +∞ n 2 F = +∞ if 2 F = +∞ n 2 F 1 n < 2 F
8 iffalse ¬ 2 F = +∞ if 2 F = +∞ n 2 F 1 n = 2 F 1 n
9 8 adantl F : 0 +∞ n ¬ 2 F = +∞ if 2 F = +∞ n 2 F 1 n = 2 F 1 n
10 itg2cl F : 0 +∞ 2 F *
11 xrrebnd 2 F * 2 F −∞ < 2 F 2 F < +∞
12 10 11 syl F : 0 +∞ 2 F −∞ < 2 F 2 F < +∞
13 itg2ge0 F : 0 +∞ 0 2 F
14 mnflt0 −∞ < 0
15 mnfxr −∞ *
16 0xr 0 *
17 xrltletr −∞ * 0 * 2 F * −∞ < 0 0 2 F −∞ < 2 F
18 15 16 10 17 mp3an12i F : 0 +∞ −∞ < 0 0 2 F −∞ < 2 F
19 14 18 mpani F : 0 +∞ 0 2 F −∞ < 2 F
20 13 19 mpd F : 0 +∞ −∞ < 2 F
21 20 biantrurd F : 0 +∞ 2 F < +∞ −∞ < 2 F 2 F < +∞
22 nltpnft 2 F * 2 F = +∞ ¬ 2 F < +∞
23 10 22 syl F : 0 +∞ 2 F = +∞ ¬ 2 F < +∞
24 23 con2bid F : 0 +∞ 2 F < +∞ ¬ 2 F = +∞
25 12 21 24 3bitr2rd F : 0 +∞ ¬ 2 F = +∞ 2 F
26 25 biimpa F : 0 +∞ ¬ 2 F = +∞ 2 F
27 26 adantlr F : 0 +∞ n ¬ 2 F = +∞ 2 F
28 nnrp n n +
29 28 rpreccld n 1 n +
30 29 ad2antlr F : 0 +∞ n ¬ 2 F = +∞ 1 n +
31 27 30 ltsubrpd F : 0 +∞ n ¬ 2 F = +∞ 2 F 1 n < 2 F
32 9 31 eqbrtrd F : 0 +∞ n ¬ 2 F = +∞ if 2 F = +∞ n 2 F 1 n < 2 F
33 7 32 pm2.61dan F : 0 +∞ n if 2 F = +∞ n 2 F 1 n < 2 F
34 nnrecre n 1 n
35 34 ad2antlr F : 0 +∞ n ¬ 2 F = +∞ 1 n
36 27 35 resubcld F : 0 +∞ n ¬ 2 F = +∞ 2 F 1 n
37 2 36 ifclda F : 0 +∞ n if 2 F = +∞ n 2 F 1 n
38 37 rexrd F : 0 +∞ n if 2 F = +∞ n 2 F 1 n *
39 10 adantr F : 0 +∞ n 2 F *
40 xrltnle if 2 F = +∞ n 2 F 1 n * 2 F * if 2 F = +∞ n 2 F 1 n < 2 F ¬ 2 F if 2 F = +∞ n 2 F 1 n
41 38 39 40 syl2anc F : 0 +∞ n if 2 F = +∞ n 2 F 1 n < 2 F ¬ 2 F if 2 F = +∞ n 2 F 1 n
42 33 41 mpbid F : 0 +∞ n ¬ 2 F if 2 F = +∞ n 2 F 1 n
43 itg2leub F : 0 +∞ if 2 F = +∞ n 2 F 1 n * 2 F if 2 F = +∞ n 2 F 1 n f dom 1 f f F 1 f if 2 F = +∞ n 2 F 1 n
44 38 43 syldan F : 0 +∞ n 2 F if 2 F = +∞ n 2 F 1 n f dom 1 f f F 1 f if 2 F = +∞ n 2 F 1 n
45 42 44 mtbid F : 0 +∞ n ¬ f dom 1 f f F 1 f if 2 F = +∞ n 2 F 1 n
46 rexanali f dom 1 f f F ¬ 1 f if 2 F = +∞ n 2 F 1 n ¬ f dom 1 f f F 1 f if 2 F = +∞ n 2 F 1 n
47 45 46 sylibr F : 0 +∞ n f dom 1 f f F ¬ 1 f if 2 F = +∞ n 2 F 1 n
48 itg1cl f dom 1 1 f
49 ltnle if 2 F = +∞ n 2 F 1 n 1 f if 2 F = +∞ n 2 F 1 n < 1 f ¬ 1 f if 2 F = +∞ n 2 F 1 n
50 37 48 49 syl2an F : 0 +∞ n f dom 1 if 2 F = +∞ n 2 F 1 n < 1 f ¬ 1 f if 2 F = +∞ n 2 F 1 n
51 50 anbi2d F : 0 +∞ n f dom 1 f f F if 2 F = +∞ n 2 F 1 n < 1 f f f F ¬ 1 f if 2 F = +∞ n 2 F 1 n
52 51 rexbidva F : 0 +∞ n f dom 1 f f F if 2 F = +∞ n 2 F 1 n < 1 f f dom 1 f f F ¬ 1 f if 2 F = +∞ n 2 F 1 n
53 47 52 mpbird F : 0 +∞ n f dom 1 f f F if 2 F = +∞ n 2 F 1 n < 1 f
54 53 ralrimiva F : 0 +∞ n f dom 1 f f F if 2 F = +∞ n 2 F 1 n < 1 f
55 ovex V
56 i1ff x dom 1 x :
57 reex V
58 57 57 elmap x x :
59 56 58 sylibr x dom 1 x
60 59 ssriv dom 1
61 55 60 ssexi dom 1 V
62 nnenom ω
63 breq1 f = g n f f F g n f F
64 fveq2 f = g n 1 f = 1 g n
65 64 breq2d f = g n if 2 F = +∞ n 2 F 1 n < 1 f if 2 F = +∞ n 2 F 1 n < 1 g n
66 63 65 anbi12d f = g n f f F if 2 F = +∞ n 2 F 1 n < 1 f g n f F if 2 F = +∞ n 2 F 1 n < 1 g n
67 61 62 66 axcc4 n f dom 1 f f F if 2 F = +∞ n 2 F 1 n < 1 f g g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n
68 54 67 syl F : 0 +∞ g g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n
69 simprl F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n g : dom 1
70 simpl g n f F if 2 F = +∞ n 2 F 1 n < 1 g n g n f F
71 70 ralimi n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n n g n f F
72 71 ad2antll F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n n g n f F
73 10 adantr F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n 2 F *
74 ffvelrn g : dom 1 n g n dom 1
75 itg1cl g n dom 1 1 g n
76 74 75 syl g : dom 1 n 1 g n
77 76 fmpttd g : dom 1 n 1 g n :
78 77 ad2antrl F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n n 1 g n :
79 78 frnd F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n ran n 1 g n
80 ressxr *
81 79 80 sstrdi F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n ran n 1 g n *
82 supxrcl ran n 1 g n * sup ran n 1 g n * < *
83 81 82 syl F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n sup ran n 1 g n * < *
84 38 adantlr F : 0 +∞ g : dom 1 n if 2 F = +∞ n 2 F 1 n *
85 76 adantll F : 0 +∞ g : dom 1 n 1 g n
86 85 rexrd F : 0 +∞ g : dom 1 n 1 g n *
87 xrltle if 2 F = +∞ n 2 F 1 n * 1 g n * if 2 F = +∞ n 2 F 1 n < 1 g n if 2 F = +∞ n 2 F 1 n 1 g n
88 84 86 87 syl2anc F : 0 +∞ g : dom 1 n if 2 F = +∞ n 2 F 1 n < 1 g n if 2 F = +∞ n 2 F 1 n 1 g n
89 2fveq3 n = m 1 g n = 1 g m
90 89 cbvmptv n 1 g n = m 1 g m
91 90 rneqi ran n 1 g n = ran m 1 g m
92 77 adantl F : 0 +∞ g : dom 1 n 1 g n :
93 92 frnd F : 0 +∞ g : dom 1 ran n 1 g n
94 93 80 sstrdi F : 0 +∞ g : dom 1 ran n 1 g n *
95 94 adantr F : 0 +∞ g : dom 1 n ran n 1 g n *
96 91 95 eqsstrrid F : 0 +∞ g : dom 1 n ran m 1 g m *
97 2fveq3 m = n 1 g m = 1 g n
98 eqid m 1 g m = m 1 g m
99 fvex 1 g n V
100 97 98 99 fvmpt n m 1 g m n = 1 g n
101 fvex 1 g m V
102 101 98 fnmpti m 1 g m Fn
103 fnfvelrn m 1 g m Fn n m 1 g m n ran m 1 g m
104 102 103 mpan n m 1 g m n ran m 1 g m
105 100 104 eqeltrrd n 1 g n ran m 1 g m
106 105 adantl F : 0 +∞ g : dom 1 n 1 g n ran m 1 g m
107 supxrub ran m 1 g m * 1 g n ran m 1 g m 1 g n sup ran m 1 g m * <
108 96 106 107 syl2anc F : 0 +∞ g : dom 1 n 1 g n sup ran m 1 g m * <
109 91 supeq1i sup ran n 1 g n * < = sup ran m 1 g m * <
110 95 82 syl F : 0 +∞ g : dom 1 n sup ran n 1 g n * < *
111 109 110 eqeltrrid F : 0 +∞ g : dom 1 n sup ran m 1 g m * < *
112 xrletr if 2 F = +∞ n 2 F 1 n * 1 g n * sup ran m 1 g m * < * if 2 F = +∞ n 2 F 1 n 1 g n 1 g n sup ran m 1 g m * < if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * <
113 84 86 111 112 syl3anc F : 0 +∞ g : dom 1 n if 2 F = +∞ n 2 F 1 n 1 g n 1 g n sup ran m 1 g m * < if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * <
114 108 113 mpan2d F : 0 +∞ g : dom 1 n if 2 F = +∞ n 2 F 1 n 1 g n if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * <
115 88 114 syld F : 0 +∞ g : dom 1 n if 2 F = +∞ n 2 F 1 n < 1 g n if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * <
116 115 adantld F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * <
117 116 ralimdva F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n n if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * <
118 117 impr F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n n if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * <
119 breq2 x = sup ran m 1 g m * < if 2 F = +∞ n 2 F 1 n x if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * <
120 119 ralbidv x = sup ran m 1 g m * < n if 2 F = +∞ n 2 F 1 n x n if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * <
121 breq2 x = sup ran m 1 g m * < 2 F x 2 F sup ran m 1 g m * <
122 120 121 imbi12d x = sup ran m 1 g m * < n if 2 F = +∞ n 2 F 1 n x 2 F x n if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * < 2 F sup ran m 1 g m * <
123 elxr x * x x = +∞ x = −∞
124 simplrl F : 0 +∞ x x < 2 F 2 F = +∞ x
125 arch x n x < n
126 124 125 syl F : 0 +∞ x x < 2 F 2 F = +∞ n x < n
127 4 adantl F : 0 +∞ x x < 2 F 2 F = +∞ if 2 F = +∞ n 2 F 1 n = n
128 127 breq2d F : 0 +∞ x x < 2 F 2 F = +∞ x < if 2 F = +∞ n 2 F 1 n x < n
129 128 rexbidv F : 0 +∞ x x < 2 F 2 F = +∞ n x < if 2 F = +∞ n 2 F 1 n n x < n
130 126 129 mpbird F : 0 +∞ x x < 2 F 2 F = +∞ n x < if 2 F = +∞ n 2 F 1 n
131 26 adantlr F : 0 +∞ x x < 2 F ¬ 2 F = +∞ 2 F
132 simplrl F : 0 +∞ x x < 2 F ¬ 2 F = +∞ x
133 131 132 resubcld F : 0 +∞ x x < 2 F ¬ 2 F = +∞ 2 F x
134 simplrr F : 0 +∞ x x < 2 F ¬ 2 F = +∞ x < 2 F
135 132 131 posdifd F : 0 +∞ x x < 2 F ¬ 2 F = +∞ x < 2 F 0 < 2 F x
136 134 135 mpbid F : 0 +∞ x x < 2 F ¬ 2 F = +∞ 0 < 2 F x
137 nnrecl 2 F x 0 < 2 F x n 1 n < 2 F x
138 133 136 137 syl2anc F : 0 +∞ x x < 2 F ¬ 2 F = +∞ n 1 n < 2 F x
139 34 adantl F : 0 +∞ x x < 2 F ¬ 2 F = +∞ n 1 n
140 131 adantr F : 0 +∞ x x < 2 F ¬ 2 F = +∞ n 2 F
141 132 adantr F : 0 +∞ x x < 2 F ¬ 2 F = +∞ n x
142 ltsub13 1 n 2 F x 1 n < 2 F x x < 2 F 1 n
143 139 140 141 142 syl3anc F : 0 +∞ x x < 2 F ¬ 2 F = +∞ n 1 n < 2 F x x < 2 F 1 n
144 8 ad2antlr F : 0 +∞ x x < 2 F ¬ 2 F = +∞ n if 2 F = +∞ n 2 F 1 n = 2 F 1 n
145 144 breq2d F : 0 +∞ x x < 2 F ¬ 2 F = +∞ n x < if 2 F = +∞ n 2 F 1 n x < 2 F 1 n
146 143 145 bitr4d F : 0 +∞ x x < 2 F ¬ 2 F = +∞ n 1 n < 2 F x x < if 2 F = +∞ n 2 F 1 n
147 146 rexbidva F : 0 +∞ x x < 2 F ¬ 2 F = +∞ n 1 n < 2 F x n x < if 2 F = +∞ n 2 F 1 n
148 138 147 mpbid F : 0 +∞ x x < 2 F ¬ 2 F = +∞ n x < if 2 F = +∞ n 2 F 1 n
149 130 148 pm2.61dan F : 0 +∞ x x < 2 F n x < if 2 F = +∞ n 2 F 1 n
150 149 expr F : 0 +∞ x x < 2 F n x < if 2 F = +∞ n 2 F 1 n
151 rexr x x *
152 xrltnle x * 2 F * x < 2 F ¬ 2 F x
153 151 10 152 syl2anr F : 0 +∞ x x < 2 F ¬ 2 F x
154 151 ad2antlr F : 0 +∞ x n x *
155 38 adantlr F : 0 +∞ x n if 2 F = +∞ n 2 F 1 n *
156 xrltnle x * if 2 F = +∞ n 2 F 1 n * x < if 2 F = +∞ n 2 F 1 n ¬ if 2 F = +∞ n 2 F 1 n x
157 154 155 156 syl2anc F : 0 +∞ x n x < if 2 F = +∞ n 2 F 1 n ¬ if 2 F = +∞ n 2 F 1 n x
158 157 rexbidva F : 0 +∞ x n x < if 2 F = +∞ n 2 F 1 n n ¬ if 2 F = +∞ n 2 F 1 n x
159 rexnal n ¬ if 2 F = +∞ n 2 F 1 n x ¬ n if 2 F = +∞ n 2 F 1 n x
160 158 159 bitrdi F : 0 +∞ x n x < if 2 F = +∞ n 2 F 1 n ¬ n if 2 F = +∞ n 2 F 1 n x
161 150 153 160 3imtr3d F : 0 +∞ x ¬ 2 F x ¬ n if 2 F = +∞ n 2 F 1 n x
162 161 con4d F : 0 +∞ x n if 2 F = +∞ n 2 F 1 n x 2 F x
163 10 adantr F : 0 +∞ x = +∞ 2 F *
164 pnfge 2 F * 2 F +∞
165 163 164 syl F : 0 +∞ x = +∞ 2 F +∞
166 simpr F : 0 +∞ x = +∞ x = +∞
167 165 166 breqtrrd F : 0 +∞ x = +∞ 2 F x
168 167 a1d F : 0 +∞ x = +∞ n if 2 F = +∞ n 2 F 1 n x 2 F x
169 1nn 1
170 169 ne0ii
171 r19.2z n if 2 F = +∞ n 2 F 1 n x n if 2 F = +∞ n 2 F 1 n x
172 170 171 mpan n if 2 F = +∞ n 2 F 1 n x n if 2 F = +∞ n 2 F 1 n x
173 37 adantlr F : 0 +∞ x = −∞ n if 2 F = +∞ n 2 F 1 n
174 mnflt if 2 F = +∞ n 2 F 1 n −∞ < if 2 F = +∞ n 2 F 1 n
175 rexr if 2 F = +∞ n 2 F 1 n if 2 F = +∞ n 2 F 1 n *
176 xrltnle −∞ * if 2 F = +∞ n 2 F 1 n * −∞ < if 2 F = +∞ n 2 F 1 n ¬ if 2 F = +∞ n 2 F 1 n −∞
177 15 175 176 sylancr if 2 F = +∞ n 2 F 1 n −∞ < if 2 F = +∞ n 2 F 1 n ¬ if 2 F = +∞ n 2 F 1 n −∞
178 174 177 mpbid if 2 F = +∞ n 2 F 1 n ¬ if 2 F = +∞ n 2 F 1 n −∞
179 173 178 syl F : 0 +∞ x = −∞ n ¬ if 2 F = +∞ n 2 F 1 n −∞
180 simplr F : 0 +∞ x = −∞ n x = −∞
181 180 breq2d F : 0 +∞ x = −∞ n if 2 F = +∞ n 2 F 1 n x if 2 F = +∞ n 2 F 1 n −∞
182 179 181 mtbird F : 0 +∞ x = −∞ n ¬ if 2 F = +∞ n 2 F 1 n x
183 182 nrexdv F : 0 +∞ x = −∞ ¬ n if 2 F = +∞ n 2 F 1 n x
184 183 pm2.21d F : 0 +∞ x = −∞ n if 2 F = +∞ n 2 F 1 n x 2 F x
185 172 184 syl5 F : 0 +∞ x = −∞ n if 2 F = +∞ n 2 F 1 n x 2 F x
186 162 168 185 3jaodan F : 0 +∞ x x = +∞ x = −∞ n if 2 F = +∞ n 2 F 1 n x 2 F x
187 123 186 sylan2b F : 0 +∞ x * n if 2 F = +∞ n 2 F 1 n x 2 F x
188 187 ralrimiva F : 0 +∞ x * n if 2 F = +∞ n 2 F 1 n x 2 F x
189 188 adantr F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n x * n if 2 F = +∞ n 2 F 1 n x 2 F x
190 109 83 eqeltrrid F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n sup ran m 1 g m * < *
191 122 189 190 rspcdva F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n n if 2 F = +∞ n 2 F 1 n sup ran m 1 g m * < 2 F sup ran m 1 g m * <
192 118 191 mpd F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n 2 F sup ran m 1 g m * <
193 192 109 breqtrrdi F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n 2 F sup ran n 1 g n * <
194 itg2ub F : 0 +∞ g n dom 1 g n f F 1 g n 2 F
195 194 3expia F : 0 +∞ g n dom 1 g n f F 1 g n 2 F
196 74 195 sylan2 F : 0 +∞ g : dom 1 n g n f F 1 g n 2 F
197 196 anassrs F : 0 +∞ g : dom 1 n g n f F 1 g n 2 F
198 197 adantrd F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n 1 g n 2 F
199 198 ralimdva F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n n 1 g n 2 F
200 199 impr F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n n 1 g n 2 F
201 eqid n 1 g n = n 1 g n
202 89 201 101 fvmpt m n 1 g n m = 1 g m
203 202 breq1d m n 1 g n m 2 F 1 g m 2 F
204 203 ralbiia m n 1 g n m 2 F m 1 g m 2 F
205 89 breq1d n = m 1 g n 2 F 1 g m 2 F
206 205 cbvralvw n 1 g n 2 F m 1 g m 2 F
207 204 206 bitr4i m n 1 g n m 2 F n 1 g n 2 F
208 200 207 sylibr F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n m n 1 g n m 2 F
209 ffn n 1 g n : n 1 g n Fn
210 breq1 z = n 1 g n m z 2 F n 1 g n m 2 F
211 210 ralrn n 1 g n Fn z ran n 1 g n z 2 F m n 1 g n m 2 F
212 78 209 211 3syl F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n z ran n 1 g n z 2 F m n 1 g n m 2 F
213 208 212 mpbird F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n z ran n 1 g n z 2 F
214 supxrleub ran n 1 g n * 2 F * sup ran n 1 g n * < 2 F z ran n 1 g n z 2 F
215 81 73 214 syl2anc F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n sup ran n 1 g n * < 2 F z ran n 1 g n z 2 F
216 213 215 mpbird F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n sup ran n 1 g n * < 2 F
217 73 83 193 216 xrletrid F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n 2 F = sup ran n 1 g n * <
218 69 72 217 3jca F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n g : dom 1 n g n f F 2 F = sup ran n 1 g n * <
219 218 ex F : 0 +∞ g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n g : dom 1 n g n f F 2 F = sup ran n 1 g n * <
220 219 eximdv F : 0 +∞ g g : dom 1 n g n f F if 2 F = +∞ n 2 F 1 n < 1 g n g g : dom 1 n g n f F 2 F = sup ran n 1 g n * <
221 68 220 mpd F : 0 +∞ g g : dom 1 n g n f F 2 F = sup ran n 1 g n * <