Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  esumpcvgval Structured version   Visualization version   GIF version

Theorem esumpcvgval 30114
Description: The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017.)
Hypotheses
Ref Expression
esumpcvgval.1 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))
esumpcvgval.2 (𝑘 = 𝑙𝐴 = 𝐵)
esumpcvgval.3 (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )
Assertion
Ref Expression
esumpcvgval (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)
Distinct variable groups:   𝑘,𝑙,𝑛   𝐴,𝑙,𝑛   𝐵,𝑘,𝑛   𝜑,𝑘,𝑛
Allowed substitution hints:   𝜑(𝑙)   𝐴(𝑘)   𝐵(𝑙)

Proof of Theorem esumpcvgval
Dummy variables 𝑠 𝑥 𝑦 𝑧 𝑏 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrltso 11959 . . . 4 < Or ℝ*
21a1i 11 . . 3 (𝜑 → < Or ℝ*)
3 nnuz 11708 . . . . 5 ℕ = (ℤ‘1)
4 1zzd 11393 . . . . 5 (𝜑 → 1 ∈ ℤ)
5 esumpcvgval.1 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))
6 esumpcvgval.2 . . . . . . . . . . . 12 (𝑘 = 𝑙𝐴 = 𝐵)
7 eqcom 2627 . . . . . . . . . . . 12 (𝑘 = 𝑙𝑙 = 𝑘)
8 eqcom 2627 . . . . . . . . . . . 12 (𝐴 = 𝐵𝐵 = 𝐴)
96, 7, 83imtr3i 280 . . . . . . . . . . 11 (𝑙 = 𝑘𝐵 = 𝐴)
109cbvmptv 4741 . . . . . . . . . 10 (𝑙 ∈ ℕ ↦ 𝐵) = (𝑘 ∈ ℕ ↦ 𝐴)
115, 10fmptd 6371 . . . . . . . . 9 (𝜑 → (𝑙 ∈ ℕ ↦ 𝐵):ℕ⟶(0[,)+∞))
1211ffvelrnda 6345 . . . . . . . 8 ((𝜑𝑥 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞))
13 elrege0 12263 . . . . . . . . 9 (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞) ↔ (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥)))
1413simplbi 476 . . . . . . . 8 (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ)
1512, 14syl 17 . . . . . . 7 ((𝜑𝑥 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ)
163, 4, 15serfre 12813 . . . . . 6 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)):ℕ⟶ℝ)
1711adantr 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑙 ∈ ℕ ↦ 𝐵):ℕ⟶(0[,)+∞))
18 simpr 477 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
1918peano2nnd 11022 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
2017, 19ffvelrnd 6346 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞))
21 elrege0 12263 . . . . . . . . . 10 (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) ↔ (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ ∧ 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
2221simprbi 480 . . . . . . . . 9 (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) → 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))
2320, 22syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))
2416ffvelrnda 6345 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ∈ ℝ)
2521simplbi 476 . . . . . . . . . 10 (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ)
2620, 25syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ)
2724, 26addge01d 10600 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))))
2823, 27mpbid 222 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
2918, 3syl6eleq 2709 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
30 seqp1 12799 . . . . . . . 8 (𝑛 ∈ (ℤ‘1) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)) = ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
3129, 30syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)) = ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
3228, 31breqtrrd 4672 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)))
33 simpr 477 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
3410fvmpt2 6278 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ 𝐴 ∈ (0[,)+∞)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
3533, 5, 34syl2anc 692 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
36 rge0ssre 12265 . . . . . . . . 9 (0[,)+∞) ⊆ ℝ
3736, 5sseldi 3593 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℝ)
3816feqmptd 6236 . . . . . . . . . 10 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)))
39 simpll 789 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑)
40 elfznn 12355 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
4140adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
4239, 41, 35syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
4337recnd 10053 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
4439, 41, 43syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ)
4542, 29, 44fsumser 14442 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
4645eqcomd 2626 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) = Σ𝑘 ∈ (1...𝑛)𝐴)
4746mpteq2dva 4735 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴))
4838, 47eqtr2d 2655 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) = seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)))
49 esumpcvgval.3 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )
5048, 49eqeltrrd 2700 . . . . . . . 8 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ∈ dom ⇝ )
513, 4, 35, 37, 50isumrecl 14477 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ℕ 𝐴 ∈ ℝ)
52 1zzd 11393 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 1 ∈ ℤ)
53 fzfid 12755 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
54 fzssuz 12367 . . . . . . . . . . . 12 (1...𝑛) ⊆ (ℤ‘1)
5554, 3sseqtr4i 3630 . . . . . . . . . . 11 (1...𝑛) ⊆ ℕ
5655a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ⊆ ℕ)
5735adantlr 750 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
5837adantlr 750 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℝ)
595adantlr 750 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))
60 elrege0 12263 . . . . . . . . . . . 12 (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
6160simprbi 480 . . . . . . . . . . 11 (𝐴 ∈ (0[,)+∞) → 0 ≤ 𝐴)
6259, 61syl 17 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 0 ≤ 𝐴)
6350adantr 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ∈ dom ⇝ )
643, 52, 53, 56, 57, 58, 62, 63isumless 14558 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)𝐴 ≤ Σ𝑘 ∈ ℕ 𝐴)
6545, 64eqbrtrrd 4668 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴)
6665ralrimiva 2963 . . . . . . 7 (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴)
67 breq2 4648 . . . . . . . . 9 (𝑠 = Σ𝑘 ∈ ℕ 𝐴 → ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴))
6867ralbidv 2983 . . . . . . . 8 (𝑠 = Σ𝑘 ∈ ℕ 𝐴 → (∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ↔ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴))
6968rspcev 3304 . . . . . . 7 ((Σ𝑘 ∈ ℕ 𝐴 ∈ ℝ ∧ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴) → ∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠)
7051, 66, 69syl2anc 692 . . . . . 6 (𝜑 → ∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠)
713, 4, 16, 32, 70climsup 14381 . . . . 5 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⇝ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
723, 4, 71, 24climrecl 14295 . . . 4 (𝜑 → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ)
7372rexrd 10074 . . 3 (𝜑 → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ*)
74 eqid 2620 . . . . . . 7 (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)
75 sumex 14399 . . . . . . 7 Σ𝑘𝑏 𝐴 ∈ V
7674, 75elrnmpti 5365 . . . . . 6 (𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴)
77 ssnnssfz 29523 . . . . . . . . . 10 (𝑏 ∈ (𝒫 ℕ ∩ Fin) → ∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚))
78 fzfid 12755 . . . . . . . . . . . . . 14 ((𝜑𝑏 ⊆ (1...𝑚)) → (1...𝑚) ∈ Fin)
79 elfznn 12355 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (1...𝑚) → 𝑘 ∈ ℕ)
8079, 5sylan2 491 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...𝑚)) → 𝐴 ∈ (0[,)+∞))
8160simplbi 476 . . . . . . . . . . . . . . . 16 (𝐴 ∈ (0[,)+∞) → 𝐴 ∈ ℝ)
8280, 81syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ)
8382adantlr 750 . . . . . . . . . . . . . 14 (((𝜑𝑏 ⊆ (1...𝑚)) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ)
8480, 61syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...𝑚)) → 0 ≤ 𝐴)
8584adantlr 750 . . . . . . . . . . . . . 14 (((𝜑𝑏 ⊆ (1...𝑚)) ∧ 𝑘 ∈ (1...𝑚)) → 0 ≤ 𝐴)
86 simpr 477 . . . . . . . . . . . . . 14 ((𝜑𝑏 ⊆ (1...𝑚)) → 𝑏 ⊆ (1...𝑚))
8778, 83, 85, 86fsumless 14509 . . . . . . . . . . . . 13 ((𝜑𝑏 ⊆ (1...𝑚)) → Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
8887ex 450 . . . . . . . . . . . 12 (𝜑 → (𝑏 ⊆ (1...𝑚) → Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
8988reximdv 3013 . . . . . . . . . . 11 (𝜑 → (∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚) → ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9089imp 445 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚)) → ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
9177, 90sylan2 491 . . . . . . . . 9 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
92 breq1 4647 . . . . . . . . . 10 (𝑥 = Σ𝑘𝑏 𝐴 → (𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴 ↔ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9392rexbidv 3048 . . . . . . . . 9 (𝑥 = Σ𝑘𝑏 𝐴 → (∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴 ↔ ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9491, 93syl5ibrcom 237 . . . . . . . 8 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (𝑥 = Σ𝑘𝑏 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9594rexlimdva 3027 . . . . . . 7 (𝜑 → (∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9695imp 445 . . . . . 6 ((𝜑 ∧ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴) → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
9776, 96sylan2b 492 . . . . 5 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
98 simpr 477 . . . . . . . . . 10 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑥 = Σ𝑘𝑏 𝐴) → 𝑥 = Σ𝑘𝑏 𝐴)
99 inss2 3826 . . . . . . . . . . . . 13 (𝒫 ℕ ∩ Fin) ⊆ Fin
100 simpr 477 . . . . . . . . . . . . 13 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → 𝑏 ∈ (𝒫 ℕ ∩ Fin))
10199, 100sseldi 3593 . . . . . . . . . . . 12 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → 𝑏 ∈ Fin)
102 simpll 789 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝜑)
103 inss1 3825 . . . . . . . . . . . . . . . . 17 (𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ
104 simplr 791 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑏 ∈ (𝒫 ℕ ∩ Fin))
105103, 104sseldi 3593 . . . . . . . . . . . . . . . 16 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑏 ∈ 𝒫 ℕ)
106105elpwid 4161 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑏 ⊆ ℕ)
107 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑘𝑏)
108106, 107sseldd 3596 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑘 ∈ ℕ)
109102, 108, 5syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝐴 ∈ (0[,)+∞))
110109, 81syl 17 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝐴 ∈ ℝ)
111101, 110fsumrecl 14446 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → Σ𝑘𝑏 𝐴 ∈ ℝ)
112111adantr 481 . . . . . . . . . 10 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑥 = Σ𝑘𝑏 𝐴) → Σ𝑘𝑏 𝐴 ∈ ℝ)
11398, 112eqeltrd 2699 . . . . . . . . 9 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑥 = Σ𝑘𝑏 𝐴) → 𝑥 ∈ ℝ)
114113r19.29an 3073 . . . . . . . 8 ((𝜑 ∧ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴) → 𝑥 ∈ ℝ)
11576, 114sylan2b 492 . . . . . . 7 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → 𝑥 ∈ ℝ)
116115adantr 481 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ∈ ℝ)
117 fzfid 12755 . . . . . . . 8 (𝜑 → (1...𝑚) ∈ Fin)
118117, 82fsumrecl 14446 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ℝ)
119118ad2antrr 761 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ℝ)
12072ad2antrr 761 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ)
121 simprr 795 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
122 frn 6040 . . . . . . . . 9 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)):ℕ⟶ℝ → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
12316, 122syl 17 . . . . . . . 8 (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
124123ad2antrr 761 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
125 1nn 11016 . . . . . . . . . 10 1 ∈ ℕ
126125ne0ii 3915 . . . . . . . . 9 ℕ ≠ ∅
127 dm0rn0 5331 . . . . . . . . . . 11 (dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅)
128 fdm 6038 . . . . . . . . . . . . 13 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)):ℕ⟶ℝ → dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ℕ)
12916, 128syl 17 . . . . . . . . . . . 12 (𝜑 → dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ℕ)
130129eqeq1d 2622 . . . . . . . . . . 11 (𝜑 → (dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ℕ = ∅))
131127, 130syl5bbr 274 . . . . . . . . . 10 (𝜑 → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ℕ = ∅))
132131necon3bid 2835 . . . . . . . . 9 (𝜑 → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ↔ ℕ ≠ ∅))
133126, 132mpbiri 248 . . . . . . . 8 (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅)
134133ad2antrr 761 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅)
135 1z 11392 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
136 seqfn 12796 . . . . . . . . . . . . . . . 16 (1 ∈ ℤ → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn (ℤ‘1))
137135, 136ax-mp 5 . . . . . . . . . . . . . . 15 seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn (ℤ‘1)
1383fneq2i 5974 . . . . . . . . . . . . . . 15 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn ℕ ↔ seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn (ℤ‘1))
139137, 138mpbir 221 . . . . . . . . . . . . . 14 seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn ℕ
140 dffn5 6228 . . . . . . . . . . . . . 14 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn ℕ ↔ seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)))
141139, 140mpbi 220 . . . . . . . . . . . . 13 seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
142 fvex 6188 . . . . . . . . . . . . 13 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ∈ V
143141, 142elrnmpti 5365 . . . . . . . . . . . 12 (𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
144 r19.29 3068 . . . . . . . . . . . . 13 ((∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → ∃𝑛 ∈ ℕ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)))
145 breq1 4647 . . . . . . . . . . . . . . 15 (𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → (𝑧𝑠 ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠))
146145biimparc 504 . . . . . . . . . . . . . 14 (((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧𝑠)
147146rexlimivw 3025 . . . . . . . . . . . . 13 (∃𝑛 ∈ ℕ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧𝑠)
148144, 147syl 17 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧𝑠)
149143, 148sylan2b 492 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) → 𝑧𝑠)
150149ralrimiva 2963 . . . . . . . . . 10 (∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 → ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
151150reximi 3008 . . . . . . . . 9 (∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
15270, 151syl 17 . . . . . . . 8 (𝜑 → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
153152ad2antrr 761 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
154 simpr 477 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
155 simpll 789 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝜑)
15679adantl 482 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝑘 ∈ ℕ)
157155, 156, 35syl2anc 692 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
158154, 3syl6eleq 2709 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ (ℤ‘1))
159155, 156, 5syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ (0[,)+∞))
160159, 81syl 17 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ)
161160recnd 10053 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℂ)
162157, 158, 161fsumser 14442 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚))
163 fveq2 6178 . . . . . . . . . . . 12 (𝑛 = 𝑚 → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚))
164163eqeq2d 2630 . . . . . . . . . . 11 (𝑛 = 𝑚 → (Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ↔ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚)))
165164rspcev 3304 . . . . . . . . . 10 ((𝑚 ∈ ℕ ∧ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚)) → ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
166154, 162, 165syl2anc 692 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
167141, 142elrnmpti 5365 . . . . . . . . 9 𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
168166, 167sylibr 224 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)))
169168ad2ant2r 782 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)))
170 suprub 10969 . . . . . . 7 (((ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠) ∧ Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) → Σ𝑘 ∈ (1...𝑚)𝐴 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
171124, 134, 153, 169, 170syl31anc 1327 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
172116, 119, 120, 121, 171letrd 10179 . . . . 5 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
17397, 172rexlimddv 3031 . . . 4 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → 𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
17472adantr 481 . . . . 5 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ)
175115, 174lenltd 10168 . . . 4 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → (𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) < 𝑥))
176173, 175mpbid 222 . . 3 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → ¬ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) < 𝑥)
177 simpr1r 1117 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0 ≤ 𝑥𝑥 = +∞)) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
1781773anassrs 1288 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
17973ad3antrrr 765 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ*)
180 pnfnlt 11947 . . . . . . . 8 (sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ* → ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
181179, 180syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
182 breq1 4647 . . . . . . . . 9 (𝑥 = +∞ → (𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )))
183182notbid 308 . . . . . . . 8 (𝑥 = +∞ → (¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )))
184183adantl 482 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → (¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )))
185181, 184mpbird 247 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → ¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
186178, 185pm2.21dd 186 . . . . 5 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
187 simplll 797 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝜑)
188 simpr1l 1116 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0 ≤ 𝑥𝑥 < +∞)) → 𝑥 ∈ ℝ*)
1891883anassrs 1288 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 ∈ ℝ*)
190 simplr 791 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 0 ≤ 𝑥)
191 simpr 477 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 < +∞)
192 0xr 10071 . . . . . . . 8 0 ∈ ℝ*
193 pnfxr 10077 . . . . . . . 8 +∞ ∈ ℝ*
194 elico1 12203 . . . . . . . 8 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥𝑥 < +∞)))
195192, 193, 194mp2an 707 . . . . . . 7 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥𝑥 < +∞))
196189, 190, 191, 195syl3anbrc 1244 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 ∈ (0[,)+∞))
197 simpr1r 1117 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0 ≤ 𝑥𝑥 < +∞)) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
1981973anassrs 1288 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
199123adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
200133adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅)
201152adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
202199, 200, 2013jca 1240 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠))
203 simprl 793 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → 𝑥 ∈ (0[,)+∞))
20436, 203sseldi 3593 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → 𝑥 ∈ ℝ)
205 simprr 795 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
206 suprlub 10972 . . . . . . . . 9 (((ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠) ∧ 𝑥 ∈ ℝ) → (𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦))
207206biimpa 501 . . . . . . . 8 ((((ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) → ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦)
208202, 204, 205, 207syl21anc 1323 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦)
20940ssriv 3599 . . . . . . . . . . . . . . . . 17 (1...𝑛) ⊆ ℕ
210 ovex 6663 . . . . . . . . . . . . . . . . . 18 (1...𝑛) ∈ V
211210elpw 4155 . . . . . . . . . . . . . . . . 17 ((1...𝑛) ∈ 𝒫 ℕ ↔ (1...𝑛) ⊆ ℕ)
212209, 211mpbir 221 . . . . . . . . . . . . . . . 16 (1...𝑛) ∈ 𝒫 ℕ
213 fzfi 12754 . . . . . . . . . . . . . . . 16 (1...𝑛) ∈ Fin
214 elin 3788 . . . . . . . . . . . . . . . 16 ((1...𝑛) ∈ (𝒫 ℕ ∩ Fin) ↔ ((1...𝑛) ∈ 𝒫 ℕ ∧ (1...𝑛) ∈ Fin))
215212, 213, 214mpbir2an 954 . . . . . . . . . . . . . . 15 (1...𝑛) ∈ (𝒫 ℕ ∩ Fin)
216215a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → (1...𝑛) ∈ (𝒫 ℕ ∩ Fin))
217 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
21845adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
219217, 218eqtr4d 2657 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴)
220 sumeq1 14400 . . . . . . . . . . . . . . . 16 (𝑏 = (1...𝑛) → Σ𝑘𝑏 𝐴 = Σ𝑘 ∈ (1...𝑛)𝐴)
221220eqeq2d 2630 . . . . . . . . . . . . . . 15 (𝑏 = (1...𝑛) → (𝑦 = Σ𝑘𝑏 𝐴𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴))
222221rspcev 3304 . . . . . . . . . . . . . 14 (((1...𝑛) ∈ (𝒫 ℕ ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴)
223216, 219, 222syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴)
224223ex 450 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴))
225224rexlimdva 3027 . . . . . . . . . . 11 (𝜑 → (∃𝑛 ∈ ℕ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴))
226141, 142elrnmpti 5365 . . . . . . . . . . 11 (𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
22774, 75elrnmpti 5365 . . . . . . . . . . 11 (𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴)
228225, 226, 2273imtr4g 285 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) → 𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)))
229228ssrdv 3601 . . . . . . . . 9 (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴))
230 ssrexv 3659 . . . . . . . . 9 (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) → (∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦))
231229, 230syl 17 . . . . . . . 8 (𝜑 → (∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦))
232231imp 445 . . . . . . 7 ((𝜑 ∧ ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
233208, 232syldan 487 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
234187, 196, 198, 233syl12anc 1322 . . . . 5 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
235 simplrl 799 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) → 𝑥 ∈ ℝ*)
236 xrlelttric 29491 . . . . . . . 8 ((+∞ ∈ ℝ*𝑥 ∈ ℝ*) → (+∞ ≤ 𝑥𝑥 < +∞))
237193, 236mpan 705 . . . . . . 7 (𝑥 ∈ ℝ* → (+∞ ≤ 𝑥𝑥 < +∞))
238 xgepnf 11981 . . . . . . . 8 (𝑥 ∈ ℝ* → (+∞ ≤ 𝑥𝑥 = +∞))
239238orbi1d 738 . . . . . . 7 (𝑥 ∈ ℝ* → ((+∞ ≤ 𝑥𝑥 < +∞) ↔ (𝑥 = +∞ ∨ 𝑥 < +∞)))
240237, 239mpbid 222 . . . . . 6 (𝑥 ∈ ℝ* → (𝑥 = +∞ ∨ 𝑥 < +∞))
241235, 240syl 17 . . . . 5 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) → (𝑥 = +∞ ∨ 𝑥 < +∞))
242186, 234, 241mpjaodan 826 . . . 4 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
243 0elpw 4825 . . . . . . . . 9 ∅ ∈ 𝒫 ℕ
244 0fin 8173 . . . . . . . . 9 ∅ ∈ Fin
245 elin 3788 . . . . . . . . 9 (∅ ∈ (𝒫 ℕ ∩ Fin) ↔ (∅ ∈ 𝒫 ℕ ∧ ∅ ∈ Fin))
246243, 244, 245mpbir2an 954 . . . . . . . 8 ∅ ∈ (𝒫 ℕ ∩ Fin)
247 sum0 14433 . . . . . . . . 9 Σ𝑘 ∈ ∅ 𝐴 = 0
248247eqcomi 2629 . . . . . . . 8 0 = Σ𝑘 ∈ ∅ 𝐴
249 sumeq1 14400 . . . . . . . . . 10 (𝑏 = ∅ → Σ𝑘𝑏 𝐴 = Σ𝑘 ∈ ∅ 𝐴)
250249eqeq2d 2630 . . . . . . . . 9 (𝑏 = ∅ → (0 = Σ𝑘𝑏 𝐴 ↔ 0 = Σ𝑘 ∈ ∅ 𝐴))
251250rspcev 3304 . . . . . . . 8 ((∅ ∈ (𝒫 ℕ ∩ Fin) ∧ 0 = Σ𝑘 ∈ ∅ 𝐴) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)0 = Σ𝑘𝑏 𝐴)
252246, 248, 251mp2an 707 . . . . . . 7 𝑏 ∈ (𝒫 ℕ ∩ Fin)0 = Σ𝑘𝑏 𝐴
25374, 75elrnmpti 5365 . . . . . . 7 (0 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)0 = Σ𝑘𝑏 𝐴)
254252, 253mpbir 221 . . . . . 6 0 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)
255 breq2 4648 . . . . . . 7 (𝑦 = 0 → (𝑥 < 𝑦𝑥 < 0))
256255rspcev 3304 . . . . . 6 ((0 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ∧ 𝑥 < 0) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
257254, 256mpan 705 . . . . 5 (𝑥 < 0 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
258257adantl 482 . . . 4 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 𝑥 < 0) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
259 xrlelttric 29491 . . . . . 6 ((0 ∈ ℝ*𝑥 ∈ ℝ*) → (0 ≤ 𝑥𝑥 < 0))
260192, 259mpan 705 . . . . 5 (𝑥 ∈ ℝ* → (0 ≤ 𝑥𝑥 < 0))
261260ad2antrl 763 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → (0 ≤ 𝑥𝑥 < 0))
262242, 258, 261mpjaodan 826 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
2632, 73, 176, 262eqsupd 8348 . 2 (𝜑 → sup(ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴), ℝ*, < ) = sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
264 nfv 1841 . . 3 𝑘𝜑
265 nfcv 2762 . . 3 𝑘
266 nnex 11011 . . . 4 ℕ ∈ V
267266a1i 11 . . 3 (𝜑 → ℕ ∈ V)
268 icossicc 12245 . . . 4 (0[,)+∞) ⊆ (0[,]+∞)
269268, 5sseldi 3593 . . 3 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))
270 elex 3207 . . . . . 6 (𝑏 ∈ (𝒫 ℕ ∩ Fin) → 𝑏 ∈ V)
271270adantl 482 . . . . 5 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → 𝑏 ∈ V)
272 eqid 2620 . . . . . 6 (𝑘𝑏𝐴) = (𝑘𝑏𝐴)
273109, 272fmptd 6371 . . . . 5 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (𝑘𝑏𝐴):𝑏⟶(0[,)+∞))
274 esumpfinvallem 30110 . . . . 5 ((𝑏 ∈ V ∧ (𝑘𝑏𝐴):𝑏⟶(0[,)+∞)) → (ℂfld Σg (𝑘𝑏𝐴)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑏𝐴)))
275271, 273, 274syl2anc 692 . . . 4 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (ℂfld Σg (𝑘𝑏𝐴)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑏𝐴)))
276110recnd 10053 . . . . 5 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝐴 ∈ ℂ)
277101, 276gsumfsum 19794 . . . 4 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (ℂfld Σg (𝑘𝑏𝐴)) = Σ𝑘𝑏 𝐴)
278275, 277eqtr3d 2656 . . 3 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑏𝐴)) = Σ𝑘𝑏 𝐴)
279264, 265, 267, 269, 278esumval 30082 . 2 (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = sup(ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴), ℝ*, < ))
2803, 4, 35, 43, 71isumclim 14469 . 2 (𝜑 → Σ𝑘 ∈ ℕ 𝐴 = sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
281263, 279, 2803eqtr4d 2664 1 (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1481  wcel 1988  wne 2791  wral 2909  wrex 2910  Vcvv 3195  cin 3566  wss 3567  c0 3907  𝒫 cpw 4149   class class class wbr 4644  cmpt 4720   Or wor 5024  dom cdm 5104  ran crn 5105   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  Fincfn 7940  supcsup 8331  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924  +∞cpnf 10056  *cxr 10058   < clt 10059  cle 10060  cn 11005  cz 11362  cuz 11672  [,)cico 12162  [,]cicc 12163  ...cfz 12311  seqcseq 12784  cli 14196  Σcsu 14397  s cress 15839   Σg cgsu 16082  *𝑠cxrs 16141  fldccnfld 19727  Σ*cesum 30063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999  ax-addf 10000  ax-mulf 10001
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-iin 4514  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-supp 7281  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fsupp 8261  df-fi 8302  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-q 11774  df-rp 11818  df-xadd 11932  df-ioo 12164  df-ioc 12165  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-fl 12576  df-seq 12785  df-exp 12844  df-hash 13101  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-clim 14200  df-rlim 14201  df-sum 14398  df-struct 15840  df-ndx 15841  df-slot 15842  df-base 15844  df-sets 15845  df-ress 15846  df-plusg 15935  df-mulr 15936  df-starv 15937  df-tset 15941  df-ple 15942  df-ds 15945  df-unif 15946  df-rest 16064  df-topn 16065  df-0g 16083  df-gsum 16084  df-topgen 16085  df-ordt 16142  df-xrs 16143  df-mre 16227  df-mrc 16228  df-acs 16230  df-ps 17181  df-tsr 17182  df-mgm 17223  df-sgrp 17265  df-mnd 17276  df-submnd 17317  df-grp 17406  df-minusg 17407  df-cntz 17731  df-cmn 18176  df-abl 18177  df-mgp 18471  df-ur 18483  df-ring 18530  df-cring 18531  df-fbas 19724  df-fg 19725  df-cnfld 19728  df-top 20680  df-topon 20697  df-topsp 20718  df-bases 20731  df-ntr 20805  df-nei 20883  df-cn 21012  df-haus 21100  df-fil 21631  df-fm 21723  df-flim 21724  df-flf 21725  df-tsms 21911  df-esum 30064
This theorem is referenced by:  esumcvg  30122  esumcvgsum  30124
  Copyright terms: Public domain W3C validator