| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mbfi1flim.1 |
⊢ ( 𝜑 → 𝐹 ∈ MblFn ) |
| 2 |
|
mbfi1flimlem.2 |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ ) |
| 3 |
2
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) |
| 4 |
2
|
feqmptd |
⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ) |
| 5 |
4 1
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn ) |
| 6 |
3 5
|
mbfpos |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ∈ MblFn ) |
| 7 |
|
0re |
⊢ 0 ∈ ℝ |
| 8 |
|
ifcl |
⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ℝ ) |
| 9 |
3 7 8
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ℝ ) |
| 10 |
|
max1 |
⊢ ( ( 0 ∈ ℝ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) |
| 11 |
7 3 10
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) |
| 12 |
|
elrege0 |
⊢ ( if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ) |
| 13 |
9 11 12
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ( 0 [,) +∞ ) ) |
| 14 |
13
|
fmpttd |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) ) |
| 15 |
6 14
|
mbfi1fseq |
⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ) |
| 16 |
3
|
renegcld |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → - ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) |
| 17 |
3 5
|
mbfneg |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ - ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn ) |
| 18 |
16 17
|
mbfpos |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ∈ MblFn ) |
| 19 |
|
ifcl |
⊢ ( ( - ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ℝ ) |
| 20 |
16 7 19
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ℝ ) |
| 21 |
|
max1 |
⊢ ( ( 0 ∈ ℝ ∧ - ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) |
| 22 |
7 16 21
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) |
| 23 |
|
elrege0 |
⊢ ( if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ) |
| 24 |
20 22 23
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ ( 0 [,) +∞ ) ) |
| 25 |
24
|
fmpttd |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) ) |
| 26 |
18 25
|
mbfi1fseq |
⊢ ( 𝜑 → ∃ ℎ ( ℎ : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( ℎ ‘ 𝑛 ) ∧ ( ℎ ‘ 𝑛 ) ∘r ≤ ( ℎ ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ) |
| 27 |
|
exdistrv |
⊢ ( ∃ 𝑓 ∃ ℎ ( ( 𝑓 : ℕ ⟶ 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 |
⊢ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) → ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ) |
| 29 |
|
3simpb |
⊢ ( ( ℎ : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( ℎ ‘ 𝑛 ) ∧ ( ℎ ‘ 𝑛 ) ∘r ≤ ( ℎ ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) → ( ℎ : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ) |
| 30 |
28 29
|
anim12i |
⊢ ( ( ( 𝑓 : ℕ ⟶ 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 |
⊢ ( ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ∧ ( ℎ : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ∧ ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ) ) |
| 32 |
30 31
|
sylib |
⊢ ( ( ( 𝑓 : ℕ ⟶ 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 |
⊢ ( ∀ 𝑥 ∈ ℝ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ↔ ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ) |
| 34 |
|
i1fsub |
⊢ ( ( 𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1 ) → ( 𝑥 ∘f − 𝑦 ) ∈ dom ∫1 ) |
| 35 |
34
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ ( 𝑥 ∈ dom ∫1 ∧ 𝑦 ∈ dom ∫1 ) ) → ( 𝑥 ∘f − 𝑦 ) ∈ dom ∫1 ) |
| 36 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) → 𝑓 : ℕ ⟶ dom ∫1 ) |
| 37 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) → ℎ : ℕ ⟶ dom ∫1 ) |
| 38 |
|
nnex |
⊢ ℕ ∈ V |
| 39 |
38
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) → ℕ ∈ V ) |
| 40 |
|
inidm |
⊢ ( ℕ ∩ ℕ ) = ℕ |
| 41 |
35 36 37 39 39 40
|
off |
⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) → ( 𝑓 ∘f ∘f − ℎ ) : ℕ ⟶ dom ∫1 ) |
| 42 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) |
| 43 |
42
|
breq2d |
⊢ ( 𝑦 = 𝑥 → ( 0 ≤ ( 𝐹 ‘ 𝑦 ) ↔ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
| 44 |
43 42
|
ifbieq1d |
⊢ ( 𝑦 = 𝑥 → if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) = if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 45 |
|
eqid |
⊢ ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) |
| 46 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑥 ) ∈ V |
| 47 |
|
c0ex |
⊢ 0 ∈ V |
| 48 |
46 47
|
ifex |
⊢ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V |
| 49 |
44 45 48
|
fvmpt |
⊢ ( 𝑥 ∈ ℝ → ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) = if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 50 |
49
|
breq2d |
⊢ ( 𝑥 ∈ ℝ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ↔ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 51 |
42
|
negeqd |
⊢ ( 𝑦 = 𝑥 → - ( 𝐹 ‘ 𝑦 ) = - ( 𝐹 ‘ 𝑥 ) ) |
| 52 |
51
|
breq2d |
⊢ ( 𝑦 = 𝑥 → ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) ↔ 0 ≤ - ( 𝐹 ‘ 𝑥 ) ) ) |
| 53 |
52 51
|
ifbieq1d |
⊢ ( 𝑦 = 𝑥 → if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) = if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 54 |
|
eqid |
⊢ ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) |
| 55 |
|
negex |
⊢ - ( 𝐹 ‘ 𝑥 ) ∈ V |
| 56 |
55 47
|
ifex |
⊢ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V |
| 57 |
53 54 56
|
fvmpt |
⊢ ( 𝑥 ∈ ℝ → ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) = if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 58 |
57
|
breq2d |
⊢ ( 𝑥 ∈ ℝ → ( ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ↔ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 59 |
50 58
|
anbi12d |
⊢ ( 𝑥 ∈ ℝ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ↔ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 60 |
59
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ↔ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 61 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
| 62 |
|
1zzd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → 1 ∈ ℤ ) |
| 63 |
|
simprl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 64 |
38
|
mptex |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ V |
| 65 |
64
|
a1i |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ V ) |
| 66 |
|
simprr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 67 |
36
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ dom ∫1 ) |
| 68 |
|
i1ff |
⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ dom ∫1 → ( 𝑓 ‘ 𝑛 ) : ℝ ⟶ ℝ ) |
| 69 |
67 68
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) : ℝ ⟶ ℝ ) |
| 70 |
69
|
ffvelrnda |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ) |
| 71 |
70
|
an32s |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ) |
| 72 |
71
|
recnd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ ) |
| 73 |
72
|
fmpttd |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) : ℕ ⟶ ℂ ) |
| 74 |
73
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) : ℕ ⟶ ℂ ) |
| 75 |
74
|
ffvelrnda |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ∈ ℂ ) |
| 76 |
37
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑛 ∈ ℕ ) → ( ℎ ‘ 𝑛 ) ∈ dom ∫1 ) |
| 77 |
|
i1ff |
⊢ ( ( ℎ ‘ 𝑛 ) ∈ dom ∫1 → ( ℎ ‘ 𝑛 ) : ℝ ⟶ ℝ ) |
| 78 |
76 77
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑛 ∈ ℕ ) → ( ℎ ‘ 𝑛 ) : ℝ ⟶ ℝ ) |
| 79 |
78
|
ffvelrnda |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ) |
| 80 |
79
|
an32s |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ) |
| 81 |
80
|
recnd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ ) |
| 82 |
81
|
fmpttd |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) : ℕ ⟶ ℂ ) |
| 83 |
82
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) : ℕ ⟶ ℂ ) |
| 84 |
83
|
ffvelrnda |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ∈ ℂ ) |
| 85 |
36
|
ffnd |
⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) → 𝑓 Fn ℕ ) |
| 86 |
37
|
ffnd |
⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) → ℎ Fn ℕ ) |
| 87 |
|
eqidd |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) ) |
| 88 |
|
eqidd |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ℎ ‘ 𝑘 ) = ( ℎ ‘ 𝑘 ) ) |
| 89 |
85 86 39 39 40 87 88
|
ofval |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑘 ) = ( ( 𝑓 ‘ 𝑘 ) ∘f − ( ℎ ‘ 𝑘 ) ) ) |
| 90 |
89
|
fveq1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑘 ) ‘ 𝑥 ) = ( ( ( 𝑓 ‘ 𝑘 ) ∘f − ( ℎ ‘ 𝑘 ) ) ‘ 𝑥 ) ) |
| 91 |
90
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑘 ) ‘ 𝑥 ) = ( ( ( 𝑓 ‘ 𝑘 ) ∘f − ( ℎ ‘ 𝑘 ) ) ‘ 𝑥 ) ) |
| 92 |
36
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ dom ∫1 ) |
| 93 |
|
i1ff |
⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ dom ∫1 → ( 𝑓 ‘ 𝑘 ) : ℝ ⟶ ℝ ) |
| 94 |
|
ffn |
⊢ ( ( 𝑓 ‘ 𝑘 ) : ℝ ⟶ ℝ → ( 𝑓 ‘ 𝑘 ) Fn ℝ ) |
| 95 |
92 93 94
|
3syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) Fn ℝ ) |
| 96 |
37
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ℎ ‘ 𝑘 ) ∈ dom ∫1 ) |
| 97 |
|
i1ff |
⊢ ( ( ℎ ‘ 𝑘 ) ∈ dom ∫1 → ( ℎ ‘ 𝑘 ) : ℝ ⟶ ℝ ) |
| 98 |
|
ffn |
⊢ ( ( ℎ ‘ 𝑘 ) : ℝ ⟶ ℝ → ( ℎ ‘ 𝑘 ) Fn ℝ ) |
| 99 |
96 97 98
|
3syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ℎ ‘ 𝑘 ) Fn ℝ ) |
| 100 |
|
reex |
⊢ ℝ ∈ V |
| 101 |
100
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) → ℝ ∈ V ) |
| 102 |
|
inidm |
⊢ ( ℝ ∩ ℝ ) = ℝ |
| 103 |
|
eqidd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑥 ) ) |
| 104 |
|
eqidd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ℎ ‘ 𝑘 ) ‘ 𝑥 ) = ( ( ℎ ‘ 𝑘 ) ‘ 𝑥 ) ) |
| 105 |
95 99 101 101 102 103 104
|
ofval |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑓 ‘ 𝑘 ) ∘f − ( ℎ ‘ 𝑘 ) ) ‘ 𝑥 ) = ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑥 ) − ( ( ℎ ‘ 𝑘 ) ‘ 𝑥 ) ) ) |
| 106 |
91 105
|
eqtrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑘 ) ‘ 𝑥 ) = ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑥 ) − ( ( ℎ ‘ 𝑘 ) ‘ 𝑥 ) ) ) |
| 107 |
106
|
an32s |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑘 ) ‘ 𝑥 ) = ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑥 ) − ( ( ℎ ‘ 𝑘 ) ‘ 𝑥 ) ) ) |
| 108 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) = ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑘 ) ) |
| 109 |
108
|
fveq1d |
⊢ ( 𝑛 = 𝑘 → ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) = ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑘 ) ‘ 𝑥 ) ) |
| 110 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) |
| 111 |
|
fvex |
⊢ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑘 ) ‘ 𝑥 ) ∈ V |
| 112 |
109 110 111
|
fvmpt |
⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑘 ) ‘ 𝑥 ) ) |
| 113 |
112
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑘 ) ‘ 𝑥 ) ) |
| 114 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑘 ) ) |
| 115 |
114
|
fveq1d |
⊢ ( 𝑛 = 𝑘 → ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑥 ) ) |
| 116 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) |
| 117 |
|
fvex |
⊢ ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑥 ) ∈ V |
| 118 |
115 116 117
|
fvmpt |
⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑥 ) ) |
| 119 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( ℎ ‘ 𝑛 ) = ( ℎ ‘ 𝑘 ) ) |
| 120 |
119
|
fveq1d |
⊢ ( 𝑛 = 𝑘 → ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) = ( ( ℎ ‘ 𝑘 ) ‘ 𝑥 ) ) |
| 121 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) |
| 122 |
|
fvex |
⊢ ( ( ℎ ‘ 𝑘 ) ‘ 𝑥 ) ∈ V |
| 123 |
120 121 122
|
fvmpt |
⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( ℎ ‘ 𝑘 ) ‘ 𝑥 ) ) |
| 124 |
118 123
|
oveq12d |
⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ) = ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑥 ) − ( ( ℎ ‘ 𝑘 ) ‘ 𝑥 ) ) ) |
| 125 |
124
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ) = ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑥 ) − ( ( ℎ ‘ 𝑘 ) ‘ 𝑥 ) ) ) |
| 126 |
107 113 125
|
3eqtr4d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ) ) |
| 127 |
126
|
adantlr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ) ) |
| 128 |
61 62 63 65 66 75 84 127
|
climsub |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 129 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) → 𝐹 : ℝ ⟶ ℝ ) |
| 130 |
129
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
| 131 |
|
max0sub |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ → ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝐹 ‘ 𝑥 ) ) |
| 132 |
130 131
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) → ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝐹 ‘ 𝑥 ) ) |
| 133 |
132
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝐹 ‘ 𝑥 ) ) |
| 134 |
128 133
|
breqtrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) |
| 135 |
134
|
ex |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) |
| 136 |
60 135
|
sylbid |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) |
| 137 |
136
|
ralimdva |
⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) → ( ∀ 𝑥 ∈ ℝ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) |
| 138 |
|
ovex |
⊢ ( 𝑓 ∘f ∘f − ℎ ) ∈ V |
| 139 |
|
feq1 |
⊢ ( 𝑔 = ( 𝑓 ∘f ∘f − ℎ ) → ( 𝑔 : ℕ ⟶ dom ∫1 ↔ ( 𝑓 ∘f ∘f − ℎ ) : ℕ ⟶ dom ∫1 ) ) |
| 140 |
|
fveq1 |
⊢ ( 𝑔 = ( 𝑓 ∘f ∘f − ℎ ) → ( 𝑔 ‘ 𝑛 ) = ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ) |
| 141 |
140
|
fveq1d |
⊢ ( 𝑔 = ( 𝑓 ∘f ∘f − ℎ ) → ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) |
| 142 |
141
|
mpteq2dv |
⊢ ( 𝑔 = ( 𝑓 ∘f ∘f − ℎ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ) |
| 143 |
142
|
breq1d |
⊢ ( 𝑔 = ( 𝑓 ∘f ∘f − ℎ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) |
| 144 |
143
|
ralbidv |
⊢ ( 𝑔 = ( 𝑓 ∘f ∘f − ℎ ) → ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) |
| 145 |
139 144
|
anbi12d |
⊢ ( 𝑔 = ( 𝑓 ∘f ∘f − ℎ ) → ( ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝑓 ∘f ∘f − ℎ ) : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 146 |
138 145
|
spcev |
⊢ ( ( ( 𝑓 ∘f ∘f − ℎ ) : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓 ∘f ∘f − ℎ ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) |
| 147 |
41 137 146
|
syl6an |
⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) → ( ∀ 𝑥 ∈ ℝ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 148 |
33 147
|
syl5bir |
⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) → ( ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 149 |
148
|
expimpd |
⊢ ( 𝜑 → ( ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ∧ ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 150 |
32 149
|
syl5 |
⊢ ( 𝜑 → ( ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ∧ ( ℎ : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( ℎ ‘ 𝑛 ) ∧ ( ℎ ‘ 𝑛 ) ∘r ≤ ( ℎ ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 151 |
150
|
exlimdvv |
⊢ ( 𝜑 → ( ∃ 𝑓 ∃ ℎ ( ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑓 ‘ 𝑛 ) ∧ ( 𝑓 ‘ 𝑛 ) ∘r ≤ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ∧ ( ℎ : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( ℎ ‘ 𝑛 ) ∧ ( ℎ ‘ 𝑛 ) ∘r ≤ ( ℎ ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑦 ) , - ( 𝐹 ‘ 𝑦 ) , 0 ) ) ‘ 𝑥 ) ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 152 |
27 151
|
syl5bir |
⊢ ( 𝜑 → ( ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ 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 |
⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) |