mbfi1fseqlem6 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mbfi1fseqlem6		Structured version Visualization version GIF version

Theorem mbfi1fseqlem6 25756

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

**Hypotheses**
Ref	Expression
mbfi1fseq.1	⊢ (𝜑 → 𝐹 ∈ MblFn)
mbfi1fseq.2	⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
mbfi1fseq.3	⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))
mbfi1fseq.4	⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))

**Assertion**
Ref	Expression
mbfi1fseqlem6	⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

Distinct variable groups: 𝑔,𝑚,𝑛,𝑥,𝑦,𝐹 𝑔,𝐺,𝑛,𝑥 𝑚,𝐽 𝜑,𝑚,𝑛,𝑥,𝑦 Allowed substitution hints: 𝜑(𝑔) 𝐺(𝑦,𝑚) 𝐽(𝑥,𝑦,𝑔,𝑛)

Proof of Theorem mbfi1fseqlem6 Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbfi1fseq.1	. . 3 ⊢ (𝜑 → 𝐹 ∈ MblFn)
2		mbfi1fseq.2	. . 3 ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
3		mbfi1fseq.3	. . 3 ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))
4		mbfi1fseq.4	. . 3 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
5	1, 2, 3, 4	mbfi1fseqlem4 25754	. 2 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫₁)
6	1, 2, 3, 4	mbfi1fseqlem5 25755	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
7	6	ralrimiva 3145	. 2 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
8		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
9	8	recnd 11290	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
10	9	abscld 15476	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℝ)
11	2	ffvelcdmda 7103	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
12		elrege0 13495	. . . . . . . 8 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
13	11, 12	sylib 218	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
14	13	simpld 494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
15	10, 14	readdcld 11291	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ)
16		arch 12525	. . . . 5 ⊢ (((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ → ∃𝑘 ∈ ℕ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
17	15, 16	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑘 ∈ ℕ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
18		eqid 2736	. . . . 5 ⊢ (ℤ_≥‘𝑘) = (ℤ_≥‘𝑘)
19		nnz 12636	. . . . . 6 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
20	19	ad2antrl 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℤ)
21		nnuz 12922	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
22		1zzd 12650	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℤ)
23		halfcn 12482	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℂ
24	23	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 2) ∈ ℂ)
25		halfre 12481	. . . . . . . . . . . 12 ⊢ (1 / 2) ∈ ℝ
26		halfge0 12484	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 2)
27		absid 15336	. . . . . . . . . . . 12 ⊢ (((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 / 2))
28	25, 26, 27	mp2an 692	. . . . . . . . . . 11 ⊢ (abs‘(1 / 2)) = (1 / 2)
29		halflt1 12485	. . . . . . . . . . 11 ⊢ (1 / 2) < 1
30	28, 29	eqbrtri 5163	. . . . . . . . . 10 ⊢ (abs‘(1 / 2)) < 1
31	30	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘(1 / 2)) < 1)
32	24, 31	expcnv 15901	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛)) ⇝ 0)
33	14	recnd 11290	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
34		nnex 12273	. . . . . . . . . 10 ⊢ ℕ ∈ V
35	34	mptex 7244	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V
36	35	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V)
37		nnnn0 12535	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ₀)
38	37	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ₀)
39		oveq2 7440	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑗))
40		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))
41		ovex 7465	. . . . . . . . . . 11 ⊢ ((1 / 2)↑𝑗) ∈ V
42	39, 40, 41	fvmpt 7015	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗))
43	38, 42	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗))
44		expcl 14121	. . . . . . . . . 10 ⊢ (((1 / 2) ∈ ℂ ∧ 𝑗 ∈ ℕ₀) → ((1 / 2)↑𝑗) ∈ ℂ)
45	23, 38, 44	sylancr 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((1 / 2)↑𝑗) ∈ ℂ)
46	43, 45	eqeltrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) ∈ ℂ)
47	39	oveq2d 7448	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑥) − ((1 / 2)↑𝑛)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
48		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))
49		ovex 7465	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ V
50	47, 48, 49	fvmpt 7015	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
51	50	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
52	43	oveq2d 7448	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑥) − ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
53	51, 52	eqtr4d 2779	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗)))
54	21, 22, 32, 33, 36, 46, 53	climsubc2 15676	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ ((𝐹‘𝑥) − 0))
55	33	subid1d 11610	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) − 0) = (𝐹‘𝑥))
56	54, 55	breqtrd 5168	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥))
57	56	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥))
58	34	mptex 7244	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V
59	58	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V)
60		simprl 770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℕ)
61		eluznn 12961	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℕ)
62	60, 61	sylan 580	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℕ)
63	62, 50	syl 17	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
64	14	ad2antrr 726	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ∈ ℝ)
65	62, 37	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℕ₀)
66		reexpcl 14120	. . . . . . . 8 ⊢ (((1 / 2) ∈ ℝ ∧ 𝑗 ∈ ℕ₀) → ((1 / 2)↑𝑗) ∈ ℝ)
67	25, 65, 66	sylancr 587	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((1 / 2)↑𝑗) ∈ ℝ)
68	64, 67	resubcld 11692	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ ℝ)
69	63, 68	eqeltrd 2840	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ∈ ℝ)
70		fveq2 6905	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → (𝐺‘𝑛) = (𝐺‘𝑗))
71	70	fveq1d 6907	. . . . . . . 8 ⊢ (𝑛 = 𝑗 → ((𝐺‘𝑛)‘𝑥) = ((𝐺‘𝑗)‘𝑥))
72		eqid 2736	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))
73		fvex 6918	. . . . . . . 8 ⊢ ((𝐺‘𝑗)‘𝑥) ∈ V
74	71, 72, 73	fvmpt 7015	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥))
75	62, 74	syl 17	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥))
76	5	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝐺:ℕ⟶dom ∫₁)
77	76, 62	ffvelcdmd 7104	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗) ∈ dom ∫₁)
78		i1ff 25712	. . . . . . . 8 ⊢ ((𝐺‘𝑗) ∈ dom ∫₁ → (𝐺‘𝑗):ℝ⟶ℝ)
79	77, 78	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗):ℝ⟶ℝ)
80	8	ad2antrr 726	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ ℝ)
81	79, 80	ffvelcdmd 7104	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) ∈ ℝ)
82	75, 81	eqeltrd 2840	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ∈ ℝ)
83	33	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ∈ ℂ)
84		2nn 12340	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
85		nnexpcl 14116	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 𝑗 ∈ ℕ₀) → (2↑𝑗) ∈ ℕ)
86	84, 65, 85	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℕ)
87	86	nnred 12282	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℝ)
88	87	recnd 11290	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℂ)
89	86	nnne0d 12317	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ≠ 0)
90	83, 88, 89	divcan4d 12050	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) = (𝐹‘𝑥))
91	90	eqcomd 2742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) = (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)))
92		2cnd 12345	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 2 ∈ ℂ)
93		2ne0 12371	. . . . . . . . . . 11 ⊢ 2 ≠ 0
94	93	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 2 ≠ 0)
95		eluzelz 12889	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑘) → 𝑗 ∈ ℤ)
96	95	adantl 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℤ)
97	92, 94, 96	exprecd 14195	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗)))
98	91, 97	oveq12d 7450	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗))))
99	64, 87	remulcld 11292	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ)
100	99	recnd 11290	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℂ)
101		1cnd 11257	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 1 ∈ ℂ)
102	100, 101, 88, 89	divsubdird 12083	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗))))
103	98, 102	eqtr4d 2779	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)))
104		fllep1 13842	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))
105	99, 104	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))
106		1red 11263	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 1 ∈ ℝ)
107		reflcl 13837	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ)
108	99, 107	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ)
109	99, 106, 108	lesubaddd 11861	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1)))
110	105, 109	mpbird 257	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))))
111		peano2rem 11577	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ)
112	99, 111	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ)
113	86	nngt0d 12316	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 0 < (2↑𝑗))
114		lediv1 12134	. . . . . . . . 9 ⊢ (((((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ ∧ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 < (2↑𝑗))) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))))
115	112, 108, 87, 113, 114	syl112anc 1375	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))))
116	110, 115	mpbid 232	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
117	103, 116	eqbrtrd 5164	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
118	1, 2, 3, 4	mbfi1fseqlem2 25752	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)))
119	62, 118	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)))
120	119	fveq1d 6907	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥))
121		ovex 7465	. . . . . . . . . . 11 ⊢ (𝑗𝐽𝑥) ∈ V
122		vex 3483	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
123	121, 122	ifex 4575	. . . . . . . . . 10 ⊢ if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) ∈ V
124		c0ex 11256	. . . . . . . . . 10 ⊢ 0 ∈ V
125	123, 124	ifex 4575	. . . . . . . . 9 ⊢ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V
126		eqid 2736	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
127	126	fvmpt2 7026	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
128	80, 125, 127	sylancl 586	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
129	75, 120, 128	3eqtrd 2780	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
130	10	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ∈ ℝ)
131	15	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ)
132	62	nnred 12282	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℝ)
133	11	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ∈ (0[,)+∞))
134	133, 12	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
135	134	simprd 495	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 0 ≤ (𝐹‘𝑥))
136	130, 64	addge01d 11852	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (0 ≤ (𝐹‘𝑥) ↔ (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))))
137	135, 136	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))
138	60	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ∈ ℕ)
139	138	nnred 12282	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ∈ ℝ)
140		simplrr 777	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
141	131, 139, 140	ltled 11410	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑘)
142		eluzle 12892	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘𝑘) → 𝑘 ≤ 𝑗)
143	142	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ≤ 𝑗)
144	131, 139, 132, 141, 143	letrd 11419	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑗)
145	130, 131, 132, 137, 144	letrd 11419	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ≤ 𝑗)
146	80, 132	absled 15470	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) ≤ 𝑗 ↔ (-𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)))
147	145, 146	mpbid 232	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (-𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))
148	147	simpld 494	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → -𝑗 ≤ 𝑥)
149	147	simprd 495	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ≤ 𝑗)
150	132	renegcld 11691	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → -𝑗 ∈ ℝ)
151		elicc2 13453	. . . . . . . . . 10 ⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)))
152	150, 132, 151	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)))
153	80, 148, 149, 152	mpbir3and 1342	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ (-𝑗[,]𝑗))
154	153	iftrued 4532	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) = if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗))
155		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
156	155	fveq2d 6909	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
157		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑗)
158	157	oveq2d 7448	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑗))
159	156, 158	oveq12d 7450	. . . . . . . . . . . . . 14 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑗)))
160	159	fveq2d 6909	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑗))))
161	160, 158	oveq12d 7450	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
162		ovex 7465	. . . . . . . . . . . 12 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ V
163	161, 3, 162	ovmpoa 7589	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
164	62, 80, 163	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
165	108, 86	nndivred 12321	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ ℝ)
166		flle 13840	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))
167	99, 166	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))
168		ledivmul2 12148	. . . . . . . . . . . . 13 ⊢ (((⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 < (2↑𝑗))) → (((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))))
169	108, 64, 87, 113, 168	syl112anc 1375	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))))
170	167, 169	mpbird 257	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥))
171	9	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ ℂ)
172	171	absge0d 15484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 0 ≤ (abs‘𝑥))
173	64, 130	addge02d 11853	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (0 ≤ (abs‘𝑥) ↔ (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))))
174	172, 173	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))
175	64, 131, 132, 174, 144	letrd 11419	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ≤ 𝑗)
176	165, 64, 132, 170, 175	letrd 11419	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ 𝑗)
177	164, 176	eqbrtrd 5164	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑗𝐽𝑥) ≤ 𝑗)
178	177	iftrued 4532	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = (𝑗𝐽𝑥))
179	178, 164	eqtrd 2776	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
180	129, 154, 179	3eqtrd 2780	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
181	117, 63, 180	3brtr4d 5174	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗))
182	180, 170	eqbrtrd 5164	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ≤ (𝐹‘𝑥))
183	18, 20, 57, 59, 69, 82, 181, 182	climsqz 15678	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
184	17, 183	rexlimddv 3160	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
185	184	ralrimiva 3145	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
186	34	mptex 7244	. . . 4 ⊢ (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ∈ V
187	4, 186	eqeltri 2836	. . 3 ⊢ 𝐺 ∈ V
188		feq1 6715	. . . 4 ⊢ (𝑔 = 𝐺 → (𝑔:ℕ⟶dom ∫₁ ↔ 𝐺:ℕ⟶dom ∫₁))
189		fveq1 6904	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
190	189	breq2d 5154	. . . . . 6 ⊢ (𝑔 = 𝐺 → (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ↔ 0_𝑝 ∘_r ≤ (𝐺‘𝑛)))
191		fveq1 6904	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1)))
192	189, 191	breq12d 5155	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1)) ↔ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
193	190, 192	anbi12d 632	. . . . 5 ⊢ (𝑔 = 𝐺 → ((0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ↔ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1)))))
194	193	ralbidv 3177	. . . 4 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ↔ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1)))))
195	189	fveq1d 6907	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛)‘𝑥) = ((𝐺‘𝑛)‘𝑥))
196	195	mpteq2dv 5243	. . . . . 6 ⊢ (𝑔 = 𝐺 → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)))
197	196	breq1d 5152	. . . . 5 ⊢ (𝑔 = 𝐺 → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
198	197	ralbidv 3177	. . . 4 ⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
199	188, 194, 198	3anbi123d 1437	. . 3 ⊢ (𝑔 = 𝐺 → ((𝑔:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ (𝐺:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
200	187, 199	spcev 3605	. 2 ⊢ ((𝐺:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
201	5, 7, 185, 200	syl3anc 1372	1 ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∃wex 1778 ∈ wcel 2107 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 Vcvv 3479 ifcif 4524 class class class wbr 5142 ↦ cmpt 5224 dom cdm 5684 ⟶wf 6556 ‘cfv 6560 (class class class)co 7432 ∈ cmpo 7434 ∘_r cofr 7697 ℂcc 11154 ℝcr 11155 0cc0 11156 1c1 11157 + caddc 11159 · cmul 11161 +∞cpnf 11293 < clt 11296 ≤ cle 11297 − cmin 11493 -cneg 11494 / cdiv 11921 ℕcn 12267 2c2 12322 ℕ₀cn0 12528 ℤcz 12615 ℤ_≥cuz 12879 [,)cico 13390 [,]cicc 13391 ⌊cfl 13831 ↑cexp 14103 abscabs 15274 ⇝ cli 15521 MblFncmbf 25650 ∫₁citg1 25651 0_𝑝c0p 25705

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-inf2 9682 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233 ax-pre-sup 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-se 5637 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-isom 6569 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-of 7698 df-ofr 7699 df-om 7889 df-1st 8015 df-2nd 8016 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-2o 8508 df-er 8746 df-map 8869 df-pm 8870 df-en 8987 df-dom 8988 df-sdom 8989 df-fin 8990 df-fi 9452 df-sup 9483 df-inf 9484 df-oi 9551 df-dju 9942 df-card 9980 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-div 11922 df-nn 12268 df-2 12330 df-3 12331 df-n0 12529 df-z 12616 df-uz 12880 df-q 12992 df-rp 13036 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13392 df-ico 13394 df-icc 13395 df-fz 13549 df-fzo 13696 df-fl 13833 df-seq 14044 df-exp 14104 df-hash 14371 df-cj 15139 df-re 15140 df-im 15141 df-sqrt 15275 df-abs 15276 df-clim 15525 df-rlim 15526 df-sum 15724 df-rest 17468 df-topgen 17489 df-psmet 21357 df-xmet 21358 df-met 21359 df-bl 21360 df-mopn 21361 df-top 22901 df-topon 22918 df-bases 22954 df-cmp 23396 df-ovol 25500 df-vol 25501 df-mbf 25655 df-itg1 25656 df-0p 25706

This theorem is referenced by: mbfi1fseq 25757

W3C validator