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 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) |