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

Theorem esumpcvgval 29467
 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 11850 . . . 4 < Or ℝ*
21a1i 11 . . 3 (𝜑 → < Or ℝ*)
3 nnuz 11599 . . . . 5 ℕ = (ℤ‘1)
4 1zzd 11285 . . . . 5 (𝜑 → 1 ∈ ℤ)
5 esumpcvgval.1 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))
6 esumpcvgval.2 . . . . . . . . . . . 12 (𝑘 = 𝑙𝐴 = 𝐵)
7 eqcom 2617 . . . . . . . . . . . 12 (𝑘 = 𝑙𝑙 = 𝑘)
8 eqcom 2617 . . . . . . . . . . . 12 (𝐴 = 𝐵𝐵 = 𝐴)
96, 7, 83imtr3i 279 . . . . . . . . . . 11 (𝑙 = 𝑘𝐵 = 𝐴)
109cbvmptv 4678 . . . . . . . . . 10 (𝑙 ∈ ℕ ↦ 𝐵) = (𝑘 ∈ ℕ ↦ 𝐴)
115, 10fmptd 6292 . . . . . . . . 9 (𝜑 → (𝑙 ∈ ℕ ↦ 𝐵):ℕ⟶(0[,)+∞))
1211ffvelrnda 6267 . . . . . . . 8 ((𝜑𝑥 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞))
13 elrege0 12149 . . . . . . . . 9 (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞) ↔ (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥)))
1413simplbi 475 . . . . . . . 8 (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ)
1512, 14syl 17 . . . . . . 7 ((𝜑𝑥 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ)
163, 4, 15serfre 12692 . . . . . 6 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)):ℕ⟶ℝ)
1711adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑙 ∈ ℕ ↦ 𝐵):ℕ⟶(0[,)+∞))
18 simpr 476 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
1918peano2nnd 10914 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
2017, 19ffvelrnd 6268 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞))
21 elrege0 12149 . . . . . . . . . 10 (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) ↔ (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ ∧ 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
2221simprbi 479 . . . . . . . . 9 (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) → 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))
2320, 22syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))
2416ffvelrnda 6267 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ∈ ℝ)
2521simplbi 475 . . . . . . . . . 10 (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ)
2620, 25syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ)
2724, 26addge01d 10494 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))))
2823, 27mpbid 221 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
2918, 3syl6eleq 2698 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
30 seqp1 12678 . . . . . . . 8 (𝑛 ∈ (ℤ‘1) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)) = ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
3129, 30syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)) = ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
3228, 31breqtrrd 4611 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)))
33 simpr 476 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
3410fvmpt2 6200 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ 𝐴 ∈ (0[,)+∞)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
3533, 5, 34syl2anc 691 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
36 rge0ssre 12151 . . . . . . . . 9 (0[,)+∞) ⊆ ℝ
3736, 5sseldi 3566 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℝ)
3816feqmptd 6159 . . . . . . . . . 10 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)))
39 simpll 786 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑)
40 elfznn 12241 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
4140adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
4239, 41, 35syl2anc 691 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
4337recnd 9947 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
4439, 41, 43syl2anc 691 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ)
4542, 29, 44fsumser 14308 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
4645eqcomd 2616 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) = Σ𝑘 ∈ (1...𝑛)𝐴)
4746mpteq2dva 4672 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴))
4838, 47eqtr2d 2645 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) = seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)))
49 esumpcvgval.3 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )
5048, 49eqeltrrd 2689 . . . . . . . 8 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ∈ dom ⇝ )
513, 4, 35, 37, 50isumrecl 14338 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ℕ 𝐴 ∈ ℝ)
52 1zzd 11285 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 1 ∈ ℤ)
53 fzfid 12634 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
54 fzssuz 12253 . . . . . . . . . . . 12 (1...𝑛) ⊆ (ℤ‘1)
5554, 3sseqtr4i 3601 . . . . . . . . . . 11 (1...𝑛) ⊆ ℕ
5655a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ⊆ ℕ)
5735adantlr 747 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
5837adantlr 747 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℝ)
595adantlr 747 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))
60 elrege0 12149 . . . . . . . . . . . 12 (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
6160simprbi 479 . . . . . . . . . . 11 (𝐴 ∈ (0[,)+∞) → 0 ≤ 𝐴)
6259, 61syl 17 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 0 ≤ 𝐴)
6350adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ∈ dom ⇝ )
643, 52, 53, 56, 57, 58, 62, 63isumless 14416 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)𝐴 ≤ Σ𝑘 ∈ ℕ 𝐴)
6545, 64eqbrtrrd 4607 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴)
6665ralrimiva 2949 . . . . . . 7 (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴)
67 breq2 4587 . . . . . . . . 9 (𝑠 = Σ𝑘 ∈ ℕ 𝐴 → ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴))
6867ralbidv 2969 . . . . . . . 8 (𝑠 = Σ𝑘 ∈ ℕ 𝐴 → (∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ↔ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴))
6968rspcev 3282 . . . . . . 7 ((Σ𝑘 ∈ ℕ 𝐴 ∈ ℝ ∧ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴) → ∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠)
7051, 66, 69syl2anc 691 . . . . . 6 (𝜑 → ∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠)
713, 4, 16, 32, 70climsup 14248 . . . . 5 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⇝ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
723, 4, 71, 24climrecl 14162 . . . 4 (𝜑 → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ)
7372rexrd 9968 . . 3 (𝜑 → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ*)
74 eqid 2610 . . . . . . 7 (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)
75 sumex 14266 . . . . . . 7 Σ𝑘𝑏 𝐴 ∈ V
7674, 75elrnmpti 5297 . . . . . 6 (𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴)
77 ssnnssfz 28937 . . . . . . . . . 10 (𝑏 ∈ (𝒫 ℕ ∩ Fin) → ∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚))
78 fzfid 12634 . . . . . . . . . . . . . 14 ((𝜑𝑏 ⊆ (1...𝑚)) → (1...𝑚) ∈ Fin)
79 elfznn 12241 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (1...𝑚) → 𝑘 ∈ ℕ)
8079, 5sylan2 490 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...𝑚)) → 𝐴 ∈ (0[,)+∞))
8160simplbi 475 . . . . . . . . . . . . . . . 16 (𝐴 ∈ (0[,)+∞) → 𝐴 ∈ ℝ)
8280, 81syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ)
8382adantlr 747 . . . . . . . . . . . . . 14 (((𝜑𝑏 ⊆ (1...𝑚)) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ)
8480, 61syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...𝑚)) → 0 ≤ 𝐴)
8584adantlr 747 . . . . . . . . . . . . . 14 (((𝜑𝑏 ⊆ (1...𝑚)) ∧ 𝑘 ∈ (1...𝑚)) → 0 ≤ 𝐴)
86 simpr 476 . . . . . . . . . . . . . 14 ((𝜑𝑏 ⊆ (1...𝑚)) → 𝑏 ⊆ (1...𝑚))
8778, 83, 85, 86fsumless 14369 . . . . . . . . . . . . 13 ((𝜑𝑏 ⊆ (1...𝑚)) → Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
8887ex 449 . . . . . . . . . . . 12 (𝜑 → (𝑏 ⊆ (1...𝑚) → Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
8988reximdv 2999 . . . . . . . . . . 11 (𝜑 → (∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚) → ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9089imp 444 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚)) → ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
9177, 90sylan2 490 . . . . . . . . 9 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
92 breq1 4586 . . . . . . . . . 10 (𝑥 = Σ𝑘𝑏 𝐴 → (𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴 ↔ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9392rexbidv 3034 . . . . . . . . 9 (𝑥 = Σ𝑘𝑏 𝐴 → (∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴 ↔ ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9491, 93syl5ibrcom 236 . . . . . . . 8 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (𝑥 = Σ𝑘𝑏 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9594rexlimdva 3013 . . . . . . 7 (𝜑 → (∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9695imp 444 . . . . . 6 ((𝜑 ∧ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴) → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
9776, 96sylan2b 491 . . . . 5 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
98 simpr 476 . . . . . . . . . 10 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑥 = Σ𝑘𝑏 𝐴) → 𝑥 = Σ𝑘𝑏 𝐴)
99 inss2 3796 . . . . . . . . . . . . 13 (𝒫 ℕ ∩ Fin) ⊆ Fin
100 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → 𝑏 ∈ (𝒫 ℕ ∩ Fin))
10199, 100sseldi 3566 . . . . . . . . . . . 12 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → 𝑏 ∈ Fin)
102 simpll 786 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝜑)
103 inss1 3795 . . . . . . . . . . . . . . . . 17 (𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ
104 simplr 788 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑏 ∈ (𝒫 ℕ ∩ Fin))
105103, 104sseldi 3566 . . . . . . . . . . . . . . . 16 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑏 ∈ 𝒫 ℕ)
106105elpwid 4118 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑏 ⊆ ℕ)
107 simpr 476 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑘𝑏)
108106, 107sseldd 3569 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑘 ∈ ℕ)
109102, 108, 5syl2anc 691 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝐴 ∈ (0[,)+∞))
110109, 81syl 17 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝐴 ∈ ℝ)
111101, 110fsumrecl 14312 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → Σ𝑘𝑏 𝐴 ∈ ℝ)
112111adantr 480 . . . . . . . . . 10 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑥 = Σ𝑘𝑏 𝐴) → Σ𝑘𝑏 𝐴 ∈ ℝ)
11398, 112eqeltrd 2688 . . . . . . . . 9 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑥 = Σ𝑘𝑏 𝐴) → 𝑥 ∈ ℝ)
114113r19.29an 3059 . . . . . . . 8 ((𝜑 ∧ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴) → 𝑥 ∈ ℝ)
11576, 114sylan2b 491 . . . . . . 7 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → 𝑥 ∈ ℝ)
116115adantr 480 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ∈ ℝ)
117 fzfid 12634 . . . . . . . 8 (𝜑 → (1...𝑚) ∈ Fin)
118117, 82fsumrecl 14312 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ℝ)
119118ad2antrr 758 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ℝ)
12072ad2antrr 758 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ)
121 simprr 792 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
122 frn 5966 . . . . . . . . 9 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)):ℕ⟶ℝ → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
12316, 122syl 17 . . . . . . . 8 (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
124123ad2antrr 758 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
125 1nn 10908 . . . . . . . . . 10 1 ∈ ℕ
126125ne0ii 3882 . . . . . . . . 9 ℕ ≠ ∅
127 dm0rn0 5263 . . . . . . . . . . 11 (dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅)
128 fdm 5964 . . . . . . . . . . . . 13 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)):ℕ⟶ℝ → dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ℕ)
12916, 128syl 17 . . . . . . . . . . . 12 (𝜑 → dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ℕ)
130129eqeq1d 2612 . . . . . . . . . . 11 (𝜑 → (dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ℕ = ∅))
131127, 130syl5bbr 273 . . . . . . . . . 10 (𝜑 → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ℕ = ∅))
132131necon3bid 2826 . . . . . . . . 9 (𝜑 → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ↔ ℕ ≠ ∅))
133126, 132mpbiri 247 . . . . . . . 8 (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅)
134133ad2antrr 758 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅)
135 1z 11284 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
136 seqfn 12675 . . . . . . . . . . . . . . . 16 (1 ∈ ℤ → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn (ℤ‘1))
137135, 136ax-mp 5 . . . . . . . . . . . . . . 15 seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn (ℤ‘1)
1383fneq2i 5900 . . . . . . . . . . . . . . 15 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn ℕ ↔ seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn (ℤ‘1))
139137, 138mpbir 220 . . . . . . . . . . . . . 14 seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn ℕ
140 dffn5 6151 . . . . . . . . . . . . . 14 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn ℕ ↔ seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)))
141139, 140mpbi 219 . . . . . . . . . . . . 13 seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
142 fvex 6113 . . . . . . . . . . . . 13 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ∈ V
143141, 142elrnmpti 5297 . . . . . . . . . . . 12 (𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
144 r19.29 3054 . . . . . . . . . . . . 13 ((∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → ∃𝑛 ∈ ℕ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)))
145 breq1 4586 . . . . . . . . . . . . . . 15 (𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → (𝑧𝑠 ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠))
146145biimparc 503 . . . . . . . . . . . . . 14 (((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧𝑠)
147146rexlimivw 3011 . . . . . . . . . . . . 13 (∃𝑛 ∈ ℕ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧𝑠)
148144, 147syl 17 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧𝑠)
149143, 148sylan2b 491 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) → 𝑧𝑠)
150149ralrimiva 2949 . . . . . . . . . 10 (∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 → ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
151150reximi 2994 . . . . . . . . 9 (∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
15270, 151syl 17 . . . . . . . 8 (𝜑 → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
153152ad2antrr 758 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
154 simpr 476 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
155 simpll 786 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝜑)
15679adantl 481 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝑘 ∈ ℕ)
157155, 156, 35syl2anc 691 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
158154, 3syl6eleq 2698 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ (ℤ‘1))
159155, 156, 5syl2anc 691 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ (0[,)+∞))
160159, 81syl 17 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ)
161160recnd 9947 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℂ)
162157, 158, 161fsumser 14308 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚))
163 fveq2 6103 . . . . . . . . . . . 12 (𝑛 = 𝑚 → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚))
164163eqeq2d 2620 . . . . . . . . . . 11 (𝑛 = 𝑚 → (Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ↔ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚)))
165164rspcev 3282 . . . . . . . . . 10 ((𝑚 ∈ ℕ ∧ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚)) → ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
166154, 162, 165syl2anc 691 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
167141, 142elrnmpti 5297 . . . . . . . . 9 𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
168166, 167sylibr 223 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)))
169168ad2ant2r 779 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)))
170 suprub 10863 . . . . . . 7 (((ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠) ∧ Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) → Σ𝑘 ∈ (1...𝑚)𝐴 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
171124, 134, 153, 169, 170syl31anc 1321 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
172116, 119, 120, 121, 171letrd 10073 . . . . 5 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
17397, 172rexlimddv 3017 . . . 4 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → 𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
17472adantr 480 . . . . 5 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ)
175115, 174lenltd 10062 . . . 4 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → (𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) < 𝑥))
176173, 175mpbid 221 . . 3 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → ¬ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) < 𝑥)
177 simpr1r 1112 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0 ≤ 𝑥𝑥 = +∞)) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
1781773anassrs 1282 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
17973ad3antrrr 762 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ*)
180 pnfnlt 11838 . . . . . . . 8 (sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ* → ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
181179, 180syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
182 breq1 4586 . . . . . . . . 9 (𝑥 = +∞ → (𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )))
183182notbid 307 . . . . . . . 8 (𝑥 = +∞ → (¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )))
184183adantl 481 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → (¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )))
185181, 184mpbird 246 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → ¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
186178, 185pm2.21dd 185 . . . . 5 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
187 simplll 794 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝜑)
188 simpr1l 1111 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0 ≤ 𝑥𝑥 < +∞)) → 𝑥 ∈ ℝ*)
1891883anassrs 1282 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 ∈ ℝ*)
190 simplr 788 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 0 ≤ 𝑥)
191 simpr 476 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 < +∞)
192 0xr 9965 . . . . . . . 8 0 ∈ ℝ*
193 pnfxr 9971 . . . . . . . 8 +∞ ∈ ℝ*
194 elico1 12089 . . . . . . . 8 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥𝑥 < +∞)))
195192, 193, 194mp2an 704 . . . . . . 7 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥𝑥 < +∞))
196189, 190, 191, 195syl3anbrc 1239 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 ∈ (0[,)+∞))
197 simpr1r 1112 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0 ≤ 𝑥𝑥 < +∞)) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
1981973anassrs 1282 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
199123adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
200133adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅)
201152adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
202199, 200, 2013jca 1235 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠))
203 simprl 790 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → 𝑥 ∈ (0[,)+∞))
20436, 203sseldi 3566 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → 𝑥 ∈ ℝ)
205 simprr 792 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
206 suprlub 10864 . . . . . . . . 9 (((ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠) ∧ 𝑥 ∈ ℝ) → (𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦))
207206biimpa 500 . . . . . . . 8 ((((ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) → ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦)
208202, 204, 205, 207syl21anc 1317 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦)
20940ssriv 3572 . . . . . . . . . . . . . . . . 17 (1...𝑛) ⊆ ℕ
210 ovex 6577 . . . . . . . . . . . . . . . . . 18 (1...𝑛) ∈ V
211210elpw 4114 . . . . . . . . . . . . . . . . 17 ((1...𝑛) ∈ 𝒫 ℕ ↔ (1...𝑛) ⊆ ℕ)
212209, 211mpbir 220 . . . . . . . . . . . . . . . 16 (1...𝑛) ∈ 𝒫 ℕ
213 fzfi 12633 . . . . . . . . . . . . . . . 16 (1...𝑛) ∈ Fin
214 elin 3758 . . . . . . . . . . . . . . . 16 ((1...𝑛) ∈ (𝒫 ℕ ∩ Fin) ↔ ((1...𝑛) ∈ 𝒫 ℕ ∧ (1...𝑛) ∈ Fin))
215212, 213, 214mpbir2an 957 . . . . . . . . . . . . . . 15 (1...𝑛) ∈ (𝒫 ℕ ∩ Fin)
216215a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → (1...𝑛) ∈ (𝒫 ℕ ∩ Fin))
217 simpr 476 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
21845adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
219217, 218eqtr4d 2647 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴)
220 sumeq1 14267 . . . . . . . . . . . . . . . 16 (𝑏 = (1...𝑛) → Σ𝑘𝑏 𝐴 = Σ𝑘 ∈ (1...𝑛)𝐴)
221220eqeq2d 2620 . . . . . . . . . . . . . . 15 (𝑏 = (1...𝑛) → (𝑦 = Σ𝑘𝑏 𝐴𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴))
222221rspcev 3282 . . . . . . . . . . . . . 14 (((1...𝑛) ∈ (𝒫 ℕ ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴)
223216, 219, 222syl2anc 691 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴)
224223ex 449 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴))
225224rexlimdva 3013 . . . . . . . . . . 11 (𝜑 → (∃𝑛 ∈ ℕ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴))
226141, 142elrnmpti 5297 . . . . . . . . . . 11 (𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
22774, 75elrnmpti 5297 . . . . . . . . . . 11 (𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴)
228225, 226, 2273imtr4g 284 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) → 𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)))
229228ssrdv 3574 . . . . . . . . 9 (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴))
230 ssrexv 3630 . . . . . . . . 9 (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) → (∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦))
231229, 230syl 17 . . . . . . . 8 (𝜑 → (∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦))
232231imp 444 . . . . . . 7 ((𝜑 ∧ ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
233208, 232syldan 486 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
234187, 196, 198, 233syl12anc 1316 . . . . 5 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
235 simplrl 796 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) → 𝑥 ∈ ℝ*)
236 xrlelttric 28906 . . . . . . . 8 ((+∞ ∈ ℝ*𝑥 ∈ ℝ*) → (+∞ ≤ 𝑥𝑥 < +∞))
237193, 236mpan 702 . . . . . . 7 (𝑥 ∈ ℝ* → (+∞ ≤ 𝑥𝑥 < +∞))
238 xgepnf 28904 . . . . . . . 8 (𝑥 ∈ ℝ* → (+∞ ≤ 𝑥𝑥 = +∞))
239238orbi1d 735 . . . . . . 7 (𝑥 ∈ ℝ* → ((+∞ ≤ 𝑥𝑥 < +∞) ↔ (𝑥 = +∞ ∨ 𝑥 < +∞)))
240237, 239mpbid 221 . . . . . 6 (𝑥 ∈ ℝ* → (𝑥 = +∞ ∨ 𝑥 < +∞))
241235, 240syl 17 . . . . 5 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) → (𝑥 = +∞ ∨ 𝑥 < +∞))
242186, 234, 241mpjaodan 823 . . . 4 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
243 0elpw 4760 . . . . . . . . 9 ∅ ∈ 𝒫 ℕ
244 0fin 8073 . . . . . . . . 9 ∅ ∈ Fin
245 elin 3758 . . . . . . . . 9 (∅ ∈ (𝒫 ℕ ∩ Fin) ↔ (∅ ∈ 𝒫 ℕ ∧ ∅ ∈ Fin))
246243, 244, 245mpbir2an 957 . . . . . . . 8 ∅ ∈ (𝒫 ℕ ∩ Fin)
247 sum0 14299 . . . . . . . . 9 Σ𝑘 ∈ ∅ 𝐴 = 0
248247eqcomi 2619 . . . . . . . 8 0 = Σ𝑘 ∈ ∅ 𝐴
249 sumeq1 14267 . . . . . . . . . 10 (𝑏 = ∅ → Σ𝑘𝑏 𝐴 = Σ𝑘 ∈ ∅ 𝐴)
250249eqeq2d 2620 . . . . . . . . 9 (𝑏 = ∅ → (0 = Σ𝑘𝑏 𝐴 ↔ 0 = Σ𝑘 ∈ ∅ 𝐴))
251250rspcev 3282 . . . . . . . 8 ((∅ ∈ (𝒫 ℕ ∩ Fin) ∧ 0 = Σ𝑘 ∈ ∅ 𝐴) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)0 = Σ𝑘𝑏 𝐴)
252246, 248, 251mp2an 704 . . . . . . 7 𝑏 ∈ (𝒫 ℕ ∩ Fin)0 = Σ𝑘𝑏 𝐴
25374, 75elrnmpti 5297 . . . . . . 7 (0 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)0 = Σ𝑘𝑏 𝐴)
254252, 253mpbir 220 . . . . . 6 0 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)
255 breq2 4587 . . . . . . 7 (𝑦 = 0 → (𝑥 < 𝑦𝑥 < 0))
256255rspcev 3282 . . . . . 6 ((0 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ∧ 𝑥 < 0) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
257254, 256mpan 702 . . . . 5 (𝑥 < 0 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
258257adantl 481 . . . 4 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 𝑥 < 0) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
259 xrlelttric 28906 . . . . . 6 ((0 ∈ ℝ*𝑥 ∈ ℝ*) → (0 ≤ 𝑥𝑥 < 0))
260192, 259mpan 702 . . . . 5 (𝑥 ∈ ℝ* → (0 ≤ 𝑥𝑥 < 0))
261260ad2antrl 760 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → (0 ≤ 𝑥𝑥 < 0))
262242, 258, 261mpjaodan 823 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
2632, 73, 176, 262eqsupd 8246 . 2 (𝜑 → sup(ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴), ℝ*, < ) = sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
264 nfv 1830 . . 3 𝑘𝜑
265 nfcv 2751 . . 3 𝑘
266 nnex 10903 . . . 4 ℕ ∈ V
267266a1i 11 . . 3 (𝜑 → ℕ ∈ V)
268 icossicc 12131 . . . 4 (0[,)+∞) ⊆ (0[,]+∞)
269268, 5sseldi 3566 . . 3 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))
270 elex 3185 . . . . . 6 (𝑏 ∈ (𝒫 ℕ ∩ Fin) → 𝑏 ∈ V)
271270adantl 481 . . . . 5 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → 𝑏 ∈ V)
272 eqid 2610 . . . . . 6 (𝑘𝑏𝐴) = (𝑘𝑏𝐴)
273109, 272fmptd 6292 . . . . 5 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (𝑘𝑏𝐴):𝑏⟶(0[,)+∞))
274 esumpfinvallem 29463 . . . . 5 ((𝑏 ∈ V ∧ (𝑘𝑏𝐴):𝑏⟶(0[,)+∞)) → (ℂfld Σg (𝑘𝑏𝐴)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑏𝐴)))
275271, 273, 274syl2anc 691 . . . 4 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (ℂfld Σg (𝑘𝑏𝐴)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑏𝐴)))
276110recnd 9947 . . . . 5 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝐴 ∈ ℂ)
277101, 276gsumfsum 19632 . . . 4 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (ℂfld Σg (𝑘𝑏𝐴)) = Σ𝑘𝑏 𝐴)
278275, 277eqtr3d 2646 . . 3 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑏𝐴)) = Σ𝑘𝑏 𝐴)
279264, 265, 267, 269, 278esumval 29435 . 2 (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = sup(ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴), ℝ*, < ))
2803, 4, 35, 43, 71isumclim 14330 . 2 (𝜑 → Σ𝑘 ∈ ℕ 𝐴 = sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
281263, 279, 2803eqtr4d 2654 1 (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108   class class class wbr 4583   ↦ cmpt 4643   Or wor 4958  dom cdm 5038  ran crn 5039   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  Fincfn 7841  supcsup 8229  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818  +∞cpnf 9950  ℝ*cxr 9952   < clt 9953   ≤ cle 9954  ℕcn 10897  ℤcz 11254  ℤ≥cuz 11563  [,)cico 12048  [,]cicc 12049  ...cfz 12197  seqcseq 12663   ⇝ cli 14063  Σcsu 14264   ↾s cress 15696   Σg cgsu 15924  ℝ*𝑠cxrs 15983  ℂfldccnfld 19567  Σ*cesum 29416 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xadd 11823  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-ordt 15984  df-xrs 15985  df-mre 16069  df-mrc 16070  df-acs 16072  df-ps 17023  df-tsr 17024  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-grp 17248  df-minusg 17249  df-cntz 17573  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-cring 18373  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-ntr 20634  df-nei 20712  df-cn 20841  df-haus 20929  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-tsms 21740  df-esum 29417 This theorem is referenced by:  esumcvg  29475  esumcvgsum  29477
 Copyright terms: Public domain W3C validator