Metamath Proof Explorer

Theorem mbfi1fseqlem6

Description: Lemma for mbfi1fseq . Verify that G converges pointwise to F , and wrap up the existential quantifier. (Contributed by Mario Carneiro, 16-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses mbfi1fseq.1 ${⊢}{\phi }\to {F}\in MblFn$
mbfi1fseq.2 ${⊢}{\phi }\to {F}:ℝ⟶\left[0,\mathrm{+\infty }\right)$
mbfi1fseq.3 ${⊢}{J}=\left({m}\in ℕ,{y}\in ℝ⟼\frac{⌊{F}\left({y}\right){2}^{{m}}⌋}{{2}^{{m}}}\right)$
mbfi1fseq.4 ${⊢}{G}=\left({m}\in ℕ⟼\left({x}\in ℝ⟼if\left({x}\in \left[-{m},{m}\right],if\left({m}{J}{x}\le {m},{m}{J}{x},{m}\right),0\right)\right)\right)$
Assertion mbfi1fseqlem6 ${⊢}{\phi }\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:ℕ⟶\mathrm{dom}{\int }^{1}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({0}_{𝑝}{\le }_{f}{g}\left({n}\right)\wedge {g}\left({n}\right){\le }_{f}{g}\left({n}+1\right)\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{g}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)\right)$

Proof

