Theorem mbfi1flimlem 25707

Description: Lemma for mbfi1flim 25708. (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 7025	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ)
3	1	feqmptd 6895	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)))
4		mbfi1flim.1	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ MblFn)
5	3, 4	eqeltrrd 2840	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn)
6	2, 5	mbfpos 25636	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) ∈ MblFn)
7		0re 11137	. . . . . 6 ⊢ 0 ∈ ℝ
8		ifcl 4500	. . . . . 6 ⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ)
9	2, 7, 8	sylancl 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ)
10		max1 13128	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ (𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
11	7, 2, 10	sylancr 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
12		elrege0 13398	. . . . 5 ⊢ (if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)))
13	9, 11, 12	sylanbrc 589	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞))
14	13	fmpttd 7056	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)):ℝ⟶(0[,)+∞))
15	6, 14	mbfi1fseq 25706	. 2 ⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)))
16	2	renegcld 11568	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -(𝐹‘𝑦) ∈ ℝ)
17	2, 5	mbfneg 25635	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ -(𝐹‘𝑦)) ∈ MblFn)
18	16, 17	mbfpos 25636	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) ∈ MblFn)
19		ifcl 4500	. . . . . 6 ⊢ ((-(𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ)
20	16, 7, 19	sylancl 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ)
21		max1 13128	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ -(𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
22	7, 16, 21	sylancr 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
23		elrege0 13398	. . . . 5 ⊢ (if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)))
24	20, 22, 23	sylanbrc 589	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞))
25	24	fmpttd 7056	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)):ℝ⟶(0[,)+∞))
26	18, 25	mbfi1fseq 25706	. 2 ⊢ (𝜑 → ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
27		exdistrv 1962	. . 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 1155	. . . . . . 7 ⊢ ((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) → (𝑓:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)))
29		3simpb 1155	. . . . . . 7 ⊢ ((ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
30	28, 29	anim12i 619	. . . . . 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 662	. . . . . 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 219	. . . . 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 3099	. . . . . . 7 ⊢ (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
34		i1fsub 25693	. . . . . . . . . 10 ⊢ ((𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1) → (𝑥 ∘f − 𝑦) ∈ dom ∫1)
35	34	adantl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ (𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1)) → (𝑥 ∘f − 𝑦) ∈ dom ∫1)
36		simprl 776	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝑓:ℕ⟶dom ∫1)
37		simprr 778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℎ:ℕ⟶dom ∫1)
38		nnex 12171	. . . . . . . . . 10 ⊢ ℕ ∈ V
39	38	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℕ ∈ V)
40		inidm 4155	. . . . . . . . 9 ⊢ (ℕ ∩ ℕ) = ℕ
41	35, 36, 37, 39, 39, 40	off 7638	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1)
42		fveq2 6827	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
43	42	breq2d 5084	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (0 ≤ (𝐹‘𝑦) ↔ 0 ≤ (𝐹‘𝑥)))
44	43, 42	ifbieq1d 4479	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
45		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
46		fvex 6840	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑥) ∈ V
47		c0ex 11129	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
48	46, 47	ifex 4505	. . . . . . . . . . . . . 14 ⊢ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V
49	44, 45, 48	fvmpt 6935	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
50	49	breq2d 5084	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))
51	42	negeqd 11378	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → -(𝐹‘𝑦) = -(𝐹‘𝑥))
52	51	breq2d 5084	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (0 ≤ -(𝐹‘𝑦) ↔ 0 ≤ -(𝐹‘𝑥)))
53	52, 51	ifbieq1d 4479	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
54		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
55		negex 11382	. . . . . . . . . . . . . . 15 ⊢ -(𝐹‘𝑥) ∈ V
56	55, 47	ifex 4505	. . . . . . . . . . . . . 14 ⊢ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V
57	53, 54, 56	fvmpt 6935	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
58	57	breq2d 5084	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))
59	50, 58	anbi12d 638	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))
60	59	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))
61		nnuz 12818	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ≥‘1)
62		1zzd 12549	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → 1 ∈ ℤ)
63		simprl 776	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
64	38	mptex 7167	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ∈ V
65	64	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ∈ V)
66		simprr 778	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
67	36	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ dom ∫1)
68		i1ff 25661	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑛) ∈ dom ∫1 → (𝑓‘𝑛):ℝ⟶ℝ)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛):ℝ⟶ℝ)
70	69	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ)
71	70	an32s 658	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ)
72	71	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℂ)
73	72	fmpttd 7056	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ)
74	73	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ)
75	74	ffvelcdmda 7025	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) ∈ ℂ)
76	37	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (ℎ‘𝑛) ∈ dom ∫1)
77		i1ff 25661	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑛) ∈ dom ∫1 → (ℎ‘𝑛):ℝ⟶ℝ)
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (ℎ‘𝑛):ℝ⟶ℝ)
79	78	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ)
80	79	an32s 658	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ)
81	80	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℂ)
82	81	fmpttd 7056	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ)
83	82	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ)
84	83	ffvelcdmda 7025	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) ∈ ℂ)
85	36	ffnd 6656	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝑓 Fn ℕ)
86	37	ffnd 6656	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℎ Fn ℕ)
87		eqidd 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) = (𝑓‘𝑘))
88		eqidd 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) = (ℎ‘𝑘))
89	85, 86, 39, 39, 40, 87, 88	ofval 7631	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → ((𝑓 ∘f ∘f − ℎ)‘𝑘) = ((𝑓‘𝑘) ∘f − (ℎ‘𝑘)))
90	89	fveq1d 6829	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥))
91	90	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥))
92	36	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ dom ∫1)
93		i1ff 25661	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘) ∈ dom ∫1 → (𝑓‘𝑘):ℝ⟶ℝ)
94		ffn 6655	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘):ℝ⟶ℝ → (𝑓‘𝑘) Fn ℝ)
95	92, 93, 94	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) Fn ℝ)
96	37	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) ∈ dom ∫1)
97		i1ff 25661	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘) ∈ dom ∫1 → (ℎ‘𝑘):ℝ⟶ℝ)
98		ffn 6655	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘):ℝ⟶ℝ → (ℎ‘𝑘) Fn ℝ)
99	96, 97, 98	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) Fn ℝ)
100		reex 11120	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ∈ V
101	100	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → ℝ ∈ V)
102		inidm 4155	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ ∩ ℝ) = ℝ
103		eqidd 2740	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑓‘𝑘)‘𝑥) = ((𝑓‘𝑘)‘𝑥))
104		eqidd 2740	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((ℎ‘𝑘)‘𝑥) = ((ℎ‘𝑘)‘𝑥))
105	95, 99, 101, 101, 102, 103, 104	ofval 7631	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
106	91, 105	eqtrd 2774	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
107	106	an32s 658	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
108		fveq2 6827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝑓 ∘f ∘f − ℎ)‘𝑛) = ((𝑓 ∘f ∘f − ℎ)‘𝑘))
109	108	fveq1d 6829	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
110		eqid 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))
111		fvex 6840	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) ∈ V
112	109, 110, 111	fvmpt 6935	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
113	112	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
114		fveq2 6827	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘))
115	114	fveq1d 6829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛)‘𝑥) = ((𝑓‘𝑘)‘𝑥))
116		eqid 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))
117		fvex 6840	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓‘𝑘)‘𝑥) ∈ V
118	115, 116, 117	fvmpt 6935	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) = ((𝑓‘𝑘)‘𝑥))
119		fveq2 6827	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (ℎ‘𝑛) = (ℎ‘𝑘))
120	119	fveq1d 6829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((ℎ‘𝑛)‘𝑥) = ((ℎ‘𝑘)‘𝑥))
121		eqid 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))
122		fvex 6840	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑘)‘𝑥) ∈ V
123	120, 121, 122	fvmpt 6935	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) = ((ℎ‘𝑘)‘𝑥))
124	118, 123	oveq12d 7374	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
125	124	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
126	107, 113, 125	3eqtr4d 2784	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)))
127	126	adantlr 721	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)))
128	61, 62, 63, 65, 66, 75, 84, 127	climsub 15587	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))
129	1	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝐹:ℝ⟶ℝ)
130	129	ffvelcdmda 7025	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
131		max0sub 13139	. . . . . . . . . . . . . 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 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥))
134	128, 133	breqtrd 5098	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
135	134	ex 413	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
136	60, 135	sylbid 241	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
137	136	ralimdva 3151	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
138		ovex 7389	. . . . . . . . 9 ⊢ (𝑓 ∘f ∘f − ℎ) ∈ V
139		feq1 6633	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑔:ℕ⟶dom ∫1 ↔ (𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1))
140		fveq1 6826	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑔‘𝑛) = ((𝑓 ∘f ∘f − ℎ)‘𝑛))
141	140	fveq1d 6829	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑔‘𝑛)‘𝑥) = (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))
142	141	mpteq2dv 5166	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)))
143	142	breq1d 5082	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
144	143	ralbidv 3162	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
145	139, 144	anbi12d 638	. . . . . . . . 9 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ ((𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
146	138, 145	spcev 3544	. . . . . . . 8 ⊢ (((𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
147	41, 137, 146	syl6an 690	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
148	33, 147	biimtrrid 244	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ((∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
149	148	expimpd 454	. . . . 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 1941	. . 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 244	. 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 705	1 ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∀wral 3053  Vcvv 3431  ifcif 4454   class class class wbr 5072   ↦ cmpt 5153  dom cdm 5618   Fn wfn 6480  ⟶wf 6481  ‘cfv 6485  (class class class)co 7356   ∘_f cof 7618   ∘_r cofr 7619  ℂcc 11027  ℝcr 11028  0cc0 11029  1c1 11030   + caddc 11032  +∞cpnf 11167   ≤ cle 11171   − cmin 11368  -cneg 11369  ℕcn 12165  [,)cico 13291   ⇝ cli 15437  MblFncmbf 25599  ∫₁citg1 25600  0_𝑝c0p 25654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-inf2 9553  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-ofr 7621  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8633  df-map 8765  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9314  df-sup 9345  df-inf 9346  df-oi 9415  df-dju 9816  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-n0 12429  df-z 12516  df-uz 12780  df-q 12890  df-rp 12934  df-xneg 13054  df-xadd 13055  df-xmul 13056  df-ioo 13293  df-ico 13295  df-icc 13296  df-fz 13453  df-fzo 13600  df-fl 13742  df-seq 13955  df-exp 14015  df-hash 14284  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15441  df-rlim 15442  df-sum 15640  df-rest 17376  df-topgen 17397  df-psmet 21339  df-xmet 21340  df-met 21341  df-bl 21342  df-mopn 21343  df-top 22877  df-topon 22894  df-bases 22929  df-cmp 23370  df-ovol 25449  df-vol 25450  df-mbf 25604  df-itg1 25605  df-0p 25655

This theorem is referenced by:  mbfi1flim  25708