Step | Hyp | Ref
| Expression |
1 | | mbfi1flimlem.2 |
. . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
2 | 1 | ffvelrnda 6267 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) |
3 | 1 | feqmptd 6159 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦))) |
4 | | mbfi1flim.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ MblFn) |
5 | 3, 4 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn) |
6 | 2, 5 | mbfpos 23224 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) ∈ MblFn) |
7 | | 0re 9919 |
. . . . . 6
⊢ 0 ∈
ℝ |
8 | | ifcl 4080 |
. . . . . 6
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ) |
9 | 2, 7, 8 | sylancl 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ) |
10 | | max1 11890 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ (𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤
(𝐹‘𝑦), (𝐹‘𝑦), 0)) |
11 | 7, 2, 10 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤
(𝐹‘𝑦), (𝐹‘𝑦), 0)) |
12 | | elrege0 12149 |
. . . . 5
⊢ (if(0
≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤
(𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
(𝐹‘𝑦), (𝐹‘𝑦), 0))) |
13 | 9, 11, 12 | sylanbrc 695 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) ∈ (0[,)+∞)) |
14 | | eqid 2610 |
. . . 4
⊢ (𝑦 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0)) |
15 | 13, 14 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦),
0)):ℝ⟶(0[,)+∞)) |
16 | 6, 15 | mbfi1fseq 23294 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘𝑟 ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥))) |
17 | 2 | renegcld 10336 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -(𝐹‘𝑦) ∈ ℝ) |
18 | 2, 5 | mbfneg 23223 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ -(𝐹‘𝑦)) ∈ MblFn) |
19 | 17, 18 | mbfpos 23224 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) ∈ MblFn) |
20 | | ifcl 4080 |
. . . . . 6
⊢ ((-(𝐹‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ) |
21 | 17, 7, 20 | sylancl 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ) |
22 | | max1 11890 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ -(𝐹‘𝑦) ∈ ℝ) → 0 ≤ if(0 ≤
-(𝐹‘𝑦), -(𝐹‘𝑦), 0)) |
23 | 7, 17, 22 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤
-(𝐹‘𝑦), -(𝐹‘𝑦), 0)) |
24 | | elrege0 12149 |
. . . . 5
⊢ (if(0
≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞) ↔ (if(0 ≤
-(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
-(𝐹‘𝑦), -(𝐹‘𝑦), 0))) |
25 | 21, 23, 24 | sylanbrc 695 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) ∈ (0[,)+∞)) |
26 | | eqid 2610 |
. . . 4
⊢ (𝑦 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0)) |
27 | 25, 26 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦),
0)):ℝ⟶(0[,)+∞)) |
28 | 19, 27 | mbfi1fseq 23294 |
. 2
⊢ (𝜑 → ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘𝑟 ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) |
29 | | eeanv 2170 |
. . 3
⊢
(∃𝑓∃ℎ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘𝑟 ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘𝑟 ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) ↔ (∃𝑓(𝑓:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘𝑟 ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘𝑟 ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))) |
30 | | 3simpb 1052 |
. . . . . . 7
⊢ ((𝑓:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘𝑟 ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) → (𝑓:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥))) |
31 | | 3simpb 1052 |
. . . . . . 7
⊢ ((ℎ:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘𝑟 ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (ℎ:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) |
32 | 30, 31 | anim12i 588 |
. . . . . 6
⊢ (((𝑓:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘𝑟 ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘𝑟 ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))) |
33 | | an4 861 |
. . . . . 6
⊢ (((𝑓:ℕ⟶dom
∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) ↔ ((𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1) ∧ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))) |
34 | 32, 33 | sylib 207 |
. . . . 5
⊢ (((𝑓:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘𝑟 ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘𝑟 ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ((𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1) ∧ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)))) |
35 | | r19.26 3046 |
. . . . . . 7
⊢
(∀𝑥 ∈
ℝ ((𝑛 ∈ ℕ
↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) ↔ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) |
36 | | i1fsub 23281 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ dom ∫1
∧ 𝑦 ∈ dom
∫1) → (𝑥 ∘𝑓 − 𝑦) ∈ dom
∫1) |
37 | 36 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ (𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1))
→ (𝑥
∘𝑓 − 𝑦) ∈ dom
∫1) |
38 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → 𝑓:ℕ⟶dom
∫1) |
39 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → ℎ:ℕ⟶dom
∫1) |
40 | | nnex 10903 |
. . . . . . . . . 10
⊢ ℕ
∈ V |
41 | 40 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → ℕ ∈ V) |
42 | | inidm 3784 |
. . . . . . . . 9
⊢ (ℕ
∩ ℕ) = ℕ |
43 | 37, 38, 39, 41, 41, 42 | off 6810 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → (𝑓 ∘𝑓
∘𝑓 − ℎ):ℕ⟶dom
∫1) |
44 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
45 | 44 | breq2d 4595 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → (0 ≤ (𝐹‘𝑦) ↔ 0 ≤ (𝐹‘𝑥))) |
46 | 45, 44 | ifbieq1d 4059 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
47 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑥) ∈ V |
48 | | c0ex 9913 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
49 | 47, 48 | ifex 4106 |
. . . . . . . . . . . . . 14
⊢ if(0 ≤
(𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V |
50 | 46, 14, 49 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
51 | 50 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
52 | 44 | negeqd 10154 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → -(𝐹‘𝑦) = -(𝐹‘𝑥)) |
53 | 52 | breq2d 4595 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → (0 ≤ -(𝐹‘𝑦) ↔ 0 ≤ -(𝐹‘𝑥))) |
54 | 53, 52 | ifbieq1d 4059 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
55 | | negex 10158 |
. . . . . . . . . . . . . . 15
⊢ -(𝐹‘𝑥) ∈ V |
56 | 55, 48 | ifex 4106 |
. . . . . . . . . . . . . 14
⊢ if(0 ≤
-(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V |
57 | 54, 26, 56 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) = if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
58 | 57 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
59 | 51, 58 | anbi12d 743 |
. . . . . . . . . . 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 11599 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
62 | | 1zzd 11285 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → 1 ∈
ℤ) |
63 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
64 | 40 | mptex 6390 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) ∈ V |
65 | 64 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) ∈ V) |
66 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
67 | 38 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) → (𝑓‘𝑛) ∈ dom
∫1) |
68 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓‘𝑛) ∈ dom ∫1 → (𝑓‘𝑛):ℝ⟶ℝ) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) → (𝑓‘𝑛):ℝ⟶ℝ) |
70 | 69 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) ∧ 𝑥
∈ ℝ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ) |
71 | 70 | an32s 842 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℝ) |
72 | 71 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((𝑓‘𝑛)‘𝑥) ∈ ℂ) |
73 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) |
74 | 72, 73 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)):ℕ⟶ℂ) |
76 | 75 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓:ℕ⟶dom
∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧
𝑥 ∈ ℝ) ∧
((𝑛 ∈ ℕ ↦
((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) ∈ ℂ) |
77 | 39 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) → (ℎ‘𝑛) ∈ dom
∫1) |
78 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘𝑛) ∈ dom ∫1 → (ℎ‘𝑛):ℝ⟶ℝ) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) → (ℎ‘𝑛):ℝ⟶ℝ) |
80 | 79 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑛
∈ ℕ) ∧ 𝑥
∈ ℝ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ) |
81 | 80 | an32s 842 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℝ) |
82 | 81 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑛
∈ ℕ) → ((ℎ‘𝑛)‘𝑥) ∈ ℂ) |
83 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) |
84 | 82, 83 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (𝑛
∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)):ℕ⟶ℂ) |
86 | 85 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓:ℕ⟶dom
∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧
𝑥 ∈ ℝ) ∧
((𝑛 ∈ ℕ ↦
((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) ∈ ℂ) |
87 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:ℕ⟶dom
∫1 → 𝑓
Fn ℕ) |
88 | 38, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → 𝑓 Fn ℕ) |
89 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ:ℕ⟶dom
∫1 → ℎ
Fn ℕ) |
90 | 39, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → ℎ
Fn ℕ) |
91 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (𝑓‘𝑘) = (𝑓‘𝑘)) |
92 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (ℎ‘𝑘) = (ℎ‘𝑘)) |
93 | 88, 90, 41, 41, 42, 91, 92 | ofval 6804 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → ((𝑓
∘𝑓 ∘𝑓 − ℎ)‘𝑘) = ((𝑓‘𝑘) ∘𝑓 − (ℎ‘𝑘))) |
94 | 93 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (((𝑓
∘𝑓 ∘𝑓 − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘𝑓 − (ℎ‘𝑘))‘𝑥)) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) ∧ 𝑥
∈ ℝ) → (((𝑓
∘𝑓 ∘𝑓 − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘) ∘𝑓 − (ℎ‘𝑘))‘𝑥)) |
96 | 38 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (𝑓‘𝑘) ∈ dom
∫1) |
97 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑘) ∈ dom ∫1 → (𝑓‘𝑘):ℝ⟶ℝ) |
98 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑘):ℝ⟶ℝ → (𝑓‘𝑘) Fn ℝ) |
99 | 96, 97, 98 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (𝑓‘𝑘) Fn ℝ) |
100 | 39 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (ℎ‘𝑘) ∈ dom
∫1) |
101 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑘) ∈ dom ∫1 → (ℎ‘𝑘):ℝ⟶ℝ) |
102 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑘):ℝ⟶ℝ → (ℎ‘𝑘) Fn ℝ) |
103 | 100, 101,
102 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → (ℎ‘𝑘) Fn ℝ) |
104 | | reex 9906 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℝ
∈ V |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) → ℝ ∈ V) |
106 | | inidm 3784 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℝ
∩ ℝ) = ℝ |
107 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) ∧ 𝑥
∈ ℝ) → ((𝑓‘𝑘)‘𝑥) = ((𝑓‘𝑘)‘𝑥)) |
108 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) ∧ 𝑥
∈ ℝ) → ((ℎ‘𝑘)‘𝑥) = ((ℎ‘𝑘)‘𝑥)) |
109 | 99, 103, 105, 105, 106, 107, 108 | ofval 6804 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) ∧ 𝑥
∈ ℝ) → (((𝑓‘𝑘) ∘𝑓 − (ℎ‘𝑘))‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥))) |
110 | 95, 109 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑘
∈ ℕ) ∧ 𝑥
∈ ℝ) → (((𝑓
∘𝑓 ∘𝑓 − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥))) |
111 | 110 | an32s 842 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑘
∈ ℕ) → (((𝑓
∘𝑓 ∘𝑓 − ℎ)‘𝑘)‘𝑥) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥))) |
112 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛) = ((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑘)) |
113 | 112 | fveq1d 6105 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥) = (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑘)‘𝑥)) |
114 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) |
115 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑘)‘𝑥) ∈ V |
116 | 113, 114,
115 | fvmpt 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑘)‘𝑥)) |
117 | 116 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (((𝑓
∘𝑓 ∘𝑓 − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑘)‘𝑥)) |
118 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘)) |
119 | 118 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛)‘𝑥) = ((𝑓‘𝑘)‘𝑥)) |
120 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓‘𝑘)‘𝑥) ∈ V |
121 | 119, 73, 120 | fvmpt 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) = ((𝑓‘𝑘)‘𝑥)) |
122 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (ℎ‘𝑛) = (ℎ‘𝑘)) |
123 | 122 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((ℎ‘𝑛)‘𝑥) = ((ℎ‘𝑘)‘𝑥)) |
124 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℎ‘𝑘)‘𝑥) ∈ V |
125 | 123, 83, 124 | fvmpt 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘) = ((ℎ‘𝑘)‘𝑥)) |
126 | 121, 125 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥))) |
127 | 126 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑘
∈ ℕ) → (((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘)) = (((𝑓‘𝑘)‘𝑥) − ((ℎ‘𝑘)‘𝑥))) |
128 | 111, 117,
127 | 3eqtr4d 2654 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (((𝑓
∘𝑓 ∘𝑓 − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘))) |
129 | 128 | adantlr 747 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓:ℕ⟶dom
∫1 ∧ ℎ:ℕ⟶dom ∫1)) ∧
𝑥 ∈ ℝ) ∧
((𝑛 ∈ ℕ ↦
((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))‘𝑘) − ((𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥))‘𝑘))) |
130 | 61, 62, 63, 65, 66, 76, 86, 129 | climsub 14212 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) ⇝ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
131 | 1 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → 𝐹:ℝ⟶ℝ) |
132 | 131 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
133 | | max0sub 11901 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑥) ∈ ℝ → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥)) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥)) |
135 | 134 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥)) |
136 | 130, 135 | breqtrd 4609 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) ∧ ((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
137 | 136 | ex 449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
138 | 60, 137 | sylbid 229 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) ∧ 𝑥
∈ ℝ) → (((𝑛
∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
139 | 138 | ralimdva 2945 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
140 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑓 ∘𝑓
∘𝑓 − ℎ) ∈ V |
141 | | feq1 5939 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑓 ∘𝑓
∘𝑓 − ℎ) → (𝑔:ℕ⟶dom ∫1 ↔
(𝑓
∘𝑓 ∘𝑓 − ℎ):ℕ⟶dom
∫1)) |
142 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ∘𝑓
∘𝑓 − ℎ) → (𝑔‘𝑛) = ((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)) |
143 | 142 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑓 ∘𝑓
∘𝑓 − ℎ) → ((𝑔‘𝑛)‘𝑥) = (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) |
144 | 143 | mpteq2dv 4673 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑓 ∘𝑓
∘𝑓 − ℎ) → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥))) |
145 | 144 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑓 ∘𝑓
∘𝑓 − ℎ) → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
146 | 145 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑓 ∘𝑓
∘𝑓 − ℎ) → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ (((𝑓 ∘𝑓
∘𝑓 − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
147 | 141, 146 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑔 = (𝑓 ∘𝑓
∘𝑓 − ℎ) → ((𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ ((𝑓 ∘𝑓
∘𝑓 − ℎ):ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
(((𝑓
∘𝑓 ∘𝑓 − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
148 | 140, 147 | spcev 3273 |
. . . . . . . 8
⊢ (((𝑓 ∘𝑓
∘𝑓 − ℎ):ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
(((𝑓
∘𝑓 ∘𝑓 − ℎ)‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
149 | 43, 139, 148 | syl6an 566 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → (∀𝑥 ∈ ℝ ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
150 | 35, 149 | syl5bir 232 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1)) → ((∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
151 | 150 | expimpd 627 |
. . . . 5
⊢ (𝜑 → (((𝑓:ℕ⟶dom ∫1 ∧
ℎ:ℕ⟶dom
∫1) ∧ (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
152 | 34, 151 | syl5 33 |
. . . 4
⊢ (𝜑 → (((𝑓:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘𝑟 ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘𝑟 ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
153 | 152 | exlimdvv 1849 |
. . 3
⊢ (𝜑 → (∃𝑓∃ℎ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘𝑟 ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ (ℎ:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘𝑟 ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
154 | 29, 153 | syl5bir 232 |
. 2
⊢ (𝜑 → ((∃𝑓(𝑓:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (𝑓‘𝑛) ∧ (𝑓‘𝑛) ∘𝑟 ≤ (𝑓‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑦), (𝐹‘𝑦), 0))‘𝑥)) ∧ ∃ℎ(ℎ:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (ℎ‘𝑛) ∧ (ℎ‘𝑛) ∘𝑟 ≤ (ℎ‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((ℎ‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑦), -(𝐹‘𝑦), 0))‘𝑥))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
155 | 16, 28, 154 | mp2and 711 |
1
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |