| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mbfi1flimlem.2 | . . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) | 
| 2 | 1 | ffvelcdmda 7103 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) | 
| 3 | 1 | feqmptd 6976 | . . . . 5
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦))) | 
| 4 |  | mbfi1flim.1 | . . . . 5
⊢ (𝜑 → 𝐹 ∈ MblFn) | 
| 5 | 3, 4 | eqeltrrd 2841 | . . . 4
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn) | 
| 6 | 2, 5 | mbfpos 25687 | . . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) ∈ MblFn) | 
| 7 |  | 0re 11264 | . . . . . 6
⊢ 0 ∈
ℝ | 
| 8 |  | ifcl 4570 | . . . . . 6
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ) | 
| 9 | 2, 7, 8 | sylancl 586 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ) | 
| 10 |  | max1 13228 | . . . . . 6
⊢ ((0
∈ ℝ ∧ (𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤
(𝐹‘𝑦), (𝐹‘𝑦), 0)) | 
| 11 | 7, 2, 10 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤
(𝐹‘𝑦), (𝐹‘𝑦), 0)) | 
| 12 |  | elrege0 13495 | . . . . 5
⊢ (if(0
≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤
(𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
(𝐹‘𝑦), (𝐹‘𝑦), 0))) | 
| 13 | 9, 11, 12 | sylanbrc 583 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞)) | 
| 14 | 13 | fmpttd 7134 | . . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦),
0)):ℝ⟶(0[,)+∞)) | 
| 15 | 6, 14 | mbfi1fseq 25757 | . 2
⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥))) | 
| 16 | 2 | renegcld 11691 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -(𝐹‘𝑦) ∈ ℝ) | 
| 17 | 2, 5 | mbfneg 25686 | . . . 4
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ -(𝐹‘𝑦)) ∈ MblFn) | 
| 18 | 16, 17 | mbfpos 25687 | . . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) ∈ MblFn) | 
| 19 |  | ifcl 4570 | . . . . . 6
⊢ ((-(𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ) | 
| 20 | 16, 7, 19 | sylancl 586 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ) | 
| 21 |  | max1 13228 | . . . . . 6
⊢ ((0
∈ ℝ ∧ -(𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤
-(𝐹‘𝑦), -(𝐹‘𝑦), 0)) | 
| 22 | 7, 16, 21 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤
-(𝐹‘𝑦), -(𝐹‘𝑦), 0)) | 
| 23 |  | elrege0 13495 | . . . . 5
⊢ (if(0
≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤
-(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
-(𝐹‘𝑦), -(𝐹‘𝑦), 0))) | 
| 24 | 20, 22, 23 | sylanbrc 583 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞)) | 
| 25 | 24 | fmpttd 7134 | . . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦),
0)):ℝ⟶(0[,)+∞)) | 
| 26 | 18, 25 | mbfi1fseq 25757 | . 2
⊢ (𝜑 → ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) | 
| 27 |  | exdistrv 1954 | . . 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 1149 | . . . . . . 7
⊢ ((𝑓:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘r ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) → (𝑓:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥))) | 
| 29 |  | 3simpb 1149 | . . . . . . 7
⊢ ((ℎ:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘r ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (ℎ:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) | 
| 30 | 28, 29 | anim12i 613 | . . . . . 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 656 | . . . . . 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 218 | . . . . 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 3110 | . . . . . . 7
⊢
(∀𝑥 ∈
ℝ ((𝑛 ∈ ℕ
↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) | 
| 34 |  | i1fsub 25744 | . . . . . . . . . 10
⊢ ((𝑥 ∈ dom ∫1
∧ 𝑦 ∈ dom
∫1) → (𝑥 ∘f − 𝑦) ∈ dom
∫1) | 
| 35 | 34 | adantl 481 | . . . . . . . . 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 12273 | . . . . . . . . . 10
⊢ ℕ
∈ V | 
| 39 | 38 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → ℕ ∈ V) | 
| 40 |  | inidm 4226 | . . . . . . . . 9
⊢ (ℕ
∩ ℕ) = ℕ | 
| 41 | 35, 36, 37, 39, 39, 40 | off 7716 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → (𝑓 ∘f ∘f
− ℎ):ℕ⟶dom
∫1) | 
| 42 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) | 
| 43 | 42 | breq2d 5154 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → (0 ≤ (𝐹‘𝑦) ↔ 0 ≤ (𝐹‘𝑥))) | 
| 44 | 43, 42 | ifbieq1d 4549 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) | 
| 45 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) | 
| 46 |  | fvex 6918 | . . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑥) ∈ V | 
| 47 |  | c0ex 11256 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
V | 
| 48 | 46, 47 | ifex 4575 | . . . . . . . . . . . . . 14
⊢ if(0 ≤
(𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V | 
| 49 | 44, 45, 48 | fvmpt 7015 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) | 
| 50 | 49 | breq2d 5154 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) | 
| 51 | 42 | negeqd 11503 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → -(𝐹‘𝑦) = -(𝐹‘𝑥)) | 
| 52 | 51 | breq2d 5154 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → (0 ≤ -(𝐹‘𝑦) ↔ 0 ≤ -(𝐹‘𝑥))) | 
| 53 | 52, 51 | ifbieq1d 4549 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) | 
| 54 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) | 
| 55 |  | negex 11507 | . . . . . . . . . . . . . . 15
⊢ -(𝐹‘𝑥) ∈ V | 
| 56 | 55, 47 | ifex 4575 | . . . . . . . . . . . . . 14
⊢ if(0 ≤
-(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V | 
| 57 | 53, 54, 56 | fvmpt 7015 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) | 
| 58 | 57 | breq2d 5154 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) | 
| 59 | 50, 58 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) | 
| 60 | 59 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) | 
| 61 |  | nnuz 12922 | . . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) | 
| 62 |  | 1zzd 12650 | . . . . . . . . . . . . 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 7244 | . . . . . . . . . . . . . 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 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) → (𝑓‘𝑛) ∈ dom
∫1) | 
| 68 |  | i1ff 25712 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓‘𝑛) ∈ dom ∫1 → (𝑓‘𝑛):ℝ⟶ℝ) | 
| 69 | 67, 68 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) → (𝑓‘𝑛):ℝ⟶ℝ) | 
| 70 | 69 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) ∧ 𝑥
∈ ℝ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ) | 
| 71 | 70 | an32s 652 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ) | 
| 72 | 71 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℂ) | 
| 73 | 72 | fmpttd 7134 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ) | 
| 74 | 73 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ) | 
| 75 | 74 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓:ℕ⟶dom
∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧
𝑥 ∈ ℝ) ∧
((𝑛 ∈ ℕ ↦
((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) ∈ ℂ) | 
| 76 | 37 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) → (ℎ‘𝑛) ∈ dom
∫1) | 
| 77 |  | i1ff 25712 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘𝑛) ∈ dom ∫1 → (ℎ‘𝑛):ℝ⟶ℝ) | 
| 78 | 76, 77 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) → (ℎ‘𝑛):ℝ⟶ℝ) | 
| 79 | 78 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) ∧ 𝑥
∈ ℝ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ) | 
| 80 | 79 | an32s 652 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ) | 
| 81 | 80 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℂ) | 
| 82 | 81 | fmpttd 7134 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (𝑛
∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ) | 
| 83 | 82 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ) | 
| 84 | 83 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓:ℕ⟶dom
∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧
𝑥 ∈ ℝ) ∧
((𝑛 ∈ ℕ ↦
((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) ∈ ℂ) | 
| 85 | 36 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → 𝑓 Fn ℕ) | 
| 86 | 37 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → ℎ
Fn ℕ) | 
| 87 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (𝑓‘𝑘) = (𝑓‘𝑘)) | 
| 88 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (ℎ‘𝑘) = (ℎ‘𝑘)) | 
| 89 | 85, 86, 39, 39, 40, 87, 88 | ofval 7709 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → ((𝑓
∘f ∘f − ℎ)‘𝑘) = ((𝑓‘𝑘) ∘f − (ℎ‘𝑘))) | 
| 90 | 89 | fveq1d 6907 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (((𝑓
∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥)) | 
| 91 | 90 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) ∧ 𝑥
∈ ℝ) → (((𝑓
∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥)) | 
| 92 | 36 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (𝑓‘𝑘) ∈ dom
∫1) | 
| 93 |  | i1ff 25712 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑘) ∈ dom ∫1 → (𝑓‘𝑘):ℝ⟶ℝ) | 
| 94 |  | ffn 6735 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑘):ℝ⟶ℝ → (𝑓‘𝑘) Fn ℝ) | 
| 95 | 92, 93, 94 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (𝑓‘𝑘) Fn ℝ) | 
| 96 | 37 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (ℎ‘𝑘) ∈ dom
∫1) | 
| 97 |  | i1ff 25712 | . . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑘) ∈ dom ∫1 → (ℎ‘𝑘):ℝ⟶ℝ) | 
| 98 |  | ffn 6735 | . . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑘):ℝ⟶ℝ → (ℎ‘𝑘) Fn ℝ) | 
| 99 | 96, 97, 98 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (ℎ‘𝑘) Fn ℝ) | 
| 100 |  | reex 11247 | . . . . . . . . . . . . . . . . . . 19
⊢ ℝ
∈ V | 
| 101 | 100 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → ℝ ∈ V) | 
| 102 |  | inidm 4226 | . . . . . . . . . . . . . . . . . 18
⊢ (ℝ
∩ ℝ) = ℝ | 
| 103 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) ∧ 𝑥
∈ ℝ) → ((𝑓‘𝑘)‘𝑥) = ((𝑓‘𝑘)‘𝑥)) | 
| 104 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) ∧ 𝑥
∈ ℝ) → ((ℎ‘𝑘)‘𝑥) = ((ℎ‘𝑘)‘𝑥)) | 
| 105 | 95, 99, 101, 101, 102, 103, 104 | ofval 7709 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) ∧ 𝑥
∈ ℝ) → (((𝑓‘𝑘) ∘f − (ℎ‘𝑘))‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥))) | 
| 106 | 91, 105 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) ∧ 𝑥
∈ ℝ) → (((𝑓
∘f ∘f − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥))) | 
| 107 | 106 | an32s 652 | . . . . . . . . . . . . . . 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 2736 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f
∘f − ℎ)‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f
− ℎ)‘𝑛)‘𝑥)) | 
| 111 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∘f
∘f − ℎ)‘𝑘)‘𝑥) ∈ V | 
| 112 | 109, 110,
111 | fvmpt 7015 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f
∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f
− ℎ)‘𝑘)‘𝑥)) | 
| 113 | 112 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (((𝑓
∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘f ∘f
− ℎ)‘𝑘)‘𝑥)) | 
| 114 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘)) | 
| 115 | 114 | fveq1d 6907 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛)‘𝑥) = ((𝑓‘𝑘)‘𝑥)) | 
| 116 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) | 
| 117 |  | fvex 6918 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑓‘𝑘)‘𝑥) ∈ V | 
| 118 | 115, 116,
117 | fvmpt 7015 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) = ((𝑓‘𝑘)‘𝑥)) | 
| 119 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (ℎ‘𝑛) = (ℎ‘𝑘)) | 
| 120 | 119 | fveq1d 6907 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((ℎ‘𝑛)‘𝑥) = ((ℎ‘𝑘)‘𝑥)) | 
| 121 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) | 
| 122 |  | fvex 6918 | . . . . . . . . . . . . . . . . . 18
⊢ ((ℎ‘𝑘)‘𝑥) ∈ V | 
| 123 | 120, 121,
122 | fvmpt 7015 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) = ((ℎ‘𝑘)‘𝑥)) | 
| 124 | 118, 123 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥))) | 
| 125 | 124 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑘
∈ ℕ) → (((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥))) | 
| 126 | 107, 113,
125 | 3eqtr4d 2786 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (((𝑓
∘f ∘f − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘))) | 
| 127 | 126 | adantlr 715 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓:ℕ⟶dom
∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧
𝑥 ∈ ℝ) ∧
((𝑛 ∈ ℕ ↦
((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f
− ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘))) | 
| 128 | 61, 62, 63, 65, 66, 75, 84, 127 | climsub 15671 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f
− ℎ)‘𝑛)‘𝑥)) ⇝ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) | 
| 129 | 1 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → 𝐹:ℝ⟶ℝ) | 
| 130 | 129 | ffvelcdmda 7103 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) | 
| 131 |  | max0sub 13239 | . . . . . . . . . . . . . 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 480 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥)) | 
| 134 | 128, 133 | breqtrd 5168 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f
− ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) | 
| 135 | 134 | ex 412 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f
− ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | 
| 136 | 60, 135 | sylbid 240 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f
− ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | 
| 137 | 136 | ralimdva 3166 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f
− ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | 
| 138 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑓 ∘f
∘f − ℎ) ∈ V | 
| 139 |  | feq1 6715 | . . . . . . . . . 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 5243 | . . . . . . . . . . . 12
⊢ (𝑔 = (𝑓 ∘f ∘f
− ℎ) → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f
− ℎ)‘𝑛)‘𝑥))) | 
| 143 | 142 | breq1d 5152 | . . . . . . . . . . 11
⊢ (𝑔 = (𝑓 ∘f ∘f
− ℎ) → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f
− ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | 
| 144 | 143 | ralbidv 3177 | . . . . . . . . . 10
⊢ (𝑔 = (𝑓 ∘f ∘f
− ℎ) →
(∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘f ∘f
− ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | 
| 145 | 139, 144 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑔 = (𝑓 ∘f ∘f
− ℎ) → ((𝑔:ℕ⟶dom
∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ ((𝑓 ∘f ∘f
− ℎ):ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
(((𝑓 ∘f
∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) | 
| 146 | 138, 145 | spcev 3605 | . . . . . . . 8
⊢ (((𝑓 ∘f
∘f − ℎ):ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
(((𝑓 ∘f
∘f − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) | 
| 147 | 41, 137, 146 | syl6an 684 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) | 
| 148 | 33, 147 | biimtrrid 243 | . . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → ((∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) | 
| 149 | 148 | expimpd 453 | . . . . 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 1933 | . . 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 243 | . 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 699 | 1
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |