This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mbfi1flimlem

Description: Lemma for mbfi1flim . (Contributed by Mario Carneiro, 5-Sep-2014)

Ref Expression
Hypotheses mbfi1flim.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfi1flimlem.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
Assertion mbfi1flimlem ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 mbfi1flim.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 mbfi1flimlem.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
3 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ dom ∫1 )
68 i1ff ⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ dom ∫1 → ( 𝑓 ‘ 𝑛 ) : ℝ ⟶ ℝ )
69 67 68 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) : ℝ ⟶ ℝ )
70 69 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 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 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( ℎ ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ∈ ℂ )
76 37 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑛 ∈ ℕ ) → ( ℎ ‘ 𝑛 ) ∈ dom ∫1 )
77 i1ff ⊢ ( ( ℎ ‘ 𝑛 ) ∈ dom ∫1 → ( ℎ ‘ 𝑛 ) : ℝ ⟶ ℝ )
78 76 77 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ℎ : ℕ ⟶ dom ∫1 ) ) ∧ 𝑛 ∈ ℕ ) → ( ℎ ‘ 𝑛 ) : ℝ ⟶ ℝ )
79 78 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 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 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 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 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 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 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ 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 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) )