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 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 ) ) → ( 𝑓ff ) : ℕ ⟶ 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 ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ V
65 64 a1i ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹𝑥 ) , ( 𝐹𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹𝑥 ) , - ( 𝐹𝑥 ) , 0 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ 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 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑓ff ) ‘ 𝑘 ) = ( ( 𝑓𝑘 ) ∘f − ( 𝑘 ) ) )
90 89 fveq1d ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑓ff ) ‘ 𝑘 ) ‘ 𝑥 ) = ( ( ( 𝑓𝑘 ) ∘f − ( 𝑘 ) ) ‘ 𝑥 ) )
91 90 adantr ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 : ℕ ⟶ dom ∫1 ) ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑓ff ) ‘ 𝑘 ) ‘ 𝑥 ) = ( ( ( 𝑓𝑘 ) ∘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 ) ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑓ff ) ‘ 𝑘 ) ‘ 𝑥 ) = ( ( ( 𝑓𝑘 ) ‘ 𝑥 ) − ( ( 𝑘 ) ‘ 𝑥 ) ) )
107 106 an32s ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑓ff ) ‘ 𝑘 ) ‘ 𝑥 ) = ( ( ( 𝑓𝑘 ) ‘ 𝑥 ) − ( ( 𝑘 ) ‘ 𝑥 ) ) )
108 fveq2 ( 𝑛 = 𝑘 → ( ( 𝑓ff ) ‘ 𝑛 ) = ( ( 𝑓ff ) ‘ 𝑘 ) )
109 108 fveq1d ( 𝑛 = 𝑘 → ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) = ( ( ( 𝑓ff ) ‘ 𝑘 ) ‘ 𝑥 ) )
110 eqid ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) )
111 fvex ( ( ( 𝑓ff ) ‘ 𝑘 ) ‘ 𝑥 ) ∈ V
112 109 110 111 fvmpt ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( ( 𝑓ff ) ‘ 𝑘 ) ‘ 𝑥 ) )
113 112 adantl ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( ( 𝑓ff ) ‘ 𝑘 ) ‘ 𝑥 ) )
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 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ) )
127 126 adantlr ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹𝑥 ) , ( 𝐹𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹𝑥 ) , - ( 𝐹𝑥 ) , 0 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ) )
128 61 62 63 65 66 75 84 127 climsub ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹𝑥 ) , ( 𝐹𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹𝑥 ) , - ( 𝐹𝑥 ) , 0 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 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 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) )
135 134 ex ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ ( 𝐹𝑥 ) , ( 𝐹𝑥 ) , 0 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ) ‘ 𝑥 ) ) ⇝ if ( 0 ≤ - ( 𝐹𝑥 ) , - ( 𝐹𝑥 ) , 0 ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ) )
136 60 135 sylbid ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 : ℕ ⟶ dom ∫1 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹𝑦 ) , ( 𝐹𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹𝑦 ) , - ( 𝐹𝑦 ) , 0 ) ) ‘ 𝑥 ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ) )
137 136 ralimdva ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ dom ∫1 : ℕ ⟶ dom ∫1 ) ) → ( ∀ 𝑥 ∈ ℝ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹𝑦 ) , ( 𝐹𝑦 ) , 0 ) ) ‘ 𝑥 ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ) ‘ 𝑥 ) ) ⇝ ( ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹𝑦 ) , - ( 𝐹𝑦 ) , 0 ) ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ) )
138 ovex ( 𝑓ff ) ∈ V
139 feq1 ( 𝑔 = ( 𝑓ff ) → ( 𝑔 : ℕ ⟶ dom ∫1 ↔ ( 𝑓ff ) : ℕ ⟶ dom ∫1 ) )
140 fveq1 ( 𝑔 = ( 𝑓ff ) → ( 𝑔𝑛 ) = ( ( 𝑓ff ) ‘ 𝑛 ) )
141 140 fveq1d ( 𝑔 = ( 𝑓ff ) → ( ( 𝑔𝑛 ) ‘ 𝑥 ) = ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) )
142 141 mpteq2dv ( 𝑔 = ( 𝑓ff ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑔𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) )
143 142 breq1d ( 𝑔 = ( 𝑓ff ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑔𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ↔ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ) )
144 143 ralbidv ( 𝑔 = ( 𝑓ff ) → ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ↔ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ) )
145 139 144 anbi12d ( 𝑔 = ( 𝑓ff ) → ( ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ) ↔ ( ( 𝑓ff ) : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ) ) )
146 138 145 spcev ( ( ( 𝑓ff ) : ℕ ⟶ dom ∫1 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑓ff ) ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ 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 ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ) )