Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem17 Structured version   Visualization version   GIF version

Theorem stoweidlem17 45328
Description: This lemma proves that the function 𝑔 (as defined in [BrosowskiDeutsh] p. 91, at the end of page 91) belongs to the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem17.1 β„²π‘‘πœ‘
stoweidlem17.2 (πœ‘ β†’ 𝑁 ∈ β„•)
stoweidlem17.3 (πœ‘ β†’ 𝑋:(0...𝑁)⟢𝐴)
stoweidlem17.4 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
stoweidlem17.5 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
stoweidlem17.6 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴)
stoweidlem17.7 (πœ‘ β†’ 𝐸 ∈ ℝ)
stoweidlem17.8 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
Assertion
Ref Expression
stoweidlem17 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
Distinct variable groups:   𝑓,𝑔,𝑖,𝑑,𝐸   𝐴,𝑓,𝑔   𝑇,𝑓,𝑔,𝑖,𝑑   𝑓,𝑋,𝑔,𝑖,𝑑   πœ‘,𝑓,𝑔,𝑖   𝑖,𝑁,𝑑   π‘₯,𝑑,𝐸   π‘₯,𝐴   π‘₯,𝑇   πœ‘,π‘₯
Allowed substitution hints:   πœ‘(𝑑)   𝐴(𝑑,𝑖)   𝑁(π‘₯,𝑓,𝑔)   𝑋(π‘₯)

