Theorem mbfi1flimlem 26070

Description: Lemma for mbfi1flim 26071. (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 7105	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ)
3	1	feqmptd 6973	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)))
4		mbfi1flim.1	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ MblFn)
5	3, 4	eqeltrrd 2865	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn)
6	2, 5	mbfpos 25999	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) ∈ MblFn)
7		0re 11334	. . . . . 6 ⊢ 0 ∈ ℝ
8		ifcl 4531	. . . . . 6 ⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ)
9	2, 7, 8	sylancl 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ)
10		max1 13339	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ (𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
11	7, 2, 10	sylancr 599	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
12		elrege0 13609	. . . . 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 7136	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)):ℝ⟶(0[,)+∞))
15	6, 14	mbfi1fseq 26069	. 2 ⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)))
16	2	renegcld 11767	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -(𝐹‘𝑦) ∈ ℝ)
17	2, 5	mbfneg 25998	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ -(𝐹‘𝑦)) ∈ MblFn)
18	16, 17	mbfpos 25999	. . 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 13339	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ -(𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
22	7, 16, 21	sylancr 599	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
23		elrege0 13609	. . . . 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 7136	. . 3 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)):ℝ⟶(0[,)+∞))
26	18, 25	mbfi1fseq 26069	. 2 ⊢ (𝜑 → ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
27		exdistrv 1990	. . 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 3126	. . . . . . 7 ⊢ (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))
34		i1fsub 26056	. . . . . . . . . 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 12365	. . . . . . . . . 10 ⊢ ℕ ∈ V
39	38	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℕ ∈ V)
40		inidm 4126	. . . . . . . . 9 ⊢ (ℕ ∩ ℕ) = ℕ
41	35, 36, 37, 39, 39, 40	off 7732	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1)
42		fveq2 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
43	42	breq2d 5118	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (0 ≤ (𝐹‘𝑦) ↔ 0 ≤ (𝐹‘𝑥)))
44	43, 42	ifbieq1d 4510	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
45		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))
46		fvex 6918	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑥) ∈ V
47		c0ex 11324	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
48	46, 47	ifex 4536	. . . . . . . . . . . . . 14 ⊢ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V
49	44, 45, 48	fvmpt 7013	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))
50	49	breq2d 5118	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))
51	42	negeqd 11575	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → -(𝐹‘𝑦) = -(𝐹‘𝑥))
52	51	breq2d 5118	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (0 ≤ -(𝐹‘𝑦) ↔ 0 ≤ -(𝐹‘𝑥)))
53	52, 51	ifbieq1d 4510	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
54		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))
55		negex 11579	. . . . . . . . . . . . . . 15 ⊢ -(𝐹‘𝑥) ∈ V
56	55, 47	ifex 4536	. . . . . . . . . . . . . 14 ⊢ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V
57	53, 54, 56	fvmpt 7013	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))
58	57	breq2d 5118	. . . . . . . . . . . 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 13028	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ≥‘1)
62		1zzd 12751	. . . . . . . . . . . . 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 7249	. . . . . . . . . . . . . 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 7105	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ dom ∫1)
68		i1ff 26024	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑛) ∈ dom ∫1 → (𝑓‘𝑛):ℝ⟶ℝ)
69	67, 68	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛):ℝ⟶ℝ)
70	69	ffvelcdmda 7105	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ)
71	70	an32s 665	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ)
72	71	recnd 11361	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℂ)
73	72	fmpttd 7136	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ)
74	73	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ)
75	74	ffvelcdmda 7105	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) ∈ ℂ)
76	37	ffvelcdmda 7105	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (ℎ‘𝑛) ∈ dom ∫1)
77		i1ff 26024	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑛) ∈ dom ∫1 → (ℎ‘𝑛):ℝ⟶ℝ)
78	76, 77	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) → (ℎ‘𝑛):ℝ⟶ℝ)
79	78	ffvelcdmda 7105	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ)
80	79	an32s 665	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ)
81	80	recnd 11361	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℂ)
82	81	fmpttd 7136	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ)
83	82	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ)
84	83	ffvelcdmda 7105	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) ∈ ℂ)
85	36	ffnd 6729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → 𝑓 Fn ℕ)
86	37	ffnd 6729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → ℎ Fn ℕ)
87		eqidd 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) = (𝑓‘𝑘))
88		eqidd 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) = (ℎ‘𝑘))
89	85, 86, 39, 39, 40, 87, 88	ofval 7725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → ((𝑓 ∘f ∘f − ℎ)‘𝑘) = ((𝑓‘𝑘) ∘f − (ℎ‘𝑘)))
90	89	fveq1d 6907	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥))
91	90	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥))
92	36	ffvelcdmda 7105	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ dom ∫1)
93		i1ff 26024	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘) ∈ dom ∫1 → (𝑓‘𝑘):ℝ⟶ℝ)
94		ffn 6728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘):ℝ⟶ℝ → (𝑓‘𝑘) Fn ℝ)
95	92, 93, 94	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) Fn ℝ)
96	37	ffvelcdmda 7105	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) ∈ dom ∫1)
97		i1ff 26024	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘) ∈ dom ∫1 → (ℎ‘𝑘):ℝ⟶ℝ)
98		ffn 6728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘):ℝ⟶ℝ → (ℎ‘𝑘) Fn ℝ)
99	96, 97, 98	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → (ℎ‘𝑘) Fn ℝ)
100		reex 11315	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ∈ V
101	100	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) → ℝ ∈ V)
102		inidm 4126	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ ∩ ℝ) = ℝ
103		eqidd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑓‘𝑘)‘𝑥) = ((𝑓‘𝑘)‘𝑥))
104		eqidd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((ℎ‘𝑘)‘𝑥) = ((ℎ‘𝑘)‘𝑥))
105	95, 99, 101, 101, 102, 103, 104	ofval 7725	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
106	91, 105	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
107	106	an32s 665	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
108		fveq2 6905	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝑓 ∘f ∘f − ℎ)‘𝑛) = ((𝑓 ∘f ∘f − ℎ)‘𝑘))
109	108	fveq1d 6907	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
110		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))
111		fvex 6918	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥) ∈ V
112	109, 110, 111	fvmpt 7013	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
113	112	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f − ℎ)‘𝑘)‘𝑥))
114		fveq2 6905	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘))
115	114	fveq1d 6907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛)‘𝑥) = ((𝑓‘𝑘)‘𝑥))
116		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))
117		fvex 6918	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓‘𝑘)‘𝑥) ∈ V
118	115, 116, 117	fvmpt 7013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) = ((𝑓‘𝑘)‘𝑥))
119		fveq2 6905	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (ℎ‘𝑛) = (ℎ‘𝑘))
120	119	fveq1d 6907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((ℎ‘𝑛)‘𝑥) = ((ℎ‘𝑘)‘𝑥))
121		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))
122		fvex 6918	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑘)‘𝑥) ∈ V
123	120, 121, 122	fvmpt 7013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) = ((ℎ‘𝑘)‘𝑥))
124	118, 123	oveq12d 7458	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
125	124	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥)))
126	107, 113, 125	3eqtr4d 2808	. . . . . . . . . . . . . 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 15827	. . . . . . . . . . . 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 7105	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
131		max0sub 13350	. . . . . . . . . . . . . 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 5134	. . . . . . . . . . 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 3178	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧ ℎ:ℕ⟶dom ∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
138		ovex 7473	. . . . . . . . 9 ⊢ (𝑓 ∘f ∘f − ℎ) ∈ V
139		feq1 6706	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑔:ℕ⟶dom ∫1 ↔ (𝑓 ∘f ∘f − ℎ):ℕ⟶dom ∫1))
140		fveq1 6904	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑔‘𝑛) = ((𝑓 ∘f ∘f − ℎ)‘𝑛))
141	140	fveq1d 6907	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑔‘𝑛)‘𝑥) = (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥))
142	141	mpteq2dv 5202	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)))
143	142	breq1d 5116	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ∘f ∘f − ℎ) → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
144	143	ralbidv 3189	. . . . . . . . . 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 3564	. . . . . . . 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 1969	. . 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 2147  ∀wral 3080  Vcvv 3454  ifcif 4485   class class class wbr 5106   ↦ cmpt 5189  dom cdm 5655   Fn wfn 6550  ⟶wf 6551  ‘cfv 6555  (class class class)co 7440   ∘_f cof 7712   ∘_r cofr 7713  ℂcc 11222  ℝcr 11223  0cc0 11224  1c1 11225   + caddc 11227  +∞cpnf 11364   ≤ cle 11368   − cmin 11565   -cneg 11566  ℕcn 12359  [,)cico 13502   ⇝ cli 15677  MblFncmbf 25962  ∫₁citg1 25963  0_𝑝c0p 26017

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-inf2 9666  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301  ax-pre-sup 11302

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-isom 6564  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-of 7714  df-ofr 7715  df-om 7899  df-1st 8022  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-2o 8502  df-er 8742  df-map 8874  df-pm 8875  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-fi 9427  df-sup 9458  df-inf 9459  df-oi 9528  df-dju 10006  df-card 10044  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-div 11998  df-nn 12360  df-2 12429  df-3 12430  df-n0 12631  df-z 12718  df-uz 12990  df-q 13100  df-rp 13145  df-xneg 13265  df-xadd 13266  df-xmul 13267  df-ioo 13504  df-ico 13506  df-icc 13507  df-fz 13664  df-fzo 13813  df-fl 13956  df-seq 14169  df-exp 14229  df-hash 14499  df-cj 15292  df-re 15293  df-im 15294  df-sqrt 15428  df-abs 15429  df-clim 15681  df-rlim 15682  df-sum 15880  df-rest 17619  df-topgen 17640  df-psmet 21697  df-xmet 21698  df-met 21699  df-bl 21700  df-mopn 21701  df-top 23239  df-topon 23256  df-bases 23291  df-cmp 23732  df-ovol 25812  df-vol 25813  df-mbf 25967  df-itg1 25968  df-0p 26018

This theorem is used by:  mbfi1flim  26071