Step Hyp Ref Expression
1 mbfi1fseq.1 ${⊢}{\phi }\to {F}\in MblFn$
2 mbfi1fseq.2 ${⊢}{\phi }\to {F}:ℝ⟶\left[0,\mathrm{+\infty }\right)$
3 mbfi1fseq.3 ${⊢}{J}=\left({m}\in ℕ,{y}\in ℝ⟼\frac{⌊{F}\left({y}\right){2}^{{m}}⌋}{{2}^{{m}}}\right)$
4 mbfi1fseq.4 ${⊢}{G}=\left({m}\in ℕ⟼\left({x}\in ℝ⟼if\left({x}\in \left[-{m},{m}\right],if\left({m}{J}{x}\le {m},{m}{J}{x},{m}\right),0\right)\right)\right)$
5 1 2 3 4 mbfi1fseqlem4 ${⊢}{\phi }\to {G}:ℕ⟶\mathrm{dom}{\int }^{1}$
6 1 2 3 4 mbfi1fseqlem5 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({0}_{𝑝}{\le }_{f}{G}\left({n}\right)\wedge {G}\left({n}\right){\le }_{f}{G}\left({n}+1\right)\right)$
7 6 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({0}_{𝑝}{\le }_{f}{G}\left({n}\right)\wedge {G}\left({n}\right){\le }_{f}{G}\left({n}+1\right)\right)$
8 simpr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {x}\in ℝ$
9 8 recnd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {x}\in ℂ$
10 9 abscld ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left|{x}\right|\in ℝ$
11 2 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
12 elrege0 ${⊢}{F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)↔\left({F}\left({x}\right)\in ℝ\wedge 0\le {F}\left({x}\right)\right)$
13 11 12 sylib ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({F}\left({x}\right)\in ℝ\wedge 0\le {F}\left({x}\right)\right)$
14 13 simpld ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}\right)\in ℝ$
15 10 14 readdcld ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left|{x}\right|+{F}\left({x}\right)\in ℝ$
16 arch ${⊢}\left|{x}\right|+{F}\left({x}\right)\in ℝ\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{x}\right|+{F}\left({x}\right)<{k}$
17 15 16 syl ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{x}\right|+{F}\left({x}\right)<{k}$
18 eqid ${⊢}{ℤ}_{\ge {k}}={ℤ}_{\ge {k}}$
19 nnz ${⊢}{k}\in ℕ\to {k}\in ℤ$
20 19 ad2antrl ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\to {k}\in ℤ$
21 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
22 1zzd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to 1\in ℤ$
23 halfcn ${⊢}\frac{1}{2}\in ℂ$
24 23 a1i ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \frac{1}{2}\in ℂ$
25 halfre ${⊢}\frac{1}{2}\in ℝ$
26 halfge0 ${⊢}0\le \frac{1}{2}$
27 absid ${⊢}\left(\frac{1}{2}\in ℝ\wedge 0\le \frac{1}{2}\right)\to \left|\frac{1}{2}\right|=\frac{1}{2}$
28 25 26 27 mp2an ${⊢}\left|\frac{1}{2}\right|=\frac{1}{2}$
29 halflt1 ${⊢}\frac{1}{2}<1$
30 28 29 eqbrtri ${⊢}\left|\frac{1}{2}\right|<1$
31 30 a1i ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left|\frac{1}{2}\right|<1$
32 24 31 expcnv ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({n}\in {ℕ}_{0}⟼{\left(\frac{1}{2}\right)}^{{n}}\right)⇝0$
33 14 recnd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}\right)\in ℂ$
34 nnex ${⊢}ℕ\in \mathrm{V}$
35 34 mptex ${⊢}\left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)\in \mathrm{V}$
36 35 a1i ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)\in \mathrm{V}$
37 nnnn0 ${⊢}{j}\in ℕ\to {j}\in {ℕ}_{0}$
38 37 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to {j}\in {ℕ}_{0}$
39 oveq2 ${⊢}{n}={j}\to {\left(\frac{1}{2}\right)}^{{n}}={\left(\frac{1}{2}\right)}^{{j}}$
40 eqid ${⊢}\left({n}\in {ℕ}_{0}⟼{\left(\frac{1}{2}\right)}^{{n}}\right)=\left({n}\in {ℕ}_{0}⟼{\left(\frac{1}{2}\right)}^{{n}}\right)$
41 ovex ${⊢}{\left(\frac{1}{2}\right)}^{{j}}\in \mathrm{V}$
42 39 40 41 fvmpt ${⊢}{j}\in {ℕ}_{0}\to \left({n}\in {ℕ}_{0}⟼{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)={\left(\frac{1}{2}\right)}^{{j}}$
43 38 42 syl ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to \left({n}\in {ℕ}_{0}⟼{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)={\left(\frac{1}{2}\right)}^{{j}}$
44 expcl ${⊢}\left(\frac{1}{2}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\to {\left(\frac{1}{2}\right)}^{{j}}\in ℂ$
45 23 38 44 sylancr ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to {\left(\frac{1}{2}\right)}^{{j}}\in ℂ$
46 43 45 eqeltrd ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to \left({n}\in {ℕ}_{0}⟼{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)\in ℂ$
47 39 oveq2d ${⊢}{n}={j}\to {F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}={F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{j}}$
48 eqid ${⊢}\left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)=\left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)$
49 ovex ${⊢}{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{j}}\in \mathrm{V}$
50 47 48 49 fvmpt ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)={F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{j}}$
51 50 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to \left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)={F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{j}}$
52 43 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to {F}\left({x}\right)-\left({n}\in {ℕ}_{0}⟼{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)={F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{j}}$
53 51 52 eqtr4d ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to \left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)={F}\left({x}\right)-\left({n}\in {ℕ}_{0}⟼{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)$
54 21 22 32 33 36 46 53 climsubc2 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)⇝\left({F}\left({x}\right)-0\right)$
55 33 subid1d ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}\right)-0={F}\left({x}\right)$
56 54 55 breqtrd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)⇝{F}\left({x}\right)$
57 56 adantr ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\to \left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)⇝{F}\left({x}\right)$
58 34 mptex ${⊢}\left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)\in \mathrm{V}$
59 58 a1i ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\to \left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)\in \mathrm{V}$
60 simprl ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\to {k}\in ℕ$
61 eluznn ${⊢}\left({k}\in ℕ\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {j}\in ℕ$
62 60 61 sylan ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {j}\in ℕ$
63 62 50 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)={F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{j}}$
64 14 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right)\in ℝ$
65 62 37 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {j}\in {ℕ}_{0}$
66 reexpcl ${⊢}\left(\frac{1}{2}\in ℝ\wedge {j}\in {ℕ}_{0}\right)\to {\left(\frac{1}{2}\right)}^{{j}}\in ℝ$
67 25 65 66 sylancr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {\left(\frac{1}{2}\right)}^{{j}}\in ℝ$
68 64 67 resubcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{j}}\in ℝ$
69 63 68 eqeltrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)\in ℝ$
70 fveq2 ${⊢}{n}={j}\to {G}\left({n}\right)={G}\left({j}\right)$
71 70 fveq1d ${⊢}{n}={j}\to {G}\left({n}\right)\left({x}\right)={G}\left({j}\right)\left({x}\right)$
72 eqid ${⊢}\left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)=\left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)$
73 fvex ${⊢}{G}\left({j}\right)\left({x}\right)\in \mathrm{V}$
74 71 72 73 fvmpt ${⊢}{j}\in ℕ\to \left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)\left({j}\right)={G}\left({j}\right)\left({x}\right)$
75 62 74 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)\left({j}\right)={G}\left({j}\right)\left({x}\right)$
76 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {G}:ℕ⟶\mathrm{dom}{\int }^{1}$
77 76 62 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {G}\left({j}\right)\in \mathrm{dom}{\int }^{1}$
78 i1ff ${⊢}{G}\left({j}\right)\in \mathrm{dom}{\int }^{1}\to {G}\left({j}\right):ℝ⟶ℝ$
79 77 78 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {G}\left({j}\right):ℝ⟶ℝ$
80 8 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {x}\in ℝ$
81 79 80 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {G}\left({j}\right)\left({x}\right)\in ℝ$
82 75 81 eqeltrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)\left({j}\right)\in ℝ$
83 33 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right)\in ℂ$
84 2nn ${⊢}2\in ℕ$
85 nnexpcl ${⊢}\left(2\in ℕ\wedge {j}\in {ℕ}_{0}\right)\to {2}^{{j}}\in ℕ$
86 84 65 85 sylancr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {2}^{{j}}\in ℕ$
87 86 nnred ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {2}^{{j}}\in ℝ$
88 87 recnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {2}^{{j}}\in ℂ$
89 86 nnne0d ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {2}^{{j}}\ne 0$
90 83 88 89 divcan4d ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \frac{{F}\left({x}\right){2}^{{j}}}{{2}^{{j}}}={F}\left({x}\right)$
91 90 eqcomd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right)=\frac{{F}\left({x}\right){2}^{{j}}}{{2}^{{j}}}$
92 2cnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to 2\in ℂ$
93 2ne0 ${⊢}2\ne 0$
94 93 a1i ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to 2\ne 0$
95 eluzelz ${⊢}{j}\in {ℤ}_{\ge {k}}\to {j}\in ℤ$
96 95 adantl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {j}\in ℤ$
97 92 94 96 exprecd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {\left(\frac{1}{2}\right)}^{{j}}=\frac{1}{{2}^{{j}}}$
98 91 97 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{j}}=\left(\frac{{F}\left({x}\right){2}^{{j}}}{{2}^{{j}}}\right)-\left(\frac{1}{{2}^{{j}}}\right)$
99 64 87 remulcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right){2}^{{j}}\in ℝ$
100 99 recnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right){2}^{{j}}\in ℂ$
101 1cnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to 1\in ℂ$
102 100 101 88 89 divsubdird ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \frac{{F}\left({x}\right){2}^{{j}}-1}{{2}^{{j}}}=\left(\frac{{F}\left({x}\right){2}^{{j}}}{{2}^{{j}}}\right)-\left(\frac{1}{{2}^{{j}}}\right)$
103 98 102 eqtr4d ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{j}}=\frac{{F}\left({x}\right){2}^{{j}}-1}{{2}^{{j}}}$
104 fllep1 ${⊢}{F}\left({x}\right){2}^{{j}}\in ℝ\to {F}\left({x}\right){2}^{{j}}\le ⌊{F}\left({x}\right){2}^{{j}}⌋+1$
105 99 104 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right){2}^{{j}}\le ⌊{F}\left({x}\right){2}^{{j}}⌋+1$
106 1red ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to 1\in ℝ$
107 reflcl ${⊢}{F}\left({x}\right){2}^{{j}}\in ℝ\to ⌊{F}\left({x}\right){2}^{{j}}⌋\in ℝ$
108 99 107 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to ⌊{F}\left({x}\right){2}^{{j}}⌋\in ℝ$
109 99 106 108 lesubaddd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({F}\left({x}\right){2}^{{j}}-1\le ⌊{F}\left({x}\right){2}^{{j}}⌋↔{F}\left({x}\right){2}^{{j}}\le ⌊{F}\left({x}\right){2}^{{j}}⌋+1\right)$
110 105 109 mpbird ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right){2}^{{j}}-1\le ⌊{F}\left({x}\right){2}^{{j}}⌋$
111 peano2rem ${⊢}{F}\left({x}\right){2}^{{j}}\in ℝ\to {F}\left({x}\right){2}^{{j}}-1\in ℝ$
112 99 111 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right){2}^{{j}}-1\in ℝ$
113 86 nngt0d ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to 0<{2}^{{j}}$
114 lediv1 ${⊢}\left({F}\left({x}\right){2}^{{j}}-1\in ℝ\wedge ⌊{F}\left({x}\right){2}^{{j}}⌋\in ℝ\wedge \left({2}^{{j}}\in ℝ\wedge 0<{2}^{{j}}\right)\right)\to \left({F}\left({x}\right){2}^{{j}}-1\le ⌊{F}\left({x}\right){2}^{{j}}⌋↔\frac{{F}\left({x}\right){2}^{{j}}-1}{{2}^{{j}}}\le \frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}\right)$
115 112 108 87 113 114 syl112anc ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({F}\left({x}\right){2}^{{j}}-1\le ⌊{F}\left({x}\right){2}^{{j}}⌋↔\frac{{F}\left({x}\right){2}^{{j}}-1}{{2}^{{j}}}\le \frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}\right)$
116 110 115 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \frac{{F}\left({x}\right){2}^{{j}}-1}{{2}^{{j}}}\le \frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}$
117 103 116 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{j}}\le \frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}$
118 1 2 3 4 mbfi1fseqlem2 ${⊢}{j}\in ℕ\to {G}\left({j}\right)=\left({x}\in ℝ⟼if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)\right)$
119 62 118 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {G}\left({j}\right)=\left({x}\in ℝ⟼if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)\right)$
120 119 fveq1d ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {G}\left({j}\right)\left({x}\right)=\left({x}\in ℝ⟼if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)\right)\left({x}\right)$
121 ovex ${⊢}{j}{J}{x}\in \mathrm{V}$
122 vex ${⊢}{j}\in \mathrm{V}$
123 121 122 ifex ${⊢}if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right)\in \mathrm{V}$
124 c0ex ${⊢}0\in \mathrm{V}$
125 123 124 ifex ${⊢}if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)\in \mathrm{V}$
126 eqid ${⊢}\left({x}\in ℝ⟼if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)\right)$
127 126 fvmpt2 ${⊢}\left({x}\in ℝ\wedge if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)\in \mathrm{V}\right)\to \left({x}\in ℝ⟼if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)\right)\left({x}\right)=if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)$
128 80 125 127 sylancl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({x}\in ℝ⟼if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)\right)\left({x}\right)=if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)$
129 75 120 128 3eqtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)\left({j}\right)=if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)$
130 10 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left|{x}\right|\in ℝ$
131 15 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left|{x}\right|+{F}\left({x}\right)\in ℝ$
132 62 nnred ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {j}\in ℝ$
133 11 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
134 133 12 sylib ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({F}\left({x}\right)\in ℝ\wedge 0\le {F}\left({x}\right)\right)$
135 134 simprd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to 0\le {F}\left({x}\right)$
136 130 64 addge01d ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left(0\le {F}\left({x}\right)↔\left|{x}\right|\le \left|{x}\right|+{F}\left({x}\right)\right)$
137 135 136 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left|{x}\right|\le \left|{x}\right|+{F}\left({x}\right)$
138 60 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {k}\in ℕ$
139 138 nnred ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {k}\in ℝ$
140 simplrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left|{x}\right|+{F}\left({x}\right)<{k}$
141 131 139 140 ltled ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left|{x}\right|+{F}\left({x}\right)\le {k}$
142 eluzle ${⊢}{j}\in {ℤ}_{\ge {k}}\to {k}\le {j}$
143 142 adantl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {k}\le {j}$
144 131 139 132 141 143 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left|{x}\right|+{F}\left({x}\right)\le {j}$
145 130 131 132 137 144 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left|{x}\right|\le {j}$
146 80 132 absled ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left(\left|{x}\right|\le {j}↔\left(-{j}\le {x}\wedge {x}\le {j}\right)\right)$
147 145 146 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left(-{j}\le {x}\wedge {x}\le {j}\right)$
148 147 simpld ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to -{j}\le {x}$
149 147 simprd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {x}\le {j}$
150 132 renegcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to -{j}\in ℝ$
151 elicc2 ${⊢}\left(-{j}\in ℝ\wedge {j}\in ℝ\right)\to \left({x}\in \left[-{j},{j}\right]↔\left({x}\in ℝ\wedge -{j}\le {x}\wedge {x}\le {j}\right)\right)$
152 150 132 151 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({x}\in \left[-{j},{j}\right]↔\left({x}\in ℝ\wedge -{j}\le {x}\wedge {x}\le {j}\right)\right)$
153 80 148 149 152 mpbir3and ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {x}\in \left[-{j},{j}\right]$
154 153 iftrued ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to if\left({x}\in \left[-{j},{j}\right],if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right),0\right)=if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right)$
155 simpr ${⊢}\left({m}={j}\wedge {y}={x}\right)\to {y}={x}$
156 155 fveq2d ${⊢}\left({m}={j}\wedge {y}={x}\right)\to {F}\left({y}\right)={F}\left({x}\right)$
157 simpl ${⊢}\left({m}={j}\wedge {y}={x}\right)\to {m}={j}$
158 157 oveq2d ${⊢}\left({m}={j}\wedge {y}={x}\right)\to {2}^{{m}}={2}^{{j}}$
159 156 158 oveq12d ${⊢}\left({m}={j}\wedge {y}={x}\right)\to {F}\left({y}\right){2}^{{m}}={F}\left({x}\right){2}^{{j}}$
160 159 fveq2d ${⊢}\left({m}={j}\wedge {y}={x}\right)\to ⌊{F}\left({y}\right){2}^{{m}}⌋=⌊{F}\left({x}\right){2}^{{j}}⌋$
161 160 158 oveq12d ${⊢}\left({m}={j}\wedge {y}={x}\right)\to \frac{⌊{F}\left({y}\right){2}^{{m}}⌋}{{2}^{{m}}}=\frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}$
162 ovex ${⊢}\frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}\in \mathrm{V}$
163 161 3 162 ovmpoa ${⊢}\left({j}\in ℕ\wedge {x}\in ℝ\right)\to {j}{J}{x}=\frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}$
164 62 80 163 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {j}{J}{x}=\frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}$
165 108 86 nndivred ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}\in ℝ$
166 flle ${⊢}{F}\left({x}\right){2}^{{j}}\in ℝ\to ⌊{F}\left({x}\right){2}^{{j}}⌋\le {F}\left({x}\right){2}^{{j}}$
167 99 166 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to ⌊{F}\left({x}\right){2}^{{j}}⌋\le {F}\left({x}\right){2}^{{j}}$
168 ledivmul2 ${⊢}\left(⌊{F}\left({x}\right){2}^{{j}}⌋\in ℝ\wedge {F}\left({x}\right)\in ℝ\wedge \left({2}^{{j}}\in ℝ\wedge 0<{2}^{{j}}\right)\right)\to \left(\frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}\le {F}\left({x}\right)↔⌊{F}\left({x}\right){2}^{{j}}⌋\le {F}\left({x}\right){2}^{{j}}\right)$
169 108 64 87 113 168 syl112anc ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left(\frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}\le {F}\left({x}\right)↔⌊{F}\left({x}\right){2}^{{j}}⌋\le {F}\left({x}\right){2}^{{j}}\right)$
170 167 169 mpbird ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}\le {F}\left({x}\right)$
171 9 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {x}\in ℂ$
172 171 absge0d ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to 0\le \left|{x}\right|$
173 64 130 addge02d ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left(0\le \left|{x}\right|↔{F}\left({x}\right)\le \left|{x}\right|+{F}\left({x}\right)\right)$
174 172 173 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right)\le \left|{x}\right|+{F}\left({x}\right)$
175 64 131 132 174 144 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {F}\left({x}\right)\le {j}$
176 165 64 132 170 175 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}\le {j}$
177 164 176 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to {j}{J}{x}\le {j}$
178 177 iftrued ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right)={j}{J}{x}$
179 178 164 eqtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to if\left({j}{J}{x}\le {j},{j}{J}{x},{j}\right)=\frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}$
180 129 154 179 3eqtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)\left({j}\right)=\frac{⌊{F}\left({x}\right){2}^{{j}}⌋}{{2}^{{j}}}$
181 117 63 180 3brtr4d ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({n}\in ℕ⟼{F}\left({x}\right)-{\left(\frac{1}{2}\right)}^{{n}}\right)\left({j}\right)\le \left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)\left({j}\right)$
182 180 170 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\wedge {j}\in {ℤ}_{\ge {k}}\right)\to \left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)\left({j}\right)\le {F}\left({x}\right)$
183 18 20 57 59 69 82 181 182 climsqz ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge \left({k}\in ℕ\wedge \left|{x}\right|+{F}\left({x}\right)<{k}\right)\right)\to \left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)$
184 17 183 rexlimddv ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)$
185 184 ralrimiva ${⊢}{\phi }\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)$
186 34 mptex ${⊢}\left({m}\in ℕ⟼\left({x}\in ℝ⟼if\left({x}\in \left[-{m},{m}\right],if\left({m}{J}{x}\le {m},{m}{J}{x},{m}\right),0\right)\right)\right)\in \mathrm{V}$
187 4 186 eqeltri ${⊢}{G}\in \mathrm{V}$
188 feq1 ${⊢}{g}={G}\to \left({g}:ℕ⟶\mathrm{dom}{\int }^{1}↔{G}:ℕ⟶\mathrm{dom}{\int }^{1}\right)$
189 fveq1 ${⊢}{g}={G}\to {g}\left({n}\right)={G}\left({n}\right)$
190 189 breq2d ${⊢}{g}={G}\to \left({0}_{𝑝}{\le }_{f}{g}\left({n}\right)↔{0}_{𝑝}{\le }_{f}{G}\left({n}\right)\right)$
191 fveq1 ${⊢}{g}={G}\to {g}\left({n}+1\right)={G}\left({n}+1\right)$
192 189 191 breq12d ${⊢}{g}={G}\to \left({g}\left({n}\right){\le }_{f}{g}\left({n}+1\right)↔{G}\left({n}\right){\le }_{f}{G}\left({n}+1\right)\right)$
193 190 192 anbi12d ${⊢}{g}={G}\to \left(\left({0}_{𝑝}{\le }_{f}{g}\left({n}\right)\wedge {g}\left({n}\right){\le }_{f}{g}\left({n}+1\right)\right)↔\left({0}_{𝑝}{\le }_{f}{G}\left({n}\right)\wedge {G}\left({n}\right){\le }_{f}{G}\left({n}+1\right)\right)\right)$
194 193 ralbidv ${⊢}{g}={G}\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({0}_{𝑝}{\le }_{f}{g}\left({n}\right)\wedge {g}\left({n}\right){\le }_{f}{g}\left({n}+1\right)\right)↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({0}_{𝑝}{\le }_{f}{G}\left({n}\right)\wedge {G}\left({n}\right){\le }_{f}{G}\left({n}+1\right)\right)\right)$
195 189 fveq1d ${⊢}{g}={G}\to {g}\left({n}\right)\left({x}\right)={G}\left({n}\right)\left({x}\right)$
196 195 mpteq2dv ${⊢}{g}={G}\to \left({n}\in ℕ⟼{g}\left({n}\right)\left({x}\right)\right)=\left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)$
197 196 breq1d ${⊢}{g}={G}\to \left(\left({n}\in ℕ⟼{g}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)↔\left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)\right)$
198 197 ralbidv ${⊢}{g}={G}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{g}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)\right)$
199 188 194 198 3anbi123d ${⊢}{g}={G}\to \left(\left({g}:ℕ⟶\mathrm{dom}{\int }^{1}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({0}_{𝑝}{\le }_{f}{g}\left({n}\right)\wedge {g}\left({n}\right){\le }_{f}{g}\left({n}+1\right)\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{g}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)\right)↔\left({G}:ℕ⟶\mathrm{dom}{\int }^{1}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({0}_{𝑝}{\le }_{f}{G}\left({n}\right)\wedge {G}\left({n}\right){\le }_{f}{G}\left({n}+1\right)\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)\right)\right)$
200 187 199 spcev ${⊢}\left({G}:ℕ⟶\mathrm{dom}{\int }^{1}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({0}_{𝑝}{\le }_{f}{G}\left({n}\right)\wedge {G}\left({n}\right){\le }_{f}{G}\left({n}+1\right)\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{G}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:ℕ⟶\mathrm{dom}{\int }^{1}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({0}_{𝑝}{\le }_{f}{g}\left({n}\right)\wedge {g}\left({n}\right){\le }_{f}{g}\left({n}+1\right)\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{g}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)\right)$
201 5 7 185 200 syl3anc ${⊢}{\phi }\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:ℕ⟶\mathrm{dom}{\int }^{1}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({0}_{𝑝}{\le }_{f}{g}\left({n}\right)\wedge {g}\left({n}\right){\le }_{f}{g}\left({n}+1\right)\right)\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{g}\left({n}\right)\left({x}\right)\right)⇝{F}\left({x}\right)\right)$