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 44332
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 12480 . 2 (πœ‘ β†’ 𝑁 ∈ β„•0)
3 nn0uz 12812 . . . . 5 β„•0 = (β„€β‰₯β€˜0)
42, 3eleqtrdi 2848 . . . 4 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜0))
5 eluzfz2 13456 . . . 4 (𝑁 ∈ (β„€β‰₯β€˜0) β†’ 𝑁 ∈ (0...𝑁))
64, 5syl 17 . . 3 (πœ‘ β†’ 𝑁 ∈ (0...𝑁))
76ancli 550 . 2 (πœ‘ β†’ (πœ‘ ∧ 𝑁 ∈ (0...𝑁)))
8 eleq1 2826 . . . . 5 (𝑛 = 0 β†’ (𝑛 ∈ (0...𝑁) ↔ 0 ∈ (0...𝑁)))
98anbi2d 630 . . . 4 (𝑛 = 0 β†’ ((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) ↔ (πœ‘ ∧ 0 ∈ (0...𝑁))))
10 oveq2 7370 . . . . . . 7 (𝑛 = 0 β†’ (0...𝑛) = (0...0))
1110sumeq1d 15593 . . . . . 6 (𝑛 = 0 β†’ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
1211mpteq2dv 5212 . . . . 5 (𝑛 = 0 β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))))
1312eleq1d 2823 . . . 4 (𝑛 = 0 β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
149, 13imbi12d 345 . . 3 (𝑛 = 0 β†’ (((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ 0 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)))
15 eleq1 2826 . . . . 5 (𝑛 = π‘š β†’ (𝑛 ∈ (0...𝑁) ↔ π‘š ∈ (0...𝑁)))
1615anbi2d 630 . . . 4 (𝑛 = π‘š β†’ ((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) ↔ (πœ‘ ∧ π‘š ∈ (0...𝑁))))
17 oveq2 7370 . . . . . . 7 (𝑛 = π‘š β†’ (0...𝑛) = (0...π‘š))
1817sumeq1d 15593 . . . . . 6 (𝑛 = π‘š β†’ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
1918mpteq2dv 5212 . . . . 5 (𝑛 = π‘š β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))))
2019eleq1d 2823 . . . 4 (𝑛 = π‘š β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
2116, 20imbi12d 345 . . 3 (𝑛 = π‘š β†’ (((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)))
22 eleq1 2826 . . . . 5 (𝑛 = (π‘š + 1) β†’ (𝑛 ∈ (0...𝑁) ↔ (π‘š + 1) ∈ (0...𝑁)))
2322anbi2d 630 . . . 4 (𝑛 = (π‘š + 1) β†’ ((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) ↔ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))))
24 oveq2 7370 . . . . . . 7 (𝑛 = (π‘š + 1) β†’ (0...𝑛) = (0...(π‘š + 1)))
2524sumeq1d 15593 . . . . . 6 (𝑛 = (π‘š + 1) β†’ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
2625mpteq2dv 5212 . . . . 5 (𝑛 = (π‘š + 1) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))))
2726eleq1d 2823 . . . 4 (𝑛 = (π‘š + 1) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
2823, 27imbi12d 345 . . 3 (𝑛 = (π‘š + 1) β†’ (((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)))
29 eleq1 2826 . . . . 5 (𝑛 = 𝑁 β†’ (𝑛 ∈ (0...𝑁) ↔ 𝑁 ∈ (0...𝑁)))
3029anbi2d 630 . . . 4 (𝑛 = 𝑁 β†’ ((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) ↔ (πœ‘ ∧ 𝑁 ∈ (0...𝑁))))
31 oveq2 7370 . . . . . . 7 (𝑛 = 𝑁 β†’ (0...𝑛) = (0...𝑁))
3231sumeq1d 15593 . . . . . 6 (𝑛 = 𝑁 β†’ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
3332mpteq2dv 5212 . . . . 5 (𝑛 = 𝑁 β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))))
3433eleq1d 2823 . . . 4 (𝑛 = 𝑁 β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
3530, 34imbi12d 345 . . 3 (𝑛 = 𝑁 β†’ (((πœ‘ ∧ 𝑛 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ 𝑁 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)))
36 0z 12517 . . . . . . . . 9 0 ∈ β„€
37 fzsn 13490 . . . . . . . . 9 (0 ∈ β„€ β†’ (0...0) = {0})
3836, 37ax-mp 5 . . . . . . . 8 (0...0) = {0}
3938sumeq1i 15590 . . . . . . 7 Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ {0} (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))
4039mpteq2i 5215 . . . . . 6 (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ {0} (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
41 stoweidlem17.1 . . . . . . 7 β„²π‘‘πœ‘
42 stoweidlem17.7 . . . . . . . . . . 11 (πœ‘ β†’ 𝐸 ∈ ℝ)
4342adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝐸 ∈ ℝ)
4443recnd 11190 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝐸 ∈ β„‚)
45 stoweidlem17.3 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑋:(0...𝑁)⟢𝐴)
46 nnz 12527 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ β„• β†’ 𝑁 ∈ β„€)
47 nngt0 12191 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ β„• β†’ 0 < 𝑁)
48 0re 11164 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
49 nnre 12167 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ β„• β†’ 𝑁 ∈ ℝ)
50 ltle 11250 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ (0 < 𝑁 β†’ 0 ≀ 𝑁))
5148, 49, 50sylancr 588 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ β„• β†’ (0 < 𝑁 β†’ 0 ≀ 𝑁))
5247, 51mpd 15 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ β„• β†’ 0 ≀ 𝑁)
5346, 52jca 513 . . . . . . . . . . . . . . . 16 (𝑁 ∈ β„• β†’ (𝑁 ∈ β„€ ∧ 0 ≀ 𝑁))
541, 53syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑁 ∈ β„€ ∧ 0 ≀ 𝑁))
5536eluz1i 12778 . . . . . . . . . . . . . . 15 (𝑁 ∈ (β„€β‰₯β€˜0) ↔ (𝑁 ∈ β„€ ∧ 0 ≀ 𝑁))
5654, 55sylibr 233 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜0))
57 eluzfz1 13455 . . . . . . . . . . . . . 14 (𝑁 ∈ (β„€β‰₯β€˜0) β†’ 0 ∈ (0...𝑁))
5856, 57syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ∈ (0...𝑁))
5945, 58ffvelcdmd 7041 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘‹β€˜0) ∈ 𝐴)
60 feq1 6654 . . . . . . . . . . . . . 14 (𝑓 = (π‘‹β€˜0) β†’ (𝑓:π‘‡βŸΆβ„ ↔ (π‘‹β€˜0):π‘‡βŸΆβ„))
6160imbi2d 341 . . . . . . . . . . . . 13 (𝑓 = (π‘‹β€˜0) β†’ ((πœ‘ β†’ 𝑓:π‘‡βŸΆβ„) ↔ (πœ‘ β†’ (π‘‹β€˜0):π‘‡βŸΆβ„)))
62 stoweidlem17.8 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
6362expcom 415 . . . . . . . . . . . . 13 (𝑓 ∈ 𝐴 β†’ (πœ‘ β†’ 𝑓:π‘‡βŸΆβ„))
6461, 63vtoclga 3537 . . . . . . . . . . . 12 ((π‘‹β€˜0) ∈ 𝐴 β†’ (πœ‘ β†’ (π‘‹β€˜0):π‘‡βŸΆβ„))
6559, 64mpcom 38 . . . . . . . . . . 11 (πœ‘ β†’ (π‘‹β€˜0):π‘‡βŸΆβ„)
6665ffvelcdmda 7040 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((π‘‹β€˜0)β€˜π‘‘) ∈ ℝ)
6766recnd 11190 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((π‘‹β€˜0)β€˜π‘‘) ∈ β„‚)
6844, 67mulcld 11182 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘)) ∈ β„‚)
69 fveq2 6847 . . . . . . . . . . 11 (𝑖 = 0 β†’ (π‘‹β€˜π‘–) = (π‘‹β€˜0))
7069fveq1d 6849 . . . . . . . . . 10 (𝑖 = 0 β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) = ((π‘‹β€˜0)β€˜π‘‘))
7170oveq2d 7378 . . . . . . . . 9 (𝑖 = 0 β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘)))
7271sumsn 15638 . . . . . . . 8 ((0 ∈ β„€ ∧ (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘)) ∈ β„‚) β†’ Σ𝑖 ∈ {0} (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘)))
7336, 68, 72sylancr 588 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ {0} (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘)))
7441, 73mpteq2da 5208 . . . . . 6 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ {0} (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘))))
7540, 74eqtrid 2789 . . . . 5 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘))))
76 stoweidlem17.5 . . . . . 6 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
77 stoweidlem17.6 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴)
7841, 76, 77, 62, 42, 59stoweidlem2 44317 . . . . 5 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜0)β€˜π‘‘))) ∈ 𝐴)
7975, 78eqeltrd 2838 . . . 4 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
8079adantr 482 . . 3 ((πœ‘ ∧ 0 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
81 eqidd 2738 . . . . . . . . . . . . . . 15 (π‘Ÿ = 𝑑 β†’ 𝐸 = 𝐸)
8281cbvmptv 5223 . . . . . . . . . . . . . 14 (π‘Ÿ ∈ 𝑇 ↦ 𝐸) = (𝑑 ∈ 𝑇 ↦ 𝐸)
8382eqcomi 2746 . . . . . . . . . . . . 13 (𝑑 ∈ 𝑇 ↦ 𝐸) = (π‘Ÿ ∈ 𝑇 ↦ 𝐸)
84 simpr 486 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝑑 ∈ 𝑇)
8583, 81, 84, 43fvmptd3 6976 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) = 𝐸)
8685oveq1d 7377 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
8741, 86mpteq2da 5208 . . . . . . . . . 10 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
8887adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
8945ffvelcdmda 7040 . . . . . . . . . 10 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (π‘‹β€˜(π‘š + 1)) ∈ 𝐴)
90 simpl 484 . . . . . . . . . 10 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ πœ‘)
91 id 22 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝐸 β†’ π‘₯ = 𝐸)
9291mpteq2dv 5212 . . . . . . . . . . . . . . 15 (π‘₯ = 𝐸 β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) = (𝑑 ∈ 𝑇 ↦ 𝐸))
9392eleq1d 2823 . . . . . . . . . . . . . 14 (π‘₯ = 𝐸 β†’ ((𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴))
9493imbi2d 341 . . . . . . . . . . . . 13 (π‘₯ = 𝐸 β†’ ((πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴) ↔ (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)))
9577expcom 415 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴))
9694, 95vtoclga 3537 . . . . . . . . . . . 12 (𝐸 ∈ ℝ β†’ (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴))
9742, 96mpcom 38 . . . . . . . . . . 11 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)
9897adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)
99 fveq1 6846 . . . . . . . . . . . . . . . 16 (𝑔 = (π‘‹β€˜(π‘š + 1)) β†’ (π‘”β€˜π‘‘) = ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))
10099oveq2d 7378 . . . . . . . . . . . . . . 15 (𝑔 = (π‘‹β€˜(π‘š + 1)) β†’ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
101100mpteq2dv 5212 . . . . . . . . . . . . . 14 (𝑔 = (π‘‹β€˜(π‘š + 1)) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
102101eleq1d 2823 . . . . . . . . . . . . 13 (𝑔 = (π‘‹β€˜(π‘š + 1)) β†’ ((𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴))
103102imbi2d 341 . . . . . . . . . . . 12 (𝑔 = (π‘‹β€˜(π‘š + 1)) β†’ (((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴)))
10482eleq1i 2829 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)
105 fveq1 6846 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ (π‘“β€˜π‘‘) = ((π‘Ÿ ∈ 𝑇 ↦ 𝐸)β€˜π‘‘))
10682fveq1i 6848 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ÿ ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘)
107105, 106eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ (π‘“β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘))
108107oveq1d 7377 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘)))
109108mpteq2dv 5212 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))))
110109eleq1d 2823 . . . . . . . . . . . . . . . . . 18 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ ((𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴))
111110imbi2d 341 . . . . . . . . . . . . . . . . 17 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ 𝐸) β†’ (((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)))
112763com12 1124 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ 𝐴 ∧ πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
1131123expib 1123 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴))
114111, 113vtoclga 3537 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴))
115104, 114sylbir 234 . . . . . . . . . . . . . . 15 ((𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴))
1161153impib 1117 . . . . . . . . . . . . . 14 (((𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 ∧ πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
1171163com13 1125 . . . . . . . . . . . . 13 ((𝑔 ∈ 𝐴 ∧ πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
1181173expib 1123 . . . . . . . . . . . 12 (𝑔 ∈ 𝐴 β†’ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴))
119103, 118vtoclga 3537 . . . . . . . . . . 11 ((π‘‹β€˜(π‘š + 1)) ∈ 𝐴 β†’ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴))
1201193impib 1117 . . . . . . . . . 10 (((π‘‹β€˜(π‘š + 1)) ∈ 𝐴 ∧ πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴)
12189, 90, 98, 120syl3anc 1372 . . . . . . . . 9 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ 𝐸)β€˜π‘‘) Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴)
12288, 121eqeltrrd 2839 . . . . . . . 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 484 . . . . . . . . . 10 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ π‘š ∈ β„•0)
126 simprl 770 . . . . . . . . . 10 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ πœ‘)
1271ad2antrl 727 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ 𝑁 ∈ β„•)
128127nnnn0d 12480 . . . . . . . . . . 11 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ 𝑁 ∈ β„•0)
129 nn0re 12429 . . . . . . . . . . . . 13 (π‘š ∈ β„•0 β†’ π‘š ∈ ℝ)
130129adantr 482 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ π‘š ∈ ℝ)
131 peano2nn0 12460 . . . . . . . . . . . . . 14 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ β„•0)
132131nn0red 12481 . . . . . . . . . . . . 13 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ ℝ)
133132adantr 482 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ (π‘š + 1) ∈ ℝ)
1341nnred 12175 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ ℝ)
135134ad2antrl 727 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ 𝑁 ∈ ℝ)
136 lep1 12003 . . . . . . . . . . . . 13 (π‘š ∈ ℝ β†’ π‘š ≀ (π‘š + 1))
137125, 129, 1363syl 18 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ π‘š ≀ (π‘š + 1))
138 elfzle2 13452 . . . . . . . . . . . . 13 ((π‘š + 1) ∈ (0...𝑁) β†’ (π‘š + 1) ≀ 𝑁)
139138ad2antll 728 . . . . . . . . . . . 12 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ (π‘š + 1) ≀ 𝑁)
140130, 133, 135, 137, 139letrd 11319 . . . . . . . . . . 11 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ π‘š ≀ 𝑁)
141 elfz2nn0 13539 . . . . . . . . . . 11 (π‘š ∈ (0...𝑁) ↔ (π‘š ∈ β„•0 ∧ 𝑁 ∈ β„•0 ∧ π‘š ≀ 𝑁))
142125, 128, 140, 141syl3anbrc 1344 . . . . . . . . . 10 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ π‘š ∈ (0...𝑁))
143125, 126, 142jca32 517 . . . . . . . . 9 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ π‘š ∈ (0...𝑁))))
144143adantl 483 . . . . . . . 8 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ π‘š ∈ (0...𝑁))))
145 pm3.31 451 . . . . . . . . 9 ((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) β†’ ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ π‘š ∈ (0...𝑁))) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
146145adantr 482 . . . . . . . 8 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ π‘š ∈ (0...𝑁))) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
147144, 146mpd 15 . . . . . . 7 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
148 fveq2 6847 . . . . . . . . . . . 12 (π‘Ÿ = 𝑑 β†’ ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ) = ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))
149148oveq2d 7378 . . . . . . . . . . 11 (π‘Ÿ = 𝑑 β†’ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ)) = (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
150149cbvmptv 5223 . . . . . . . . . 10 (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
151150eleq1i 2829 . . . . . . . . 9 ((π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴)
152 fveq1 6846 . . . . . . . . . . . . . . 15 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ (π‘”β€˜π‘‘) = ((π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ)))β€˜π‘‘))
153150fveq1i 6848 . . . . . . . . . . . . . . 15 ((π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ)))β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘)
154152, 153eqtrdi 2793 . . . . . . . . . . . . . 14 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ (π‘”β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))
155154oveq2d 7378 . . . . . . . . . . . . 13 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘)))
156155mpteq2dv 5212 . . . . . . . . . . . 12 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))))
157156eleq1d 2823 . . . . . . . . . . 11 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ ((𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴))
158157imbi2d 341 . . . . . . . . . 10 (𝑔 = (π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) β†’ (((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴)))
159 fveq2 6847 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ = 𝑑 β†’ ((π‘‹β€˜π‘–)β€˜π‘Ÿ) = ((π‘‹β€˜π‘–)β€˜π‘‘))
160159oveq2d 7378 . . . . . . . . . . . . . . . . 17 (π‘Ÿ = 𝑑 β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ)) = (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
161160sumeq2sdv 15596 . . . . . . . . . . . . . . . 16 (π‘Ÿ = 𝑑 β†’ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ)) = Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
162161cbvmptv 5223 . . . . . . . . . . . . . . 15 (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
163162eleq1i 2829 . . . . . . . . . . . . . 14 ((π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
164 fveq1 6846 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ (π‘“β€˜π‘‘) = ((π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ)))β€˜π‘‘))
165162fveq1i 6848 . . . . . . . . . . . . . . . . . . . 20 ((π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ)))β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘)
166164, 165eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ (π‘“β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘))
167166oveq1d 7377 . . . . . . . . . . . . . . . . . 18 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘)))
168167mpteq2dv 5212 . . . . . . . . . . . . . . . . 17 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))))
169168eleq1d 2823 . . . . . . . . . . . . . . . 16 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ ((𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴))
170169imbi2d 341 . . . . . . . . . . . . . . 15 (𝑓 = (π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) β†’ (((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴) ↔ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)))
171 stoweidlem17.4 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
1721713com12 1124 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ 𝐴 ∧ πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
1731723expib 1123 . . . . . . . . . . . . . . 15 (𝑓 ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴))
174170, 173vtoclga 3537 . . . . . . . . . . . . . 14 ((π‘Ÿ ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘Ÿ))) ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴))
175163, 174sylbir 234 . . . . . . . . . . . . 13 ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 β†’ ((πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴))
1761753impib 1117 . . . . . . . . . . . 12 (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ∧ πœ‘ ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
1771763com13 1125 . . . . . . . . . . 11 ((𝑔 ∈ 𝐴 ∧ πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
1781773expib 1123 . . . . . . . . . 10 (𝑔 ∈ 𝐴 β†’ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴))
179158, 178vtoclga 3537 . . . . . . . . 9 ((π‘Ÿ ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘Ÿ))) ∈ 𝐴 β†’ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴))
180151, 179sylbir 234 . . . . . . . 8 ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴 β†’ ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴))
1811803impib 1117 . . . . . . 7 (((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) ∈ 𝐴 ∧ πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴)
182123, 124, 147, 181syl3anc 1372 . . . . . 6 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))) ∈ 𝐴)
183 3anass 1096 . . . . . . . . 9 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ↔ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))))
184183biimpri 227 . . . . . . . 8 ((π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))) β†’ (π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))
185184adantl 483 . . . . . . 7 (((π‘š ∈ β„•0 β†’ ((πœ‘ ∧ π‘š ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)) ∧ (π‘š ∈ β„•0 ∧ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))) β†’ (π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))
186 nfv 1918 . . . . . . . . . 10 Ⅎ𝑑 π‘š ∈ β„•0
187 nfv 1918 . . . . . . . . . 10 Ⅎ𝑑(π‘š + 1) ∈ (0...𝑁)
188186, 41, 187nf3an 1905 . . . . . . . . 9 Ⅎ𝑑(π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁))
189 simpr 486 . . . . . . . . . . . 12 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ 𝑑 ∈ 𝑇)
190 fzfid 13885 . . . . . . . . . . . . 13 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (0...π‘š) ∈ Fin)
191423ad2ant2 1135 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ 𝐸 ∈ ℝ)
192191adantr 482 . . . . . . . . . . . . . . 15 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ 𝐸 ∈ ℝ)
193192adantr 482 . . . . . . . . . . . . . 14 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...π‘š)) β†’ 𝐸 ∈ ℝ)
194 fzelp1 13500 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (0...π‘š) β†’ 𝑖 ∈ (0...(π‘š + 1)))
195194anim2i 618 . . . . . . . . . . . . . . . 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 1135 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ 𝑋:(0...𝑁)⟢𝐴)
199198adantr 482 . . . . . . . . . . . . . . . . . 18 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ 𝑋:(0...𝑁)⟢𝐴)
200 elfzuz3 13445 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š + 1) ∈ (0...𝑁) β†’ 𝑁 ∈ (β„€β‰₯β€˜(π‘š + 1)))
201 fzss2 13488 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (β„€β‰₯β€˜(π‘š + 1)) β†’ (0...(π‘š + 1)) βŠ† (0...𝑁))
202200, 201syl 17 . . . . . . . . . . . . . . . . . . . 20 ((π‘š + 1) ∈ (0...𝑁) β†’ (0...(π‘š + 1)) βŠ† (0...𝑁))
203202sselda 3949 . . . . . . . . . . . . . . . . . . 19 (((π‘š + 1) ∈ (0...𝑁) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ 𝑖 ∈ (0...𝑁))
2042033ad2antl3 1188 . . . . . . . . . . . . . . . . . 18 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ 𝑖 ∈ (0...𝑁))
205199, 204ffvelcdmd 7041 . . . . . . . . . . . . . . . . 17 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ (π‘‹β€˜π‘–) ∈ 𝐴)
206 simpl2 1193 . . . . . . . . . . . . . . . . 17 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ πœ‘)
207 feq1 6654 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (π‘‹β€˜π‘–) β†’ (𝑓:π‘‡βŸΆβ„ ↔ (π‘‹β€˜π‘–):π‘‡βŸΆβ„))
208207imbi2d 341 . . . . . . . . . . . . . . . . . 18 (𝑓 = (π‘‹β€˜π‘–) β†’ ((πœ‘ β†’ 𝑓:π‘‡βŸΆβ„) ↔ (πœ‘ β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„)))
209208, 63vtoclga 3537 . . . . . . . . . . . . . . . . 17 ((π‘‹β€˜π‘–) ∈ 𝐴 β†’ (πœ‘ β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„))
210205, 206, 209sylc 65 . . . . . . . . . . . . . . . 16 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„)
211210ffvelcdmda 7040 . . . . . . . . . . . . . . 15 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(π‘š + 1))) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
212197, 211syl 17 . . . . . . . . . . . . . 14 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...π‘š)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
213193, 212remulcld 11192 . . . . . . . . . . . . 13 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...π‘š)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
214190, 213fsumrecl 15626 . . . . . . . . . . . 12 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
215 eqid 2737 . . . . . . . . . . . . 13 (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
216215fvmpt2 6964 . . . . . . . . . . . 12 ((𝑑 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) = Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
217189, 214, 216syl2anc 585 . . . . . . . . . . 11 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) = Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
218217oveq1d 7377 . . . . . . . . . 10 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) = (Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
219 3simpc 1151 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))
220219adantr 482 . . . . . . . . . . . . . . 15 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)))
221 feq1 6654 . . . . . . . . . . . . . . . . . 18 (𝑓 = (π‘‹β€˜(π‘š + 1)) β†’ (𝑓:π‘‡βŸΆβ„ ↔ (π‘‹β€˜(π‘š + 1)):π‘‡βŸΆβ„))
222221imbi2d 341 . . . . . . . . . . . . . . . . 17 (𝑓 = (π‘‹β€˜(π‘š + 1)) β†’ ((πœ‘ β†’ 𝑓:π‘‡βŸΆβ„) ↔ (πœ‘ β†’ (π‘‹β€˜(π‘š + 1)):π‘‡βŸΆβ„)))
223222, 63vtoclga 3537 . . . . . . . . . . . . . . . 16 ((π‘‹β€˜(π‘š + 1)) ∈ 𝐴 β†’ (πœ‘ β†’ (π‘‹β€˜(π‘š + 1)):π‘‡βŸΆβ„))
22489, 90, 223sylc 65 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (π‘‹β€˜(π‘š + 1)):π‘‡βŸΆβ„)
225220, 224syl 17 . . . . . . . . . . . . . 14 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (π‘‹β€˜(π‘š + 1)):π‘‡βŸΆβ„)
226225, 189ffvelcdmd 7041 . . . . . . . . . . . . 13 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘‹β€˜(π‘š + 1))β€˜π‘‘) ∈ ℝ)
227192, 226remulcld 11192 . . . . . . . . . . . 12 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)) ∈ ℝ)
228 eqid 2737 . . . . . . . . . . . . 13 (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
229228fvmpt2 6964 . . . . . . . . . . . 12 ((𝑑 ∈ 𝑇 ∧ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)) ∈ ℝ) β†’ ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘) = (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
230189, 227, 229syl2anc 585 . . . . . . . . . . 11 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘) = (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
231230oveq2d 7378 . . . . . . . . . 10 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
232 elfzuz 13444 . . . . . . . . . . . . . 14 ((π‘š + 1) ∈ (0...𝑁) β†’ (π‘š + 1) ∈ (β„€β‰₯β€˜0))
2332323ad2ant3 1136 . . . . . . . . . . . . 13 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (π‘š + 1) ∈ (β„€β‰₯β€˜0))
234233adantr 482 . . . . . . . . . . . 12 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (π‘š + 1) ∈ (β„€β‰₯β€˜0))
235192adantr 482 . . . . . . . . . . . . 13 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ 𝐸 ∈ ℝ)
236211an32s 651 . . . . . . . . . . . . 13 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
237 remulcl 11143 . . . . . . . . . . . . . 14 ((𝐸 ∈ ℝ ∧ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
238237recnd 11190 . . . . . . . . . . . . 13 ((𝐸 ∈ ℝ ∧ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ β„‚)
239235, 236, 238syl2anc 585 . . . . . . . . . . . 12 ((((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (0...(π‘š + 1))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ β„‚)
240 fveq2 6847 . . . . . . . . . . . . . 14 (𝑖 = (π‘š + 1) β†’ (π‘‹β€˜π‘–) = (π‘‹β€˜(π‘š + 1)))
241240fveq1d 6849 . . . . . . . . . . . . 13 (𝑖 = (π‘š + 1) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) = ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))
242241oveq2d 7378 . . . . . . . . . . . 12 (𝑖 = (π‘š + 1) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))
243234, 239, 242fsumm1 15643 . . . . . . . . . . 11 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (Σ𝑖 ∈ (0...((π‘š + 1) βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
244 nn0cn 12430 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„•0 β†’ π‘š ∈ β„‚)
2452443ad2ant1 1134 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ π‘š ∈ β„‚)
246245adantr 482 . . . . . . . . . . . . . . 15 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ π‘š ∈ β„‚)
247 1cnd 11157 . . . . . . . . . . . . . . 15 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ 1 ∈ β„‚)
248246, 247pncand 11520 . . . . . . . . . . . . . 14 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘š + 1) βˆ’ 1) = π‘š)
249248oveq2d 7378 . . . . . . . . . . . . 13 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (0...((π‘š + 1) βˆ’ 1)) = (0...π‘š))
250249sumeq1d 15593 . . . . . . . . . . . 12 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (0...((π‘š + 1) βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
251250oveq1d 7377 . . . . . . . . . . 11 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ (Σ𝑖 ∈ (0...((π‘š + 1) βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))) = (Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
252243, 251eqtrd 2777 . . . . . . . . . 10 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘))))
253218, 231, 2523eqtr4rd 2788 . . . . . . . . 9 (((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘)))
254188, 253mpteq2da 5208 . . . . . . . 8 ((π‘š ∈ β„•0 ∧ πœ‘ ∧ (π‘š + 1) ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(π‘š + 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...π‘š)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ (𝐸 Β· ((π‘‹β€˜(π‘š + 1))β€˜π‘‘)))β€˜π‘‘))))
255254eleq1d 2823 . . . . . . 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 422 . . . 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 12605 . 2 (𝑁 ∈ β„•0 β†’ ((πœ‘ ∧ 𝑁 ∈ (0...𝑁)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴))
2612, 7, 260sylc 65 1 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  β„²wnf 1786   ∈ wcel 2107   βŠ† wss 3915  {csn 4591   class class class wbr 5110   ↦ cmpt 5193  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  β„•cn 12160  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  ...cfz 13431  Ξ£csu 15577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-fz 13432  df-fzo 13575  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-sum 15578
This theorem is referenced by:  stoweidlem60  44375
  Copyright terms: Public domain W3C validator