Theorem mbfi1flimlem 24422

Description: Lemma for mbfi1flim 24423. (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	ffvelrnda 6842	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ)
3	1	feqmptd 6721	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)))
4		mbfi1flim.1	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ MblFn)
5	3, 4	eqeltrrd 2853	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn)
6	2, 5	mbfpos 24351	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) ∈ MblFn)
7		0re 10681	. . . . . 6 ⊢ 0 ∈ ℝ
8		ifcl 4465	. . . . . 6 ⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ)
9	2, 7, 8	sylancl 589	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ)
10		max1 12619	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ (𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
11	7, 2, 10	sylancr 590	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
12		elrege0 12886	. . . . 5 ⊢ (if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)))
13	9, 11, 12	sylanbrc 586	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞))
14	13	fmpttd 6870	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)):ℝ⟶(0[,)+∞))
15	6, 14	mbfi1fseq 24421	. 2 ⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)))
16	2	renegcld 11105	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -(𝐹‘𝑦) ∈ ℝ)
17	2, 5	mbfneg 24350	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ -(𝐹‘𝑦)) ∈ MblFn)
18	16, 17	mbfpos 24351	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) ∈ MblFn)
19		ifcl 4465	. . . . . 6 ⊢ ((-(𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ)
20	16, 7, 19	sylancl 589	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ)
21		max1 12619	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ -(𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
22	7, 16, 21	sylancr 590	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
23		elrege0 12886	. . . . 5 ⊢ (if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)))
24	20, 22, 23	sylanbrc 586	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞))
25	24	fmpttd 6870	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)):ℝ⟶(0[,)+∞))
26	18, 25	mbfi1fseq 24421	. 2 ⊢ (𝜑 → ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
27		exdistrv 1956	. . 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 1146	. . . . . . 7 ⊢ ((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) → (𝑓:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)))
29		3simpb 1146	. . . . . . 7 ⊢ ((ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
30	28, 29	anim12i 615	. . . . . 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 655	. . . . . 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 221	. . . . 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 24408	. . . . . . . . . 10 ⊢ ((𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1) → (𝑥 ∘f − 𝑦) ∈ dom ∫1)
35	34	adantl 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ (𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1)) → (𝑥 ∘f − 𝑦) ∈ dom ∫1)
36		simprl 770	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝑓:ℕ⟶dom ∫1)
37		simprr 772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℎ:ℕ⟶dom ∫1)
38		nnex 11680	. . . . . . . . . 10 ⊢ ℕ ∈ V
39	38	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℕ ∈ V)
40		inidm 4123	. . . . . . . . 9 ⊢ (ℕ ∩ ℕ) = ℕ
41	35, 36, 37, 39, 39, 40	off 7422	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1)
42		fveq2 6658	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
43	42	breq2d 5044	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (0 ≤ (𝐹‘𝑦) ↔ 0 ≤ (𝐹‘𝑥)))
44	43, 42	ifbieq1d 4444	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
45		eqid 2758	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
46		fvex 6671	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑥) ∈ V
47		c0ex 10673	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
48	46, 47	ifex 4470	. . . . . . . . . . . . . 14 ⊢ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V
49	44, 45, 48	fvmpt 6759	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
50	49	breq2d 5044	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))
51	42	negeqd 10918	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → -(𝐹‘𝑦) = -(𝐹‘𝑥))
52	51	breq2d 5044	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (0 ≤ -(𝐹‘𝑦) ↔ 0 ≤ -(𝐹‘𝑥)))
53	52, 51	ifbieq1d 4444	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
54		eqid 2758	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
55		negex 10922	. . . . . . . . . . . . . . 15 ⊢ -(𝐹‘𝑥) ∈ V
56	55, 47	ifex 4470	. . . . . . . . . . . . . 14 ⊢ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V
57	53, 54, 56	fvmpt 6759	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
58	57	breq2d 5044	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))
59	50, 58	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))
60	59	adantl 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))
61		nnuz 12321	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ≥‘1)
62		1zzd 12052	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → 1 ∈ ℤ)
63		simprl 770	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
64	38	mptex 6977	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ∈ V
65	64	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ∈ V)
66		simprr 772	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
67	36	ffvelrnda 6842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ dom ∫1)
68		i1ff 24376	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑛) ∈ dom ∫1 → (𝑓‘𝑛):ℝ⟶ℝ)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛):ℝ⟶ℝ)
70	69	ffvelrnda 6842	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ)
71	70	an32s 651	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ)
72	71	recnd 10707	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℂ)
73	72	fmpttd 6870	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ)
74	73	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ)
75	74	ffvelrnda 6842	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) ∈ ℂ)
76	37	ffvelrnda 6842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (ℎ‘𝑛) ∈ dom ∫1)
77		i1ff 24376	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑛) ∈ dom ∫1 → (ℎ‘𝑛):ℝ⟶ℝ)
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (ℎ‘𝑛):ℝ⟶ℝ)
79	78	ffvelrnda 6842	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ)
80	79	an32s 651	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ)
81	80	recnd 10707	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℂ)
82	81	fmpttd 6870	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ)
83	82	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ)
84	83	ffvelrnda 6842	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) ∈ ℂ)
85	36	ffnd 6499	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝑓 Fn ℕ)
86	37	ffnd 6499	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℎ Fn ℕ)
87		eqidd 2759	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) = (𝑓‘𝑘))
88		eqidd 2759	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) = (ℎ‘𝑘))
89	85, 86, 39, 39, 40, 87, 88	ofval 7415	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → ((𝑓 ∘f ∘f − ℎ)‘𝑘) = ((𝑓‘𝑘) ∘f − (ℎ‘𝑘)))
90	89	fveq1d 6660	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥))
91	90	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥))
92	36	ffvelrnda 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ dom ∫1)
93		i1ff 24376	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘) ∈ dom ∫1 → (𝑓‘𝑘):ℝ⟶ℝ)
94		ffn 6498	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘):ℝ⟶ℝ → (𝑓‘𝑘) Fn ℝ)
95	92, 93, 94	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) Fn ℝ)
96	37	ffvelrnda 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) ∈ dom ∫1)
97		i1ff 24376	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘) ∈ dom ∫1 → (ℎ‘𝑘):ℝ⟶ℝ)
98		ffn 6498	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘):ℝ⟶ℝ → (ℎ‘𝑘) Fn ℝ)
99	96, 97, 98	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) Fn ℝ)
100		reex 10666	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ∈ V
101	100	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → ℝ ∈ V)
102		inidm 4123	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ ∩ ℝ) = ℝ
103		eqidd 2759	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑓‘𝑘)‘𝑥) = ((𝑓‘𝑘)‘𝑥))
104		eqidd 2759	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((ℎ‘𝑘)‘𝑥) = ((ℎ‘𝑘)‘𝑥))
105	95, 99, 101, 101, 102, 103, 104	ofval 7415	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
106	91, 105	eqtrd 2793	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
107	106	an32s 651	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
108		fveq2 6658	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝑓 ∘f ∘f − ℎ)‘𝑛) = ((𝑓 ∘f ∘f − ℎ)‘𝑘))
109	108	fveq1d 6660	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
110		eqid 2758	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))
111		fvex 6671	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) ∈ V
112	109, 110, 111	fvmpt 6759	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
113	112	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
114		fveq2 6658	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘))
115	114	fveq1d 6660	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛)‘𝑥) = ((𝑓‘𝑘)‘𝑥))
116		eqid 2758	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))
117		fvex 6671	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓‘𝑘)‘𝑥) ∈ V
118	115, 116, 117	fvmpt 6759	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) = ((𝑓‘𝑘)‘𝑥))
119		fveq2 6658	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (ℎ‘𝑛) = (ℎ‘𝑘))
120	119	fveq1d 6660	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((ℎ‘𝑛)‘𝑥) = ((ℎ‘𝑘)‘𝑥))
121		eqid 2758	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))
122		fvex 6671	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑘)‘𝑥) ∈ V
123	120, 121, 122	fvmpt 6759	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) = ((ℎ‘𝑘)‘𝑥))
124	118, 123	oveq12d 7168	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
125	124	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
126	107, 113, 125	3eqtr4d 2803	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)))
127	126	adantlr 714	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)))
128	61, 62, 63, 65, 66, 75, 84, 127	climsub 15038	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))
129	1	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝐹:ℝ⟶ℝ)
130	129	ffvelrnda 6842	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
131		max0sub 12630	. . . . . . . . . . . . . 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 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥))
134	128, 133	breqtrd 5058	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
135	134	ex 416	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
136	60, 135	sylbid 243	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
137	136	ralimdva 3108	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
138		ovex 7183	. . . . . . . . 9 ⊢ (𝑓 ∘f ∘f − ℎ) ∈ V
139		feq1 6479	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑔:ℕ⟶dom ∫1 ↔ (𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1))
140		fveq1 6657	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑔‘𝑛) = ((𝑓 ∘f ∘f − ℎ)‘𝑛))
141	140	fveq1d 6660	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑔‘𝑛)‘𝑥) = (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))
142	141	mpteq2dv 5128	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)))
143	142	breq1d 5042	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
144	143	ralbidv 3126	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
145	139, 144	anbi12d 633	. . . . . . . . 9 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ ((𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
146	138, 145	spcev 3525	. . . . . . . 8 ⊢ (((𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
147	41, 137, 146	syl6an 683	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
148	33, 147	syl5bir 246	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ((∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
149	148	expimpd 457	. . . . 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 1935	. . 3 ⊢ (𝜑 → (∃𝑓∃ℎ((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
152	27, 151	syl5bir 246	. 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 698	1 ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3070  Vcvv 3409  ifcif 4420   class class class wbr 5032   ↦ cmpt 5112  dom cdm 5524   Fn wfn 6330  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150   ∘_f cof 7403   ∘_r cofr 7404  ℂcc 10573  ℝcr 10574  0cc0 10575  1c1 10576   + caddc 10578  +∞cpnf 10710   ≤ cle 10714   − cmin 10908  -cneg 10909  ℕcn 11674  [,)cico 12781   ⇝ cli 14889  MblFncmbf 24314  ∫₁citg1 24315  0_𝑝c0p 24369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7405  df-ofr 7406  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-2o 8113  df-er 8299  df-map 8418  df-pm 8419  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-fi 8908  df-sup 8939  df-inf 8940  df-oi 9007  df-dju 9363  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-n0 11935  df-z 12021  df-uz 12283  df-q 12389  df-rp 12431  df-xneg 12548  df-xadd 12549  df-xmul 12550  df-ioo 12783  df-ico 12785  df-icc 12786  df-fz 12940  df-fzo 13083  df-fl 13211  df-seq 13419  df-exp 13480  df-hash 13741  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-clim 14893  df-rlim 14894  df-sum 15091  df-rest 16754  df-topgen 16775  df-psmet 20158  df-xmet 20159  df-met 20160  df-bl 20161  df-mopn 20162  df-top 21594  df-topon 21611  df-bases 21646  df-cmp 22087  df-ovol 24164  df-vol 24165  df-mbf 24319  df-itg1 24320  df-0p 24370

This theorem is referenced by:  mbfi1flim  24423