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 30587
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 12174 . . . 4 < Or ℝ*
21a1i 11 . . 3 (𝜑 → < Or ℝ*)
3 nnuz 11923 . . . . 5 ℕ = (ℤ‘1)
4 1zzd 11655 . . . . 5 (𝜑 → 1 ∈ ℤ)
5 esumpcvgval.1 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))
6 esumpcvgval.2 . . . . . . . . . . . 12 (𝑘 = 𝑙𝐴 = 𝐵)
7 eqcom 2772 . . . . . . . . . . . 12 (𝑘 = 𝑙𝑙 = 𝑘)
8 eqcom 2772 . . . . . . . . . . . 12 (𝐴 = 𝐵𝐵 = 𝐴)
96, 7, 83imtr3i 282 . . . . . . . . . . 11 (𝑙 = 𝑘𝐵 = 𝐴)
109cbvmptv 4909 . . . . . . . . . 10 (𝑙 ∈ ℕ ↦ 𝐵) = (𝑘 ∈ ℕ ↦ 𝐴)
115, 10fmptd 6574 . . . . . . . . 9 (𝜑 → (𝑙 ∈ ℕ ↦ 𝐵):ℕ⟶(0[,)+∞))
1211ffvelrnda 6549 . . . . . . . 8 ((𝜑𝑥 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞))
13 elrege0 12482 . . . . . . . . 9 (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞) ↔ (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥)))
1413simplbi 491 . . . . . . . 8 (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ)
1512, 14syl 17 . . . . . . 7 ((𝜑𝑥 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ)
163, 4, 15serfre 13037 . . . . . 6 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)):ℕ⟶ℝ)
1711adantr 472 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑙 ∈ ℕ ↦ 𝐵):ℕ⟶(0[,)+∞))
18 simpr 477 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
1918peano2nnd 11293 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
2017, 19ffvelrnd 6550 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞))
21 elrege0 12482 . . . . . . . . . 10 (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) ↔ (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ ∧ 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
2221simprbi 490 . . . . . . . . 9 (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) → 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))
2320, 22syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))
2416ffvelrnda 6549 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ∈ ℝ)
2521simplbi 491 . . . . . . . . . 10 (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ)
2620, 25syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ)
2724, 26addge01d 10869 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))))
2823, 27mpbid 223 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
2918, 3syl6eleq 2854 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
30 seqp1 13023 . . . . . . . 8 (𝑛 ∈ (ℤ‘1) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)) = ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
3129, 30syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)) = ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))
3228, 31breqtrrd 4837 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)))
33 simpr 477 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
3410fvmpt2 6480 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ 𝐴 ∈ (0[,)+∞)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
3533, 5, 34syl2anc 579 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
36 rge0ssre 12484 . . . . . . . . 9 (0[,)+∞) ⊆ ℝ
3736, 5sseldi 3759 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℝ)
3816feqmptd 6438 . . . . . . . . . 10 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)))
39 simpll 783 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑)
40 elfznn 12577 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
4140adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
4239, 41, 35syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
4337recnd 10322 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
4439, 41, 43syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ)
4542, 29, 44fsumser 14746 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
4645eqcomd 2771 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) = Σ𝑘 ∈ (1...𝑛)𝐴)
4746mpteq2dva 4903 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴))
4838, 47eqtr2d 2800 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) = seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)))
49 esumpcvgval.3 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )
5048, 49eqeltrrd 2845 . . . . . . . 8 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ∈ dom ⇝ )
513, 4, 35, 37, 50isumrecl 14781 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ℕ 𝐴 ∈ ℝ)
52 1zzd 11655 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 1 ∈ ℤ)
53 fzfid 12980 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
54 fzssuz 12589 . . . . . . . . . . . 12 (1...𝑛) ⊆ (ℤ‘1)
5554, 3sseqtr4i 3798 . . . . . . . . . . 11 (1...𝑛) ⊆ ℕ
5655a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ⊆ ℕ)
5735adantlr 706 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
5837adantlr 706 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℝ)
595adantlr 706 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞))
60 elrege0 12482 . . . . . . . . . . . 12 (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
6160simprbi 490 . . . . . . . . . . 11 (𝐴 ∈ (0[,)+∞) → 0 ≤ 𝐴)
6259, 61syl 17 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 0 ≤ 𝐴)
6350adantr 472 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ∈ dom ⇝ )
643, 52, 53, 56, 57, 58, 62, 63isumless 14861 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)𝐴 ≤ Σ𝑘 ∈ ℕ 𝐴)
6545, 64eqbrtrrd 4833 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴)
6665ralrimiva 3113 . . . . . . 7 (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴)
67 brralrspcev 4869 . . . . . . 7 ((Σ𝑘 ∈ ℕ 𝐴 ∈ ℝ ∧ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴) → ∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠)
6851, 66, 67syl2anc 579 . . . . . 6 (𝜑 → ∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠)
693, 4, 16, 32, 68climsup 14685 . . . . 5 (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⇝ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
703, 4, 69, 24climrecl 14599 . . . 4 (𝜑 → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ)
7170rexrd 10343 . . 3 (𝜑 → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ*)
72 eqid 2765 . . . . . . 7 (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)
73 sumex 14703 . . . . . . 7 Σ𝑘𝑏 𝐴 ∈ V
7472, 73elrnmpti 5545 . . . . . 6 (𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴)
75 ssnnssfz 29998 . . . . . . . . . 10 (𝑏 ∈ (𝒫 ℕ ∩ Fin) → ∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚))
76 fzfid 12980 . . . . . . . . . . . . . 14 ((𝜑𝑏 ⊆ (1...𝑚)) → (1...𝑚) ∈ Fin)
77 elfznn 12577 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (1...𝑚) → 𝑘 ∈ ℕ)
7877, 5sylan2 586 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...𝑚)) → 𝐴 ∈ (0[,)+∞))
7960simplbi 491 . . . . . . . . . . . . . . . 16 (𝐴 ∈ (0[,)+∞) → 𝐴 ∈ ℝ)
8078, 79syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ)
8180adantlr 706 . . . . . . . . . . . . . 14 (((𝜑𝑏 ⊆ (1...𝑚)) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ)
8278, 61syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...𝑚)) → 0 ≤ 𝐴)
8382adantlr 706 . . . . . . . . . . . . . 14 (((𝜑𝑏 ⊆ (1...𝑚)) ∧ 𝑘 ∈ (1...𝑚)) → 0 ≤ 𝐴)
84 simpr 477 . . . . . . . . . . . . . 14 ((𝜑𝑏 ⊆ (1...𝑚)) → 𝑏 ⊆ (1...𝑚))
8576, 81, 83, 84fsumless 14812 . . . . . . . . . . . . 13 ((𝜑𝑏 ⊆ (1...𝑚)) → Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
8685ex 401 . . . . . . . . . . . 12 (𝜑 → (𝑏 ⊆ (1...𝑚) → Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
8786reximdv 3162 . . . . . . . . . . 11 (𝜑 → (∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚) → ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
8887imp 395 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚)) → ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
8975, 88sylan2 586 . . . . . . . . 9 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
90 breq1 4812 . . . . . . . . . 10 (𝑥 = Σ𝑘𝑏 𝐴 → (𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴 ↔ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9190rexbidv 3199 . . . . . . . . 9 (𝑥 = Σ𝑘𝑏 𝐴 → (∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴 ↔ ∃𝑚 ∈ ℕ Σ𝑘𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9289, 91syl5ibrcom 238 . . . . . . . 8 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (𝑥 = Σ𝑘𝑏 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9392rexlimdva 3178 . . . . . . 7 (𝜑 → (∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴))
9493imp 395 . . . . . 6 ((𝜑 ∧ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴) → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
9574, 94sylan2b 587 . . . . 5 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
96 simpr 477 . . . . . . . . . 10 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑥 = Σ𝑘𝑏 𝐴) → 𝑥 = Σ𝑘𝑏 𝐴)
97 inss2 3993 . . . . . . . . . . . . 13 (𝒫 ℕ ∩ Fin) ⊆ Fin
98 simpr 477 . . . . . . . . . . . . 13 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → 𝑏 ∈ (𝒫 ℕ ∩ Fin))
9997, 98sseldi 3759 . . . . . . . . . . . 12 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → 𝑏 ∈ Fin)
100 simpll 783 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝜑)
101 inss1 3992 . . . . . . . . . . . . . . . . 17 (𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ
102 simplr 785 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑏 ∈ (𝒫 ℕ ∩ Fin))
103101, 102sseldi 3759 . . . . . . . . . . . . . . . 16 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑏 ∈ 𝒫 ℕ)
104103elpwid 4327 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑏 ⊆ ℕ)
105 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑘𝑏)
106104, 105sseldd 3762 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝑘 ∈ ℕ)
107100, 106, 5syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝐴 ∈ (0[,)+∞))
108107, 79syl 17 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝐴 ∈ ℝ)
10999, 108fsumrecl 14750 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → Σ𝑘𝑏 𝐴 ∈ ℝ)
110109adantr 472 . . . . . . . . . 10 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑥 = Σ𝑘𝑏 𝐴) → Σ𝑘𝑏 𝐴 ∈ ℝ)
11196, 110eqeltrd 2844 . . . . . . . . 9 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑥 = Σ𝑘𝑏 𝐴) → 𝑥 ∈ ℝ)
112111r19.29an 3224 . . . . . . . 8 ((𝜑 ∧ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘𝑏 𝐴) → 𝑥 ∈ ℝ)
11374, 112sylan2b 587 . . . . . . 7 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → 𝑥 ∈ ℝ)
114113adantr 472 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ∈ ℝ)
115 fzfid 12980 . . . . . . . 8 (𝜑 → (1...𝑚) ∈ Fin)
116115, 80fsumrecl 14750 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ℝ)
117116ad2antrr 717 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ℝ)
11870ad2antrr 717 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ)
119 simprr 789 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)
12016frnd 6230 . . . . . . . 8 (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
121120ad2antrr 717 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
122 1nn 11287 . . . . . . . . . 10 1 ∈ ℕ
123122ne0ii 4088 . . . . . . . . 9 ℕ ≠ ∅
124 dm0rn0 5510 . . . . . . . . . . 11 (dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅)
12516fdmd 6232 . . . . . . . . . . . 12 (𝜑 → dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ℕ)
126125eqeq1d 2767 . . . . . . . . . . 11 (𝜑 → (dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ℕ = ∅))
127124, 126syl5bbr 276 . . . . . . . . . 10 (𝜑 → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ℕ = ∅))
128127necon3bid 2981 . . . . . . . . 9 (𝜑 → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ↔ ℕ ≠ ∅))
129123, 128mpbiri 249 . . . . . . . 8 (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅)
130129ad2antrr 717 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅)
131 1z 11654 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
132 seqfn 13020 . . . . . . . . . . . . . . . 16 (1 ∈ ℤ → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn (ℤ‘1))
133131, 132ax-mp 5 . . . . . . . . . . . . . . 15 seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn (ℤ‘1)
1343fneq2i 6164 . . . . . . . . . . . . . . 15 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn ℕ ↔ seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn (ℤ‘1))
135133, 134mpbir 222 . . . . . . . . . . . . . 14 seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn ℕ
136 dffn5 6430 . . . . . . . . . . . . . 14 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) Fn ℕ ↔ seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)))
137135, 136mpbi 221 . . . . . . . . . . . . 13 seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
138 fvex 6388 . . . . . . . . . . . . 13 (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ∈ V
139137, 138elrnmpti 5545 . . . . . . . . . . . 12 (𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
140 r19.29 3219 . . . . . . . . . . . . 13 ((∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → ∃𝑛 ∈ ℕ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)))
141 breq1 4812 . . . . . . . . . . . . . . 15 (𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → (𝑧𝑠 ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠))
142141biimparc 471 . . . . . . . . . . . . . 14 (((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧𝑠)
143142rexlimivw 3176 . . . . . . . . . . . . 13 (∃𝑛 ∈ ℕ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧𝑠)
144140, 143syl 17 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧𝑠)
145139, 144sylan2b 587 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) → 𝑧𝑠)
146145ralrimiva 3113 . . . . . . . . . 10 (∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 → ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
147146reximi 3157 . . . . . . . . 9 (∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
14868, 147syl 17 . . . . . . . 8 (𝜑 → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
149148ad2antrr 717 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
150 simpr 477 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
151 simpll 783 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝜑)
15277adantl 473 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝑘 ∈ ℕ)
153151, 152, 35syl2anc 579 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴)
154150, 3syl6eleq 2854 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ (ℤ‘1))
155151, 152, 5syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ (0[,)+∞))
156155, 79syl 17 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ)
157156recnd 10322 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℂ)
158153, 154, 157fsumser 14746 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚))
159 fveq2 6375 . . . . . . . . . . 11 (𝑛 = 𝑚 → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚))
160159rspceeqv 3479 . . . . . . . . . 10 ((𝑚 ∈ ℕ ∧ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚)) → ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
161150, 158, 160syl2anc 579 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
162137, 138elrnmpti 5545 . . . . . . . . 9 𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
163161, 162sylibr 225 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)))
164163ad2ant2r 753 . . . . . . 7 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)))
165 suprub 11238 . . . . . . 7 (((ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠) ∧ Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) → Σ𝑘 ∈ (1...𝑚)𝐴 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
166121, 130, 149, 164, 165syl31anc 1492 . . . . . 6 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
167114, 117, 118, 119, 166letrd 10448 . . . . 5 (((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
16895, 167rexlimddv 3182 . . . 4 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → 𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
16970adantr 472 . . . . 5 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ)
170113, 169lenltd 10437 . . . 4 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → (𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) < 𝑥))
171168, 170mpbid 223 . . 3 ((𝜑𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)) → ¬ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) < 𝑥)
172 simpr1r 1307 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0 ≤ 𝑥𝑥 = +∞)) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
1731723anassrs 1469 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
17471ad3antrrr 721 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ*)
175 pnfnlt 12162 . . . . . . . 8 (sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈ ℝ* → ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
176174, 175syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
177 breq1 4812 . . . . . . . . 9 (𝑥 = +∞ → (𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )))
178177notbid 309 . . . . . . . 8 (𝑥 = +∞ → (¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )))
179178adantl 473 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → (¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬ +∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )))
180176, 179mpbird 248 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → ¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
181173, 180pm2.21dd 186 . . . . 5 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 = +∞) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
182 simplll 791 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝜑)
183 simpr1l 1305 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0 ≤ 𝑥𝑥 < +∞)) → 𝑥 ∈ ℝ*)
1841833anassrs 1469 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 ∈ ℝ*)
185 simplr 785 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 0 ≤ 𝑥)
186 simpr 477 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 < +∞)
187 0xr 10340 . . . . . . . 8 0 ∈ ℝ*
188 pnfxr 10346 . . . . . . . 8 +∞ ∈ ℝ*
189 elico1 12420 . . . . . . . 8 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥𝑥 < +∞)))
190187, 188, 189mp2an 683 . . . . . . 7 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥𝑥 < +∞))
191184, 185, 186, 190syl3anbrc 1443 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 ∈ (0[,)+∞))
192 simpr1r 1307 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0 ≤ 𝑥𝑥 < +∞)) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
1931923anassrs 1469 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
194120adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ)
195129adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅)
196148adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠)
197194, 195, 1963jca 1158 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠))
198 simprl 787 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → 𝑥 ∈ (0[,)+∞))
19936, 198sseldi 3759 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → 𝑥 ∈ ℝ)
200 simprr 789 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
201 suprlub 11241 . . . . . . . . 9 (((ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠) ∧ 𝑥 ∈ ℝ) → (𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦))
202201biimpa 468 . . . . . . . 8 ((((ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧𝑠) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) → ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦)
203197, 199, 200, 202syl21anc 866 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦)
20440ssriv 3765 . . . . . . . . . . . . . . . . 17 (1...𝑛) ⊆ ℕ
205 ovex 6874 . . . . . . . . . . . . . . . . . 18 (1...𝑛) ∈ V
206205elpw 4321 . . . . . . . . . . . . . . . . 17 ((1...𝑛) ∈ 𝒫 ℕ ↔ (1...𝑛) ⊆ ℕ)
207204, 206mpbir 222 . . . . . . . . . . . . . . . 16 (1...𝑛) ∈ 𝒫 ℕ
208 fzfi 12979 . . . . . . . . . . . . . . . 16 (1...𝑛) ∈ Fin
209 elin 3958 . . . . . . . . . . . . . . . 16 ((1...𝑛) ∈ (𝒫 ℕ ∩ Fin) ↔ ((1...𝑛) ∈ 𝒫 ℕ ∧ (1...𝑛) ∈ Fin))
210207, 208, 209mpbir2an 702 . . . . . . . . . . . . . . 15 (1...𝑛) ∈ (𝒫 ℕ ∩ Fin)
211210a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → (1...𝑛) ∈ (𝒫 ℕ ∩ Fin))
212 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
21345adantr 472 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
214212, 213eqtr4d 2802 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴)
215 sumeq1 14704 . . . . . . . . . . . . . . 15 (𝑏 = (1...𝑛) → Σ𝑘𝑏 𝐴 = Σ𝑘 ∈ (1...𝑛)𝐴)
216215rspceeqv 3479 . . . . . . . . . . . . . 14 (((1...𝑛) ∈ (𝒫 ℕ ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴)
217211, 214, 216syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴)
218217ex 401 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴))
219218rexlimdva 3178 . . . . . . . . . . 11 (𝜑 → (∃𝑛 ∈ ℕ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴))
220137, 138elrnmpti 5545 . . . . . . . . . . 11 (𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))
22172, 73elrnmpti 5545 . . . . . . . . . . 11 (𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘𝑏 𝐴)
222219, 220, 2213imtr4g 287 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) → 𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)))
223222ssrdv 3767 . . . . . . . . 9 (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴))
224 ssrexv 3827 . . . . . . . . 9 (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) → (∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦))
225223, 224syl 17 . . . . . . . 8 (𝜑 → (∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦))
226225imp 395 . . . . . . 7 ((𝜑 ∧ ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
227203, 226syldan 585 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
228182, 191, 193, 227syl12anc 865 . . . . 5 ((((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) ∧ 𝑥 < +∞) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
229 simplrl 795 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) → 𝑥 ∈ ℝ*)
230 xrlelttric 29966 . . . . . . . 8 ((+∞ ∈ ℝ*𝑥 ∈ ℝ*) → (+∞ ≤ 𝑥𝑥 < +∞))
231188, 230mpan 681 . . . . . . 7 (𝑥 ∈ ℝ* → (+∞ ≤ 𝑥𝑥 < +∞))
232 xgepnf 12198 . . . . . . . 8 (𝑥 ∈ ℝ* → (+∞ ≤ 𝑥𝑥 = +∞))
233232orbi1d 940 . . . . . . 7 (𝑥 ∈ ℝ* → ((+∞ ≤ 𝑥𝑥 < +∞) ↔ (𝑥 = +∞ ∨ 𝑥 < +∞)))
234231, 233mpbid 223 . . . . . 6 (𝑥 ∈ ℝ* → (𝑥 = +∞ ∨ 𝑥 < +∞))
235229, 234syl 17 . . . . 5 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) → (𝑥 = +∞ ∨ 𝑥 < +∞))
236181, 228, 235mpjaodan 981 . . . 4 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0 ≤ 𝑥) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
237 0elpw 4992 . . . . . . . . 9 ∅ ∈ 𝒫 ℕ
238 0fin 8395 . . . . . . . . 9 ∅ ∈ Fin
239 elin 3958 . . . . . . . . 9 (∅ ∈ (𝒫 ℕ ∩ Fin) ↔ (∅ ∈ 𝒫 ℕ ∧ ∅ ∈ Fin))
240237, 238, 239mpbir2an 702 . . . . . . . 8 ∅ ∈ (𝒫 ℕ ∩ Fin)
241 sum0 14737 . . . . . . . . 9 Σ𝑘 ∈ ∅ 𝐴 = 0
242241eqcomi 2774 . . . . . . . 8 0 = Σ𝑘 ∈ ∅ 𝐴
243 sumeq1 14704 . . . . . . . . 9 (𝑏 = ∅ → Σ𝑘𝑏 𝐴 = Σ𝑘 ∈ ∅ 𝐴)
244243rspceeqv 3479 . . . . . . . 8 ((∅ ∈ (𝒫 ℕ ∩ Fin) ∧ 0 = Σ𝑘 ∈ ∅ 𝐴) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)0 = Σ𝑘𝑏 𝐴)
245240, 242, 244mp2an 683 . . . . . . 7 𝑏 ∈ (𝒫 ℕ ∩ Fin)0 = Σ𝑘𝑏 𝐴
24672, 73elrnmpti 5545 . . . . . . 7 (0 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)0 = Σ𝑘𝑏 𝐴)
247245, 246mpbir 222 . . . . . 6 0 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)
248 breq2 4813 . . . . . . 7 (𝑦 = 0 → (𝑥 < 𝑦𝑥 < 0))
249248rspcev 3461 . . . . . 6 ((0 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴) ∧ 𝑥 < 0) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
250247, 249mpan 681 . . . . 5 (𝑥 < 0 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
251250adantl 473 . . . 4 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 𝑥 < 0) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
252 xrlelttric 29966 . . . . . 6 ((0 ∈ ℝ*𝑥 ∈ ℝ*) → (0 ≤ 𝑥𝑥 < 0))
253187, 252mpan 681 . . . . 5 (𝑥 ∈ ℝ* → (0 ≤ 𝑥𝑥 < 0))
254253ad2antrl 719 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → (0 ≤ 𝑥𝑥 < 0))
255236, 251, 254mpjaodan 981 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴)𝑥 < 𝑦)
2562, 71, 171, 255eqsupd 8570 . 2 (𝜑 → sup(ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴), ℝ*, < ) = sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
257 nfv 2009 . . 3 𝑘𝜑
258 nfcv 2907 . . 3 𝑘
259 nnex 11281 . . . 4 ℕ ∈ V
260259a1i 11 . . 3 (𝜑 → ℕ ∈ V)
261 icossicc 12463 . . . 4 (0[,)+∞) ⊆ (0[,]+∞)
262261, 5sseldi 3759 . . 3 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞))
263 elex 3365 . . . . . 6 (𝑏 ∈ (𝒫 ℕ ∩ Fin) → 𝑏 ∈ V)
264263adantl 473 . . . . 5 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → 𝑏 ∈ V)
265107fmpttd 6575 . . . . 5 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (𝑘𝑏𝐴):𝑏⟶(0[,)+∞))
266 esumpfinvallem 30583 . . . . 5 ((𝑏 ∈ V ∧ (𝑘𝑏𝐴):𝑏⟶(0[,)+∞)) → (ℂfld Σg (𝑘𝑏𝐴)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑏𝐴)))
267264, 265, 266syl2anc 579 . . . 4 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (ℂfld Σg (𝑘𝑏𝐴)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑏𝐴)))
268108recnd 10322 . . . . 5 (((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑘𝑏) → 𝐴 ∈ ℂ)
26999, 268gsumfsum 20086 . . . 4 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → (ℂfld Σg (𝑘𝑏𝐴)) = Σ𝑘𝑏 𝐴)
270267, 269eqtr3d 2801 . . 3 ((𝜑𝑏 ∈ (𝒫 ℕ ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑏𝐴)) = Σ𝑘𝑏 𝐴)
271257, 258, 260, 262, 270esumval 30555 . 2 (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = sup(ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ Σ𝑘𝑏 𝐴), ℝ*, < ))
2723, 4, 35, 43, 69isumclim 14773 . 2 (𝜑 → Σ𝑘 ∈ ℕ 𝐴 = sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))
273256, 271, 2723eqtr4d 2809 1 (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  Vcvv 3350  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315   class class class wbr 4809  cmpt 4888   Or wor 5197  dom cdm 5277  ran crn 5278   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  Fincfn 8160  supcsup 8553  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192  +∞cpnf 10325  *cxr 10327   < clt 10328  cle 10329  cn 11274  cz 11624  cuz 11886  [,)cico 12379  [,]cicc 12380  ...cfz 12533  seqcseq 13008  cli 14500  Σcsu 14701  s cress 16131   Σg cgsu 16367  *𝑠cxrs 16426  fldccnfld 20019  Σ*cesum 30536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xadd 12147  df-ioo 12381  df-ioc 12382  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-clim 14504  df-rlim 14505  df-sum 14702  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-mulr 16228  df-starv 16229  df-tset 16233  df-ple 16234  df-ds 16236  df-unif 16237  df-rest 16349  df-topn 16350  df-0g 16368  df-gsum 16369  df-topgen 16370  df-ordt 16427  df-xrs 16428  df-mre 16512  df-mrc 16513  df-acs 16515  df-ps 17466  df-tsr 17467  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-submnd 17602  df-grp 17692  df-minusg 17693  df-cntz 18013  df-cmn 18461  df-abl 18462  df-mgp 18757  df-ur 18769  df-ring 18816  df-cring 18817  df-fbas 20016  df-fg 20017  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-ntr 21104  df-nei 21182  df-cn 21311  df-haus 21399  df-fil 21929  df-fm 22021  df-flim 22022  df-flf 22023  df-tsms 22209  df-esum 30537
This theorem is referenced by:  esumcvg  30595  esumcvgsum  30597
  Copyright terms: Public domain W3C validator