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 25649

Description: Lemma for mbfi1fseq 25650. 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 25647	. 2 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫₁)
6	1, 2, 3, 4	mbfi1fseqlem5 25648	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
7	6	ralrimiva 3124	. 2 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
8		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
9	8	recnd 11140	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
10	9	abscld 15346	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℝ)
11	2	ffvelcdmda 7017	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
12		elrege0 13354	. . . . . . . 8 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
13	11, 12	sylib 218	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
14	13	simpld 494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
15	10, 14	readdcld 11141	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ)
16		arch 12378	. . . . 5 ⊢ (((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ → ∃𝑘 ∈ ℕ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
17	15, 16	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑘 ∈ ℕ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
18		eqid 2731	. . . . 5 ⊢ (ℤ_≥‘𝑘) = (ℤ_≥‘𝑘)
19		nnz 12489	. . . . . 6 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
20	19	ad2antrl 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℤ)
21		nnuz 12775	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
22		1zzd 12503	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℤ)
23		halfcn 12335	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℂ
24	23	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 2) ∈ ℂ)
25		halfre 12334	. . . . . . . . . . . 12 ⊢ (1 / 2) ∈ ℝ
26		halfge0 12337	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 2)
27		absid 15203	. . . . . . . . . . . 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 12338	. . . . . . . . . . 11 ⊢ (1 / 2) < 1
30	28, 29	eqbrtri 5112	. . . . . . . . . 10 ⊢ (abs‘(1 / 2)) < 1
31	30	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘(1 / 2)) < 1)
32	24, 31	expcnv 15771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛)) ⇝ 0)
33	14	recnd 11140	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
34		nnex 12131	. . . . . . . . . 10 ⊢ ℕ ∈ V
35	34	mptex 7157	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V
36	35	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V)
37		nnnn0 12388	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ₀)
38	37	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ₀)
39		oveq2 7354	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑗))
40		eqid 2731	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))
41		ovex 7379	. . . . . . . . . . 11 ⊢ ((1 / 2)↑𝑗) ∈ V
42	39, 40, 41	fvmpt 6929	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗))
43	38, 42	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗))
44		expcl 13986	. . . . . . . . . 10 ⊢ (((1 / 2) ∈ ℂ ∧ 𝑗 ∈ ℕ₀) → ((1 / 2)↑𝑗) ∈ ℂ)
45	23, 38, 44	sylancr 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((1 / 2)↑𝑗) ∈ ℂ)
46	43, 45	eqeltrd 2831	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) ∈ ℂ)
47	39	oveq2d 7362	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑥) − ((1 / 2)↑𝑛)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
48		eqid 2731	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))
49		ovex 7379	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ V
50	47, 48, 49	fvmpt 6929	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
51	50	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
52	43	oveq2d 7362	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑥) − ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
53	51, 52	eqtr4d 2769	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗)))
54	21, 22, 32, 33, 36, 46, 53	climsubc2 15546	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ ((𝐹‘𝑥) − 0))
55	33	subid1d 11461	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) − 0) = (𝐹‘𝑥))
56	54, 55	breqtrd 5117	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥))
57	56	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥))
58	34	mptex 7157	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V
59	58	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V)
60		simprl 770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℕ)
61		eluznn 12816	. . . . . . . 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 13985	. . . . . . . 8 ⊢ (((1 / 2) ∈ ℝ ∧ 𝑗 ∈ ℕ₀) → ((1 / 2)↑𝑗) ∈ ℝ)
67	25, 65, 66	sylancr 587	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((1 / 2)↑𝑗) ∈ ℝ)
68	64, 67	resubcld 11545	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ ℝ)
69	63, 68	eqeltrd 2831	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ∈ ℝ)
70		fveq2 6822	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → (𝐺‘𝑛) = (𝐺‘𝑗))
71	70	fveq1d 6824	. . . . . . . 8 ⊢ (𝑛 = 𝑗 → ((𝐺‘𝑛)‘𝑥) = ((𝐺‘𝑗)‘𝑥))
72		eqid 2731	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))
73		fvex 6835	. . . . . . . 8 ⊢ ((𝐺‘𝑗)‘𝑥) ∈ V
74	71, 72, 73	fvmpt 6929	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥))
75	62, 74	syl 17	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥))
76	5	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝐺:ℕ⟶dom ∫₁)
77	76, 62	ffvelcdmd 7018	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗) ∈ dom ∫₁)
78		i1ff 25605	. . . . . . . 8 ⊢ ((𝐺‘𝑗) ∈ dom ∫₁ → (𝐺‘𝑗):ℝ⟶ℝ)
79	77, 78	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗):ℝ⟶ℝ)
80	8	ad2antrr 726	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ ℝ)
81	79, 80	ffvelcdmd 7018	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) ∈ ℝ)
82	75, 81	eqeltrd 2831	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ∈ ℝ)
83	33	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ∈ ℂ)
84		2nn 12198	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
85		nnexpcl 13981	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 𝑗 ∈ ℕ₀) → (2↑𝑗) ∈ ℕ)
86	84, 65, 85	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℕ)
87	86	nnred 12140	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℝ)
88	87	recnd 11140	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℂ)
89	86	nnne0d 12175	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ≠ 0)
90	83, 88, 89	divcan4d 11903	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) = (𝐹‘𝑥))
91	90	eqcomd 2737	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) = (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)))
92		2cnd 12203	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 2 ∈ ℂ)
93		2ne0 12229	. . . . . . . . . . 11 ⊢ 2 ≠ 0
94	93	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 2 ≠ 0)
95		eluzelz 12742	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑘) → 𝑗 ∈ ℤ)
96	95	adantl 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℤ)
97	92, 94, 96	exprecd 14061	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗)))
98	91, 97	oveq12d 7364	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗))))
99	64, 87	remulcld 11142	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ)
100	99	recnd 11140	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℂ)
101		1cnd 11107	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 1 ∈ ℂ)
102	100, 101, 88, 89	divsubdird 11936	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗))))
103	98, 102	eqtr4d 2769	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)))
104		fllep1 13705	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))
105	99, 104	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))
106		1red 11113	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 1 ∈ ℝ)
107		reflcl 13700	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ)
108	99, 107	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ)
109	99, 106, 108	lesubaddd 11714	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1)))
110	105, 109	mpbird 257	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))))
111		peano2rem 11428	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ)
112	99, 111	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ)
113	86	nngt0d 12174	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 0 < (2↑𝑗))
114		lediv1 11987	. . . . . . . . 9 ⊢ (((((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ ∧ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 < (2↑𝑗))) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))))
115	112, 108, 87, 113, 114	syl112anc 1376	. . . . . . . 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 5113	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
118	1, 2, 3, 4	mbfi1fseqlem2 25645	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)))
119	62, 118	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)))
120	119	fveq1d 6824	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥))
121		ovex 7379	. . . . . . . . . . 11 ⊢ (𝑗𝐽𝑥) ∈ V
122		vex 3440	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
123	121, 122	ifex 4526	. . . . . . . . . 10 ⊢ if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) ∈ V
124		c0ex 11106	. . . . . . . . . 10 ⊢ 0 ∈ V
125	123, 124	ifex 4526	. . . . . . . . 9 ⊢ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V
126		eqid 2731	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
127	126	fvmpt2 6940	. . . . . . . . 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 2770	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
130	10	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ∈ ℝ)
131	15	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ)
132	62	nnred 12140	. . . . . . . . . . . 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 11705	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (0 ≤ (𝐹‘𝑥) ↔ (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))))
137	135, 136	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))
138	60	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ∈ ℕ)
139	138	nnred 12140	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ∈ ℝ)
140		simplrr 777	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
141	131, 139, 140	ltled 11261	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑘)
142		eluzle 12745	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘𝑘) → 𝑘 ≤ 𝑗)
143	142	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ≤ 𝑗)
144	131, 139, 132, 141, 143	letrd 11270	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑗)
145	130, 131, 132, 137, 144	letrd 11270	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ≤ 𝑗)
146	80, 132	absled 15340	. . . . . . . . . . 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 11544	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → -𝑗 ∈ ℝ)
151		elicc2 13311	. . . . . . . . . 10 ⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)))
152	150, 132, 151	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)))
153	80, 148, 149, 152	mpbir3and 1343	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ (-𝑗[,]𝑗))
154	153	iftrued 4483	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) = if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗))
155		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
156	155	fveq2d 6826	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
157		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑗)
158	157	oveq2d 7362	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑗))
159	156, 158	oveq12d 7364	. . . . . . . . . . . . . 14 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑗)))
160	159	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑗))))
161	160, 158	oveq12d 7364	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
162		ovex 7379	. . . . . . . . . . . 12 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ V
163	161, 3, 162	ovmpoa 7501	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
164	62, 80, 163	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
165	108, 86	nndivred 12179	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ ℝ)
166		flle 13703	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))
167	99, 166	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))
168		ledivmul2 12001	. . . . . . . . . . . . 13 ⊢ (((⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 < (2↑𝑗))) → (((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))))
169	108, 64, 87, 113, 168	syl112anc 1376	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))))
170	167, 169	mpbird 257	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥))
171	9	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ ℂ)
172	171	absge0d 15354	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 0 ≤ (abs‘𝑥))
173	64, 130	addge02d 11706	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (0 ≤ (abs‘𝑥) ↔ (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))))
174	172, 173	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))
175	64, 131, 132, 174, 144	letrd 11270	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ≤ 𝑗)
176	165, 64, 132, 170, 175	letrd 11270	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ 𝑗)
177	164, 176	eqbrtrd 5113	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑗𝐽𝑥) ≤ 𝑗)
178	177	iftrued 4483	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = (𝑗𝐽𝑥))
179	178, 164	eqtrd 2766	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
180	129, 154, 179	3eqtrd 2770	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
181	117, 63, 180	3brtr4d 5123	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗))
182	180, 170	eqbrtrd 5113	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ≤ (𝐹‘𝑥))
183	18, 20, 57, 59, 69, 82, 181, 182	climsqz 15548	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
184	17, 183	rexlimddv 3139	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
185	184	ralrimiva 3124	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
186	34	mptex 7157	. . . 4 ⊢ (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ∈ V
187	4, 186	eqeltri 2827	. . 3 ⊢ 𝐺 ∈ V
188		feq1 6629	. . . 4 ⊢ (𝑔 = 𝐺 → (𝑔:ℕ⟶dom ∫₁ ↔ 𝐺:ℕ⟶dom ∫₁))
189		fveq1 6821	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
190	189	breq2d 5103	. . . . . 6 ⊢ (𝑔 = 𝐺 → (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ↔ 0_𝑝 ∘_r ≤ (𝐺‘𝑛)))
191		fveq1 6821	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1)))
192	189, 191	breq12d 5104	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1)) ↔ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
193	190, 192	anbi12d 632	. . . . 5 ⊢ (𝑔 = 𝐺 → ((0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ↔ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1)))))
194	193	ralbidv 3155	. . . 4 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ↔ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1)))))
195	189	fveq1d 6824	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛)‘𝑥) = ((𝐺‘𝑛)‘𝑥))
196	195	mpteq2dv 5185	. . . . . 6 ⊢ (𝑔 = 𝐺 → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)))
197	196	breq1d 5101	. . . . 5 ⊢ (𝑔 = 𝐺 → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
198	197	ralbidv 3155	. . . 4 ⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
199	188, 194, 198	3anbi123d 1438	. . 3 ⊢ (𝑔 = 𝐺 → ((𝑔:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ (𝐺:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
200	187, 199	spcev 3561	. 2 ⊢ ((𝐺:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
201	5, 7, 185, 200	syl3anc 1373	1 ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∃wex 1780 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 Vcvv 3436 ifcif 4475 class class class wbr 5091 ↦ cmpt 5172 dom cdm 5616 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 ∈ cmpo 7348 ∘_r cofr 7609 ℂcc 11004 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 +∞cpnf 11143 < clt 11146 ≤ cle 11147 − cmin 11344 -cneg 11345 / cdiv 11774 ℕcn 12125 2c2 12180 ℕ₀cn0 12381 ℤcz 12468 ℤ_≥cuz 12732 [,)cico 13247 [,]cicc 13248 ⌊cfl 13694 ↑cexp 13968 abscabs 15141 ⇝ cli 15391 MblFncmbf 25543 ∫₁citg1 25544 0_𝑝c0p 25598

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-inf2 9531 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-se 5570 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-ofr 7611 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-er 8622 df-map 8752 df-pm 8753 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-fi 9295 df-sup 9326 df-inf 9327 df-oi 9396 df-dju 9794 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-z 12469 df-uz 12733 df-q 12847 df-rp 12891 df-xneg 13011 df-xadd 13012 df-xmul 13013 df-ioo 13249 df-ico 13251 df-icc 13252 df-fz 13408 df-fzo 13555 df-fl 13696 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-rlim 15396 df-sum 15594 df-rest 17326 df-topgen 17347 df-psmet 21284 df-xmet 21285 df-met 21286 df-bl 21287 df-mopn 21288 df-top 22810 df-topon 22827 df-bases 22862 df-cmp 23303 df-ovol 25393 df-vol 25394 df-mbf 25548 df-itg1 25549 df-0p 25599

This theorem is referenced by: mbfi1fseq 25650

W3C validator