Metamath Proof Explorer

Theorem stoweidlem17

Description: This lemma proves that the function g (as defined in BrosowskiDeutsh p. 91, at the end of page 91) belongs to the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem17.1 ⊢ Ⅎ 𝑡 𝜑
stoweidlem17.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
stoweidlem17.3 ⊢ ( 𝜑 → 𝑋 : ( 0 ... 𝑁 ) ⟶ 𝐴 )
stoweidlem17.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem17.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem17.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem17.7 ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
stoweidlem17.8 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
Assertion stoweidlem17 ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 stoweidlem17.1 ⊢ Ⅎ 𝑡 𝜑
2 stoweidlem17.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 stoweidlem17.3 ⊢ ( 𝜑 → 𝑋 : ( 0 ... 𝑁 ) ⟶ 𝐴 )
4 stoweidlem17.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
5 stoweidlem17.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
6 stoweidlem17.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
7 stoweidlem17.7 ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
8 stoweidlem17.8 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
9 2 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
10 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
11 9 10 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
12 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 𝑁 ∈ ( 0 ... 𝑁 ) )
13 11 12 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
14 13 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝑁 ∈ ( 0 ... 𝑁 ) ) )
15 eleq1 ⊢ ( 𝑛 = 0 → ( 𝑛 ∈ ( 0 ... 𝑁 ) ↔ 0 ∈ ( 0 ... 𝑁 ) ) )
16 15 anbi2d ⊢ ( 𝑛 = 0 → ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 0 ∈ ( 0 ... 𝑁 ) ) ) )
17 oveq2 ⊢ ( 𝑛 = 0 → ( 0 ... 𝑛 ) = ( 0 ... 0 ) )
18 17 sumeq1d ⊢ ( 𝑛 = 0 → Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = Σ 𝑖 ∈ ( 0 ... 0 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
19 18 mpteq2dv ⊢ ( 𝑛 = 0 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 0 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
20 19 eleq1d ⊢ ( 𝑛 = 0 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 0 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
21 16 20 imbi12d ⊢ ( 𝑛 = 0 → ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 0 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 0 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
22 eleq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ∈ ( 0 ... 𝑁 ) ↔ 𝑚 ∈ ( 0 ... 𝑁 ) ) )
23 22 anbi2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ) )
24 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 0 ... 𝑛 ) = ( 0 ... 𝑚 ) )
25 24 sumeq1d ⊢ ( 𝑛 = 𝑚 → Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
26 25 mpteq2dv ⊢ ( 𝑛 = 𝑚 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
27 26 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
28 23 27 imbi12d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
29 eleq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
30 29 anbi2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) )
31 oveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 0 ... 𝑛 ) = ( 0 ... ( 𝑚 + 1 ) ) )
32 31 sumeq1d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
33 32 mpteq2dv ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
34 33 eleq1d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
35 30 34 imbi12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
36 eleq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∈ ( 0 ... 𝑁 ) ↔ 𝑁 ∈ ( 0 ... 𝑁 ) ) )
37 36 anbi2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑁 ∈ ( 0 ... 𝑁 ) ) ) )
38 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
39 38 sumeq1d ⊢ ( 𝑛 = 𝑁 → Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
40 39 mpteq2dv ⊢ ( 𝑛 = 𝑁 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
41 40 eleq1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
42 37 41 imbi12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
43 0z ⊢ 0 ∈ ℤ
44 fzsn ⊢ ( 0 ∈ ℤ → ( 0 ... 0 ) = { 0 } )
45 43 44 ax-mp ⊢ ( 0 ... 0 ) = { 0 }
46 45 sumeq1i ⊢ Σ 𝑖 ∈ ( 0 ... 0 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = Σ 𝑖 ∈ { 0 } ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
47 46 mpteq2i ⊢ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 0 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ { 0 } ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
48 7 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝐸 ∈ ℝ )
49 48 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝐸 ∈ ℂ )
50 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
51 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
52 0re ⊢ 0 ∈ ℝ
53 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
54 ltle ⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < 𝑁 → 0 ≤ 𝑁 ) )
55 52 53 54 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 0 < 𝑁 → 0 ≤ 𝑁 ) )
56 51 55 mpd ⊢ ( 𝑁 ∈ ℕ → 0 ≤ 𝑁 )
57 50 56 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
58 2 57 syl ⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
59 43 eluz1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
60 58 59 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
61 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑁 ) )
62 60 61 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
63 3 62 ffvelrnd ⊢ ( 𝜑 → ( 𝑋 ‘ 0 ) ∈ 𝐴 )
64 feq1 ⊢ ( 𝑓 = ( 𝑋 ‘ 0 ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝑋 ‘ 0 ) : 𝑇 ⟶ ℝ ) )
65 64 imbi2d ⊢ ( 𝑓 = ( 𝑋 ‘ 0 ) → ( ( 𝜑 → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( 𝜑 → ( 𝑋 ‘ 0 ) : 𝑇 ⟶ ℝ ) ) )
66 8 expcom ⊢ ( 𝑓 ∈ 𝐴 → ( 𝜑 → 𝑓 : 𝑇 ⟶ ℝ ) )
67 65 66 vtoclga ⊢ ( ( 𝑋 ‘ 0 ) ∈ 𝐴 → ( 𝜑 → ( 𝑋 ‘ 0 ) : 𝑇 ⟶ ℝ ) )
68 63 67 mpcom ⊢ ( 𝜑 → ( 𝑋 ‘ 0 ) : 𝑇 ⟶ ℝ )
69 68 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) ∈ ℝ )
70 69 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) ∈ ℂ )
71 49 70 mulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐸 · ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) ) ∈ ℂ )
72 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 0 ) )
73 72 fveq1d ⊢ ( 𝑖 = 0 → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) )
74 73 oveq2d ⊢ ( 𝑖 = 0 → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝐸 · ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) ) )
75 74 sumsn ⊢ ( ( 0 ∈ ℤ ∧ ( 𝐸 · ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) ) ∈ ℂ ) → Σ 𝑖 ∈ { 0 } ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝐸 · ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) ) )
76 43 71 75 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ { 0 } ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝐸 · ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) ) )
77 1 76 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ { 0 } ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) ) ) )
78 47 77 eqtrid ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 0 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) ) ) )
79 1 5 6 8 7 63 stoweidlem2 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ 0 ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
80 78 79 eqeltrd ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 0 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
81 80 adantr ⊢ ( ( 𝜑 ∧ 0 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 0 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
82 eqidd ⊢ ( 𝑟 = 𝑡 → 𝐸 = 𝐸 )
83 82 cbvmptv ⊢ ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) = ( 𝑡 ∈ 𝑇 ↦ 𝐸 )
84 83 eqcomi ⊢ ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) = ( 𝑟 ∈ 𝑇 ↦ 𝐸 )
85 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
86 84 82 85 48 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) = 𝐸 )
87 86 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) = ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) )
88 1 87 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) )
89 88 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) )
90 3 ffvelrnda ⊢ ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ ( 𝑚 + 1 ) ) ∈ 𝐴 )
91 simpl ⊢ ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → 𝜑 )
92 id ⊢ ( 𝑥 = 𝐸 → 𝑥 = 𝐸 )
93 92 mpteq2dv ⊢ ( 𝑥 = 𝐸 → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) = ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) )
94 93 eleq1d ⊢ ( 𝑥 = 𝐸 → ( ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ) )
95 94 imbi2d ⊢ ( 𝑥 = 𝐸 → ( ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ) ↔ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ) ) )
96 6 expcom ⊢ ( 𝑥 ∈ ℝ → ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ) )
97 95 96 vtoclga ⊢ ( 𝐸 ∈ ℝ → ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ) )
98 7 97 mpcom ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 )
99 98 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 )
100 fveq1 ⊢ ( 𝑔 = ( 𝑋 ‘ ( 𝑚 + 1 ) ) → ( 𝑔 ‘ 𝑡 ) = ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) )
101 100 oveq2d ⊢ ( 𝑔 = ( 𝑋 ‘ ( 𝑚 + 1 ) ) → ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) )
102 101 mpteq2dv ⊢ ( 𝑔 = ( 𝑋 ‘ ( 𝑚 + 1 ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) )
103 102 eleq1d ⊢ ( 𝑔 = ( 𝑋 ‘ ( 𝑚 + 1 ) ) → ( ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
104 103 imbi2d ⊢ ( 𝑔 = ( 𝑋 ‘ ( 𝑚 + 1 ) ) → ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
105 83 eleq1i ⊢ ( ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 )
106 fveq1 ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) → ( 𝑓 ‘ 𝑡 ) = ( ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) )
107 83 fveq1i ⊢ ( ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) = ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 )
108 106 107 eqtrdi ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) → ( 𝑓 ‘ 𝑡 ) = ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) )
109 108 oveq1d ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
110 109 mpteq2dv ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
111 110 eleq1d ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
112 111 imbi2d ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) → ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
113 5 3com12 ⊢ ( ( 𝑓 ∈ 𝐴 ∧ 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
114 113 3expib ⊢ ( 𝑓 ∈ 𝐴 → ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
115 112 114 vtoclga ⊢ ( ( 𝑟 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 → ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
116 105 115 sylbir ⊢ ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 → ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
117 116 3impib ⊢ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ∧ 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
118 117 3com13 ⊢ ( ( 𝑔 ∈ 𝐴 ∧ 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
119 118 3expib ⊢ ( 𝑔 ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
120 104 119 vtoclga ⊢ ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
121 120 3impib ⊢ ( ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ∈ 𝐴 ∧ 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
122 90 91 99 121 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ 𝐸 ) ‘ 𝑡 ) · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
123 89 122 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
124 123 ad2antll ⊢ ( ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) ) → ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
125 simprrl ⊢ ( ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) ) → 𝜑 )
126 simpl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → 𝑚 ∈ ℕ0 )
127 simprl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → 𝜑 )
128 2 ad2antrl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ )
129 128 nnnn0d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
130 nn0re ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℝ )
131 130 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → 𝑚 ∈ ℝ )
132 peano2nn0 ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ0 )
133 132 nn0red ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℝ )
134 133 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 + 1 ) ∈ ℝ )
135 2 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
136 135 ad2antrl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → 𝑁 ∈ ℝ )
137 lep1 ⊢ ( 𝑚 ∈ ℝ → 𝑚 ≤ ( 𝑚 + 1 ) )
138 126 130 137 3syl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → 𝑚 ≤ ( 𝑚 + 1 ) )
139 elfzle2 ⊢ ( ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) → ( 𝑚 + 1 ) ≤ 𝑁 )
140 139 ad2antll ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 + 1 ) ≤ 𝑁 )
141 131 134 136 138 140 letrd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → 𝑚 ≤ 𝑁 )
142 elfz2nn0 ⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑚 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑚 ≤ 𝑁 ) )
143 126 129 141 142 syl3anbrc ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → 𝑚 ∈ ( 0 ... 𝑁 ) )
144 126 127 143 jca32 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ) )
145 144 adantl ⊢ ( ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) ) → ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ) )
146 pm3.31 ⊢ ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) → ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
147 146 adantr ⊢ ( ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) ) → ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
148 145 147 mpd ⊢ ( ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
149 fveq2 ⊢ ( 𝑟 = 𝑡 → ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) = ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) )
150 149 oveq2d ⊢ ( 𝑟 = 𝑡 → ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) = ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) )
151 150 cbvmptv ⊢ ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) )
152 151 eleq1i ⊢ ( ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
153 fveq1 ⊢ ( 𝑔 = ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) → ( 𝑔 ‘ 𝑡 ) = ( ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) ‘ 𝑡 ) )
154 151 fveq1i ⊢ ( ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) ‘ 𝑡 ) = ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 )
155 153 154 eqtrdi ⊢ ( 𝑔 = ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) → ( 𝑔 ‘ 𝑡 ) = ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) )
156 155 oveq2d ⊢ ( 𝑔 = ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) → ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) = ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) )
157 156 mpteq2dv ⊢ ( 𝑔 = ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )
158 157 eleq1d ⊢ ( 𝑔 = ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) → ( ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
159 158 imbi2d ⊢ ( 𝑔 = ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) → ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
160 fveq2 ⊢ ( 𝑟 = 𝑡 → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) = ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
161 160 oveq2d ⊢ ( 𝑟 = 𝑡 → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) = ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
162 161 sumeq2sdv ⊢ ( 𝑟 = 𝑡 → Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) = Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
163 162 cbvmptv ⊢ ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
164 163 eleq1i ⊢ ( ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
165 fveq1 ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) → ( 𝑓 ‘ 𝑡 ) = ( ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) ‘ 𝑡 ) )
166 163 fveq1i ⊢ ( ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) ‘ 𝑡 ) = ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 )
167 165 166 eqtrdi ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) → ( 𝑓 ‘ 𝑡 ) = ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) )
168 167 oveq1d ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) = ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) )
169 168 mpteq2dv ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) )
170 169 eleq1d ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
171 170 imbi2d ⊢ ( 𝑓 = ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) → ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
172 4 3com12 ⊢ ( ( 𝑓 ∈ 𝐴 ∧ 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
173 172 3expib ⊢ ( 𝑓 ∈ 𝐴 → ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
174 171 173 vtoclga ⊢ ( ( 𝑟 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑟 ) ) ) ∈ 𝐴 → ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
175 164 174 sylbir ⊢ ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 → ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
176 175 3impib ⊢ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ∧ 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
177 176 3com13 ⊢ ( ( 𝑔 ∈ 𝐴 ∧ 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
178 177 3expib ⊢ ( 𝑔 ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
179 159 178 vtoclga ⊢ ( ( 𝑟 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑟 ) ) ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
180 152 179 sylbir ⊢ ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
181 180 3impib ⊢ ( ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 ∧ 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
182 124 125 148 181 syl3anc ⊢ ( ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
183 3anass ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) )
184 183 biimpri ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
185 184 adantl ⊢ ( ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) ) → ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
186 nfv ⊢ Ⅎ 𝑡 𝑚 ∈ ℕ0
187 nfv ⊢ Ⅎ 𝑡 ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 )
188 186 1 187 nf3an ⊢ Ⅎ 𝑡 ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) )
189 simpr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
190 fzfid ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 0 ... 𝑚 ) ∈ Fin )
191 7 3ad2ant2 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → 𝐸 ∈ ℝ )
192 191 adantr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝐸 ∈ ℝ )
193 192 adantr ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → 𝐸 ∈ ℝ )
194 fzelp1 ⊢ ( 𝑖 ∈ ( 0 ... 𝑚 ) → 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) )
195 194 anim2i ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) )
196 an32 ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) ↔ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) ∧ 𝑡 ∈ 𝑇 ) )
197 195 196 sylib ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) ∧ 𝑡 ∈ 𝑇 ) )
198 3 3ad2ant2 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → 𝑋 : ( 0 ... 𝑁 ) ⟶ 𝐴 )
199 198 adantr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) → 𝑋 : ( 0 ... 𝑁 ) ⟶ 𝐴 )
200 elfzuz3 ⊢ ( ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) )
201 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) → ( 0 ... ( 𝑚 + 1 ) ) ⊆ ( 0 ... 𝑁 ) )
202 200 201 syl ⊢ ( ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) → ( 0 ... ( 𝑚 + 1 ) ) ⊆ ( 0 ... 𝑁 ) )
203 202 sselda ⊢ ( ( ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
204 203 3ad2antl3 ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
205 199 204 ffvelrnd ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) → ( 𝑋 ‘ 𝑖 ) ∈ 𝐴 )
206 simpl2 ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) → 𝜑 )
207 feq1 ⊢ ( 𝑓 = ( 𝑋 ‘ 𝑖 ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
208 207 imbi2d ⊢ ( 𝑓 = ( 𝑋 ‘ 𝑖 ) → ( ( 𝜑 → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( 𝜑 → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) ) )
209 208 66 vtoclga ⊢ ( ( 𝑋 ‘ 𝑖 ) ∈ 𝐴 → ( 𝜑 → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
210 205 206 209 sylc ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
211 210 ffvelrnda ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
212 197 211 syl ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
213 193 212 remulcld ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
214 190 213 fsumrecl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
215 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
216 215 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
217 189 214 216 syl2anc ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
218 217 oveq1d ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) = ( Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) )
219 3simpc ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
220 219 adantr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
221 feq1 ⊢ ( 𝑓 = ( 𝑋 ‘ ( 𝑚 + 1 ) ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝑋 ‘ ( 𝑚 + 1 ) ) : 𝑇 ⟶ ℝ ) )
222 221 imbi2d ⊢ ( 𝑓 = ( 𝑋 ‘ ( 𝑚 + 1 ) ) → ( ( 𝜑 → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( 𝜑 → ( 𝑋 ‘ ( 𝑚 + 1 ) ) : 𝑇 ⟶ ℝ ) ) )
223 222 66 vtoclga ⊢ ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ∈ 𝐴 → ( 𝜑 → ( 𝑋 ‘ ( 𝑚 + 1 ) ) : 𝑇 ⟶ ℝ ) )
224 90 91 223 sylc ⊢ ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ ( 𝑚 + 1 ) ) : 𝑇 ⟶ ℝ )
225 220 224 syl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑋 ‘ ( 𝑚 + 1 ) ) : 𝑇 ⟶ ℝ )
226 225 189 ffvelrnd ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ∈ ℝ )
227 192 226 remulcld ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ∈ ℝ )
228 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) )
229 228 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ∈ ℝ ) → ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) = ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) )
230 189 227 229 syl2anc ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) = ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) )
231 230 oveq2d ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) = ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) )
232 elfzuz ⊢ ( ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) → ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
233 232 3ad2ant3 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
234 233 adantr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
235 192 adantr ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) → 𝐸 ∈ ℝ )
236 211 an32s ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
237 remulcl ⊢ ( ( 𝐸 ∈ ℝ ∧ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
238 237 recnd ⊢ ( ( 𝐸 ∈ ℝ ∧ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℂ )
239 235 236 238 syl2anc ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℂ )
240 fveq2 ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ ( 𝑚 + 1 ) ) )
241 240 fveq1d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) )
242 241 oveq2d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) )
243 234 239 242 fsumm1 ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( Σ 𝑖 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) )
244 nn0cn ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℂ )
245 244 3ad2ant1 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → 𝑚 ∈ ℂ )
246 245 adantr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝑚 ∈ ℂ )
247 1cnd ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → 1 ∈ ℂ )
248 246 247 pncand ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
249 248 oveq2d ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) = ( 0 ... 𝑚 ) )
250 249 sumeq1d ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
251 250 oveq1d ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( Σ 𝑖 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) = ( Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) )
252 243 251 eqtrd ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) )
253 218 231 252 3eqtr4rd ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) )
254 188 253 mpteq2da ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )
255 254 eleq1d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
256 185 255 syl ⊢ ( ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) + ( ( 𝑡 ∈ 𝑇 ↦ ( 𝐸 · ( ( 𝑋 ‘ ( 𝑚 + 1 ) ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
257 182 256 mpbird ⊢ ( ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
258 257 exp32 ⊢ ( ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) → ( 𝑚 ∈ ℕ0 → ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
259 258 pm2.86i ⊢ ( 𝑚 ∈ ℕ0 → ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) → ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... ( 𝑚 + 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
260 21 28 35 42 81 259 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑁 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
261 9 14 260 sylc ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 )