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 ⊢φ→∃gg:ℕ⟶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∈ℝ⟼if0≤F⁡yF⁡y0∈MblFn
7 0re ⊢0∈ℝ
8 ifcl ⊢F⁡y∈ℝ∧0∈ℝ→if0≤F⁡yF⁡y0∈ℝ
9 3 7 8 sylancl ⊢φ∧y∈ℝ→if0≤F⁡yF⁡y0∈ℝ
10 max1 ⊢0∈ℝ∧F⁡y∈ℝ→0≤if0≤F⁡yF⁡y0
11 7 3 10 sylancr ⊢φ∧y∈ℝ→0≤if0≤F⁡yF⁡y0
12 elrege0 ⊢if0≤F⁡yF⁡y0∈0+∞↔if0≤F⁡yF⁡y0∈ℝ∧0≤if0≤F⁡yF⁡y0
13 9 11 12 sylanbrc ⊢φ∧y∈ℝ→if0≤F⁡yF⁡y0∈0+∞
14 13 fmpttd ⊢φ→y∈ℝ⟼if0≤F⁡yF⁡y0:ℝ⟶0+∞
15 6 14 mbfi1fseq ⊢φ→∃ff:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤ff⁡n∧f⁡n≤ff⁡n+1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x
16 3 renegcld ⊢φ∧y∈ℝ→−F⁡y∈ℝ
17 3 5 mbfneg ⊢φ→y∈ℝ⟼−F⁡y∈MblFn
18 16 17 mbfpos ⊢φ→y∈ℝ⟼if0≤−F⁡y−F⁡y0∈MblFn
19 ifcl ⊢−F⁡y∈ℝ∧0∈ℝ→if0≤−F⁡y−F⁡y0∈ℝ
20 16 7 19 sylancl ⊢φ∧y∈ℝ→if0≤−F⁡y−F⁡y0∈ℝ
21 max1 ⊢0∈ℝ∧−F⁡y∈ℝ→0≤if0≤−F⁡y−F⁡y0
22 7 16 21 sylancr ⊢φ∧y∈ℝ→0≤if0≤−F⁡y−F⁡y0
23 elrege0 ⊢if0≤−F⁡y−F⁡y0∈0+∞↔if0≤−F⁡y−F⁡y0∈ℝ∧0≤if0≤−F⁡y−F⁡y0
24 20 22 23 sylanbrc ⊢φ∧y∈ℝ→if0≤−F⁡y−F⁡y0∈0+∞
25 24 fmpttd ⊢φ→y∈ℝ⟼if0≤−F⁡y−F⁡y0:ℝ⟶0+∞
26 18 25 mbfi1fseq ⊢φ→∃hh:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤fh⁡n∧h⁡n≤fh⁡n+1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x
27 exdistrv ⊢∃f∃hf:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤ff⁡n∧f⁡n≤ff⁡n+1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧h:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤fh⁡n∧h⁡n≤fh⁡n+1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x↔∃ff:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤ff⁡n∧f⁡n≤ff⁡n+1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧∃hh:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤fh⁡n∧h⁡n≤fh⁡n+1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x
28 3simpb ⊢f:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤ff⁡n∧f⁡n≤ff⁡n+1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x→f:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x
29 3simpb ⊢h:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤fh⁡n∧h⁡n≤fh⁡n+1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→h:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x
30 28 29 anim12i ⊢f:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤ff⁡n∧f⁡n≤ff⁡n+1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧h:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤fh⁡n∧h⁡n≤fh⁡n+1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→f:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧h:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x
31 an4 ⊢f:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧h:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x↔f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x
32 30 31 sylib ⊢f:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤ff⁡n∧f⁡n≤ff⁡n+1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧h:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤fh⁡n∧h⁡n≤fh⁡n+1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x
33 r19.26 ⊢∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧n∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x↔∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x
34 i1fsub ⊢x∈dom⁡∫1∧y∈dom⁡∫1→x−fy∈dom⁡∫1
35 34 adantl ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈dom⁡∫1∧y∈dom⁡∫1→x−fy∈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⁡−fh:ℕ⟶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→if0≤F⁡yF⁡y0=if0≤F⁡xF⁡x0
45 eqid ⊢y∈ℝ⟼if0≤F⁡yF⁡y0=y∈ℝ⟼if0≤F⁡yF⁡y0
46 fvex ⊢F⁡x∈V
47 c0ex ⊢0∈V
48 46 47 ifex ⊢if0≤F⁡xF⁡x0∈V
49 44 45 48 fvmpt ⊢x∈ℝ→y∈ℝ⟼if0≤F⁡yF⁡y0⁡x=if0≤F⁡xF⁡x0
50 49 breq2d ⊢x∈ℝ→n∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x↔n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0
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→if0≤−F⁡y−F⁡y0=if0≤−F⁡x−F⁡x0
54 eqid ⊢y∈ℝ⟼if0≤−F⁡y−F⁡y0=y∈ℝ⟼if0≤−F⁡y−F⁡y0
55 negex ⊢−F⁡x∈V
56 55 47 ifex ⊢if0≤−F⁡x−F⁡x0∈V
57 53 54 56 fvmpt ⊢x∈ℝ→y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x=if0≤−F⁡x−F⁡x0
58 57 breq2d ⊢x∈ℝ→n∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x↔n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0
59 50 58 anbi12d ⊢x∈ℝ→n∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧n∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x↔n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0
60 59 adantl ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ→n∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧n∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x↔n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0
61 nnuz ⊢ℕ=ℤ≥1
62 1zzd ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ∧n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0→1∈ℤ
63 simprl ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ∧n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0→n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0
64 38 mptex ⊢n∈ℕ⟼f∘f⁡−fh⁡n⁡x∈V
65 64 a1i ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ∧n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0→n∈ℕ⟼f∘f⁡−fh⁡n⁡x∈V
66 simprr ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ∧n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0→n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0
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⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0→n∈ℕ⟼f⁡n⁡x:ℕ⟶ℂ
75 74 ffvelcdmda ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ∧n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0∧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⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0→n∈ℕ⟼h⁡n⁡x:ℕ⟶ℂ
84 83 ffvelcdmda ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ∧n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0∧k∈ℕ→n∈ℕ⟼h⁡n⁡x⁡k∈ℂ
85 36 ffnd ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1→fFnℕ
86 37 ffnd ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1→hFnℕ
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⁡−fh⁡k=f⁡k−fh⁡k
90 89 fveq1d ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧k∈ℕ→f∘f⁡−fh⁡k⁡x=f⁡k−fh⁡k⁡x
91 90 adantr ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧k∈ℕ∧x∈ℝ→f∘f⁡−fh⁡k⁡x=f⁡k−fh⁡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⁡kFnℝ
95 92 93 94 3syl ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧k∈ℕ→f⁡kFnℝ
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⁡kFnℝ
99 96 97 98 3syl ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧k∈ℕ→h⁡kFnℝ
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−fh⁡k⁡x=f⁡k⁡x−h⁡k⁡x
106 91 105 eqtrd ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧k∈ℕ∧x∈ℝ→f∘f⁡−fh⁡k⁡x=f⁡k⁡x−h⁡k⁡x
107 106 an32s ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ∧k∈ℕ→f∘f⁡−fh⁡k⁡x=f⁡k⁡x−h⁡k⁡x
108 fveq2 ⊢n=k→f∘f⁡−fh⁡n=f∘f⁡−fh⁡k
109 108 fveq1d ⊢n=k→f∘f⁡−fh⁡n⁡x=f∘f⁡−fh⁡k⁡x
110 eqid ⊢n∈ℕ⟼f∘f⁡−fh⁡n⁡x=n∈ℕ⟼f∘f⁡−fh⁡n⁡x
111 fvex ⊢f∘f⁡−fh⁡k⁡x∈V
112 109 110 111 fvmpt ⊢k∈ℕ→n∈ℕ⟼f∘f⁡−fh⁡n⁡x⁡k=f∘f⁡−fh⁡k⁡x
113 112 adantl ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ∧k∈ℕ→n∈ℕ⟼f∘f⁡−fh⁡n⁡x⁡k=f∘f⁡−fh⁡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⁡−fh⁡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⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0∧k∈ℕ→n∈ℕ⟼f∘f⁡−fh⁡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⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0→n∈ℕ⟼f∘f⁡−fh⁡n⁡x⇝if0≤F⁡xF⁡x0−if0≤−F⁡x−F⁡x0
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∈ℝ→if0≤F⁡xF⁡x0−if0≤−F⁡x−F⁡x0=F⁡x
132 130 131 syl ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ→if0≤F⁡xF⁡x0−if0≤−F⁡x−F⁡x0=F⁡x
133 132 adantr ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ∧n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0→if0≤F⁡xF⁡x0−if0≤−F⁡x−F⁡x0=F⁡x
134 128 133 breqtrd ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ∧n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0→n∈ℕ⟼f∘f⁡−fh⁡n⁡x⇝F⁡x
135 134 ex ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ→n∈ℕ⟼f⁡n⁡x⇝if0≤F⁡xF⁡x0∧n∈ℕ⟼h⁡n⁡x⇝if0≤−F⁡x−F⁡x0→n∈ℕ⟼f∘f⁡−fh⁡n⁡x⇝F⁡x
136 60 135 sylbid ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧x∈ℝ→n∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧n∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→n∈ℕ⟼f∘f⁡−fh⁡n⁡x⇝F⁡x
137 136 ralimdva ⊢φ∧f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1→∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧n∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→∀x∈ℝn∈ℕ⟼f∘f⁡−fh⁡n⁡x⇝F⁡x
138 ovex ⊢f∘f⁡−fh∈V
139 feq1 ⊢g=f∘f⁡−fh→g:ℕ⟶dom⁡∫1↔f∘f⁡−fh:ℕ⟶dom⁡∫1
140 fveq1 ⊢g=f∘f⁡−fh→g⁡n=f∘f⁡−fh⁡n
141 140 fveq1d ⊢g=f∘f⁡−fh→g⁡n⁡x=f∘f⁡−fh⁡n⁡x
142 141 mpteq2dv ⊢g=f∘f⁡−fh→n∈ℕ⟼g⁡n⁡x=n∈ℕ⟼f∘f⁡−fh⁡n⁡x
143 142 breq1d ⊢g=f∘f⁡−fh→n∈ℕ⟼g⁡n⁡x⇝F⁡x↔n∈ℕ⟼f∘f⁡−fh⁡n⁡x⇝F⁡x
144 143 ralbidv ⊢g=f∘f⁡−fh→∀x∈ℝn∈ℕ⟼g⁡n⁡x⇝F⁡x↔∀x∈ℝn∈ℕ⟼f∘f⁡−fh⁡n⁡x⇝F⁡x
145 139 144 anbi12d ⊢g=f∘f⁡−fh→g:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼g⁡n⁡x⇝F⁡x↔f∘f⁡−fh:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼f∘f⁡−fh⁡n⁡x⇝F⁡x
146 138 145 spcev ⊢f∘f⁡−fh:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼f∘f⁡−fh⁡n⁡x⇝F⁡x→∃gg:ℕ⟶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∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧n∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→∃gg:ℕ⟶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∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→∃gg:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼g⁡n⁡x⇝F⁡x
149 148 expimpd ⊢φ→f:ℕ⟶dom⁡∫1∧h:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→∃gg:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼g⁡n⁡x⇝F⁡x
150 32 149 syl5 ⊢φ→f:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤ff⁡n∧f⁡n≤ff⁡n+1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧h:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤fh⁡n∧h⁡n≤fh⁡n+1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→∃gg:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼g⁡n⁡x⇝F⁡x
151 150 exlimdvv ⊢φ→∃f∃hf:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤ff⁡n∧f⁡n≤ff⁡n+1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧h:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤fh⁡n∧h⁡n≤fh⁡n+1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→∃gg:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼g⁡n⁡x⇝F⁡x
152 27 151 biimtrrid ⊢φ→∃ff:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤ff⁡n∧f⁡n≤ff⁡n+1∧∀x∈ℝn∈ℕ⟼f⁡n⁡x⇝y∈ℝ⟼if0≤F⁡yF⁡y0⁡x∧∃hh:ℕ⟶dom⁡∫1∧∀n∈ℕ0𝑝≤fh⁡n∧h⁡n≤fh⁡n+1∧∀x∈ℝn∈ℕ⟼h⁡n⁡x⇝y∈ℝ⟼if0≤−F⁡y−F⁡y0⁡x→∃gg:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼g⁡n⁡x⇝F⁡x
153 15 26 152 mp2and ⊢φ→∃gg:ℕ⟶dom⁡∫1∧∀x∈ℝn∈ℕ⟼g⁡n⁡x⇝F⁡x