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 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfi1fseq.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
mbfi1fseq.3 ⊢ 𝐽 = ( 𝑚 ∈ ℕ , 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) )
mbfi1fseq.4 ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 𝐽 𝑥 ) ≤ 𝑚 , ( 𝑚 𝐽 𝑥 ) , 𝑚 ) , 0 ) ) )
Assertion mbfi1fseqlem6 ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )

Proof

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