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

Theorem stoweidlem20 45034
Description: If a set A of real functions from a common domain T is closed under the sum of two functions, then it is closed under the sum of a finite number of functions, indexed by G. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem20.1 β„²π‘‘πœ‘
stoweidlem20.2 𝐹 = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘))
stoweidlem20.3 (πœ‘ β†’ 𝑀 ∈ β„•)
stoweidlem20.4 (πœ‘ β†’ 𝐺:(1...𝑀)⟢𝐴)
stoweidlem20.5 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
stoweidlem20.6 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
Assertion
Ref Expression
stoweidlem20 (πœ‘ β†’ 𝐹 ∈ 𝐴)
Distinct variable groups:   𝑓,𝑔,𝑖,𝑑,𝐺   𝐴,𝑓,𝑔   𝑇,𝑓,𝑔,𝑖,𝑑   πœ‘,𝑓,𝑔,𝑖   𝑖,𝑀,𝑑
Allowed substitution hints:   πœ‘(𝑑)   𝐴(𝑑,𝑖)   𝐹(𝑑,𝑓,𝑔,𝑖)   𝑀(𝑓,𝑔)

Proof of Theorem stoweidlem20
Dummy variables 𝑦 𝑛 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem20.2 . 2 𝐹 = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘))
2 stoweidlem20.3 . . 3 (πœ‘ β†’ 𝑀 ∈ β„•)
32nnred 12231 . . . . 5 (πœ‘ β†’ 𝑀 ∈ ℝ)
43leidd 11784 . . . 4 (πœ‘ β†’ 𝑀 ≀ 𝑀)
54ancli 547 . . 3 (πœ‘ β†’ (πœ‘ ∧ 𝑀 ≀ 𝑀))
6 eleq1 2819 . . . . 5 (𝑛 = 𝑀 β†’ (𝑛 ∈ β„• ↔ 𝑀 ∈ β„•))
7 breq1 5150 . . . . . . 7 (𝑛 = 𝑀 β†’ (𝑛 ≀ 𝑀 ↔ 𝑀 ≀ 𝑀))
87anbi2d 627 . . . . . 6 (𝑛 = 𝑀 β†’ ((πœ‘ ∧ 𝑛 ≀ 𝑀) ↔ (πœ‘ ∧ 𝑀 ≀ 𝑀)))
9 oveq2 7419 . . . . . . . . 9 (𝑛 = 𝑀 β†’ (1...𝑛) = (1...𝑀))
109sumeq1d 15651 . . . . . . . 8 (𝑛 = 𝑀 β†’ Σ𝑖 ∈ (1...𝑛)((πΊβ€˜π‘–)β€˜π‘‘) = Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘))
1110mpteq2dv 5249 . . . . . . 7 (𝑛 = 𝑀 β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((πΊβ€˜π‘–)β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)))
1211eleq1d 2816 . . . . . 6 (𝑛 = 𝑀 β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴))
138, 12imbi12d 343 . . . . 5 (𝑛 = 𝑀 β†’ (((πœ‘ ∧ 𝑛 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) ↔ ((πœ‘ ∧ 𝑀 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)))
146, 13imbi12d 343 . . . 4 (𝑛 = 𝑀 β†’ ((𝑛 ∈ β„• β†’ ((πœ‘ ∧ 𝑛 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)) ↔ (𝑀 ∈ β„• β†’ ((πœ‘ ∧ 𝑀 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴))))
15 breq1 5150 . . . . . . 7 (π‘₯ = 1 β†’ (π‘₯ ≀ 𝑀 ↔ 1 ≀ 𝑀))
1615anbi2d 627 . . . . . 6 (π‘₯ = 1 β†’ ((πœ‘ ∧ π‘₯ ≀ 𝑀) ↔ (πœ‘ ∧ 1 ≀ 𝑀)))
17 oveq2 7419 . . . . . . . . 9 (π‘₯ = 1 β†’ (1...π‘₯) = (1...1))
1817sumeq1d 15651 . . . . . . . 8 (π‘₯ = 1 β†’ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘) = Σ𝑖 ∈ (1...1)((πΊβ€˜π‘–)β€˜π‘‘))
1918mpteq2dv 5249 . . . . . . 7 (π‘₯ = 1 β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((πΊβ€˜π‘–)β€˜π‘‘)))
2019eleq1d 2816 . . . . . 6 (π‘₯ = 1 β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴))
2116, 20imbi12d 343 . . . . 5 (π‘₯ = 1 β†’ (((πœ‘ ∧ π‘₯ ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) ↔ ((πœ‘ ∧ 1 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)))
22 breq1 5150 . . . . . . 7 (π‘₯ = 𝑦 β†’ (π‘₯ ≀ 𝑀 ↔ 𝑦 ≀ 𝑀))
2322anbi2d 627 . . . . . 6 (π‘₯ = 𝑦 β†’ ((πœ‘ ∧ π‘₯ ≀ 𝑀) ↔ (πœ‘ ∧ 𝑦 ≀ 𝑀)))
24 oveq2 7419 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ (1...π‘₯) = (1...𝑦))
2524sumeq1d 15651 . . . . . . . 8 (π‘₯ = 𝑦 β†’ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘) = Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))
2625mpteq2dv 5249 . . . . . . 7 (π‘₯ = 𝑦 β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)))
2726eleq1d 2816 . . . . . 6 (π‘₯ = 𝑦 β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴))
2823, 27imbi12d 343 . . . . 5 (π‘₯ = 𝑦 β†’ (((πœ‘ ∧ π‘₯ ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) ↔ ((πœ‘ ∧ 𝑦 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)))
29 breq1 5150 . . . . . . 7 (π‘₯ = (𝑦 + 1) β†’ (π‘₯ ≀ 𝑀 ↔ (𝑦 + 1) ≀ 𝑀))
3029anbi2d 627 . . . . . 6 (π‘₯ = (𝑦 + 1) β†’ ((πœ‘ ∧ π‘₯ ≀ 𝑀) ↔ (πœ‘ ∧ (𝑦 + 1) ≀ 𝑀)))
31 oveq2 7419 . . . . . . . . 9 (π‘₯ = (𝑦 + 1) β†’ (1...π‘₯) = (1...(𝑦 + 1)))
3231sumeq1d 15651 . . . . . . . 8 (π‘₯ = (𝑦 + 1) β†’ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘) = Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘))
3332mpteq2dv 5249 . . . . . . 7 (π‘₯ = (𝑦 + 1) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘)))
3433eleq1d 2816 . . . . . 6 (π‘₯ = (𝑦 + 1) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴))
3530, 34imbi12d 343 . . . . 5 (π‘₯ = (𝑦 + 1) β†’ (((πœ‘ ∧ π‘₯ ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) ↔ ((πœ‘ ∧ (𝑦 + 1) ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)))
36 breq1 5150 . . . . . . 7 (π‘₯ = 𝑛 β†’ (π‘₯ ≀ 𝑀 ↔ 𝑛 ≀ 𝑀))
3736anbi2d 627 . . . . . 6 (π‘₯ = 𝑛 β†’ ((πœ‘ ∧ π‘₯ ≀ 𝑀) ↔ (πœ‘ ∧ 𝑛 ≀ 𝑀)))
38 oveq2 7419 . . . . . . . . 9 (π‘₯ = 𝑛 β†’ (1...π‘₯) = (1...𝑛))
3938sumeq1d 15651 . . . . . . . 8 (π‘₯ = 𝑛 β†’ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘) = Σ𝑖 ∈ (1...𝑛)((πΊβ€˜π‘–)β€˜π‘‘))
4039mpteq2dv 5249 . . . . . . 7 (π‘₯ = 𝑛 β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((πΊβ€˜π‘–)β€˜π‘‘)))
4140eleq1d 2816 . . . . . 6 (π‘₯ = 𝑛 β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴))
4237, 41imbi12d 343 . . . . 5 (π‘₯ = 𝑛 β†’ (((πœ‘ ∧ π‘₯ ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...π‘₯)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) ↔ ((πœ‘ ∧ 𝑛 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)))
43 stoweidlem20.1 . . . . . . . . 9 β„²π‘‘πœ‘
44 1z 12596 . . . . . . . . . 10 1 ∈ β„€
45 stoweidlem20.4 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐺:(1...𝑀)⟢𝐴)
46 nnuz 12869 . . . . . . . . . . . . . . . 16 β„• = (β„€β‰₯β€˜1)
472, 46eleqtrdi 2841 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
48 eluzfz1 13512 . . . . . . . . . . . . . . 15 (𝑀 ∈ (β„€β‰₯β€˜1) β†’ 1 ∈ (1...𝑀))
4947, 48syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 1 ∈ (1...𝑀))
5045, 49ffvelcdmd 7086 . . . . . . . . . . . . 13 (πœ‘ β†’ (πΊβ€˜1) ∈ 𝐴)
5150ancli 547 . . . . . . . . . . . . 13 (πœ‘ β†’ (πœ‘ ∧ (πΊβ€˜1) ∈ 𝐴))
52 eleq1 2819 . . . . . . . . . . . . . . . 16 (𝑓 = (πΊβ€˜1) β†’ (𝑓 ∈ 𝐴 ↔ (πΊβ€˜1) ∈ 𝐴))
5352anbi2d 627 . . . . . . . . . . . . . . 15 (𝑓 = (πΊβ€˜1) β†’ ((πœ‘ ∧ 𝑓 ∈ 𝐴) ↔ (πœ‘ ∧ (πΊβ€˜1) ∈ 𝐴)))
54 feq1 6697 . . . . . . . . . . . . . . 15 (𝑓 = (πΊβ€˜1) β†’ (𝑓:π‘‡βŸΆβ„ ↔ (πΊβ€˜1):π‘‡βŸΆβ„))
5553, 54imbi12d 343 . . . . . . . . . . . . . 14 (𝑓 = (πΊβ€˜1) β†’ (((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„) ↔ ((πœ‘ ∧ (πΊβ€˜1) ∈ 𝐴) β†’ (πΊβ€˜1):π‘‡βŸΆβ„)))
56 stoweidlem20.6 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
5755, 56vtoclg 3541 . . . . . . . . . . . . 13 ((πΊβ€˜1) ∈ 𝐴 β†’ ((πœ‘ ∧ (πΊβ€˜1) ∈ 𝐴) β†’ (πΊβ€˜1):π‘‡βŸΆβ„))
5850, 51, 57sylc 65 . . . . . . . . . . . 12 (πœ‘ β†’ (πΊβ€˜1):π‘‡βŸΆβ„)
5958ffvelcdmda 7085 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((πΊβ€˜1)β€˜π‘‘) ∈ ℝ)
6059recnd 11246 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((πΊβ€˜1)β€˜π‘‘) ∈ β„‚)
61 fveq2 6890 . . . . . . . . . . . 12 (𝑖 = 1 β†’ (πΊβ€˜π‘–) = (πΊβ€˜1))
6261fveq1d 6892 . . . . . . . . . . 11 (𝑖 = 1 β†’ ((πΊβ€˜π‘–)β€˜π‘‘) = ((πΊβ€˜1)β€˜π‘‘))
6362fsum1 15697 . . . . . . . . . 10 ((1 ∈ β„€ ∧ ((πΊβ€˜1)β€˜π‘‘) ∈ β„‚) β†’ Σ𝑖 ∈ (1...1)((πΊβ€˜π‘–)β€˜π‘‘) = ((πΊβ€˜1)β€˜π‘‘))
6444, 60, 63sylancr 585 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (1...1)((πΊβ€˜π‘–)β€˜π‘‘) = ((πΊβ€˜1)β€˜π‘‘))
6543, 64mpteq2da 5245 . . . . . . . 8 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((πΊβ€˜π‘–)β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ ((πΊβ€˜1)β€˜π‘‘)))
6658feqmptd 6959 . . . . . . . 8 (πœ‘ β†’ (πΊβ€˜1) = (𝑑 ∈ 𝑇 ↦ ((πΊβ€˜1)β€˜π‘‘)))
6765, 66eqtr4d 2773 . . . . . . 7 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((πΊβ€˜π‘–)β€˜π‘‘)) = (πΊβ€˜1))
6867, 50eqeltrd 2831 . . . . . 6 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)
6968adantr 479 . . . . 5 ((πœ‘ ∧ 1 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)
70 simprl 767 . . . . . . 7 (((𝑦 ∈ β„• ∧ ((πœ‘ ∧ 𝑦 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)) ∧ (πœ‘ ∧ (𝑦 + 1) ≀ 𝑀)) β†’ πœ‘)
71 simpll 763 . . . . . . 7 (((𝑦 ∈ β„• ∧ ((πœ‘ ∧ 𝑦 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)) ∧ (πœ‘ ∧ (𝑦 + 1) ≀ 𝑀)) β†’ 𝑦 ∈ β„•)
72 simprr 769 . . . . . . 7 (((𝑦 ∈ β„• ∧ ((πœ‘ ∧ 𝑦 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)) ∧ (πœ‘ ∧ (𝑦 + 1) ≀ 𝑀)) β†’ (𝑦 + 1) ≀ 𝑀)
73 simp1 1134 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ πœ‘)
74 nnre 12223 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ 𝑦 ∈ ℝ)
75743ad2ant2 1132 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ 𝑦 ∈ ℝ)
76 1red 11219 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ 1 ∈ ℝ)
7775, 76readdcld 11247 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ (𝑦 + 1) ∈ ℝ)
7823ad2ant1 1131 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ 𝑀 ∈ β„•)
7978nnred 12231 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ 𝑀 ∈ ℝ)
8075lep1d 12149 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ 𝑦 ≀ (𝑦 + 1))
81 simp3 1136 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ (𝑦 + 1) ≀ 𝑀)
8275, 77, 79, 80, 81letrd 11375 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ 𝑦 ≀ 𝑀)
8373, 82jca 510 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ (πœ‘ ∧ 𝑦 ≀ 𝑀))
8470, 71, 72, 83syl3anc 1369 . . . . . . . 8 (((𝑦 ∈ β„• ∧ ((πœ‘ ∧ 𝑦 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)) ∧ (πœ‘ ∧ (𝑦 + 1) ≀ 𝑀)) β†’ (πœ‘ ∧ 𝑦 ≀ 𝑀))
85 simplr 765 . . . . . . . 8 (((𝑦 ∈ β„• ∧ ((πœ‘ ∧ 𝑦 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)) ∧ (πœ‘ ∧ (𝑦 + 1) ≀ 𝑀)) β†’ ((πœ‘ ∧ 𝑦 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴))
8684, 85mpd 15 . . . . . . 7 (((𝑦 ∈ β„• ∧ ((πœ‘ ∧ 𝑦 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)) ∧ (πœ‘ ∧ (𝑦 + 1) ≀ 𝑀)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)
87 nfv 1915 . . . . . . . . . . 11 Ⅎ𝑑 𝑦 ∈ β„•
88 nfv 1915 . . . . . . . . . . 11 Ⅎ𝑑(𝑦 + 1) ≀ 𝑀
8943, 87, 88nf3an 1902 . . . . . . . . . 10 Ⅎ𝑑(πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀)
90 simpl2 1190 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ 𝑦 ∈ β„•)
9190, 46eleqtrdi 2841 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ 𝑦 ∈ (β„€β‰₯β€˜1))
92 simpll1 1210 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ πœ‘)
93 1zzd 12597 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ 1 ∈ β„€)
942nnzd 12589 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑀 ∈ β„€)
95943ad2ant1 1131 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ 𝑀 ∈ β„€)
9695ad2antrr 722 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ 𝑀 ∈ β„€)
97 elfzelz 13505 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...(𝑦 + 1)) β†’ 𝑖 ∈ β„€)
9897adantl 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ 𝑖 ∈ β„€)
99 elfzle1 13508 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...(𝑦 + 1)) β†’ 1 ≀ 𝑖)
10099adantl 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ 1 ≀ 𝑖)
10197zred 12670 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...(𝑦 + 1)) β†’ 𝑖 ∈ ℝ)
102101adantl 480 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ 𝑖 ∈ ℝ)
10377ad2antrr 722 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ (𝑦 + 1) ∈ ℝ)
10479ad2antrr 722 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ 𝑀 ∈ ℝ)
105 elfzle2 13509 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...(𝑦 + 1)) β†’ 𝑖 ≀ (𝑦 + 1))
106105adantl 480 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ 𝑖 ≀ (𝑦 + 1))
107 simpll3 1212 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ (𝑦 + 1) ≀ 𝑀)
108102, 103, 104, 106, 107letrd 11375 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ 𝑖 ≀ 𝑀)
10993, 96, 98, 100, 108elfzd 13496 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ 𝑖 ∈ (1...𝑀))
110 simplr 765 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ 𝑑 ∈ 𝑇)
11145ffvelcdmda 7085 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ (πΊβ€˜π‘–) ∈ 𝐴)
1121113adant3 1130 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ (πΊβ€˜π‘–) ∈ 𝐴)
113 simp1 1134 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ πœ‘)
114113, 112jca 510 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ (πœ‘ ∧ (πΊβ€˜π‘–) ∈ 𝐴))
115 eleq1 2819 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (πΊβ€˜π‘–) β†’ (𝑓 ∈ 𝐴 ↔ (πΊβ€˜π‘–) ∈ 𝐴))
116115anbi2d 627 . . . . . . . . . . . . . . . . . 18 (𝑓 = (πΊβ€˜π‘–) β†’ ((πœ‘ ∧ 𝑓 ∈ 𝐴) ↔ (πœ‘ ∧ (πΊβ€˜π‘–) ∈ 𝐴)))
117 feq1 6697 . . . . . . . . . . . . . . . . . 18 (𝑓 = (πΊβ€˜π‘–) β†’ (𝑓:π‘‡βŸΆβ„ ↔ (πΊβ€˜π‘–):π‘‡βŸΆβ„))
118116, 117imbi12d 343 . . . . . . . . . . . . . . . . 17 (𝑓 = (πΊβ€˜π‘–) β†’ (((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„) ↔ ((πœ‘ ∧ (πΊβ€˜π‘–) ∈ 𝐴) β†’ (πΊβ€˜π‘–):π‘‡βŸΆβ„)))
119118, 56vtoclg 3541 . . . . . . . . . . . . . . . 16 ((πΊβ€˜π‘–) ∈ 𝐴 β†’ ((πœ‘ ∧ (πΊβ€˜π‘–) ∈ 𝐴) β†’ (πΊβ€˜π‘–):π‘‡βŸΆβ„))
120112, 114, 119sylc 65 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ (πΊβ€˜π‘–):π‘‡βŸΆβ„)
121 simp3 1136 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ 𝑑 ∈ 𝑇)
122120, 121ffvelcdmd 7086 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ ((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
123122recnd 11246 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ ((πΊβ€˜π‘–)β€˜π‘‘) ∈ β„‚)
12492, 109, 110, 123syl3anc 1369 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) β†’ ((πΊβ€˜π‘–)β€˜π‘‘) ∈ β„‚)
125 fveq2 6890 . . . . . . . . . . . . 13 (𝑖 = (𝑦 + 1) β†’ (πΊβ€˜π‘–) = (πΊβ€˜(𝑦 + 1)))
126125fveq1d 6892 . . . . . . . . . . . 12 (𝑖 = (𝑦 + 1) β†’ ((πΊβ€˜π‘–)β€˜π‘‘) = ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))
12791, 124, 126fsump1 15706 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘) = (Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘) + ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)))
128 simpr 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ 𝑑 ∈ 𝑇)
129 fzfid 13942 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ (1...𝑦) ∈ Fin)
130 simpll1 1210 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) β†’ πœ‘)
131 1zzd 12597 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) β†’ 1 ∈ β„€)
13295ad2antrr 722 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑀 ∈ β„€)
133 elfzelz 13505 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑦) β†’ 𝑖 ∈ β„€)
134133adantl 480 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑖 ∈ β„€)
135 elfzle1 13508 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑦) β†’ 1 ≀ 𝑖)
136135adantl 480 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) β†’ 1 ≀ 𝑖)
137133zred 12670 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑦) β†’ 𝑖 ∈ ℝ)
138137adantl 480 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑖 ∈ ℝ)
13977adantr 479 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) β†’ (𝑦 + 1) ∈ ℝ)
14079adantr 479 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑀 ∈ ℝ)
14175adantr 479 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑦 ∈ ℝ)
142 elfzle2 13509 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (1...𝑦) β†’ 𝑖 ≀ 𝑦)
143142adantl 480 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑖 ≀ 𝑦)
144 letrp1 12062 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑖 ≀ 𝑦) β†’ 𝑖 ≀ (𝑦 + 1))
145138, 141, 143, 144syl3anc 1369 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑖 ≀ (𝑦 + 1))
146 simpl3 1191 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) β†’ (𝑦 + 1) ≀ 𝑀)
147138, 139, 140, 145, 146letrd 11375 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑖 ≀ 𝑀)
148147adantlr 711 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑖 ≀ 𝑀)
149131, 132, 134, 136, 148elfzd 13496 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑖 ∈ (1...𝑀))
150 simplr 765 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) β†’ 𝑑 ∈ 𝑇)
151130, 149, 150, 122syl3anc 1369 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) β†’ ((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
152129, 151fsumrecl 15684 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
153 eqid 2730 . . . . . . . . . . . . . 14 (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))
154153fvmpt2 7008 . . . . . . . . . . . . 13 ((𝑑 ∈ 𝑇 ∧ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) = Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))
155128, 152, 154syl2anc 582 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) = Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))
156155oveq1d 7426 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)) = (Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘) + ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)))
157127, 156eqtr4d 2773 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘) = (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)))
15889, 157mpteq2da 5245 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))))
159158adantr 479 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))))
160 1zzd 12597 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ 1 ∈ β„€)
161 peano2nn 12228 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ β„• β†’ (𝑦 + 1) ∈ β„•)
162161nnzd 12589 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ β„• β†’ (𝑦 + 1) ∈ β„€)
1631623ad2ant2 1132 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ (𝑦 + 1) ∈ β„€)
164161nnge1d 12264 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ β„• β†’ 1 ≀ (𝑦 + 1))
1651643ad2ant2 1132 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ 1 ≀ (𝑦 + 1))
166160, 95, 163, 165, 81elfzd 13496 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ (𝑦 + 1) ∈ (1...𝑀))
16745ffvelcdmda 7085 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑦 + 1) ∈ (1...𝑀)) β†’ (πΊβ€˜(𝑦 + 1)) ∈ 𝐴)
16873, 166, 167syl2anc 582 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ (πΊβ€˜(𝑦 + 1)) ∈ 𝐴)
169 eleq1 2819 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (πΊβ€˜(𝑦 + 1)) β†’ (𝑓 ∈ 𝐴 ↔ (πΊβ€˜(𝑦 + 1)) ∈ 𝐴))
170169anbi2d 627 . . . . . . . . . . . . . . . . . 18 (𝑓 = (πΊβ€˜(𝑦 + 1)) β†’ ((πœ‘ ∧ 𝑓 ∈ 𝐴) ↔ (πœ‘ ∧ (πΊβ€˜(𝑦 + 1)) ∈ 𝐴)))
171 feq1 6697 . . . . . . . . . . . . . . . . . 18 (𝑓 = (πΊβ€˜(𝑦 + 1)) β†’ (𝑓:π‘‡βŸΆβ„ ↔ (πΊβ€˜(𝑦 + 1)):π‘‡βŸΆβ„))
172170, 171imbi12d 343 . . . . . . . . . . . . . . . . 17 (𝑓 = (πΊβ€˜(𝑦 + 1)) β†’ (((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„) ↔ ((πœ‘ ∧ (πΊβ€˜(𝑦 + 1)) ∈ 𝐴) β†’ (πΊβ€˜(𝑦 + 1)):π‘‡βŸΆβ„)))
173172, 56vtoclg 3541 . . . . . . . . . . . . . . . 16 ((πΊβ€˜(𝑦 + 1)) ∈ 𝐴 β†’ ((πœ‘ ∧ (πΊβ€˜(𝑦 + 1)) ∈ 𝐴) β†’ (πΊβ€˜(𝑦 + 1)):π‘‡βŸΆβ„))
174173anabsi7 667 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (πΊβ€˜(𝑦 + 1)) ∈ 𝐴) β†’ (πΊβ€˜(𝑦 + 1)):π‘‡βŸΆβ„)
17573, 168, 174syl2anc 582 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ (πΊβ€˜(𝑦 + 1)):π‘‡βŸΆβ„)
176175ffvelcdmda 7085 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘) ∈ ℝ)
177 eqid 2730 . . . . . . . . . . . . . 14 (𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))
178177fvmpt2 7008 . . . . . . . . . . . . 13 ((𝑑 ∈ 𝑇 ∧ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘) ∈ ℝ) β†’ ((𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))β€˜π‘‘) = ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))
179128, 176, 178syl2anc 582 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ ((𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))β€˜π‘‘) = ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))
180179oveq2d 7427 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ 𝑑 ∈ 𝑇) β†’ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))β€˜π‘‘)) = (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)))
18189, 180mpteq2da 5245 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))))
182181adantr 479 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))))
183 simpl1 1189 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) β†’ πœ‘)
184 simpr 483 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)
185166adantr 479 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) β†’ (𝑦 + 1) ∈ (1...𝑀))
186174feqmptd 6959 . . . . . . . . . . . . 13 ((πœ‘ ∧ (πΊβ€˜(𝑦 + 1)) ∈ 𝐴) β†’ (πΊβ€˜(𝑦 + 1)) = (𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)))
187167, 186syldan 589 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 + 1) ∈ (1...𝑀)) β†’ (πΊβ€˜(𝑦 + 1)) = (𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)))
188187, 167eqeltrrd 2832 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 + 1) ∈ (1...𝑀)) β†’ (𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)) ∈ 𝐴)
189183, 185, 188syl2anc 582 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)) ∈ 𝐴)
190 stoweidlem20.5 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
191 nfmpt1 5255 . . . . . . . . . . 11 Ⅎ𝑑(𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))
192 nfmpt1 5255 . . . . . . . . . . 11 Ⅎ𝑑(𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))
193190, 191, 192stoweidlem8 45022 . . . . . . . . . 10 ((πœ‘ ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴 ∧ (𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘)) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))β€˜π‘‘))) ∈ 𝐴)
194183, 184, 189, 193syl3anc 1369 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((𝑑 ∈ 𝑇 ↦ ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))β€˜π‘‘))) ∈ 𝐴)
195182, 194eqeltrrd 2832 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘))β€˜π‘‘) + ((πΊβ€˜(𝑦 + 1))β€˜π‘‘))) ∈ 𝐴)
196159, 195eqeltrd 2831 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ β„• ∧ (𝑦 + 1) ≀ 𝑀) ∧ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)
19770, 71, 72, 86, 196syl31anc 1371 . . . . . 6 (((𝑦 ∈ β„• ∧ ((πœ‘ ∧ 𝑦 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)) ∧ (πœ‘ ∧ (𝑦 + 1) ≀ 𝑀)) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)
198197exp31 418 . . . . 5 (𝑦 ∈ β„• β†’ (((πœ‘ ∧ 𝑦 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴) β†’ ((πœ‘ ∧ (𝑦 + 1) ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)))
19921, 28, 35, 42, 69, 198nnind 12234 . . . 4 (𝑛 ∈ β„• β†’ ((πœ‘ ∧ 𝑛 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴))
20014, 199vtoclg 3541 . . 3 (𝑀 ∈ β„• β†’ (𝑀 ∈ β„• β†’ ((πœ‘ ∧ 𝑀 ≀ 𝑀) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)))
2012, 2, 5, 200syl3c 66 . 2 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)) ∈ 𝐴)
2021, 201eqeltrid 2835 1 (πœ‘ β†’ 𝐹 ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539  β„²wnf 1783   ∈ wcel 2104   class class class wbr 5147   ↦ cmpt 5230  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411  β„‚cc 11110  β„cr 11111  1c1 11113   + caddc 11115   ≀ cle 11253  β„•cn 12216  β„€cz 12562  β„€β‰₯cuz 12826  ...cfz 13488  Ξ£csu 15636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  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 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-rp 12979  df-fz 13489  df-fzo 13632  df-seq 13971  df-exp 14032  df-hash 14295  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-clim 15436  df-sum 15637
This theorem is referenced by:  stoweidlem32  45046
  Copyright terms: Public domain W3C validator