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 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )