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

Theorem esumfsup 30437
Description: Formulating an extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.)
Hypothesis
Ref Expression
esumfsup.1 𝑘𝐹
Assertion
Ref Expression
esumfsup (𝐹:ℕ⟶(0[,]+∞) → Σ*𝑘 ∈ ℕ(𝐹𝑘) = sup(ran seq1( +𝑒 , 𝐹), ℝ*, < ))

Proof of Theorem esumfsup
Dummy variables 𝑎 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1z 11595 . . . . . 6 1 ∈ ℤ
2 seqfn 13003 . . . . . 6 (1 ∈ ℤ → seq1( +𝑒 , 𝐹) Fn (ℤ‘1))
31, 2ax-mp 5 . . . . 5 seq1( +𝑒 , 𝐹) Fn (ℤ‘1)
4 nnuz 11912 . . . . . 6 ℕ = (ℤ‘1)
54fneq2i 6143 . . . . 5 (seq1( +𝑒 , 𝐹) Fn ℕ ↔ seq1( +𝑒 , 𝐹) Fn (ℤ‘1))
63, 5mpbir 221 . . . 4 seq1( +𝑒 , 𝐹) Fn ℕ
7 iccssxr 12445 . . . . . 6 (0[,]+∞) ⊆ ℝ*
8 esumfsup.1 . . . . . . . 8 𝑘𝐹
98esumfzf 30436 . . . . . . 7 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) = (seq1( +𝑒 , 𝐹)‘𝑛))
10 ovex 6837 . . . . . . . 8 (1...𝑛) ∈ V
11 nfcv 2898 . . . . . . . . . . 11 𝑘
12 nfcv 2898 . . . . . . . . . . 11 𝑘(0[,]+∞)
138, 11, 12nff 6198 . . . . . . . . . 10 𝑘 𝐹:ℕ⟶(0[,]+∞)
14 nfv 1988 . . . . . . . . . 10 𝑘 𝑛 ∈ ℕ
1513, 14nfan 1973 . . . . . . . . 9 𝑘(𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ)
16 simpll 807 . . . . . . . . . . 11 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞))
17 1nn 11219 . . . . . . . . . . . . 13 1 ∈ ℕ
18 fzssnn 12574 . . . . . . . . . . . . 13 (1 ∈ ℕ → (1...𝑛) ⊆ ℕ)
1917, 18mp1i 13 . . . . . . . . . . . 12 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1...𝑛) ⊆ ℕ)
20 simpr 479 . . . . . . . . . . . 12 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛))
2119, 20sseldd 3741 . . . . . . . . . . 11 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
2216, 21ffvelrnd 6519 . . . . . . . . . 10 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐹𝑘) ∈ (0[,]+∞))
2322ex 449 . . . . . . . . 9 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (1...𝑛) → (𝐹𝑘) ∈ (0[,]+∞)))
2415, 23ralrimi 3091 . . . . . . . 8 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1...𝑛)(𝐹𝑘) ∈ (0[,]+∞))
25 nfcv 2898 . . . . . . . . 9 𝑘(1...𝑛)
2625esumcl 30397 . . . . . . . 8 (((1...𝑛) ∈ V ∧ ∀𝑘 ∈ (1...𝑛)(𝐹𝑘) ∈ (0[,]+∞)) → Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ∈ (0[,]+∞))
2710, 24, 26sylancr 698 . . . . . . 7 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ∈ (0[,]+∞))
289, 27eqeltrrd 2836 . . . . . 6 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (seq1( +𝑒 , 𝐹)‘𝑛) ∈ (0[,]+∞))
297, 28sseldi 3738 . . . . 5 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (seq1( +𝑒 , 𝐹)‘𝑛) ∈ ℝ*)
3029ralrimiva 3100 . . . 4 (𝐹:ℕ⟶(0[,]+∞) → ∀𝑛 ∈ ℕ (seq1( +𝑒 , 𝐹)‘𝑛) ∈ ℝ*)
31 fnfvrnss 6549 . . . 4 ((seq1( +𝑒 , 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (seq1( +𝑒 , 𝐹)‘𝑛) ∈ ℝ*) → ran seq1( +𝑒 , 𝐹) ⊆ ℝ*)
326, 30, 31sylancr 698 . . 3 (𝐹:ℕ⟶(0[,]+∞) → ran seq1( +𝑒 , 𝐹) ⊆ ℝ*)
33 nnex 11214 . . . . 5 ℕ ∈ V
34 ffvelrn 6516 . . . . . . 7 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ (0[,]+∞))
3534ex 449 . . . . . 6 (𝐹:ℕ⟶(0[,]+∞) → (𝑘 ∈ ℕ → (𝐹𝑘) ∈ (0[,]+∞)))
3613, 35ralrimi 3091 . . . . 5 (𝐹:ℕ⟶(0[,]+∞) → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ (0[,]+∞))
3711esumcl 30397 . . . . 5 ((ℕ ∈ V ∧ ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ (0[,]+∞)) → Σ*𝑘 ∈ ℕ(𝐹𝑘) ∈ (0[,]+∞))
3833, 36, 37sylancr 698 . . . 4 (𝐹:ℕ⟶(0[,]+∞) → Σ*𝑘 ∈ ℕ(𝐹𝑘) ∈ (0[,]+∞))
397, 38sseldi 3738 . . 3 (𝐹:ℕ⟶(0[,]+∞) → Σ*𝑘 ∈ ℕ(𝐹𝑘) ∈ ℝ*)
40 fvelrnb 6401 . . . . . . . . 9 (seq1( +𝑒 , 𝐹) Fn ℕ → (𝑥 ∈ ran seq1( +𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑥))
416, 40mp1i 13 . . . . . . . 8 (𝐹:ℕ⟶(0[,]+∞) → (𝑥 ∈ ran seq1( +𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑥))
42 eqcom 2763 . . . . . . . . . 10 *𝑘 ∈ (1...𝑛)(𝐹𝑘) = 𝑥𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘))
439eqeq1d 2758 . . . . . . . . . 10 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) = 𝑥 ↔ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑥))
4442, 43syl5bbr 274 . . . . . . . . 9 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ↔ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑥))
4544rexbidva 3183 . . . . . . . 8 (𝐹:ℕ⟶(0[,]+∞) → (∃𝑛 ∈ ℕ 𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑥))
4641, 45bitr4d 271 . . . . . . 7 (𝐹:ℕ⟶(0[,]+∞) → (𝑥 ∈ ran seq1( +𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ 𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
4746biimpa 502 . . . . . 6 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ran seq1( +𝑒 , 𝐹)) → ∃𝑛 ∈ ℕ 𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘))
4833a1i 11 . . . . . . . . 9 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ℕ ∈ V)
4934adantlr 753 . . . . . . . . 9 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ (0[,]+∞))
5017, 18mp1i 13 . . . . . . . . 9 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆ ℕ)
5115, 48, 49, 50esummono 30421 . . . . . . . 8 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘))
5251ralrimiva 3100 . . . . . . 7 (𝐹:ℕ⟶(0[,]+∞) → ∀𝑛 ∈ ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘))
5352adantr 472 . . . . . 6 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ran seq1( +𝑒 , 𝐹)) → ∀𝑛 ∈ ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘))
5447, 53jca 555 . . . . 5 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ran seq1( +𝑒 , 𝐹)) → (∃𝑛 ∈ ℕ 𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ∧ ∀𝑛 ∈ ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘)))
55 r19.29r 3207 . . . . 5 ((∃𝑛 ∈ ℕ 𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ∧ ∀𝑛 ∈ ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘)) → ∃𝑛 ∈ ℕ (𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ∧ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘)))
56 breq1 4803 . . . . . . 7 (𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) → (𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘) ↔ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘)))
5756biimpar 503 . . . . . 6 ((𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ∧ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘)) → 𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘))
5857rexlimivw 3163 . . . . 5 (∃𝑛 ∈ ℕ (𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ∧ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘)) → 𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘))
5954, 55, 583syl 18 . . . 4 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ran seq1( +𝑒 , 𝐹)) → 𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘))
6059ralrimiva 3100 . . 3 (𝐹:ℕ⟶(0[,]+∞) → ∀𝑥 ∈ ran seq1( +𝑒 , 𝐹)𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘))
61 nfv 1988 . . . . . . . . . . 11 𝑘 𝑥 ∈ ℝ
6213, 61nfan 1973 . . . . . . . . . 10 𝑘(𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ)
63 nfcv 2898 . . . . . . . . . . 11 𝑘𝑥
64 nfcv 2898 . . . . . . . . . . 11 𝑘 <
6511nfesum1 30407 . . . . . . . . . . 11 𝑘Σ*𝑘 ∈ ℕ(𝐹𝑘)
6663, 64, 65nfbr 4847 . . . . . . . . . 10 𝑘 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)
6762, 66nfan 1973 . . . . . . . . 9 𝑘((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘))
6833a1i 11 . . . . . . . . 9 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → ℕ ∈ V)
69 simplll 815 . . . . . . . . . 10 ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(0[,]+∞))
7069, 34sylancom 704 . . . . . . . . 9 ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ (0[,]+∞))
71 simplr 809 . . . . . . . . . 10 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → 𝑥 ∈ ℝ)
7271rexrd 10277 . . . . . . . . 9 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → 𝑥 ∈ ℝ*)
73 simpr 479 . . . . . . . . 9 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘))
7467, 68, 70, 72, 73esumlub 30427 . . . . . . . 8 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)𝑥 < Σ*𝑘𝑎(𝐹𝑘))
75 ssnnssfz 29854 . . . . . . . . . 10 (𝑎 ∈ (𝒫 ℕ ∩ Fin) → ∃𝑛 ∈ ℕ 𝑎 ⊆ (1...𝑛))
76 r19.42v 3226 . . . . . . . . . . 11 (∃𝑛 ∈ ℕ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ↔ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ ∃𝑛 ∈ ℕ 𝑎 ⊆ (1...𝑛)))
77 nfv 1988 . . . . . . . . . . . . . 14 𝑘 𝑎 ⊆ (1...𝑛)
7867, 77nfan 1973 . . . . . . . . . . . . 13 𝑘(((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ⊆ (1...𝑛))
7910a1i 11 . . . . . . . . . . . . 13 ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → (1...𝑛) ∈ V)
80 simp-4l 825 . . . . . . . . . . . . . 14 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞))
8117, 18ax-mp 5 . . . . . . . . . . . . . . 15 (1...𝑛) ⊆ ℕ
82 simpr 479 . . . . . . . . . . . . . . 15 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛))
8381, 82sseldi 3738 . . . . . . . . . . . . . 14 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
8480, 83ffvelrnd 6519 . . . . . . . . . . . . 13 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → (𝐹𝑘) ∈ (0[,]+∞))
85 simpr 479 . . . . . . . . . . . . 13 ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → 𝑎 ⊆ (1...𝑛))
8678, 79, 84, 85esummono 30421 . . . . . . . . . . . 12 ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘))
8786reximi 3145 . . . . . . . . . . 11 (∃𝑛 ∈ ℕ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → ∃𝑛 ∈ ℕ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘))
8876, 87sylbir 225 . . . . . . . . . 10 ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ ∃𝑛 ∈ ℕ 𝑎 ⊆ (1...𝑛)) → ∃𝑛 ∈ ℕ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘))
8975, 88sylan2 492 . . . . . . . . 9 ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) → ∃𝑛 ∈ ℕ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘))
9089ralrimiva 3100 . . . . . . . 8 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → ∀𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘))
91 r19.29r 3207 . . . . . . . . 9 ((∃𝑎 ∈ (𝒫 ℕ ∩ Fin)𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ ∀𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)(𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ ∃𝑛 ∈ ℕ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
92 r19.42v 3226 . . . . . . . . . 10 (∃𝑛 ∈ ℕ (𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)) ↔ (𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ ∃𝑛 ∈ ℕ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
9392rexbii 3175 . . . . . . . . 9 (∃𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ (𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)) ↔ ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)(𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ ∃𝑛 ∈ ℕ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
9491, 93sylibr 224 . . . . . . . 8 ((∃𝑎 ∈ (𝒫 ℕ ∩ Fin)𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ ∀𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ (𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
9574, 90, 94syl2anc 696 . . . . . . 7 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ (𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
96 simp-4r 827 . . . . . . . . . . 11 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
9796rexrd 10277 . . . . . . . . . 10 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ*)
98 vex 3339 . . . . . . . . . . . 12 𝑎 ∈ V
99 nfcv 2898 . . . . . . . . . . . . . . . 16 𝑘𝑎
10099nfel1 2913 . . . . . . . . . . . . . . 15 𝑘 𝑎 ∈ (𝒫 ℕ ∩ Fin)
10167, 100nfan 1973 . . . . . . . . . . . . . 14 𝑘(((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin))
102101, 14nfan 1973 . . . . . . . . . . . . 13 𝑘((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ)
103 simp-5l 829 . . . . . . . . . . . . . . 15 ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘𝑎) → 𝐹:ℕ⟶(0[,]+∞))
104 simpllr 817 . . . . . . . . . . . . . . . . 17 ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘𝑎) → 𝑎 ∈ (𝒫 ℕ ∩ Fin))
105 inss1 3972 . . . . . . . . . . . . . . . . . 18 (𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ
106105sseli 3736 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (𝒫 ℕ ∩ Fin) → 𝑎 ∈ 𝒫 ℕ)
107 elpwi 4308 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ 𝒫 ℕ → 𝑎 ⊆ ℕ)
108104, 106, 1073syl 18 . . . . . . . . . . . . . . . 16 ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘𝑎) → 𝑎 ⊆ ℕ)
109 simpr 479 . . . . . . . . . . . . . . . 16 ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘𝑎) → 𝑘𝑎)
110108, 109sseldd 3741 . . . . . . . . . . . . . . 15 ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘𝑎) → 𝑘 ∈ ℕ)
111103, 110ffvelrnd 6519 . . . . . . . . . . . . . 14 ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘𝑎) → (𝐹𝑘) ∈ (0[,]+∞))
112111ex 449 . . . . . . . . . . . . 13 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → (𝑘𝑎 → (𝐹𝑘) ∈ (0[,]+∞)))
113102, 112ralrimi 3091 . . . . . . . . . . . 12 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → ∀𝑘𝑎 (𝐹𝑘) ∈ (0[,]+∞))
11499esumcl 30397 . . . . . . . . . . . 12 ((𝑎 ∈ V ∧ ∀𝑘𝑎 (𝐹𝑘) ∈ (0[,]+∞)) → Σ*𝑘𝑎(𝐹𝑘) ∈ (0[,]+∞))
11598, 113, 114sylancr 698 . . . . . . . . . . 11 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → Σ*𝑘𝑎(𝐹𝑘) ∈ (0[,]+∞))
1167, 115sseldi 3738 . . . . . . . . . 10 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → Σ*𝑘𝑎(𝐹𝑘) ∈ ℝ*)
117 simp-5l 829 . . . . . . . . . . . . . . 15 ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞))
118 simpr 479 . . . . . . . . . . . . . . . 16 ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛))
11981, 118sseldi 3738 . . . . . . . . . . . . . . 15 ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
120117, 119ffvelrnd 6519 . . . . . . . . . . . . . 14 ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐹𝑘) ∈ (0[,]+∞))
121120ex 449 . . . . . . . . . . . . 13 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (1...𝑛) → (𝐹𝑘) ∈ (0[,]+∞)))
122102, 121ralrimi 3091 . . . . . . . . . . . 12 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1...𝑛)(𝐹𝑘) ∈ (0[,]+∞))
12310, 122, 26sylancr 698 . . . . . . . . . . 11 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ∈ (0[,]+∞))
1247, 123sseldi 3738 . . . . . . . . . 10 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ∈ ℝ*)
125 xrltletr 12177 . . . . . . . . . 10 ((𝑥 ∈ ℝ* ∧ Σ*𝑘𝑎(𝐹𝑘) ∈ ℝ* ∧ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ∈ ℝ*) → ((𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)) → 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
12697, 116, 124, 125syl3anc 1477 . . . . . . . . 9 (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → ((𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)) → 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
127126reximdva 3151 . . . . . . . 8 ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) → (∃𝑛 ∈ ℕ (𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
128127rexlimdva 3165 . . . . . . 7 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → (∃𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ (𝑥 < Σ*𝑘𝑎(𝐹𝑘) ∧ Σ*𝑘𝑎(𝐹𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
12995, 128mpd 15 . . . . . 6 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘))
130 fvelrnb 6401 . . . . . . . . . 10 (seq1( +𝑒 , 𝐹) Fn ℕ → (𝑦 ∈ ran seq1( +𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑦))
1316, 130mp1i 13 . . . . . . . . 9 (𝐹:ℕ⟶(0[,]+∞) → (𝑦 ∈ ran seq1( +𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑦))
132 eqcom 2763 . . . . . . . . . . 11 *𝑘 ∈ (1...𝑛)(𝐹𝑘) = 𝑦𝑦 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘))
1339eqeq1d 2758 . . . . . . . . . . 11 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) = 𝑦 ↔ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑦))
134132, 133syl5bbr 274 . . . . . . . . . 10 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (𝑦 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ↔ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑦))
135134rexbidva 3183 . . . . . . . . 9 (𝐹:ℕ⟶(0[,]+∞) → (∃𝑛 ∈ ℕ 𝑦 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑦))
136131, 135bitr4d 271 . . . . . . . 8 (𝐹:ℕ⟶(0[,]+∞) → (𝑦 ∈ ran seq1( +𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ 𝑦 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
137 simpr 479 . . . . . . . . 9 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑦 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)) → 𝑦 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘))
138137breq2d 4812 . . . . . . . 8 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑦 = Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)) → (𝑥 < 𝑦𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
13927, 136, 138rexxfr2d 5028 . . . . . . 7 (𝐹:ℕ⟶(0[,]+∞) → (∃𝑦 ∈ ran seq1( +𝑒 , 𝐹)𝑥 < 𝑦 ↔ ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
140139ad2antrr 764 . . . . . 6 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → (∃𝑦 ∈ ran seq1( +𝑒 , 𝐹)𝑥 < 𝑦 ↔ ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹𝑘)))
141129, 140mpbird 247 . . . . 5 (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘)) → ∃𝑦 ∈ ran seq1( +𝑒 , 𝐹)𝑥 < 𝑦)
142141ex 449 . . . 4 ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘) → ∃𝑦 ∈ ran seq1( +𝑒 , 𝐹)𝑥 < 𝑦))
143142ralrimiva 3100 . . 3 (𝐹:ℕ⟶(0[,]+∞) → ∀𝑥 ∈ ℝ (𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘) → ∃𝑦 ∈ ran seq1( +𝑒 , 𝐹)𝑥 < 𝑦))
144 supxr2 12333 . . 3 (((ran seq1( +𝑒 , 𝐹) ⊆ ℝ* ∧ Σ*𝑘 ∈ ℕ(𝐹𝑘) ∈ ℝ*) ∧ (∀𝑥 ∈ ran seq1( +𝑒 , 𝐹)𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹𝑘) ∧ ∀𝑥 ∈ ℝ (𝑥 < Σ*𝑘 ∈ ℕ(𝐹𝑘) → ∃𝑦 ∈ ran seq1( +𝑒 , 𝐹)𝑥 < 𝑦))) → sup(ran seq1( +𝑒 , 𝐹), ℝ*, < ) = Σ*𝑘 ∈ ℕ(𝐹𝑘))
14532, 39, 60, 143, 144syl22anc 1478 . 2 (𝐹:ℕ⟶(0[,]+∞) → sup(ran seq1( +𝑒 , 𝐹), ℝ*, < ) = Σ*𝑘 ∈ ℕ(𝐹𝑘))
146145eqcomd 2762 1 (𝐹:ℕ⟶(0[,]+∞) → Σ*𝑘 ∈ ℕ(𝐹𝑘) = sup(ran seq1( +𝑒 , 𝐹), ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1628  wcel 2135  wnfc 2885  wral 3046  wrex 3047  Vcvv 3336  cin 3710  wss 3711  𝒫 cpw 4298   class class class wbr 4800  ran crn 5263   Fn wfn 6040  wf 6041  cfv 6045  (class class class)co 6809  Fincfn 8117  supcsup 8507  cr 10123  0cc0 10124  1c1 10125  +∞cpnf 10259  *cxr 10261   < clt 10262  cle 10263  cn 11208  cz 11565  cuz 11875   +𝑒 cxad 12133  [,]cicc 12367  ...cfz 12515  seqcseq 12991  Σ*cesum 30394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-inf2 8707  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201  ax-pre-sup 10202  ax-addf 10203  ax-mulf 10204
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-fal 1634  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-iin 4671  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-se 5222  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-isom 6054  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-of 7058  df-om 7227  df-1st 7329  df-2nd 7330  df-supp 7460  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-2o 7726  df-oadd 7729  df-er 7907  df-map 8021  df-pm 8022  df-ixp 8071  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-fsupp 8437  df-fi 8478  df-sup 8509  df-inf 8510  df-oi 8576  df-card 8951  df-cda 9178  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-div 10873  df-nn 11209  df-2 11267  df-3 11268  df-4 11269  df-5 11270  df-6 11271  df-7 11272  df-8 11273  df-9 11274  df-n0 11481  df-z 11566  df-dec 11682  df-uz 11876  df-q 11978  df-rp 12022  df-xneg 12135  df-xadd 12136  df-xmul 12137  df-ioo 12368  df-ioc 12369  df-ico 12370  df-icc 12371  df-fz 12516  df-fzo 12656  df-fl 12783  df-mod 12859  df-seq 12992  df-exp 13051  df-fac 13251  df-bc 13280  df-hash 13308  df-shft 14002  df-cj 14034  df-re 14035  df-im 14036  df-sqrt 14170  df-abs 14171  df-limsup 14397  df-clim 14414  df-rlim 14415  df-sum 14612  df-ef 14993  df-sin 14995  df-cos 14996  df-pi 14998  df-struct 16057  df-ndx 16058  df-slot 16059  df-base 16061  df-sets 16062  df-ress 16063  df-plusg 16152  df-mulr 16153  df-starv 16154  df-sca 16155  df-vsca 16156  df-ip 16157  df-tset 16158  df-ple 16159  df-ds 16162  df-unif 16163  df-hom 16164  df-cco 16165  df-rest 16281  df-topn 16282  df-0g 16300  df-gsum 16301  df-topgen 16302  df-pt 16303  df-prds 16306  df-ordt 16359  df-xrs 16360  df-qtop 16365  df-imas 16366  df-xps 16368  df-mre 16444  df-mrc 16445  df-acs 16447  df-ps 17397  df-tsr 17398  df-plusf 17438  df-mgm 17439  df-sgrp 17481  df-mnd 17492  df-mhm 17532  df-submnd 17533  df-grp 17622  df-minusg 17623  df-sbg 17624  df-mulg 17738  df-subg 17788  df-cntz 17946  df-cmn 18391  df-abl 18392  df-mgp 18686  df-ur 18698  df-ring 18745  df-cring 18746  df-subrg 18976  df-abv 19015  df-lmod 19063  df-scaf 19064  df-sra 19370  df-rgmod 19371  df-psmet 19936  df-xmet 19937  df-met 19938  df-bl 19939  df-mopn 19940  df-fbas 19941  df-fg 19942  df-cnfld 19945  df-top 20897  df-topon 20914  df-topsp 20935  df-bases 20948  df-cld 21021  df-ntr 21022  df-cls 21023  df-nei 21100  df-lp 21138  df-perf 21139  df-cn 21229  df-cnp 21230  df-haus 21317  df-tx 21563  df-hmeo 21756  df-fil 21847  df-fm 21939  df-flim 21940  df-flf 21941  df-tmd 22073  df-tgp 22074  df-tsms 22127  df-trg 22160  df-xms 22322  df-ms 22323  df-tms 22324  df-nm 22584  df-ngp 22585  df-nrg 22587  df-nlm 22588  df-ii 22877  df-cncf 22878  df-limc 23825  df-dv 23826  df-log 24498  df-esum 30395
This theorem is referenced by:  esumfsupre  30438  esumsup  30456
  Copyright terms: Public domain W3C validator