Proof of Theorem stoweidlem17
Dummy variables π‘š π‘Ÿ 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem17.2 . . 3 (πœ‘ β†’ 𝑁 ∈ β„•)
21nnnn0d 12554 . 2 (πœ‘ β†’ 𝑁 ∈ β„•0)
3 nn0uz 12886 . . . . 5 β„•0 = (β„€β‰₯β€˜0)
42, 3eleqtrdi 2838 . . . 4 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜0))
5 eluzfz2 13533 . . . 4 (𝑁 ∈ (β„€β‰₯β€˜0) β†’ 𝑁 ∈ (0...𝑁))
64, 5syl 17 . . 3 (πœ‘ β†’ 𝑁 ∈ (0...𝑁))
76ancli 548 . 2 (πœ‘ β†’ (πœ‘ ∧ 𝑁 ∈ (0...𝑁)))
8 eleq1 2816 . . . . 5 (𝑛 = 0 β†’ (𝑛 ∈ (0...𝑁) ↔ 0 ∈ (0...𝑁)))
98anbi2d 628 . . . 4 (𝑛 = 0 β†’ ((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) ↔ (πœ‘ ∧ 0 ∈ (0...𝑁))))
10 oveq2 7422 . . . . . . 7 (𝑛 = 0 β†’ (0...𝑛) = (0...0))
1110sumeq1d 15671 . . . . . 6 (𝑛 = 0 β†’ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
1211mpteq2dv 5244 . . . . 5 (𝑛 = 0 β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))))
1312eleq1d 2813 . . . 4 (𝑛 = 0 β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
149, 13imbi12d 344 . . 3 (𝑛 = 0 β†’ (((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ 0 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)))
15 eleq1 2816 . . . . 5 (𝑛 = π‘š β†’ (𝑛 ∈ (0...𝑁) ↔ π‘š ∈ (0...𝑁)))
1615anbi2d 628 . . . 4 (𝑛 = π‘š β†’ ((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) ↔ (πœ‘ ∧ π‘š ∈ (0...𝑁))))
17 oveq2 7422 . . . . . . 7 (𝑛 = π‘š β†’ (0...𝑛) = (0...π‘š))
1817sumeq1d 15671 . . . . . 6 (𝑛 = π‘š β†’ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
1918mpteq2dv 5244 . . . . 5 (𝑛 = π‘š β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))))
2019eleq1d 2813 . . . 4 (𝑛 = π‘š β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
2116, 20imbi12d 344 . . 3 (𝑛 = π‘š β†’ (((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)))
22 eleq1 2816 . . . . 5 (𝑛 = (π‘š + 1) β†’ (𝑛 ∈ (0...𝑁) ↔ (π‘š + 1) ∈ (0...𝑁)))
2322anbi2d 628 . . . 4 (𝑛 = (π‘š + 1) β†’ ((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) ↔ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))))
24 oveq2 7422 . . . . . . 7 (𝑛 = (π‘š + 1) β†’ (0...𝑛) = (0...(π‘š + 1)))
2524sumeq1d 15671 . . . . . 6 (𝑛 = (π‘š + 1) β†’ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
2625mpteq2dv 5244 . . . . 5 (𝑛 = (π‘š + 1) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))))
2726eleq1d 2813 . . . 4 (𝑛 = (π‘š + 1) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
2823, 27imbi12d 344 . . 3 (𝑛 = (π‘š + 1) β†’ (((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)))
29 eleq1 2816 . . . . 5 (𝑛 = 𝑁 β†’ (𝑛 ∈ (0...𝑁) ↔ 𝑁 ∈ (0...𝑁)))
3029anbi2d 628 . . . 4 (𝑛 = 𝑁 β†’ ((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) ↔ (πœ‘ ∧ 𝑁 ∈ (0...𝑁))))
31 oveq2 7422 . . . . . . 7 (𝑛 = 𝑁 β†’ (0...𝑛) = (0...𝑁))
3231sumeq1d 15671 . . . . . 6 (𝑛 = 𝑁 β†’ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
3332mpteq2dv 5244 . . . . 5 (𝑛 = 𝑁 β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))))
3433eleq1d 2813 . . . 4 (𝑛 = 𝑁 β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
3530, 34imbi12d 344 . . 3 (𝑛 = 𝑁 β†’ (((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ 𝑁 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)))
36 0z 12591 . . . . . . . . 9 0 ∈ β„€
37 fzsn 13567 . . . . . . . . 9 (0 ∈ β„€ β†’ (0...0) = {0})
3836, 37ax-mp 5 . . . . . . . 8 (0...0) = {0}
3938sumeq1i 15668 . . . . . . 7 Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ {0} (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))
4039mpteq2i 5247 . . . . . 6 (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ {0} (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
41 stoweidlem17.1 . . . . . . 7 β„²π‘‘πœ‘
42 stoweidlem17.7 . . . . . . . . . . 11 (πœ‘ β†’ 𝐸 ∈ ℝ)
4342adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝐸 ∈ ℝ)
4443recnd 11264 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝐸 ∈ β„‚)
45 stoweidlem17.3 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑋:(0...𝑁)⟢𝐴)
46 nnz 12601 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ β„• β†’ 𝑁 ∈ β„€)
47 nngt0 12265 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ β„• β†’ 0 < 𝑁)
48 0re 11238 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
49 nnre 12241 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ β„• β†’ 𝑁 ∈ ℝ)
50 ltle 11324 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ (0 < 𝑁 β†’ 0 ≀ 𝑁))
5148, 49, 50sylancr 586 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ β„• β†’ (0 < 𝑁 β†’ 0 ≀ 𝑁))
5247, 51mpd 15 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ β„• β†’ 0 ≀ 𝑁)
5346, 52jca 511 . . . . . . . . . . . . . . . 16 (𝑁 ∈ β„• β†’ (𝑁 ∈ β„€ ∧ 0 ≀ 𝑁))
541, 53syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑁 ∈ β„€ ∧ 0 ≀ 𝑁))
5536eluz1i 12852 . . . . . . . . . . . . . . 15 (𝑁 ∈ (β„€β‰₯β€˜0) ↔ (𝑁 ∈ β„€ ∧ 0 ≀ 𝑁))
5654, 55sylibr 233 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜0))
57 eluzfz1 13532 . . . . . . . . . . . . . 14 (𝑁 ∈ (β„€β‰₯β€˜0) β†’ 0 ∈ (0...𝑁))
5856, 57syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ∈ (0...𝑁))
5945, 58ffvelcdmd 7089 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘‹β€˜0) ∈ 𝐴)
60 feq1 6697 . . . . . . . . . . . . . 14 (𝑓 = (π‘‹β€˜0) β†’ (𝑓:π‘‡βŸΆβ„ ↔ (π‘‹β€˜0):π‘‡βŸΆβ„))
6160imbi2d 340 . . . . . . . . . . . . 13 (𝑓 = (π‘‹β€˜0) β†’ ((πœ‘ β†’ 𝑓:π‘‡βŸΆβ„) ↔ (πœ‘ β†’ (π‘‹β€˜0):π‘‡βŸΆβ„)))
62 stoweidlem17.8 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
6362expcom 413 . . . . . . . . . . . . 13 (𝑓 ∈ 𝐴 β†’ (πœ‘ β†’ 𝑓:π‘‡βŸΆβ„))
6461, 63vtoclga 3561 . . . . . . . . . . . 12 ((π‘‹β€˜0) ∈ 𝐴 β†’ (πœ‘ β†’ (π‘‹β€˜0):π‘‡βŸΆβ„))
6559, 64mpcom 38 . . . . . . . . . . 11 (πœ‘ β†’ (π‘‹β€˜0):π‘‡βŸΆβ„)
6665ffvelcdmda 7088 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((π‘‹β€˜0)β€˜π‘‘) ∈ ℝ)
6766recnd 11264 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((π‘‹β€˜0)β€˜π‘‘) ∈ β„‚)
6844, 67mulcld 11256 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘)) ∈ β„‚)
69 fveq2 6891 . . . . . . . . . . 11 (𝑖 = 0 β†’ (π‘‹β€˜π‘–) = (π‘‹β€˜0))
7069fveq1d 6893 . . . . . . . . . 10 (𝑖 = 0 β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) = ((π‘‹β€˜0)β€˜π‘‘))
7170oveq2d 7430 . . . . . . . . 9 (𝑖 = 0 β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘)))
7271sumsn 15716 . . . . . . . 8 ((0 ∈ β„€ ∧ (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘)) ∈ β„‚) β†’ Σ𝑖 ∈ {0} (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘)))
7336, 68, 72sylancr 586 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ {0} (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘)))
7441, 73mpteq2da 5240 . . . . . 6 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ {0} (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘))))
7540, 74eqtrid 2779 . . . . 5 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘))))
76 stoweidlem17.5 . . . . . 6 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
77 stoweidlem17.6 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴)
7841, 76, 77, 62, 42, 59stoweidlem2 45313 . . . . 5 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘))) ∈ 𝐴)
7975, 78eqeltrd 2828 . . . 4 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
8079adantr 480 . . 3 ((πœ‘ ∧ 0 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
81 eqidd 2728 . . . . . . . . . . . . . . 15 (π‘Ÿ = 𝑑 β†’ 𝐸 = 𝐸)
8281cbvmptv 5255 . . . . . . . . . . . . . 14 (π‘Ÿ ∈ 𝑇 ↦ 𝐸) = (𝑑 ∈ 𝑇 ↦ 𝐸)
8382eqcomi 2736 . . . . . . . . . . . . 13 (𝑑 ∈ 𝑇 ↦ 𝐸) = (π‘Ÿ ∈ 𝑇 ↦ 𝐸)
84 simpr 484 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝑑 ∈ 𝑇)
8583, 81, 84, 43fvmptd3 7022 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) = 𝐸)
8685oveq1d 7429 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
8741, 86mpteq2da 5240 . . . . . . . . . 10 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
8887adantr 480 . . . . . . . . 9 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
8945ffvelcdmda 7088 . . . . . . . . . 10 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (π‘‹β€˜(π‘š + 1)) ∈ 𝐴)
90 simpl 482 . . . . . . . . . 10 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ πœ‘)
91 id 22 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝐸 β†’ π‘₯ = 𝐸)
9291mpteq2dv 5244 . . . . . . . . . . . . . . 15 (π‘₯ = 𝐸 β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) = (𝑑 ∈ 𝑇 ↦ 𝐸))
9392eleq1d 2813 . . . . . . . . . . . . . 14 (π‘₯ = 𝐸 β†’ ((𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴))
9493imbi2d 340 . . . . . . . . . . . . 13 (π‘₯ = 𝐸 β†’ ((πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴) ↔ (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)))
9577expcom 413 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴))
9694, 95vtoclga 3561 . . . . . . . . . . . 12 (𝐸 ∈ ℝ β†’ (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴))
9742, 96mpcom 38 . . . . . . . . . . 11 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)
9897adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)
99 fveq1 6890 . . . . . . . . . . . . . . . 16 (𝑔 = (π‘‹β€˜(π‘š + 1)) β†’ (π‘”β€˜π‘‘) = ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))
10099oveq2d 7430 . . . . . . . . . . . . . . 15 (𝑔 = (π‘‹β€˜(π‘š + 1)) β†’ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
101100mpteq2dv 5244 . . . . . . . . . . . . . 14 (𝑔 = (π‘‹β€˜(π‘š + 1)) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
102101eleq1d 2813 . . . . . . . . . . . . 13 (𝑔 = (π‘‹β€˜(π‘š + 1)) β†’ ((𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴))
103102imbi2d 340 . . . . . . . . . . . 12 (𝑔 = (π‘‹β€˜(π‘š + 1)) β†’ (((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴)))
10482eleq1i 2819 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)
105 fveq1 6890 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ (π‘“β€˜π‘‘) = ((π‘Ÿ ∈ 𝑇 ↦ 𝐸)β€˜π‘‘))
10682fveq1i 6892 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ÿ ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘)
107105, 106eqtrdi 2783 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ (π‘“β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘))
108107oveq1d 7429 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘)))
109108mpteq2dv 5244 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))))
110109eleq1d 2813 . . . . . . . . . . . . . . . . . 18 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ ((𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴))
111110imbi2d 340 . . . . . . . . . . . . . . . . 17 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ (((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)))
112763com12 1121 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ 𝐴 ∧ πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
1131123expib 1120 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴))
114111, 113vtoclga 3561 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴))
115104, 114sylbir 234 . . . . . . . . . . . . . . 15 ((𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴))
1161153impib 1114 . . . . . . . . . . . . . 14 (((𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 ∧ πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
1171163com13 1122 . . . . . . . . . . . . 13 ((𝑔 ∈ 𝐴 ∧ πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
1181173expib 1120 . . . . . . . . . . . 12 (𝑔 ∈ 𝐴 β†’ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴))
119103, 118vtoclga 3561 . . . . . . . . . . 11 ((π‘‹β€˜(π‘š + 1)) ∈ 𝐴 β†’ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴))
1201193impib 1114 . . . . . . . . . 10 (((π‘‹β€˜(π‘š + 1)) ∈ 𝐴 ∧ πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴)
12189, 90, 98, 120syl3anc 1369 . . . . . . . . 9 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴)
12288, 121eqeltrrd 2829 . . . . . . . 8 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴)
123122ad2antll 728 . . . . . . 7 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴)
124 simprrl 780 . . . . . . 7 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ πœ‘)
125 simpl 482 . . . . . . . . . 10 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ π‘š ∈ β„•0)
126 simprl 770 . . . . . . . . . 10 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ πœ‘)
1271ad2antrl 727 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ 𝑁 ∈ β„•)
128127nnnn0d 12554 . . . . . . . . . . 11 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ 𝑁 ∈ β„•0)
129 nn0re 12503 . . . . . . . . . . . . 13 (π‘š ∈ β„•0 β†’ π‘š ∈ ℝ)
130129adantr 480 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ π‘š ∈ ℝ)
131 peano2nn0 12534 . . . . . . . . . . . . . 14 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ β„•0)
132131nn0red 12555 . . . . . . . . . . . . 13 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ ℝ)
133132adantr 480 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ (π‘š + 1) ∈ ℝ)
1341nnred 12249 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ ℝ)
135134ad2antrl 727 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ 𝑁 ∈ ℝ)
136 lep1 12077 . . . . . . . . . . . . 13 (π‘š ∈ ℝ β†’ π‘š ≀ (π‘š + 1))
137125, 129, 1363syl 18 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ π‘š ≀ (π‘š + 1))
138 elfzle2 13529 . . . . . . . . . . . . 13 ((π‘š + 1) ∈ (0...𝑁) β†’ (π‘š + 1) ≀ 𝑁)
139138ad2antll 728 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ (π‘š + 1) ≀ 𝑁)
140130, 133, 135, 137, 139letrd 11393 . . . . . . . . . . 11 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ π‘š ≀ 𝑁)
141 elfz2nn0 13616 . . . . . . . . . . 11 (π‘š ∈ (0...𝑁) ↔ (π‘š ∈ β„•0 ∧ 𝑁 ∈ β„•0 ∧ π‘š ≀ 𝑁))
142125, 128, 140, 141syl3anbrc 1341 . . . . . . . . . 10 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ π‘š ∈ (0...𝑁))
143125, 126, 142jca32 515 . . . . . . . . 9 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ π‘š ∈ (0...𝑁))))
144143adantl 481 . . . . . . . 8 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ π‘š ∈ (0...𝑁))))
145 pm3.31 449 . . . . . . . . 9 ((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) β†’ ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ π‘š ∈ (0...𝑁))) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
146145adantr 480 . . . . . . . 8 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ π‘š ∈ (0...𝑁))) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
147144, 146mpd 15 . . . . . . 7 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
148 fveq2 6891 . . . . . . . . . . . 12 (π‘Ÿ = 𝑑 β†’ ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ) = ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))
149148oveq2d 7430 . . . . . . . . . . 11 (π‘Ÿ = 𝑑 β†’ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ)) = (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
150149cbvmptv 5255 . . . . . . . . . 10 (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
151150eleq1i 2819 . . . . . . . . 9 ((π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴)
152 fveq1 6890 . . . . . . . . . . . . . . 15 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ (π‘”β€˜π‘‘) = ((π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ)))β€˜π‘‘))
153150fveq1i 6892 . . . . . . . . . . . . . . 15 ((π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ)))β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘)
154152, 153eqtrdi 2783 . . . . . . . . . . . . . 14 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ (π‘”β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))
155154oveq2d 7430 . . . . . . . . . . . . 13 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘)))
156155mpteq2dv 5244 . . . . . . . . . . . 12 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))))
157156eleq1d 2813 . . . . . . . . . . 11 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ ((𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴))
158157imbi2d 340 . . . . . . . . . 10 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ (((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴)))
159 fveq2 6891 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ = 𝑑 β†’ ((π‘‹β€˜π‘–)β€˜π‘Ÿ) = ((π‘‹β€˜π‘–)β€˜π‘‘))
160159oveq2d 7430 . . . . . . . . . . . . . . . . 17 (π‘Ÿ = 𝑑 β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ)) = (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
161160sumeq2sdv 15674 . . . . . . . . . . . . . . . 16 (π‘Ÿ = 𝑑 β†’ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ)) = Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
162161cbvmptv 5255 . . . . . . . . . . . . . . 15 (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
163162eleq1i 2819 . . . . . . . . . . . . . 14 ((π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
164 fveq1 6890 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ (π‘“β€˜π‘‘) = ((π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ)))β€˜π‘‘))
165162fveq1i 6892 . . . . . . . . . . . . . . . . . . . 20 ((π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ)))β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘)
166164, 165eqtrdi 2783 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ (π‘“β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘))
167166oveq1d 7429 . . . . . . . . . . . . . . . . . 18 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘)))
168167mpteq2dv 5244 . . . . . . . . . . . . . . . . 17 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))))
169168eleq1d 2813 . . . . . . . . . . . . . . . 16 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ ((𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴))
170169imbi2d 340 . . . . . . . . . . . . . . 15 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ (((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)))
171 stoweidlem17.4 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
1721713com12 1121 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ 𝐴 ∧ πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
1731723expib 1120 . . . . . . . . . . . . . . 15 (𝑓 ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴))
174170, 173vtoclga 3561 . . . . . . . . . . . . . 14 ((π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴))
175163, 174sylbir 234 . . . . . . . . . . . . 13 ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴))
1761753impib 1114 . . . . . . . . . . . 12 (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ∧ πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
1771763com13 1122 . . . . . . . . . . 11 ((𝑔 ∈ 𝐴 ∧ πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
1781773expib 1120 . . . . . . . . . 10 (𝑔 ∈ 𝐴 β†’ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴))
179158, 178vtoclga 3561 . . . . . . . . 9 ((π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) ∈ 𝐴 β†’ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴))
180151, 179sylbir 234 . . . . . . . 8 ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴 β†’ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴))
1811803impib 1114 . . . . . . 7 (((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴 ∧ πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴)
182123, 124, 147, 181syl3anc 1369 . . . . . 6 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴)
183 3anass 1093 . . . . . . . . 9 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ↔ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))))
184183biimpri 227 . . . . . . . 8 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ (π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))
185184adantl 481 . . . . . . 7 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ (π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))
186 nfv 1910 . . . . . . . . . 10 Ⅎ𝑑 π‘š ∈ β„•0
187 nfv 1910 . . . . . . . . . 10 Ⅎ𝑑(π‘š + 1) ∈ (0...𝑁)
188186, 41, 187nf3an 1897 . . . . . . . . 9 Ⅎ𝑑(π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))
189 simpr 484 . . . . . . . . . . . 12 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ 𝑑 ∈ 𝑇)
190 fzfid 13962 . . . . . . . . . . . . 13 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (0...π‘š) ∈ Fin)
191423ad2ant2 1132 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ 𝐸 ∈ ℝ)
192191adantr 480 . . . . . . . . . . . . . . 15 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ 𝐸 ∈ ℝ)
193192adantr 480 . . . . . . . . . . . . . 14 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...π‘š)) β†’ 𝐸 ∈ ℝ)
194 fzelp1 13577 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (0...π‘š) β†’ 𝑖 ∈ (0...(π‘š + 1)))
195194anim2i 616 . . . . . . . . . . . . . . . 16 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...π‘š)) β†’ (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...(π‘š + 1))))
196 an32 645 . . . . . . . . . . . . . . . 16 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...(π‘š + 1))) ↔ (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) ∧ 𝑑 ∈ 𝑇))
197195, 196sylib 217 . . . . . . . . . . . . . . 15 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...π‘š)) β†’ (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) ∧ 𝑑 ∈ 𝑇))
198453ad2ant2 1132 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ 𝑋:(0...𝑁)⟢𝐴)
199198adantr 480 . . . . . . . . . . . . . . . . . 18 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ 𝑋:(0...𝑁)⟢𝐴)
200 elfzuz3 13522 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š + 1) ∈ (0...𝑁) β†’ 𝑁 ∈ (β„€β‰₯β€˜(π‘š + 1)))
201 fzss2 13565 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (β„€β‰₯β€˜(π‘š + 1)) β†’ (0...(π‘š + 1)) βŠ† (0...𝑁))
202200, 201syl 17 . . . . . . . . . . . . . . . . . . . 20 ((π‘š + 1) ∈ (0...𝑁) β†’ (0...(π‘š + 1)) βŠ† (0...𝑁))
203202sselda 3978 . . . . . . . . . . . . . . . . . . 19 (((π‘š + 1) ∈ (0...𝑁) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ 𝑖 ∈ (0...𝑁))
2042033ad2antl3 1185 . . . . . . . . . . . . . . . . . 18 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ 𝑖 ∈ (0...𝑁))
205199, 204ffvelcdmd 7089 . . . . . . . . . . . . . . . . 17 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ (π‘‹β€˜π‘–) ∈ 𝐴)
206 simpl2 1190 . . . . . . . . . . . . . . . . 17 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ πœ‘)
207 feq1 6697 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (π‘‹β€˜π‘–) β†’ (𝑓:π‘‡βŸΆβ„ ↔ (π‘‹β€˜π‘–):π‘‡βŸΆβ„))
208207imbi2d 340 . . . . . . . . . . . . . . . . . 18 (𝑓 = (π‘‹β€˜π‘–) β†’ ((πœ‘ β†’ 𝑓:π‘‡βŸΆβ„) ↔ (πœ‘ β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„)))
209208, 63vtoclga 3561 . . . . . . . . . . . . . . . . 17 ((π‘‹β€˜π‘–) ∈ 𝐴 β†’ (πœ‘ β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„))
210205, 206, 209sylc 65 . . . . . . . . . . . . . . . 16 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„)
211210ffvelcdmda 7088 . . . . . . . . . . . . . . 15 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
212197, 211syl 17 . . . . . . . . . . . . . 14 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...π‘š)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
213193, 212remulcld 11266 . . . . . . . . . . . . 13 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...π‘š)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
214190, 213fsumrecl 15704 . . . . . . . . . . . 12 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
215 eqid 2727 . . . . . . . . . . . . 13 (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
216215fvmpt2 7010 . . . . . . . . . . . 12 ((𝑑 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) = Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
217189, 214, 216syl2anc 583 . . . . . . . . . . 11 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) = Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
218217oveq1d 7429 . . . . . . . . . 10 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) = (Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
219 3simpc 1148 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))
220219adantr 480 . . . . . . . . . . . . . . 15 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))
221 feq1 6697 . . . . . . . . . . . . . . . . . 18 (𝑓 = (π‘‹β€˜(π‘š + 1)) β†’ (𝑓:π‘‡βŸΆβ„ ↔ (π‘‹β€˜(π‘š + 1)):π‘‡βŸΆβ„))
222221imbi2d 340 . . . . . . . . . . . . . . . . 17 (𝑓 = (π‘‹β€˜(π‘š + 1)) β†’ ((πœ‘ β†’ 𝑓:π‘‡βŸΆβ„) ↔ (πœ‘ β†’ (π‘‹β€˜(π‘š + 1)):π‘‡βŸΆβ„)))
223222, 63vtoclga 3561 . . . . . . . . . . . . . . . 16 ((π‘‹β€˜(π‘š + 1)) ∈ 𝐴 β†’ (πœ‘ β†’ (π‘‹β€˜(π‘š + 1)):π‘‡βŸΆβ„))
22489, 90, 223sylc 65 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (π‘‹β€˜(π‘š + 1)):π‘‡βŸΆβ„)
225220, 224syl 17 . . . . . . . . . . . . . 14 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (π‘‹β€˜(π‘š + 1)):π‘‡βŸΆβ„)
226225, 189ffvelcdmd 7089 . . . . . . . . . . . . 13 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘‹β€˜(π‘š + 1))β€˜π‘‘) ∈ ℝ)
227192, 226remulcld 11266 . . . . . . . . . . . 12 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)) ∈ ℝ)
228 eqid 2727 . . . . . . . . . . . . 13 (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
229228fvmpt2 7010 . . . . . . . . . . . 12 ((𝑑 ∈ 𝑇 ∧ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)) ∈ ℝ) β†’ ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘) = (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
230189, 227, 229syl2anc 583 . . . . . . . . . . 11 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘) = (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
231230oveq2d 7430 . . . . . . . . . 10 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
232 elfzuz 13521 . . . . . . . . . . . . . 14 ((π‘š + 1) ∈ (0...𝑁) β†’ (π‘š + 1) ∈ (β„€β‰₯β€˜0))
2332323ad2ant3 1133 . . . . . . . . . . . . 13 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (π‘š + 1) ∈ (β„€β‰₯β€˜0))
234233adantr 480 . . . . . . . . . . . 12 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (π‘š + 1) ∈ (β„€β‰₯β€˜0))
235192adantr 480 . . . . . . . . . . . . 13 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ 𝐸 ∈ ℝ)
236211an32s 651 . . . . . . . . . . . . 13 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
237 remulcl 11215 . . . . . . . . . . . . . 14 ((𝐸 ∈ ℝ ∧ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
238237recnd 11264 . . . . . . . . . . . . 13 ((𝐸 ∈ ℝ ∧ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ β„‚)
239235, 236, 238syl2anc 583 . . . . . . . . . . . 12 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ β„‚)
240 fveq2 6891 . . . . . . . . . . . . . 14 (𝑖 = (π‘š + 1) β†’ (π‘‹β€˜π‘–) = (π‘‹β€˜(π‘š + 1)))
241240fveq1d 6893 . . . . . . . . . . . . 13 (𝑖 = (π‘š + 1) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) = ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))
242241oveq2d 7430 . . . . . . . . . . . 12 (𝑖 = (π‘š + 1) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
243234, 239, 242fsumm1 15721 . . . . . . . . . . 11 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (Σ𝑖 ∈ (0...((π‘š + 1) βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
244 nn0cn 12504 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„•0 β†’ π‘š ∈ β„‚)
2452443ad2ant1 1131 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ π‘š ∈ β„‚)
246245adantr 480 . . . . . . . . . . . . . . 15 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ π‘š ∈ β„‚)
247 1cnd 11231 . . . . . . . . . . . . . . 15 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ 1 ∈ β„‚)
248246, 247pncand 11594 . . . . . . . . . . . . . 14 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘š + 1) βˆ’ 1) = π‘š)
249248oveq2d 7430 . . . . . . . . . . . . 13 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (0...((π‘š + 1) βˆ’ 1)) = (0...π‘š))
250249sumeq1d 15671 . . . . . . . . . . . 12 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (0...((π‘š + 1) βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
251250oveq1d 7429 . . . . . . . . . . 11 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (Σ𝑖 ∈ (0...((π‘š + 1) βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) = (Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
252243, 251eqtrd 2767 . . . . . . . . . 10 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
253218, 231, 2523eqtr4rd 2778 . . . . . . . . 9 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘)))
254188, 253mpteq2da 5240 . . . . . . . 8 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))))
255254eleq1d 2813 . . . . . . 7 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴))
256185, 255syl 17 . . . . . 6 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴))
257182, 256mpbird 257 . . . . 5 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
258257exp32 420 . . . 4 ((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) β†’ (π‘š ∈ β„•0 β†’ ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)))
259258pm2.86i 110 . . 3 (π‘š ∈ β„•0 β†’ (((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)))
26014, 21, 28, 35, 80, 259nn0ind 12679 . 2 (𝑁 ∈ β„•0 β†’ ((πœ‘ ∧ 𝑁 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
2612, 7, 260sylc 65 1 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534  β„²wnf 1778   ∈ wcel 2099   βŠ† wss 3944  {csn 4624   class class class wbr 5142   ↦ cmpt 5225  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   Β· cmul 11135   < clt 11270   ≀ cle 11271   βˆ’ cmin 11466  β„•cn 12234  β„•0cn0 12494  β„€cz 12580  β„€β‰₯cuz 12844  ...cfz 13508  Ξ£csu 15656
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9457  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-z 12581  df-uz 12845  df-rp 12999  df-fz 13509  df-fzo 13652  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-clim 15456  df-sum 15657
This theorem is referenced by:  stoweidlem60  45371
  Copyright terms: Public domain W3C validator