# Metamath Proof Explorer

## Theorem iblulm

Description: A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses itgulm.z $⊢ Z = ℤ ≥ M$
itgulm.m $⊢ φ → M ∈ ℤ$
itgulm.f $⊢ φ → F : Z ⟶ 𝐿 1$
itgulm.u
itgulm.s $⊢ φ → vol ⁡ S ∈ ℝ$
Assertion iblulm $⊢ φ → G ∈ 𝐿 1$

### Proof

Step Hyp Ref Expression
1 itgulm.z $⊢ Z = ℤ ≥ M$
2 itgulm.m $⊢ φ → M ∈ ℤ$
3 itgulm.f $⊢ φ → F : Z ⟶ 𝐿 1$
4 itgulm.u
5 itgulm.s $⊢ φ → vol ⁡ S ∈ ℝ$
6 3 ffnd $⊢ φ → F Fn Z$
7 ulmf2
8 6 4 7 syl2anc $⊢ φ → F : Z ⟶ ℂ S$
9 eqidd $⊢ φ ∧ k ∈ Z ∧ x ∈ S → F ⁡ k ⁡ x = F ⁡ k ⁡ x$
10 eqidd $⊢ φ ∧ x ∈ S → G ⁡ x = G ⁡ x$
11 1rp $⊢ 1 ∈ ℝ +$
12 11 a1i $⊢ φ → 1 ∈ ℝ +$
13 1 2 8 9 10 4 12 ulmi $⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1$
14 1 r19.2uz $⊢ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → ∃ k ∈ Z ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1$
15 13 14 syl $⊢ φ → ∃ k ∈ Z ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1$
16 ulmcl
17 4 16 syl $⊢ φ → G : S ⟶ ℂ$
18 17 adantr $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → G : S ⟶ ℂ$
19 18 feqmptd $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → G = z ∈ S ⟼ G ⁡ z$
20 8 ffvelrnda $⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ S$
21 elmapi $⊢ F ⁡ k ∈ ℂ S → F ⁡ k : S ⟶ ℂ$
22 20 21 syl $⊢ φ ∧ k ∈ Z → F ⁡ k : S ⟶ ℂ$
23 22 adantrr $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → F ⁡ k : S ⟶ ℂ$
24 23 ffvelrnda $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 ∧ z ∈ S → F ⁡ k ⁡ z ∈ ℂ$
25 18 ffvelrnda $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 ∧ z ∈ S → G ⁡ z ∈ ℂ$
26 24 25 nncand $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 ∧ z ∈ S → F ⁡ k ⁡ z − F ⁡ k ⁡ z − G ⁡ z = G ⁡ z$
27 26 mpteq2dva $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → z ∈ S ⟼ F ⁡ k ⁡ z − F ⁡ k ⁡ z − G ⁡ z = z ∈ S ⟼ G ⁡ z$
28 19 27 eqtr4d $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → G = z ∈ S ⟼ F ⁡ k ⁡ z − F ⁡ k ⁡ z − G ⁡ z$
29 23 feqmptd $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → F ⁡ k = z ∈ S ⟼ F ⁡ k ⁡ z$
30 3 ffvelrnda $⊢ φ ∧ k ∈ Z → F ⁡ k ∈ 𝐿 1$
31 30 adantrr $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → F ⁡ k ∈ 𝐿 1$
32 29 31 eqeltrrd $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → z ∈ S ⟼ F ⁡ k ⁡ z ∈ 𝐿 1$
33 24 25 subcld $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 ∧ z ∈ S → F ⁡ k ⁡ z − G ⁡ z ∈ ℂ$
34 ulmscl
35 4 34 syl $⊢ φ → S ∈ V$
36 35 adantr $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → S ∈ V$
37 36 24 25 29 19 offval2 $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → F ⁡ k − f G = z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z$
38 iblmbf $⊢ F ⁡ k ∈ 𝐿 1 → F ⁡ k ∈ MblFn$
39 31 38 syl $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → F ⁡ k ∈ MblFn$
40 iblmbf $⊢ x ∈ 𝐿 1 → x ∈ MblFn$
41 40 ssriv $⊢ 𝐿 1 ⊆ MblFn$
42 fss $⊢ F : Z ⟶ 𝐿 1 ∧ 𝐿 1 ⊆ MblFn → F : Z ⟶ MblFn$
43 3 41 42 sylancl $⊢ φ → F : Z ⟶ MblFn$
44 1 2 43 4 mbfulm $⊢ φ → G ∈ MblFn$
45 44 adantr $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → G ∈ MblFn$
46 39 45 mbfsub $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → F ⁡ k − f G ∈ MblFn$
47 37 46 eqeltrrd $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ∈ MblFn$
48 eqid $⊢ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z = z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z$
49 48 33 dmmptd $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → dom ⁡ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z = S$
50 49 fveq2d $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → vol ⁡ dom ⁡ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z = vol ⁡ S$
51 5 adantr $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → vol ⁡ S ∈ ℝ$
52 50 51 eqeltrd $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → vol ⁡ dom ⁡ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ∈ ℝ$
53 1re $⊢ 1 ∈ ℝ$
54 22 ffvelrnda $⊢ φ ∧ k ∈ Z ∧ x ∈ S → F ⁡ k ⁡ x ∈ ℂ$
55 17 adantr $⊢ φ ∧ k ∈ Z → G : S ⟶ ℂ$
56 55 ffvelrnda $⊢ φ ∧ k ∈ Z ∧ x ∈ S → G ⁡ x ∈ ℂ$
57 54 56 subcld $⊢ φ ∧ k ∈ Z ∧ x ∈ S → F ⁡ k ⁡ x − G ⁡ x ∈ ℂ$
58 57 abscld $⊢ φ ∧ k ∈ Z ∧ x ∈ S → F ⁡ k ⁡ x − G ⁡ x ∈ ℝ$
59 ltle $⊢ F ⁡ k ⁡ x − G ⁡ x ∈ ℝ ∧ 1 ∈ ℝ → F ⁡ k ⁡ x − G ⁡ x < 1 → F ⁡ k ⁡ x − G ⁡ x ≤ 1$
60 58 53 59 sylancl $⊢ φ ∧ k ∈ Z ∧ x ∈ S → F ⁡ k ⁡ x − G ⁡ x < 1 → F ⁡ k ⁡ x − G ⁡ x ≤ 1$
61 fveq2 $⊢ z = x → F ⁡ k ⁡ z = F ⁡ k ⁡ x$
62 fveq2 $⊢ z = x → G ⁡ z = G ⁡ x$
63 61 62 oveq12d $⊢ z = x → F ⁡ k ⁡ z − G ⁡ z = F ⁡ k ⁡ x − G ⁡ x$
64 ovex $⊢ F ⁡ k ⁡ x − G ⁡ x ∈ V$
65 63 48 64 fvmpt $⊢ x ∈ S → z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x = F ⁡ k ⁡ x − G ⁡ x$
66 65 adantl $⊢ φ ∧ k ∈ Z ∧ x ∈ S → z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x = F ⁡ k ⁡ x − G ⁡ x$
67 66 fveq2d $⊢ φ ∧ k ∈ Z ∧ x ∈ S → z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x = F ⁡ k ⁡ x − G ⁡ x$
68 67 breq1d $⊢ φ ∧ k ∈ Z ∧ x ∈ S → z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ 1 ↔ F ⁡ k ⁡ x − G ⁡ x ≤ 1$
69 60 68 sylibrd $⊢ φ ∧ k ∈ Z ∧ x ∈ S → F ⁡ k ⁡ x − G ⁡ x < 1 → z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ 1$
70 69 ralimdva $⊢ φ ∧ k ∈ Z → ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → ∀ x ∈ S z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ 1$
71 70 impr $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → ∀ x ∈ S z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ 1$
72 49 raleqdv $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → ∀ x ∈ dom ⁡ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ 1 ↔ ∀ x ∈ S z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ 1$
73 71 72 mpbird $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → ∀ x ∈ dom ⁡ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ 1$
74 brralrspcev $⊢ 1 ∈ ℝ ∧ ∀ x ∈ dom ⁡ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ 1 → ∃ r ∈ ℝ ∀ x ∈ dom ⁡ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ r$
75 53 73 74 sylancr $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → ∃ r ∈ ℝ ∀ x ∈ dom ⁡ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ r$
76 bddibl $⊢ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ∈ MblFn ∧ vol ⁡ dom ⁡ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ∈ ℝ ∧ ∃ r ∈ ℝ ∀ x ∈ dom ⁡ z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ⁡ x ≤ r → z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ∈ 𝐿 1$
77 47 52 75 76 syl3anc $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → z ∈ S ⟼ F ⁡ k ⁡ z − G ⁡ z ∈ 𝐿 1$
78 24 32 33 77 iblsub $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → z ∈ S ⟼ F ⁡ k ⁡ z − F ⁡ k ⁡ z − G ⁡ z ∈ 𝐿 1$
79 28 78 eqeltrd $⊢ φ ∧ k ∈ Z ∧ ∀ x ∈ S F ⁡ k ⁡ x − G ⁡ x < 1 → G ∈ 𝐿 1$
80 15 79 rexlimddv $⊢ φ → G ∈ 𝐿 1$