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 26021

Description: Lemma for mbfi1fseq 26022. 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 26019	. 2 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫₁)
6	1, 2, 3, 4	mbfi1fseqlem5 26020	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
7	6	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
8		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
9	8	recnd 11318	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
10	9	abscld 15586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℝ)
11	2	ffvelcdmda 7076	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
12		elrege0 13566	. . . . . . . 8 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
13	11, 12	sylib 221	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
14	13	simpld 500	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
15	10, 14	readdcld 11319	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ)
16		arch 12584	. . . . 5 ⊢ (((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ → ∃𝑘 ∈ ℕ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
17	15, 16	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑘 ∈ ℕ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
18		eqid 2761	. . . . 5 ⊢ (ℤ_≥‘𝑘) = (ℤ_≥‘𝑘)
19		nnz 12695	. . . . . 6 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
20	19	ad2antrl 741	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℤ)
21		nnuz 12985	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
22		1zzd 12708	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℤ)
23		halfcn 12541	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℂ
24	23	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 2) ∈ ℂ)
25		halfre 12540	. . . . . . . . . . . 12 ⊢ (1 / 2) ∈ ℝ
26		halfge0 12543	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 2)
27		absid 15443	. . . . . . . . . . . 12 ⊢ (((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 / 2))
28	25, 26, 27	mp2an 705	. . . . . . . . . . 11 ⊢ (abs‘(1 / 2)) = (1 / 2)
29		halflt1 12544	. . . . . . . . . . 11 ⊢ (1 / 2) < 1
30	28, 29	eqbrtri 5126	. . . . . . . . . 10 ⊢ (abs‘(1 / 2)) < 1
31	30	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘(1 / 2)) < 1)
32	24, 31	expcnv 16013	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛)) ⇝ 0)
33	14	recnd 11318	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
34		nnex 12322	. . . . . . . . . 10 ⊢ ℕ ∈ V
35	34	mptex 7221	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V
36	35	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V)
37		nnnn0 12594	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ₀)
38	37	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ₀)
39		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑗))
40		eqid 2761	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))
41		ovex 7445	. . . . . . . . . . 11 ⊢ ((1 / 2)↑𝑗) ∈ V
42	39, 40, 41	fvmpt 6985	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗))
43	38, 42	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗))
44		expcl 14202	. . . . . . . . . 10 ⊢ (((1 / 2) ∈ ℂ ∧ 𝑗 ∈ ℕ₀) → ((1 / 2)↑𝑗) ∈ ℂ)
45	23, 38, 44	sylancr 599	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((1 / 2)↑𝑗) ∈ ℂ)
46	43, 45	eqeltrd 2861	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) ∈ ℂ)
47	39	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑥) − ((1 / 2)↑𝑛)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
48		eqid 2761	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))
49		ovex 7445	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ V
50	47, 48, 49	fvmpt 6985	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
51	50	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
52	43	oveq2d 7428	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑥) − ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
53	51, 52	eqtr4d 2799	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗)))
54	21, 22, 32, 33, 36, 46, 53	climsubc2 15786	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ ((𝐹‘𝑥) − 0))
55	33	subid1d 11639	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) − 0) = (𝐹‘𝑥))
56	54, 55	breqtrd 5131	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥))
57	56	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥))
58	34	mptex 7221	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V
59	58	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V)
60		simprl 783	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℕ)
61		eluznn 13026	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℕ)
62	60, 61	sylan 592	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℕ)
63	62, 50	syl 18	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
64	14	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ∈ ℝ)
65	62, 37	syl 18	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℕ₀)
66		reexpcl 14201	. . . . . . . 8 ⊢ (((1 / 2) ∈ ℝ ∧ 𝑗 ∈ ℕ₀) → ((1 / 2)↑𝑗) ∈ ℝ)
67	25, 65, 66	sylancr 599	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((1 / 2)↑𝑗) ∈ ℝ)
68	64, 67	resubcld 11725	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ ℝ)
69	63, 68	eqeltrd 2861	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ∈ ℝ)
70		fveq2 6877	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → (𝐺‘𝑛) = (𝐺‘𝑗))
71	70	fveq1d 6879	. . . . . . . 8 ⊢ (𝑛 = 𝑗 → ((𝐺‘𝑛)‘𝑥) = ((𝐺‘𝑗)‘𝑥))
72		eqid 2761	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))
73		fvex 6890	. . . . . . . 8 ⊢ ((𝐺‘𝑗)‘𝑥) ∈ V
74	71, 72, 73	fvmpt 6985	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥))
75	62, 74	syl 18	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥))
76	5	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝐺:ℕ⟶dom ∫₁)
77	76, 62	ffvelcdmd 7077	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗) ∈ dom ∫₁)
78		i1ff 25977	. . . . . . . 8 ⊢ ((𝐺‘𝑗) ∈ dom ∫₁ → (𝐺‘𝑗):ℝ⟶ℝ)
79	77, 78	syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗):ℝ⟶ℝ)
80	8	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ ℝ)
81	79, 80	ffvelcdmd 7077	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) ∈ ℝ)
82	75, 81	eqeltrd 2861	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ∈ ℝ)
83	33	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ∈ ℂ)
84		2nn 12397	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
85		nnexpcl 14197	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 𝑗 ∈ ℕ₀) → (2↑𝑗) ∈ ℕ)
86	84, 65, 85	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℕ)
87	86	nnred 12331	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℝ)
88	87	recnd 11318	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℂ)
89	86	nnne0d 12369	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ≠ 0)
90	83, 88, 89	divcan4d 12080	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) = (𝐹‘𝑥))
91	90	eqcomd 2767	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) = (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)))
92		2cnd 12402	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 2 ∈ ℂ)
93		2ne0 12430	. . . . . . . . . . 11 ⊢ 2 ≠ 0
94	93	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 2 ≠ 0)
95		eluzelz 12956	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑘) → 𝑗 ∈ ℤ)
96	95	adantl 487	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℤ)
97	92, 94, 96	exprecd 14277	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗)))
98	91, 97	oveq12d 7430	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗))))
99	64, 87	remulcld 11320	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ)
100	99	recnd 11318	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℂ)
101		1cnd 11283	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 1 ∈ ℂ)
102	100, 101, 88, 89	divsubdird 12113	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗))))
103	98, 102	eqtr4d 2799	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)))
104		fllep1 13921	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))
105	99, 104	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))
106		1red 11290	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 1 ∈ ℝ)
107		reflcl 13916	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ)
108	99, 107	syl 18	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ)
109	99, 106, 108	lesubaddd 11894	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1)))
110	105, 109	mpbird 260	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))))
111		peano2rem 11606	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ)
112	99, 111	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ)
113	86	nngt0d 12368	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 0 < (2↑𝑗))
114		lediv1 12163	. . . . . . . . 9 ⊢ (((((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ ∧ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 < (2↑𝑗))) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))))
115	112, 108, 87, 113, 114	syl112anc 1401	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))))
116	110, 115	mpbid 235	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
117	103, 116	eqbrtrd 5127	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
118	1, 2, 3, 4	mbfi1fseqlem2 26017	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)))
119	62, 118	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)))
120	119	fveq1d 6879	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥))
121		ovex 7445	. . . . . . . . . . 11 ⊢ (𝑗𝐽𝑥) ∈ V
122		vex 3455	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
123	121, 122	ifex 4533	. . . . . . . . . 10 ⊢ if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) ∈ V
124		c0ex 11281	. . . . . . . . . 10 ⊢ 0 ∈ V
125	123, 124	ifex 4533	. . . . . . . . 9 ⊢ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V
126		eqid 2761	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
127	126	fvmpt2 6997	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
128	80, 125, 127	sylancl 598	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
129	75, 120, 128	3eqtrd 2800	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
130	10	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ∈ ℝ)
131	15	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ)
132	62	nnred 12331	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℝ)
133	11	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ∈ (0[,)+∞))
134	133, 12	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
135	134	simprd 501	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 0 ≤ (𝐹‘𝑥))
136	130, 64	addge01d 11885	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (0 ≤ (𝐹‘𝑥) ↔ (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))))
137	135, 136	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))
138	60	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ∈ ℕ)
139	138	nnred 12331	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ∈ ℝ)
140		simplrr 790	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
141	131, 139, 140	ltled 11439	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑘)
142		eluzle 12959	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘𝑘) → 𝑘 ≤ 𝑗)
143	142	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ≤ 𝑗)
144	131, 139, 132, 141, 143	letrd 11448	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑗)
145	130, 131, 132, 137, 144	letrd 11448	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ≤ 𝑗)
146	80, 132	absled 15580	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) ≤ 𝑗 ↔ (-𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)))
147	145, 146	mpbid 235	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (-𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))
148	147	simpld 500	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → -𝑗 ≤ 𝑥)
149	147	simprd 501	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ≤ 𝑗)
150	132	renegcld 11724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → -𝑗 ∈ ℝ)
151		elicc2 13523	. . . . . . . . . 10 ⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)))
152	150, 132, 151	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)))
153	80, 148, 149, 152	mpbir3and 1361	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ (-𝑗[,]𝑗))
154	153	iftrued 4490	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) = if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗))
155		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
156	155	fveq2d 6881	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
157		simpl 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑗)
158	157	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑗))
159	156, 158	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑗)))
160	159	fveq2d 6881	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑗))))
161	160, 158	oveq12d 7430	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
162		ovex 7445	. . . . . . . . . . . 12 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ V
163	161, 3, 162	ovmpoa 7567	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
164	62, 80, 163	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
165	108, 86	nndivred 12373	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ ℝ)
166		flle 13919	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))
167	99, 166	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))
168		ledivmul2 12177	. . . . . . . . . . . . 13 ⊢ (((⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 < (2↑𝑗))) → (((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))))
169	108, 64, 87, 113, 168	syl112anc 1401	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))))
170	167, 169	mpbird 260	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥))
171	9	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ ℂ)
172	171	absge0d 15594	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 0 ≤ (abs‘𝑥))
173	64, 130	addge02d 11886	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (0 ≤ (abs‘𝑥) ↔ (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))))
174	172, 173	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))
175	64, 131, 132, 174, 144	letrd 11448	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ≤ 𝑗)
176	165, 64, 132, 170, 175	letrd 11448	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ 𝑗)
177	164, 176	eqbrtrd 5127	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑗𝐽𝑥) ≤ 𝑗)
178	177	iftrued 4490	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = (𝑗𝐽𝑥))
179	178, 164	eqtrd 2796	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
180	129, 154, 179	3eqtrd 2800	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
181	117, 63, 180	3brtr4d 5137	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗))
182	180, 170	eqbrtrd 5127	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ≤ (𝐹‘𝑥))
183	18, 20, 57, 59, 69, 82, 181, 182	climsqz 15788	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
184	17, 183	rexlimddv 3170	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
185	184	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
186	34	mptex 7221	. . . 4 ⊢ (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ∈ V
187	4, 186	eqeltri 2857	. . 3 ⊢ 𝐺 ∈ V
188		feq1 6679	. . . 4 ⊢ (𝑔 = 𝐺 → (𝑔:ℕ⟶dom ∫₁ ↔ 𝐺:ℕ⟶dom ∫₁))
189		fveq1 6876	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
190	189	breq2d 5115	. . . . . 6 ⊢ (𝑔 = 𝐺 → (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ↔ 0_𝑝 ∘_r ≤ (𝐺‘𝑛)))
191		fveq1 6876	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1)))
192	189, 191	breq12d 5116	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1)) ↔ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
193	190, 192	anbi12d 644	. . . . 5 ⊢ (𝑔 = 𝐺 → ((0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ↔ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1)))))
194	193	ralbidv 3186	. . . 4 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ↔ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1)))))
195	189	fveq1d 6879	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛)‘𝑥) = ((𝐺‘𝑛)‘𝑥))
196	195	mpteq2dv 5199	. . . . . 6 ⊢ (𝑔 = 𝐺 → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)))
197	196	breq1d 5113	. . . . 5 ⊢ (𝑔 = 𝐺 → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
198	197	ralbidv 3186	. . . 4 ⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
199	188, 194, 198	3anbi123d 1464	. . 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 1398	1 ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 Vcvv 3451 ifcif 4482 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5651 ⟶wf 6527 ‘cfv 6531 (class class class)co 7412 ∈ cmpo 7414 ∘_r cofr 7681 ℂcc 11179 ℝcr 11180 0cc0 11181 1c1 11182 + caddc 11184 · cmul 11186 +∞cpnf 11321 < clt 11324 ≤ cle 11325 − cmin 11522 -cneg 11523 / cdiv 11954 ℕcn 12316 2c2 12378 ℕ₀cn0 12587 ℤcz 12674 ℤ_≥cuz 12946 [,)cico 13459 [,]cicc 13460 ⌊cfl 13910 ↑cexp 14184 abscabs 15381 ⇝ cli 15631 MblFncmbf 25915 ∫₁citg1 25916 0_𝑝c0p 25970

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-inf2 9626 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7682 df-ofr 7683 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-2o 8461 df-er 8701 df-map 8833 df-pm 8834 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fi 9387 df-sup 9418 df-inf 9419 df-oi 9488 df-dju 9963 df-card 10001 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-n0 12588 df-z 12675 df-uz 12947 df-q 13057 df-rp 13102 df-xneg 13222 df-xadd 13223 df-xmul 13224 df-ioo 13461 df-ico 13463 df-icc 13464 df-fz 13621 df-fzo 13769 df-fl 13912 df-seq 14125 df-exp 14185 df-hash 14455 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-clim 15635 df-rlim 15636 df-sum 15834 df-rest 17573 df-topgen 17594 df-psmet 21650 df-xmet 21651 df-met 21652 df-bl 21653 df-mopn 21654 df-top 23192 df-topon 23209 df-bases 23244 df-cmp 23685 df-ovol 25765 df-vol 25766 df-mbf 25920 df-itg1 25921 df-0p 25971

This theorem is used by: mbfi1fseq 26022

W3C validator