Theorem mbfi1flimlem 25951

Description: Lemma for mbfi1flim 25952. (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 7080	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ)
3	1	feqmptd 6950	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)))
4		mbfi1flim.1	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ MblFn)
5	3, 4	eqeltrrd 2863	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn)
6	2, 5	mbfpos 25880	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) ∈ MblFn)
7		0re 11237	. . . . . 6 ⊢ 0 ∈ ℝ
8		ifcl 4531	. . . . . 6 ⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ)
9	2, 7, 8	sylancl 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ)
10		max1 13239	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ (𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
11	7, 2, 10	sylancr 599	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
12		elrege0 13509	. . . . 5 ⊢ (if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)))
13	9, 11, 12	sylanbrc 595	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞))
14	13	fmpttd 7111	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)):ℝ⟶(0[,)+∞))
15	6, 14	mbfi1fseq 25950	. 2 ⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)))
16	2	renegcld 11668	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -(𝐹‘𝑦) ∈ ℝ)
17	2, 5	mbfneg 25879	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ -(𝐹‘𝑦)) ∈ MblFn)
18	16, 17	mbfpos 25880	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) ∈ MblFn)
19		ifcl 4531	. . . . . 6 ⊢ ((-(𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ)
20	16, 7, 19	sylancl 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ)
21		max1 13239	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ -(𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
22	7, 16, 21	sylancr 599	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
23		elrege0 13509	. . . . 5 ⊢ (if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)))
24	20, 22, 23	sylanbrc 595	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞))
25	24	fmpttd 7111	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)):ℝ⟶(0[,)+∞))
26	18, 25	mbfi1fseq 25950	. 2 ⊢ (𝜑 → ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
27		exdistrv 1988	. . 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 1167	. . . . . . 7 ⊢ ((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) → (𝑓:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)))
29		3simpb 1167	. . . . . . 7 ⊢ ((ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
30	28, 29	anim12i 625	. . . . . 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 669	. . . . . 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 3124	. . . . . . 7 ⊢ (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
34		i1fsub 25937	. . . . . . . . . 10 ⊢ ((𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1) → (𝑥 ∘f − 𝑦) ∈ dom ∫1)
35	34	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ (𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1)) → (𝑥 ∘f − 𝑦) ∈ dom ∫1)
36		simprl 783	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝑓:ℕ⟶dom ∫1)
37		simprr 785	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℎ:ℕ⟶dom ∫1)
38		nnex 12266	. . . . . . . . . 10 ⊢ ℕ ∈ V
39	38	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℕ ∈ V)
40		inidm 4175	. . . . . . . . 9 ⊢ (ℕ ∩ ℕ) = ℕ
41	35, 36, 37, 39, 39, 40	off 7699	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1)
42		fveq2 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
43	42	breq2d 5119	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (0 ≤ (𝐹‘𝑦) ↔ 0 ≤ (𝐹‘𝑥)))
44	43, 42	ifbieq1d 4510	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
45		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
46		fvex 6895	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑥) ∈ V
47		c0ex 11227	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
48	46, 47	ifex 4536	. . . . . . . . . . . . . 14 ⊢ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V
49	44, 45, 48	fvmpt 6990	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
50	49	breq2d 5119	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))
51	42	negeqd 11478	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → -(𝐹‘𝑦) = -(𝐹‘𝑥))
52	51	breq2d 5119	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (0 ≤ -(𝐹‘𝑦) ↔ 0 ≤ -(𝐹‘𝑥)))
53	52, 51	ifbieq1d 4510	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
54		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
55		negex 11482	. . . . . . . . . . . . . . 15 ⊢ -(𝐹‘𝑥) ∈ V
56	55, 47	ifex 4536	. . . . . . . . . . . . . 14 ⊢ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V
57	53, 54, 56	fvmpt 6990	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
58	57	breq2d 5119	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))
59	50, 58	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))
60	59	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))
61		nnuz 12929	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ≥‘1)
62		1zzd 12652	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → 1 ∈ ℤ)
63		simprl 783	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
64	38	mptex 7225	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ∈ V
65	64	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ∈ V)
66		simprr 785	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
67	36	ffvelcdmda 7080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ dom ∫1)
68		i1ff 25905	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑛) ∈ dom ∫1 → (𝑓‘𝑛):ℝ⟶ℝ)
69	67, 68	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛):ℝ⟶ℝ)
70	69	ffvelcdmda 7080	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ)
71	70	an32s 665	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ)
72	71	recnd 11264	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℂ)
73	72	fmpttd 7111	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ)
74	73	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ)
75	74	ffvelcdmda 7080	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) ∈ ℂ)
76	37	ffvelcdmda 7080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (ℎ‘𝑛) ∈ dom ∫1)
77		i1ff 25905	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑛) ∈ dom ∫1 → (ℎ‘𝑛):ℝ⟶ℝ)
78	76, 77	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (ℎ‘𝑛):ℝ⟶ℝ)
79	78	ffvelcdmda 7080	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ)
80	79	an32s 665	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ)
81	80	recnd 11264	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℂ)
82	81	fmpttd 7111	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ)
83	82	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ)
84	83	ffvelcdmda 7080	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) ∈ ℂ)
85	36	ffnd 6707	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝑓 Fn ℕ)
86	37	ffnd 6707	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℎ Fn ℕ)
87		eqidd 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) = (𝑓‘𝑘))
88		eqidd 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) = (ℎ‘𝑘))
89	85, 86, 39, 39, 40, 87, 88	ofval 7692	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → ((𝑓 ∘f ∘f − ℎ)‘𝑘) = ((𝑓‘𝑘) ∘f − (ℎ‘𝑘)))
90	89	fveq1d 6884	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥))
91	90	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥))
92	36	ffvelcdmda 7080	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ dom ∫1)
93		i1ff 25905	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘) ∈ dom ∫1 → (𝑓‘𝑘):ℝ⟶ℝ)
94		ffn 6706	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘):ℝ⟶ℝ → (𝑓‘𝑘) Fn ℝ)
95	92, 93, 94	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) Fn ℝ)
96	37	ffvelcdmda 7080	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) ∈ dom ∫1)
97		i1ff 25905	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘) ∈ dom ∫1 → (ℎ‘𝑘):ℝ⟶ℝ)
98		ffn 6706	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘):ℝ⟶ℝ → (ℎ‘𝑘) Fn ℝ)
99	96, 97, 98	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) Fn ℝ)
100		reex 11218	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ∈ V
101	100	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → ℝ ∈ V)
102		inidm 4175	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ ∩ ℝ) = ℝ
103		eqidd 2763	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑓‘𝑘)‘𝑥) = ((𝑓‘𝑘)‘𝑥))
104		eqidd 2763	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((ℎ‘𝑘)‘𝑥) = ((ℎ‘𝑘)‘𝑥))
105	95, 99, 101, 101, 102, 103, 104	ofval 7692	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
106	91, 105	eqtrd 2797	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
107	106	an32s 665	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
108		fveq2 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝑓 ∘f ∘f − ℎ)‘𝑛) = ((𝑓 ∘f ∘f − ℎ)‘𝑘))
109	108	fveq1d 6884	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
110		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))
111		fvex 6895	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) ∈ V
112	109, 110, 111	fvmpt 6990	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
113	112	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
114		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘))
115	114	fveq1d 6884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛)‘𝑥) = ((𝑓‘𝑘)‘𝑥))
116		eqid 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))
117		fvex 6895	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓‘𝑘)‘𝑥) ∈ V
118	115, 116, 117	fvmpt 6990	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) = ((𝑓‘𝑘)‘𝑥))
119		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (ℎ‘𝑛) = (ℎ‘𝑘))
120	119	fveq1d 6884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((ℎ‘𝑛)‘𝑥) = ((ℎ‘𝑘)‘𝑥))
121		eqid 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))
122		fvex 6895	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑘)‘𝑥) ∈ V
123	120, 121, 122	fvmpt 6990	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) = ((ℎ‘𝑘)‘𝑥))
124	118, 123	oveq12d 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
125	124	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
126	107, 113, 125	3eqtr4d 2807	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)))
127	126	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)))
128	61, 62, 63, 65, 66, 75, 84, 127	climsub 15723	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))
129	1	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝐹:ℝ⟶ℝ)
130	129	ffvelcdmda 7080	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
131		max0sub 13250	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) ∈ ℝ → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥))
132	130, 131	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥))
133	132	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥))
134	128, 133	breqtrd 5135	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))
135	134	ex 418	. . . . . . . . . 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 3176	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
138		ovex 7449	. . . . . . . . 9 ⊢ (𝑓 ∘f ∘f − ℎ) ∈ V
139		feq1 6684	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑔:ℕ⟶dom ∫1 ↔ (𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1))
140		fveq1 6881	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑔‘𝑛) = ((𝑓 ∘f ∘f − ℎ)‘𝑛))
141	140	fveq1d 6884	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑔‘𝑛)‘𝑥) = (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))
142	141	mpteq2dv 5203	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)))
143	142	breq1d 5117	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
144	143	ralbidv 3187	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
145	139, 144	anbi12d 644	. . . . . . . . 9 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ ((𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
146	138, 145	spcev 3563	. . . . . . . 8 ⊢ (((𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
147	41, 137, 146	syl6an 697	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
148	33, 147	biimtrrid 246	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ((∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
149	148	expimpd 459	. . . . 5 ⊢ (𝜑 → (((𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1) ∧ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
150	32, 149	syl5 35	. . . 4 ⊢ (𝜑 → (((𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))))
151	150	exlimdvv 1967	. . 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 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 712	1 ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∀wral 3078  Vcvv 3453  ifcif 4485   class class class wbr 5107   ↦ cmpt 5190  dom cdm 5659   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537  (class class class)co 7416   ∘_f cof 7679   ∘_r cofr 7680  ℂcc 11125  ℝcr 11126  0cc0 11127  1c1 11128   + caddc 11130  +∞cpnf 11267   ≤ cle 11271   − cmin 11468  -cneg 11469  ℕcn 12260  [,)cico 13402   ⇝ cli 15573  MblFncmbf 25843  ∫₁citg1 25844  0_𝑝c0p 25898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-inf2 9623  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7681  df-ofr 7682  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-2o 8459  df-er 8699  df-map 8831  df-pm 8832  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fi 9384  df-sup 9415  df-inf 9416  df-oi 9485  df-dju 9909  df-card 9947  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-div 11899  df-nn 12261  df-2 12330  df-3 12331  df-n0 12532  df-z 12619  df-uz 12891  df-q 13001  df-rp 13045  df-xneg 13165  df-xadd 13166  df-xmul 13167  df-ioo 13404  df-ico 13406  df-icc 13407  df-fz 13564  df-fzo 13712  df-fl 13855  df-seq 14068  df-exp 14128  df-hash 14397  df-cj 15188  df-re 15189  df-im 15190  df-sqrt 15324  df-abs 15325  df-clim 15577  df-rlim 15578  df-sum 15776  df-rest 17511  df-topgen 17532  df-psmet 21578  df-xmet 21579  df-met 21580  df-bl 21581  df-mopn 21582  df-top 23120  df-topon 23137  df-bases 23172  df-cmp 23613  df-ovol 25693  df-vol 25694  df-mbf 25848  df-itg1 25849  df-0p 25899

This theorem is used by:  mbfi1flim  25952