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 25916

Description: Lemma for mbfi1fseq 25917. 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 25914	. 2 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫₁)
6	1, 2, 3, 4	mbfi1fseqlem5 25915	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
7	6	ralrimiva 3160	. 2 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
8		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
9	8	recnd 11255	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
10	9	abscld 15516	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℝ)
11	2	ffvelcdmda 7086	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
12		elrege0 13499	. . . . . . . 8 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
13	11, 12	sylib 221	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
14	13	simpld 500	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
15	10, 14	readdcld 11256	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ)
16		arch 12519	. . . . 5 ⊢ (((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ → ∃𝑘 ∈ ℕ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
17	15, 16	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑘 ∈ ℕ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
18		eqid 2766	. . . . 5 ⊢ (ℤ_≥‘𝑘) = (ℤ_≥‘𝑘)
19		nnz 12630	. . . . . 6 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
20	19	ad2antrl 741	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℤ)
21		nnuz 12919	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
22		1zzd 12643	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℤ)
23		halfcn 12476	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℂ
24	23	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 2) ∈ ℂ)
25		halfre 12475	. . . . . . . . . . . 12 ⊢ (1 / 2) ∈ ℝ
26		halfge0 12478	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 2)
27		absid 15373	. . . . . . . . . . . 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 12479	. . . . . . . . . . 11 ⊢ (1 / 2) < 1
30	28, 29	eqbrtri 5137	. . . . . . . . . 10 ⊢ (abs‘(1 / 2)) < 1
31	30	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘(1 / 2)) < 1)
32	24, 31	expcnv 15944	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛)) ⇝ 0)
33	14	recnd 11255	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
34		nnex 12257	. . . . . . . . . 10 ⊢ ℕ ∈ V
35	34	mptex 7228	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V
36	35	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V)
37		nnnn0 12529	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ₀)
38	37	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ₀)
39		oveq2 7431	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑗))
40		eqid 2766	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))
41		ovex 7456	. . . . . . . . . . 11 ⊢ ((1 / 2)↑𝑗) ∈ V
42	39, 40, 41	fvmpt 6996	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗))
43	38, 42	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗))
44		expcl 14135	. . . . . . . . . 10 ⊢ (((1 / 2) ∈ ℂ ∧ 𝑗 ∈ ℕ₀) → ((1 / 2)↑𝑗) ∈ ℂ)
45	23, 38, 44	sylancr 599	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((1 / 2)↑𝑗) ∈ ℂ)
46	43, 45	eqeltrd 2866	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗) ∈ ℂ)
47	39	oveq2d 7439	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → ((𝐹‘𝑥) − ((1 / 2)↑𝑛)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
48		eqid 2766	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))
49		ovex 7456	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ V
50	47, 48, 49	fvmpt 6996	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
51	50	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
52	43	oveq2d 7439	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑥) − ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗)))
53	51, 52	eqtr4d 2804	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((𝑛 ∈ ℕ₀ ↦ ((1 / 2)↑𝑛))‘𝑗)))
54	21, 22, 32, 33, 36, 46, 53	climsubc2 15716	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ ((𝐹‘𝑥) − 0))
55	33	subid1d 11576	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) − 0) = (𝐹‘𝑥))
56	54, 55	breqtrd 5142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥))
57	56	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥))
58	34	mptex 7228	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V
59	58	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V)
60		simprl 783	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℕ)
61		eluznn 12960	. . . . . . . 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 14134	. . . . . . . 8 ⊢ (((1 / 2) ∈ ℝ ∧ 𝑗 ∈ ℕ₀) → ((1 / 2)↑𝑗) ∈ ℝ)
67	25, 65, 66	sylancr 599	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((1 / 2)↑𝑗) ∈ ℝ)
68	64, 67	resubcld 11660	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ ℝ)
69	63, 68	eqeltrd 2866	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ∈ ℝ)
70		fveq2 6888	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → (𝐺‘𝑛) = (𝐺‘𝑗))
71	70	fveq1d 6890	. . . . . . . 8 ⊢ (𝑛 = 𝑗 → ((𝐺‘𝑛)‘𝑥) = ((𝐺‘𝑗)‘𝑥))
72		eqid 2766	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))
73		fvex 6901	. . . . . . . 8 ⊢ ((𝐺‘𝑗)‘𝑥) ∈ V
74	71, 72, 73	fvmpt 6996	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥))
75	62, 74	syl 18	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥))
76	5	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝐺:ℕ⟶dom ∫₁)
77	76, 62	ffvelcdmd 7087	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗) ∈ dom ∫₁)
78		i1ff 25872	. . . . . . . 8 ⊢ ((𝐺‘𝑗) ∈ dom ∫₁ → (𝐺‘𝑗):ℝ⟶ℝ)
79	77, 78	syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗):ℝ⟶ℝ)
80	8	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ ℝ)
81	79, 80	ffvelcdmd 7087	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) ∈ ℝ)
82	75, 81	eqeltrd 2866	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ∈ ℝ)
83	33	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ∈ ℂ)
84		2nn 12332	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
85		nnexpcl 14130	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 𝑗 ∈ ℕ₀) → (2↑𝑗) ∈ ℕ)
86	84, 65, 85	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℕ)
87	86	nnred 12266	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℝ)
88	87	recnd 11255	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ∈ ℂ)
89	86	nnne0d 12304	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (2↑𝑗) ≠ 0)
90	83, 88, 89	divcan4d 12015	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) = (𝐹‘𝑥))
91	90	eqcomd 2772	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) = (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)))
92		2cnd 12337	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 2 ∈ ℂ)
93		2ne0 12365	. . . . . . . . . . 11 ⊢ 2 ≠ 0
94	93	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 2 ≠ 0)
95		eluzelz 12890	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑘) → 𝑗 ∈ ℤ)
96	95	adantl 487	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑗 ∈ ℤ)
97	92, 94, 96	exprecd 14210	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗)))
98	91, 97	oveq12d 7441	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗))))
99	64, 87	remulcld 11257	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ)
100	99	recnd 11255	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℂ)
101		1cnd 11220	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 1 ∈ ℂ)
102	100, 101, 88, 89	divsubdird 12048	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗))))
103	98, 102	eqtr4d 2804	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)))
104		fllep1 13854	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))
105	99, 104	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))
106		1red 11227	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 1 ∈ ℝ)
107		reflcl 13849	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ)
108	99, 107	syl 18	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ)
109	99, 106, 108	lesubaddd 11829	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1)))
110	105, 109	mpbird 260	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))))
111		peano2rem 11543	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ)
112	99, 111	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ)
113	86	nngt0d 12303	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 0 < (2↑𝑗))
114		lediv1 12098	. . . . . . . . 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 5138	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
118	1, 2, 3, 4	mbfi1fseqlem2 25912	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)))
119	62, 118	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)))
120	119	fveq1d 6890	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥))
121		ovex 7456	. . . . . . . . . . 11 ⊢ (𝑗𝐽𝑥) ∈ V
122		vex 3462	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
123	121, 122	ifex 4543	. . . . . . . . . 10 ⊢ if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) ∈ V
124		c0ex 11218	. . . . . . . . . 10 ⊢ 0 ∈ V
125	123, 124	ifex 4543	. . . . . . . . 9 ⊢ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V
126		eqid 2766	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
127	126	fvmpt2 7008	. . . . . . . . 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 2805	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
130	10	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ∈ ℝ)
131	15	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ)
132	62	nnred 12266	. . . . . . . . . . . 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 11820	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (0 ≤ (𝐹‘𝑥) ↔ (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))))
137	135, 136	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))
138	60	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ∈ ℕ)
139	138	nnred 12266	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ∈ ℝ)
140		simplrr 790	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)
141	131, 139, 140	ltled 11376	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑘)
142		eluzle 12893	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘𝑘) → 𝑘 ≤ 𝑗)
143	142	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑘 ≤ 𝑗)
144	131, 139, 132, 141, 143	letrd 11385	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑗)
145	130, 131, 132, 137, 144	letrd 11385	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (abs‘𝑥) ≤ 𝑗)
146	80, 132	absled 15510	. . . . . . . . . . 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 11659	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → -𝑗 ∈ ℝ)
151		elicc2 13456	. . . . . . . . . 10 ⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)))
152	150, 132, 151	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)))
153	80, 148, 149, 152	mpbir3and 1361	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 𝑥 ∈ (-𝑗[,]𝑗))
154	153	iftrued 4500	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) = if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗))
155		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
156	155	fveq2d 6892	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
157		simpl 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑗)
158	157	oveq2d 7439	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑗))
159	156, 158	oveq12d 7441	. . . . . . . . . . . . . 14 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑗)))
160	159	fveq2d 6892	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑗))))
161	160, 158	oveq12d 7441	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
162		ovex 7456	. . . . . . . . . . . 12 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ V
163	161, 3, 162	ovmpoa 7578	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
164	62, 80, 163	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
165	108, 86	nndivred 12308	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ ℝ)
166		flle 13852	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))
167	99, 166	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))
168		ledivmul2 12112	. . . . . . . . . . . . 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 15524	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → 0 ≤ (abs‘𝑥))
173	64, 130	addge02d 11821	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (0 ≤ (abs‘𝑥) ↔ (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))))
174	172, 173	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))
175	64, 131, 132, 174, 144	letrd 11385	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝐹‘𝑥) ≤ 𝑗)
176	165, 64, 132, 170, 175	letrd 11385	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ 𝑗)
177	164, 176	eqbrtrd 5138	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → (𝑗𝐽𝑥) ≤ 𝑗)
178	177	iftrued 4500	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = (𝑗𝐽𝑥))
179	178, 164	eqtrd 2801	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
180	129, 154, 179	3eqtrd 2805	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))
181	117, 63, 180	3brtr4d 5148	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗))
182	180, 170	eqbrtrd 5138	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ_≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ≤ (𝐹‘𝑥))
183	18, 20, 57, 59, 69, 82, 181, 182	climsqz 15718	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
184	17, 183	rexlimddv 3175	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
185	184	ralrimiva 3160	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
186	34	mptex 7228	. . . 4 ⊢ (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ∈ V
187	4, 186	eqeltri 2862	. . 3 ⊢ 𝐺 ∈ V
188		feq1 6690	. . . 4 ⊢ (𝑔 = 𝐺 → (𝑔:ℕ⟶dom ∫₁ ↔ 𝐺:ℕ⟶dom ∫₁))
189		fveq1 6887	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
190	189	breq2d 5126	. . . . . 6 ⊢ (𝑔 = 𝐺 → (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ↔ 0_𝑝 ∘_r ≤ (𝐺‘𝑛)))
191		fveq1 6887	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1)))
192	189, 191	breq12d 5127	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1)) ↔ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))))
193	190, 192	anbi12d 644	. . . . 5 ⊢ (𝑔 = 𝐺 → ((0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ↔ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1)))))
194	193	ralbidv 3191	. . . 4 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ↔ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1)))))
195	189	fveq1d 6890	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛)‘𝑥) = ((𝐺‘𝑛)‘𝑥))
196	195	mpteq2dv 5210	. . . . . 6 ⊢ (𝑔 = 𝐺 → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)))
197	196	breq1d 5124	. . . . 5 ⊢ (𝑔 = 𝐺 → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
198	197	ralbidv 3191	. . . 4 ⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
199	188, 194, 198	3anbi123d 1464	. . 3 ⊢ (𝑔 = 𝐺 → ((𝑔:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘_r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ (𝐺:ℕ⟶dom ∫₁ ∧ ∀𝑛 ∈ ℕ (0_𝑝 ∘_r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘_r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
200	187, 199	spcev 3568	. 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 2146 ≠ wne 2961 ∀wral 3082 ∃wrex 3092 Vcvv 3458 ifcif 4492 class class class wbr 5114 ↦ cmpt 5197 dom cdm 5666 ⟶wf 6539 ‘cfv 6543 (class class class)co 7423 ∈ cmpo 7425 ∘_r cofr 7686 ℂcc 11116 ℝcr 11117 0cc0 11118 1c1 11119 + caddc 11121 · cmul 11123 +∞cpnf 11258 < clt 11261 ≤ cle 11262 − cmin 11459 -cneg 11460 / cdiv 11889 ℕcn 12251 2c2 12313 ℕ₀cn0 12522 ℤcz 12609 ℤ_≥cuz 12880 [,)cico 13392 [,]cicc 13393 ⌊cfl 13843 ↑cexp 14117 abscabs 15311 ⇝ cli 15561 MblFncmbf 25810 ∫₁citg1 25811 0_𝑝c0p 25865

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-inf2 9620 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-se 5620 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-of 7687 df-ofr 7688 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-er 8703 df-map 8835 df-pm 8836 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-fi 9381 df-sup 9412 df-inf 9413 df-oi 9482 df-dju 9906 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-n0 12523 df-z 12610 df-uz 12881 df-q 12991 df-rp 13035 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13394 df-ico 13396 df-icc 13397 df-fz 13554 df-fzo 13702 df-fl 13845 df-seq 14058 df-exp 14118 df-hash 14387 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-clim 15565 df-rlim 15566 df-sum 15764 df-rest 17500 df-topgen 17521 df-psmet 21551 df-xmet 21552 df-met 21553 df-bl 21554 df-mopn 21555 df-top 23088 df-topon 23105 df-bases 23140 df-cmp 23581 df-ovol 25660 df-vol 25661 df-mbf 25815 df-itg1 25816 df-0p 25866

This theorem is used by: mbfi1fseq 25917

W3C validator