Metamath Proof Explorer

Theorem mbfi1flimlem

Description: Lemma for mbfi1flim . (Contributed by Mario Carneiro, 5-Sep-2014)

Ref Expression
Hypotheses mbfi1flim.1 ⊢ φ → F ∈ MblFn
mbfi1flimlem.2 ⊢ φ → F : ℝ ⟶ ℝ
Assertion mbfi1flimlem ⊢ φ → ∃ g g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x

Proof

Step Hyp Ref Expression
1 mbfi1flim.1 ⊢ φ → F ∈ MblFn
2 mbfi1flimlem.2 ⊢ φ → F : ℝ ⟶ ℝ
3 2 ffvelcdmda ⊢ φ ∧ y ∈ ℝ → F ⁡ y ∈ ℝ
4 2 feqmptd ⊢ φ → F = y ∈ ℝ ⟼ F ⁡ y
5 4 1 eqeltrrd ⊢ φ → y ∈ ℝ ⟼ F ⁡ y ∈ MblFn
6 3 5 mbfpos ⊢ φ → y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ∈ MblFn
7 0re ⊢ 0 ∈ ℝ
8 ifcl ⊢ F ⁡ y ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ F ⁡ y F ⁡ y 0 ∈ ℝ
9 3 7 8 sylancl ⊢ φ ∧ y ∈ ℝ → if 0 ≤ F ⁡ y F ⁡ y 0 ∈ ℝ
10 max1 ⊢ 0 ∈ ℝ ∧ F ⁡ y ∈ ℝ → 0 ≤ if 0 ≤ F ⁡ y F ⁡ y 0
11 7 3 10 sylancr ⊢ φ ∧ y ∈ ℝ → 0 ≤ if 0 ≤ F ⁡ y F ⁡ y 0
12 elrege0 ⊢ if 0 ≤ F ⁡ y F ⁡ y 0 ∈ 0 +∞ ↔ if 0 ≤ F ⁡ y F ⁡ y 0 ∈ ℝ ∧ 0 ≤ if 0 ≤ F ⁡ y F ⁡ y 0
13 9 11 12 sylanbrc ⊢ φ ∧ y ∈ ℝ → if 0 ≤ F ⁡ y F ⁡ y 0 ∈ 0 +∞
14 13 fmpttd ⊢ φ → y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 : ℝ ⟶ 0 +∞
15 6 14 mbfi1fseq ⊢ φ → ∃ f f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f f ⁡ n ∧ f ⁡ n ≤ f f ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x
16 3 renegcld ⊢ φ ∧ y ∈ ℝ → − F ⁡ y ∈ ℝ
17 3 5 mbfneg ⊢ φ → y ∈ ℝ ⟼ − F ⁡ y ∈ MblFn
18 16 17 mbfpos ⊢ φ → y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ∈ MblFn
19 ifcl ⊢ − F ⁡ y ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ − F ⁡ y − F ⁡ y 0 ∈ ℝ
20 16 7 19 sylancl ⊢ φ ∧ y ∈ ℝ → if 0 ≤ − F ⁡ y − F ⁡ y 0 ∈ ℝ
21 max1 ⊢ 0 ∈ ℝ ∧ − F ⁡ y ∈ ℝ → 0 ≤ if 0 ≤ − F ⁡ y − F ⁡ y 0
22 7 16 21 sylancr ⊢ φ ∧ y ∈ ℝ → 0 ≤ if 0 ≤ − F ⁡ y − F ⁡ y 0
23 elrege0 ⊢ if 0 ≤ − F ⁡ y − F ⁡ y 0 ∈ 0 +∞ ↔ if 0 ≤ − F ⁡ y − F ⁡ y 0 ∈ ℝ ∧ 0 ≤ if 0 ≤ − F ⁡ y − F ⁡ y 0
24 20 22 23 sylanbrc ⊢ φ ∧ y ∈ ℝ → if 0 ≤ − F ⁡ y − F ⁡ y 0 ∈ 0 +∞
25 24 fmpttd ⊢ φ → y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 : ℝ ⟶ 0 +∞
26 18 25 mbfi1fseq ⊢ φ → ∃ h h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f h ⁡ n ∧ h ⁡ n ≤ f h ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x
27 exdistrv ⊢ ∃ f ∃ h f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f f ⁡ n ∧ f ⁡ n ≤ f f ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f h ⁡ n ∧ h ⁡ n ≤ f h ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x ↔ ∃ f f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f f ⁡ n ∧ f ⁡ n ≤ f f ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ ∃ h h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f h ⁡ n ∧ h ⁡ n ≤ f h ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x
28 3simpb ⊢ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f f ⁡ n ∧ f ⁡ n ≤ f f ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x → f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x
29 3simpb ⊢ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f h ⁡ n ∧ h ⁡ n ≤ f h ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x
30 28 29 anim12i ⊢ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f f ⁡ n ∧ f ⁡ n ≤ f f ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f h ⁡ n ∧ h ⁡ n ≤ f h ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x
31 an4 ⊢ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x ↔ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x
32 30 31 sylib ⊢ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f f ⁡ n ∧ f ⁡ n ≤ f f ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f h ⁡ n ∧ h ⁡ n ≤ f h ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x
33 r19.26 ⊢ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x ↔ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x
34 i1fsub ⊢ x ∈ dom ⁡ ∫ 1 ∧ y ∈ dom ⁡ ∫ 1 → x − f y ∈ dom ⁡ ∫ 1
35 34 adantl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ dom ⁡ ∫ 1 ∧ y ∈ dom ⁡ ∫ 1 → x − f y ∈ dom ⁡ ∫ 1
36 simprl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 → f : ℕ ⟶ dom ⁡ ∫ 1
37 simprr ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 → h : ℕ ⟶ dom ⁡ ∫ 1
38 nnex ⊢ ℕ ∈ V
39 38 a1i ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 → ℕ ∈ V
40 inidm ⊢ ℕ ∩ ℕ = ℕ
41 35 36 37 39 39 40 off ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 → f ∘ f ⁡ − f h : ℕ ⟶ dom ⁡ ∫ 1
42 fveq2 ⊢ y = x → F ⁡ y = F ⁡ x
43 42 breq2d ⊢ y = x → 0 ≤ F ⁡ y ↔ 0 ≤ F ⁡ x
44 43 42 ifbieq1d ⊢ y = x → if 0 ≤ F ⁡ y F ⁡ y 0 = if 0 ≤ F ⁡ x F ⁡ x 0
45 eqid ⊢ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 = y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0
46 fvex ⊢ F ⁡ x ∈ V
47 c0ex ⊢ 0 ∈ V
48 46 47 ifex ⊢ if 0 ≤ F ⁡ x F ⁡ x 0 ∈ V
49 44 45 48 fvmpt ⊢ x ∈ ℝ → y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x = if 0 ≤ F ⁡ x F ⁡ x 0
50 49 breq2d ⊢ x ∈ ℝ → n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ↔ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0
51 42 negeqd ⊢ y = x → − F ⁡ y = − F ⁡ x
52 51 breq2d ⊢ y = x → 0 ≤ − F ⁡ y ↔ 0 ≤ − F ⁡ x
53 52 51 ifbieq1d ⊢ y = x → if 0 ≤ − F ⁡ y − F ⁡ y 0 = if 0 ≤ − F ⁡ x − F ⁡ x 0
54 eqid ⊢ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 = y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0
55 negex ⊢ − F ⁡ x ∈ V
56 55 47 ifex ⊢ if 0 ≤ − F ⁡ x − F ⁡ x 0 ∈ V
57 53 54 56 fvmpt ⊢ x ∈ ℝ → y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x = if 0 ≤ − F ⁡ x − F ⁡ x 0
58 57 breq2d ⊢ x ∈ ℝ → n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x ↔ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0
59 50 58 anbi12d ⊢ x ∈ ℝ → n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x ↔ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0
60 59 adantl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ → n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x ↔ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0
61 nnuz ⊢ ℕ = ℤ ≥ 1
62 1zzd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 → 1 ∈ ℤ
63 simprl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 → n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0
64 38 mptex ⊢ n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ∈ V
65 64 a1i ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 → n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ∈ V
66 simprr ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 → n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0
67 36 ffvelcdmda ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ n ∈ ℕ → f ⁡ n ∈ dom ⁡ ∫ 1
68 i1ff ⊢ f ⁡ n ∈ dom ⁡ ∫ 1 → f ⁡ n : ℝ ⟶ ℝ
69 67 68 syl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ n ∈ ℕ → f ⁡ n : ℝ ⟶ ℝ
70 69 ffvelcdmda ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ n ∈ ℕ ∧ x ∈ ℝ → f ⁡ n ⁡ x ∈ ℝ
71 70 an32s ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ → f ⁡ n ⁡ x ∈ ℝ
72 71 recnd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ → f ⁡ n ⁡ x ∈ ℂ
73 72 fmpttd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ → n ∈ ℕ ⟼ f ⁡ n ⁡ x : ℕ ⟶ ℂ
74 73 adantr ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 → n ∈ ℕ ⟼ f ⁡ n ⁡ x : ℕ ⟶ ℂ
75 74 ffvelcdmda ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 ∧ k ∈ ℕ → n ∈ ℕ ⟼ f ⁡ n ⁡ x ⁡ k ∈ ℂ
76 37 ffvelcdmda ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ n ∈ ℕ → h ⁡ n ∈ dom ⁡ ∫ 1
77 i1ff ⊢ h ⁡ n ∈ dom ⁡ ∫ 1 → h ⁡ n : ℝ ⟶ ℝ
78 76 77 syl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ n ∈ ℕ → h ⁡ n : ℝ ⟶ ℝ
79 78 ffvelcdmda ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ n ∈ ℕ ∧ x ∈ ℝ → h ⁡ n ⁡ x ∈ ℝ
80 79 an32s ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ → h ⁡ n ⁡ x ∈ ℝ
81 80 recnd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ → h ⁡ n ⁡ x ∈ ℂ
82 81 fmpttd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ → n ∈ ℕ ⟼ h ⁡ n ⁡ x : ℕ ⟶ ℂ
83 82 adantr ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 → n ∈ ℕ ⟼ h ⁡ n ⁡ x : ℕ ⟶ ℂ
84 83 ffvelcdmda ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 ∧ k ∈ ℕ → n ∈ ℕ ⟼ h ⁡ n ⁡ x ⁡ k ∈ ℂ
85 36 ffnd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 → f Fn ℕ
86 37 ffnd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 → h Fn ℕ
87 eqidd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ → f ⁡ k = f ⁡ k
88 eqidd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ → h ⁡ k = h ⁡ k
89 85 86 39 39 40 87 88 ofval ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ → f ∘ f ⁡ − f h ⁡ k = f ⁡ k − f h ⁡ k
90 89 fveq1d ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ → f ∘ f ⁡ − f h ⁡ k ⁡ x = f ⁡ k − f h ⁡ k ⁡ x
91 90 adantr ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ ∧ x ∈ ℝ → f ∘ f ⁡ − f h ⁡ k ⁡ x = f ⁡ k − f h ⁡ k ⁡ x
92 36 ffvelcdmda ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ → f ⁡ k ∈ dom ⁡ ∫ 1
93 i1ff ⊢ f ⁡ k ∈ dom ⁡ ∫ 1 → f ⁡ k : ℝ ⟶ ℝ
94 ffn ⊢ f ⁡ k : ℝ ⟶ ℝ → f ⁡ k Fn ℝ
95 92 93 94 3syl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ → f ⁡ k Fn ℝ
96 37 ffvelcdmda ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ → h ⁡ k ∈ dom ⁡ ∫ 1
97 i1ff ⊢ h ⁡ k ∈ dom ⁡ ∫ 1 → h ⁡ k : ℝ ⟶ ℝ
98 ffn ⊢ h ⁡ k : ℝ ⟶ ℝ → h ⁡ k Fn ℝ
99 96 97 98 3syl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ → h ⁡ k Fn ℝ
100 reex ⊢ ℝ ∈ V
101 100 a1i ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ → ℝ ∈ V
102 inidm ⊢ ℝ ∩ ℝ = ℝ
103 eqidd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ ∧ x ∈ ℝ → f ⁡ k ⁡ x = f ⁡ k ⁡ x
104 eqidd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ ∧ x ∈ ℝ → h ⁡ k ⁡ x = h ⁡ k ⁡ x
105 95 99 101 101 102 103 104 ofval ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ ∧ x ∈ ℝ → f ⁡ k − f h ⁡ k ⁡ x = f ⁡ k ⁡ x − h ⁡ k ⁡ x
106 91 105 eqtrd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ k ∈ ℕ ∧ x ∈ ℝ → f ∘ f ⁡ − f h ⁡ k ⁡ x = f ⁡ k ⁡ x − h ⁡ k ⁡ x
107 106 an32s ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ k ∈ ℕ → f ∘ f ⁡ − f h ⁡ k ⁡ x = f ⁡ k ⁡ x − h ⁡ k ⁡ x
108 fveq2 ⊢ n = k → f ∘ f ⁡ − f h ⁡ n = f ∘ f ⁡ − f h ⁡ k
109 108 fveq1d ⊢ n = k → f ∘ f ⁡ − f h ⁡ n ⁡ x = f ∘ f ⁡ − f h ⁡ k ⁡ x
110 eqid ⊢ n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x = n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x
111 fvex ⊢ f ∘ f ⁡ − f h ⁡ k ⁡ x ∈ V
112 109 110 111 fvmpt ⊢ k ∈ ℕ → n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⁡ k = f ∘ f ⁡ − f h ⁡ k ⁡ x
113 112 adantl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ k ∈ ℕ → n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⁡ k = f ∘ f ⁡ − f h ⁡ k ⁡ x
114 fveq2 ⊢ n = k → f ⁡ n = f ⁡ k
115 114 fveq1d ⊢ n = k → f ⁡ n ⁡ x = f ⁡ k ⁡ x
116 eqid ⊢ n ∈ ℕ ⟼ f ⁡ n ⁡ x = n ∈ ℕ ⟼ f ⁡ n ⁡ x
117 fvex ⊢ f ⁡ k ⁡ x ∈ V
118 115 116 117 fvmpt ⊢ k ∈ ℕ → n ∈ ℕ ⟼ f ⁡ n ⁡ x ⁡ k = f ⁡ k ⁡ x
119 fveq2 ⊢ n = k → h ⁡ n = h ⁡ k
120 119 fveq1d ⊢ n = k → h ⁡ n ⁡ x = h ⁡ k ⁡ x
121 eqid ⊢ n ∈ ℕ ⟼ h ⁡ n ⁡ x = n ∈ ℕ ⟼ h ⁡ n ⁡ x
122 fvex ⊢ h ⁡ k ⁡ x ∈ V
123 120 121 122 fvmpt ⊢ k ∈ ℕ → n ∈ ℕ ⟼ h ⁡ n ⁡ x ⁡ k = h ⁡ k ⁡ x
124 118 123 oveq12d ⊢ k ∈ ℕ → n ∈ ℕ ⟼ f ⁡ n ⁡ x ⁡ k − n ∈ ℕ ⟼ h ⁡ n ⁡ x ⁡ k = f ⁡ k ⁡ x − h ⁡ k ⁡ x
125 124 adantl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ k ∈ ℕ → n ∈ ℕ ⟼ f ⁡ n ⁡ x ⁡ k − n ∈ ℕ ⟼ h ⁡ n ⁡ x ⁡ k = f ⁡ k ⁡ x − h ⁡ k ⁡ x
126 107 113 125 3eqtr4d ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ k ∈ ℕ → n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⁡ k = n ∈ ℕ ⟼ f ⁡ n ⁡ x ⁡ k − n ∈ ℕ ⟼ h ⁡ n ⁡ x ⁡ k
127 126 adantlr ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 ∧ k ∈ ℕ → n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⁡ k = n ∈ ℕ ⟼ f ⁡ n ⁡ x ⁡ k − n ∈ ℕ ⟼ h ⁡ n ⁡ x ⁡ k
128 61 62 63 65 66 75 84 127 climsub ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 → n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 − if 0 ≤ − F ⁡ x − F ⁡ x 0
129 2 adantr ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 → F : ℝ ⟶ ℝ
130 129 ffvelcdmda ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ → F ⁡ x ∈ ℝ
131 max0sub ⊢ F ⁡ x ∈ ℝ → if 0 ≤ F ⁡ x F ⁡ x 0 − if 0 ≤ − F ⁡ x − F ⁡ x 0 = F ⁡ x
132 130 131 syl ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ → if 0 ≤ F ⁡ x F ⁡ x 0 − if 0 ≤ − F ⁡ x − F ⁡ x 0 = F ⁡ x
133 132 adantr ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 → if 0 ≤ F ⁡ x F ⁡ x 0 − if 0 ≤ − F ⁡ x − F ⁡ x 0 = F ⁡ x
134 128 133 breqtrd ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ ∧ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 → n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⇝ F ⁡ x
135 134 ex ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ → n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ if 0 ≤ F ⁡ x F ⁡ x 0 ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ if 0 ≤ − F ⁡ x − F ⁡ x 0 → n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⇝ F ⁡ x
136 60 135 sylbid ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ x ∈ ℝ → n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⇝ F ⁡ x
137 136 ralimdva ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 → ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → ∀ x ∈ ℝ n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⇝ F ⁡ x
138 ovex ⊢ f ∘ f ⁡ − f h ∈ V
139 feq1 ⊢ g = f ∘ f ⁡ − f h → g : ℕ ⟶ dom ⁡ ∫ 1 ↔ f ∘ f ⁡ − f h : ℕ ⟶ dom ⁡ ∫ 1
140 fveq1 ⊢ g = f ∘ f ⁡ − f h → g ⁡ n = f ∘ f ⁡ − f h ⁡ n
141 140 fveq1d ⊢ g = f ∘ f ⁡ − f h → g ⁡ n ⁡ x = f ∘ f ⁡ − f h ⁡ n ⁡ x
142 141 mpteq2dv ⊢ g = f ∘ f ⁡ − f h → n ∈ ℕ ⟼ g ⁡ n ⁡ x = n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x
143 142 breq1d ⊢ g = f ∘ f ⁡ − f h → n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x ↔ n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⇝ F ⁡ x
144 143 ralbidv ⊢ g = f ∘ f ⁡ − f h → ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x ↔ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⇝ F ⁡ x
145 139 144 anbi12d ⊢ g = f ∘ f ⁡ − f h → g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x ↔ f ∘ f ⁡ − f h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⇝ F ⁡ x
146 138 145 spcev ⊢ f ∘ f ⁡ − f h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ∘ f ⁡ − f h ⁡ n ⁡ x ⇝ F ⁡ x → ∃ g g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x
147 41 137 146 syl6an ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 → ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → ∃ g g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x
148 33 147 biimtrrid ⊢ φ ∧ f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 → ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → ∃ g g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x
149 148 expimpd ⊢ φ → f : ℕ ⟶ dom ⁡ ∫ 1 ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → ∃ g g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x
150 32 149 syl5 ⊢ φ → f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f f ⁡ n ∧ f ⁡ n ≤ f f ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f h ⁡ n ∧ h ⁡ n ≤ f h ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → ∃ g g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x
151 150 exlimdvv ⊢ φ → ∃ f ∃ h f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f f ⁡ n ∧ f ⁡ n ≤ f f ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f h ⁡ n ∧ h ⁡ n ≤ f h ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → ∃ g g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x
152 27 151 biimtrrid ⊢ φ → ∃ f f : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f f ⁡ n ∧ f ⁡ n ≤ f f ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ f ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ F ⁡ y F ⁡ y 0 ⁡ x ∧ ∃ h h : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ n ∈ ℕ 0 𝑝 ≤ f h ⁡ n ∧ h ⁡ n ≤ f h ⁡ n + 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ h ⁡ n ⁡ x ⇝ y ∈ ℝ ⟼ if 0 ≤ − F ⁡ y − F ⁡ y 0 ⁡ x → ∃ g g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x
153 15 26 152 mp2and ⊢ φ → ∃ g g : ℕ ⟶ dom ⁡ ∫ 1 ∧ ∀ x ∈ ℝ n ∈ ℕ ⟼ g ⁡ n ⁡ x ⇝ F ⁡ x