Theorem mbfi1flimlem 25710

Description: Lemma for mbfi1flim 25711. (Contributed by Mario Carneiro, 5-Sep-2014.)

Hypotheses

Ref	Expression
mbfi1flim.1	⊢ (𝜑 → 𝐹 ∈ MblFn)
mbfi1flimlem.2	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)

Assertion

Ref	Expression
mbfi1flimlem	⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

Distinct variable groups:   𝑔,𝑛,𝑥,𝐹   𝜑,𝑔,𝑛,𝑥

Proof of Theorem mbfi1flimlem

Dummy variables 𝑦 𝑓 ℎ 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbfi1flimlem.2	. . . . 5 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
2	1	ffvelcdmda 7028	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ)
3	1	feqmptd 6898	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)))
4		mbfi1flim.1	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ MblFn)
5	3, 4	eqeltrrd 2842	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn)
6	2, 5	mbfpos 25639	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) ∈ MblFn)
7		0re 11142	. . . . . 6 ⊢ 0 ∈ ℝ
8		ifcl 4502	. . . . . 6 ⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ)
9	2, 7, 8	sylancl 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ)
10		max1 13132	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ (𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
11	7, 2, 10	sylancr 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
12		elrege0 13402	. . . . 5 ⊢ (if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)))
13	9, 11, 12	sylanbrc 590	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞))
14	13	fmpttd 7059	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)):ℝ⟶(0[,)+∞))
15	6, 14	mbfi1fseq 25709	. 2 ⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)))
16	2	renegcld 11573	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -(𝐹‘𝑦) ∈ ℝ)
17	2, 5	mbfneg 25638	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ -(𝐹‘𝑦)) ∈ MblFn)
18	16, 17	mbfpos 25639	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) ∈ MblFn)
19		ifcl 4502	. . . . . 6 ⊢ ((-(𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ)
20	16, 7, 19	sylancl 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ)
21		max1 13132	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ -(𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
22	7, 16, 21	sylancr 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
23		elrege0 13402	. . . . 5 ⊢ (if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)))
24	20, 22, 23	sylanbrc 590	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞))
25	24	fmpttd 7059	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)):ℝ⟶(0[,)+∞))
26	18, 25	mbfi1fseq 25709	. 2 ⊢ (𝜑 → ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
27		exdistrv 1963	. . 3 ⊢ (∃𝑓∃ℎ((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) ↔ (∃𝑓(𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))))
28		3simpb 1156	. . . . . . 7 ⊢ ((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) → (𝑓:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)))
29		3simpb 1156	. . . . . . 7 ⊢ ((ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
30	28, 29	anim12i 620	. . . . . 6 ⊢ (((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))))
31		an4 663	. . . . . 6 ⊢ (((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) ↔ ((𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1) ∧ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))))
32	30, 31	sylib 220	. . . . 5 ⊢ (((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ((𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1) ∧ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))))
33		r19.26 3101	. . . . . . 7 ⊢ (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
34		i1fsub 25696	. . . . . . . . . 10 ⊢ ((𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1) → (𝑥 ∘f − 𝑦) ∈ dom ∫1)
35	34	adantl 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ (𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1)) → (𝑥 ∘f − 𝑦) ∈ dom ∫1)
36		simprl 777	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝑓:ℕ⟶dom ∫1)
37		simprr 779	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℎ:ℕ⟶dom ∫1)
38		nnex 12175	. . . . . . . . . 10 ⊢ ℕ ∈ V
39	38	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℕ ∈ V)
40		inidm 4157	. . . . . . . . 9 ⊢ (ℕ ∩ ℕ) = ℕ
41	35, 36, 37, 39, 39, 40	off 7641	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1)
42		fveq2 6830	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
43	42	breq2d 5086	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (0 ≤ (𝐹‘𝑦) ↔ 0 ≤ (𝐹‘𝑥)))
44	43, 42	ifbieq1d 4481	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
45		eqid 2741	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
46		fvex 6843	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑥) ∈ V
47		c0ex 11134	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
48	46, 47	ifex 4507	. . . . . . . . . . . . . 14 ⊢ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V
49	44, 45, 48	fvmpt 6938	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
50	49	breq2d 5086	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))
51	42	negeqd 11383	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → -(𝐹‘𝑦) = -(𝐹‘𝑥))
52	51	breq2d 5086	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (0 ≤ -(𝐹‘𝑦) ↔ 0 ≤ -(𝐹‘𝑥)))
53	52, 51	ifbieq1d 4481	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
54		eqid 2741	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
55		negex 11387	. . . . . . . . . . . . . . 15 ⊢ -(𝐹‘𝑥) ∈ V
56	55, 47	ifex 4507	. . . . . . . . . . . . . 14 ⊢ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V
57	53, 54, 56	fvmpt 6938	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
58	57	breq2d 5086	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))
59	50, 58	anbi12d 639	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))
60	59	adantl 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))
61		nnuz 12822	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ≥‘1)
62		1zzd 12553	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → 1 ∈ ℤ)
63		simprl 777	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
64	38	mptex 7170	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ∈ V
65	64	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ∈ V)
66		simprr 779	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
67	36	ffvelcdmda 7028	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ dom ∫1)
68		i1ff 25664	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑛) ∈ dom ∫1 → (𝑓‘𝑛):ℝ⟶ℝ)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛):ℝ⟶ℝ)
70	69	ffvelcdmda 7028	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ)
71	70	an32s 659	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ)
72	71	recnd 11169	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℂ)
73	72	fmpttd 7059	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ)
74	73	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ)
75	74	ffvelcdmda 7028	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) ∈ ℂ)
76	37	ffvelcdmda 7028	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (ℎ‘𝑛) ∈ dom ∫1)
77		i1ff 25664	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑛) ∈ dom ∫1 → (ℎ‘𝑛):ℝ⟶ℝ)
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (ℎ‘𝑛):ℝ⟶ℝ)
79	78	ffvelcdmda 7028	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ)
80	79	an32s 659	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ)
81	80	recnd 11169	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℂ)
82	81	fmpttd 7059	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ)
83	82	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ)
84	83	ffvelcdmda 7028	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) ∈ ℂ)
85	36	ffnd 6659	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝑓 Fn ℕ)
86	37	ffnd 6659	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℎ Fn ℕ)
87		eqidd 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) = (𝑓‘𝑘))
88		eqidd 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) = (ℎ‘𝑘))
89	85, 86, 39, 39, 40, 87, 88	ofval 7634	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → ((𝑓 ∘f ∘f − ℎ)‘𝑘) = ((𝑓‘𝑘) ∘f − (ℎ‘𝑘)))
90	89	fveq1d 6832	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥))
91	90	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥))
92	36	ffvelcdmda 7028	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ dom ∫1)
93		i1ff 25664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘) ∈ dom ∫1 → (𝑓‘𝑘):ℝ⟶ℝ)
94		ffn 6658	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘):ℝ⟶ℝ → (𝑓‘𝑘) Fn ℝ)
95	92, 93, 94	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) Fn ℝ)
96	37	ffvelcdmda 7028	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) ∈ dom ∫1)
97		i1ff 25664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘) ∈ dom ∫1 → (ℎ‘𝑘):ℝ⟶ℝ)
98		ffn 6658	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘):ℝ⟶ℝ → (ℎ‘𝑘) Fn ℝ)
99	96, 97, 98	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) Fn ℝ)
100		reex 11125	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ∈ V
101	100	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → ℝ ∈ V)
102		inidm 4157	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ ∩ ℝ) = ℝ
103		eqidd 2742	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑓‘𝑘)‘𝑥) = ((𝑓‘𝑘)‘𝑥))
104		eqidd 2742	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((ℎ‘𝑘)‘𝑥) = ((ℎ‘𝑘)‘𝑥))
105	95, 99, 101, 101, 102, 103, 104	ofval 7634	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
106	91, 105	eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
107	106	an32s 659	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
108		fveq2 6830	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝑓 ∘f ∘f − ℎ)‘𝑛) = ((𝑓 ∘f ∘f − ℎ)‘𝑘))
109	108	fveq1d 6832	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
110		eqid 2741	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))
111		fvex 6843	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) ∈ V
112	109, 110, 111	fvmpt 6938	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
113	112	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
114		fveq2 6830	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘))
115	114	fveq1d 6832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛)‘𝑥) = ((𝑓‘𝑘)‘𝑥))
116		eqid 2741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))
117		fvex 6843	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓‘𝑘)‘𝑥) ∈ V
118	115, 116, 117	fvmpt 6938	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) = ((𝑓‘𝑘)‘𝑥))
119		fveq2 6830	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (ℎ‘𝑛) = (ℎ‘𝑘))
120	119	fveq1d 6832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((ℎ‘𝑛)‘𝑥) = ((ℎ‘𝑘)‘𝑥))
121		eqid 2741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))
122		fvex 6843	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑘)‘𝑥) ∈ V
123	120, 121, 122	fvmpt 6938	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) = ((ℎ‘𝑘)‘𝑥))
124	118, 123	oveq12d 7377	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
125	124	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
126	107, 113, 125	3eqtr4d 2786	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)))
127	126	adantlr 722	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)))
128	61, 62, 63, 65, 66, 75, 84, 127	climsub 15591	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))
129	1	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝐹:ℝ⟶ℝ)
130	129	ffvelcdmda 7028	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
131		max0sub 13143	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) ∈ ℝ → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥))
132	130, 131	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥))
133	132	adantr 482	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥))
134	128, 133	breqtrd 5100	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
135	134	ex 414	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
136	60, 135	sylbid 242	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
137	136	ralimdva 3153	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
138		ovex 7392	. . . . . . . . 9 ⊢ (𝑓 ∘f ∘f − ℎ) ∈ V
139		feq1 6636	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑔:ℕ⟶dom ∫1 ↔ (𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1))
140		fveq1 6829	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑔‘𝑛) = ((𝑓 ∘f ∘f − ℎ)‘𝑛))
141	140	fveq1d 6832	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑔‘𝑛)‘𝑥) = (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))
142	141	mpteq2dv 5168	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)))
143	142	breq1d 5084	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
144	143	ralbidv 3164	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
145	139, 144	anbi12d 639	. . . . . . . . 9 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ ((𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
146	138, 145	spcev 3545	. . . . . . . 8 ⊢ (((𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
147	41, 137, 146	syl6an 691	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
148	33, 147	biimtrrid 245	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ((∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
149	148	expimpd 455	. . . . 5 ⊢ (𝜑 → (((𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1) ∧ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
150	32, 149	syl5 34	. . . 4 ⊢ (𝜑 → (((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
151	150	exlimdvv 1942	. . 3 ⊢ (𝜑 → (∃𝑓∃ℎ((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
152	27, 151	biimtrrid 245	. 2 ⊢ (𝜑 → ((∃𝑓(𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
153	15, 26, 152	mp2and 706	1 ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   ∧ w3a 1093   = wceq 1548  ∃wex 1787   ∈ wcel 2121  ∀wral 3055  Vcvv 3433  ifcif 4456   class class class wbr 5074   ↦ cmpt 5155  dom cdm 5620   Fn wfn 6483  ⟶wf 6484  ‘cfv 6488  (class class class)co 7359   ∘_f cof 7621   ∘_r cofr 7622  ℂcc 11032  ℝcr 11033  0cc0 11034  1c1 11035   + caddc 11037  +∞cpnf 11172   ≤ cle 11176   − cmin 11373  -cneg 11374  ℕcn 12169  [,)cico 13295   ⇝ cli 15441  MblFncmbf 25602  ∫₁citg1 25603  0_𝑝c0p 25657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7681  ax-inf2 9557  ax-cnex 11090  ax-resscn 11091  ax-1cn 11092  ax-icn 11093  ax-addcl 11094  ax-addrcl 11095  ax-mulcl 11096  ax-mulrcl 11097  ax-mulcom 11098  ax-addass 11099  ax-mulass 11100  ax-distr 11101  ax-i2m1 11102  ax-1ne0 11103  ax-1rid 11104  ax-rnegex 11105  ax-rrecex 11106  ax-cnre 11107  ax-pre-lttri 11108  ax-pre-lttrn 11109  ax-pre-ltadd 11110  ax-pre-mulgt0 11111  ax-pre-sup 11112

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3725  df-csb 3833  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3904  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-int 4880  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-se 5574  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-isom 6497  df-riota 7316  df-ov 7362  df-oprab 7363  df-mpo 7364  df-of 7623  df-ofr 7624  df-om 7810  df-1st 7933  df-2nd 7934  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8343  df-1o 8399  df-2o 8400  df-er 8637  df-map 8769  df-pm 8770  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fi 9318  df-sup 9349  df-inf 9350  df-oi 9419  df-dju 9820  df-card 9858  df-pnf 11177  df-mnf 11178  df-xr 11179  df-ltxr 11180  df-le 11181  df-sub 11375  df-neg 11376  df-div 11804  df-nn 12170  df-2 12239  df-3 12240  df-n0 12433  df-z 12520  df-uz 12784  df-q 12894  df-rp 12938  df-xneg 13058  df-xadd 13059  df-xmul 13060  df-ioo 13297  df-ico 13299  df-icc 13300  df-fz 13457  df-fzo 13604  df-fl 13746  df-seq 13959  df-exp 14019  df-hash 14288  df-cj 15056  df-re 15057  df-im 15058  df-sqrt 15192  df-abs 15193  df-clim 15445  df-rlim 15446  df-sum 15644  df-rest 17380  df-topgen 17401  df-psmet 21342  df-xmet 21343  df-met 21344  df-bl 21345  df-mopn 21346  df-top 22880  df-topon 22897  df-bases 22932  df-cmp 23373  df-ovol 25452  df-vol 25453  df-mbf 25607  df-itg1 25608  df-0p 25658

This theorem is referenced by:  mbfi1flim  25711