Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsummulc2 Structured version   Visualization version   GIF version

Theorem fsummulc2 15134
 Description: A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
Hypotheses
Ref Expression
fsummulc2.1 (𝜑𝐴 ∈ Fin)
fsummulc2.2 (𝜑𝐶 ∈ ℂ)
fsummulc2.3 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
Assertion
Ref Expression
fsummulc2 (𝜑 → (𝐶 · Σ𝑘𝐴 𝐵) = Σ𝑘𝐴 (𝐶 · 𝐵))
Distinct variable groups:   𝐴,𝑘   𝐶,𝑘   𝜑,𝑘
Allowed substitution hint:   𝐵(𝑘)

Proof of Theorem fsummulc2
Dummy variables 𝑓 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fsummulc2.2 . . . 4 (𝜑𝐶 ∈ ℂ)
21mul01d 10832 . . 3 (𝜑 → (𝐶 · 0) = 0)
3 sumeq1 15040 . . . . . 6 (𝐴 = ∅ → Σ𝑘𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵)
4 sum0 15073 . . . . . 6 Σ𝑘 ∈ ∅ 𝐵 = 0
53, 4eqtrdi 2852 . . . . 5 (𝐴 = ∅ → Σ𝑘𝐴 𝐵 = 0)
65oveq2d 7155 . . . 4 (𝐴 = ∅ → (𝐶 · Σ𝑘𝐴 𝐵) = (𝐶 · 0))
7 sumeq1 15040 . . . . 5 (𝐴 = ∅ → Σ𝑘𝐴 (𝐶 · 𝐵) = Σ𝑘 ∈ ∅ (𝐶 · 𝐵))
8 sum0 15073 . . . . 5 Σ𝑘 ∈ ∅ (𝐶 · 𝐵) = 0
97, 8eqtrdi 2852 . . . 4 (𝐴 = ∅ → Σ𝑘𝐴 (𝐶 · 𝐵) = 0)
106, 9eqeq12d 2817 . . 3 (𝐴 = ∅ → ((𝐶 · Σ𝑘𝐴 𝐵) = Σ𝑘𝐴 (𝐶 · 𝐵) ↔ (𝐶 · 0) = 0))
112, 10syl5ibrcom 250 . 2 (𝜑 → (𝐴 = ∅ → (𝐶 · Σ𝑘𝐴 𝐵) = Σ𝑘𝐴 (𝐶 · 𝐵)))
12 addcl 10612 . . . . . . . . 9 ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑛 + 𝑚) ∈ ℂ)
1312adantl 485 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑛 + 𝑚) ∈ ℂ)
141adantr 484 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → 𝐶 ∈ ℂ)
15 adddi 10619 . . . . . . . . . 10 ((𝐶 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝐶 · (𝑛 + 𝑚)) = ((𝐶 · 𝑛) + (𝐶 · 𝑚)))
16153expb 1117 . . . . . . . . 9 ((𝐶 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝐶 · (𝑛 + 𝑚)) = ((𝐶 · 𝑛) + (𝐶 · 𝑚)))
1714, 16sylan 583 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝐶 · (𝑛 + 𝑚)) = ((𝐶 · 𝑛) + (𝐶 · 𝑚)))
18 simprl 770 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (♯‘𝐴) ∈ ℕ)
19 nnuz 12273 . . . . . . . . 9 ℕ = (ℤ‘1)
2018, 19eleqtrdi 2903 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (♯‘𝐴) ∈ (ℤ‘1))
21 fsummulc2.3 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
2221fmpttd 6860 . . . . . . . . . . 11 (𝜑 → (𝑘𝐴𝐵):𝐴⟶ℂ)
2322ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝑘𝐴𝐵):𝐴⟶ℂ)
24 simprr 772 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)
2524adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)
26 f1of 6594 . . . . . . . . . . 11 (𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑓:(1...(♯‘𝐴))⟶𝐴)
2725, 26syl 17 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → 𝑓:(1...(♯‘𝐴))⟶𝐴)
28 fco 6509 . . . . . . . . . 10 (((𝑘𝐴𝐵):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘𝐴𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
2923, 27, 28syl2anc 587 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((𝑘𝐴𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
30 simpr 488 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → 𝑛 ∈ (1...(♯‘𝐴)))
3129, 30ffvelrnd 6833 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴𝐵) ∘ 𝑓)‘𝑛) ∈ ℂ)
3227, 30ffvelrnd 6833 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝑓𝑛) ∈ 𝐴)
33 simpr 488 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → 𝑘𝐴)
341adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → 𝐶 ∈ ℂ)
3534, 21mulcld 10654 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → (𝐶 · 𝐵) ∈ ℂ)
36 eqid 2801 . . . . . . . . . . . . . . 15 (𝑘𝐴 ↦ (𝐶 · 𝐵)) = (𝑘𝐴 ↦ (𝐶 · 𝐵))
3736fvmpt2 6760 . . . . . . . . . . . . . 14 ((𝑘𝐴 ∧ (𝐶 · 𝐵) ∈ ℂ) → ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑘) = (𝐶 · 𝐵))
3833, 35, 37syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑘) = (𝐶 · 𝐵))
39 eqid 2801 . . . . . . . . . . . . . . . 16 (𝑘𝐴𝐵) = (𝑘𝐴𝐵)
4039fvmpt2 6760 . . . . . . . . . . . . . . 15 ((𝑘𝐴𝐵 ∈ ℂ) → ((𝑘𝐴𝐵)‘𝑘) = 𝐵)
4133, 21, 40syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → ((𝑘𝐴𝐵)‘𝑘) = 𝐵)
4241oveq2d 7155 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝐶 · ((𝑘𝐴𝐵)‘𝑘)) = (𝐶 · 𝐵))
4338, 42eqtr4d 2839 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑘) = (𝐶 · ((𝑘𝐴𝐵)‘𝑘)))
4443ralrimiva 3152 . . . . . . . . . . 11 (𝜑 → ∀𝑘𝐴 ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑘) = (𝐶 · ((𝑘𝐴𝐵)‘𝑘)))
4544ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ∀𝑘𝐴 ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑘) = (𝐶 · ((𝑘𝐴𝐵)‘𝑘)))
46 nffvmpt1 6660 . . . . . . . . . . . 12 𝑘((𝑘𝐴 ↦ (𝐶 · 𝐵))‘(𝑓𝑛))
47 nfcv 2958 . . . . . . . . . . . . 13 𝑘𝐶
48 nfcv 2958 . . . . . . . . . . . . 13 𝑘 ·
49 nffvmpt1 6660 . . . . . . . . . . . . 13 𝑘((𝑘𝐴𝐵)‘(𝑓𝑛))
5047, 48, 49nfov 7169 . . . . . . . . . . . 12 𝑘(𝐶 · ((𝑘𝐴𝐵)‘(𝑓𝑛)))
5146, 50nfeq 2971 . . . . . . . . . . 11 𝑘((𝑘𝐴 ↦ (𝐶 · 𝐵))‘(𝑓𝑛)) = (𝐶 · ((𝑘𝐴𝐵)‘(𝑓𝑛)))
52 fveq2 6649 . . . . . . . . . . . 12 (𝑘 = (𝑓𝑛) → ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑘) = ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘(𝑓𝑛)))
53 fveq2 6649 . . . . . . . . . . . . 13 (𝑘 = (𝑓𝑛) → ((𝑘𝐴𝐵)‘𝑘) = ((𝑘𝐴𝐵)‘(𝑓𝑛)))
5453oveq2d 7155 . . . . . . . . . . . 12 (𝑘 = (𝑓𝑛) → (𝐶 · ((𝑘𝐴𝐵)‘𝑘)) = (𝐶 · ((𝑘𝐴𝐵)‘(𝑓𝑛))))
5552, 54eqeq12d 2817 . . . . . . . . . . 11 (𝑘 = (𝑓𝑛) → (((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑘) = (𝐶 · ((𝑘𝐴𝐵)‘𝑘)) ↔ ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘(𝑓𝑛)) = (𝐶 · ((𝑘𝐴𝐵)‘(𝑓𝑛)))))
5651, 55rspc 3562 . . . . . . . . . 10 ((𝑓𝑛) ∈ 𝐴 → (∀𝑘𝐴 ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑘) = (𝐶 · ((𝑘𝐴𝐵)‘𝑘)) → ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘(𝑓𝑛)) = (𝐶 · ((𝑘𝐴𝐵)‘(𝑓𝑛)))))
5732, 45, 56sylc 65 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘(𝑓𝑛)) = (𝐶 · ((𝑘𝐴𝐵)‘(𝑓𝑛))))
5826ad2antll 728 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴)
59 fvco3 6741 . . . . . . . . . 10 ((𝑓:(1...(♯‘𝐴))⟶𝐴𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴 ↦ (𝐶 · 𝐵)) ∘ 𝑓)‘𝑛) = ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘(𝑓𝑛)))
6058, 59sylan 583 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴 ↦ (𝐶 · 𝐵)) ∘ 𝑓)‘𝑛) = ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘(𝑓𝑛)))
61 fvco3 6741 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝐴))⟶𝐴𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴𝐵) ∘ 𝑓)‘𝑛) = ((𝑘𝐴𝐵)‘(𝑓𝑛)))
6258, 61sylan 583 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴𝐵) ∘ 𝑓)‘𝑛) = ((𝑘𝐴𝐵)‘(𝑓𝑛)))
6362oveq2d 7155 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐶 · (((𝑘𝐴𝐵) ∘ 𝑓)‘𝑛)) = (𝐶 · ((𝑘𝐴𝐵)‘(𝑓𝑛))))
6457, 60, 633eqtr4d 2846 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴 ↦ (𝐶 · 𝐵)) ∘ 𝑓)‘𝑛) = (𝐶 · (((𝑘𝐴𝐵) ∘ 𝑓)‘𝑛)))
6513, 17, 20, 31, 64seqdistr 13421 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (seq1( + , ((𝑘𝐴 ↦ (𝐶 · 𝐵)) ∘ 𝑓))‘(♯‘𝐴)) = (𝐶 · (seq1( + , ((𝑘𝐴𝐵) ∘ 𝑓))‘(♯‘𝐴))))
66 fveq2 6649 . . . . . . . 8 (𝑚 = (𝑓𝑛) → ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑚) = ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘(𝑓𝑛)))
6735fmpttd 6860 . . . . . . . . . 10 (𝜑 → (𝑘𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ)
6867adantr 484 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (𝑘𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ)
6968ffvelrnda 6832 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑚𝐴) → ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑚) ∈ ℂ)
7066, 18, 24, 69, 60fsum 15072 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → Σ𝑚𝐴 ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑚) = (seq1( + , ((𝑘𝐴 ↦ (𝐶 · 𝐵)) ∘ 𝑓))‘(♯‘𝐴)))
71 fveq2 6649 . . . . . . . . 9 (𝑚 = (𝑓𝑛) → ((𝑘𝐴𝐵)‘𝑚) = ((𝑘𝐴𝐵)‘(𝑓𝑛)))
7222adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (𝑘𝐴𝐵):𝐴⟶ℂ)
7372ffvelrnda 6832 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑚𝐴) → ((𝑘𝐴𝐵)‘𝑚) ∈ ℂ)
7471, 18, 24, 73, 62fsum 15072 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → Σ𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = (seq1( + , ((𝑘𝐴𝐵) ∘ 𝑓))‘(♯‘𝐴)))
7574oveq2d 7155 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (𝐶 · Σ𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚)) = (𝐶 · (seq1( + , ((𝑘𝐴𝐵) ∘ 𝑓))‘(♯‘𝐴))))
7665, 70, 753eqtr4rd 2847 . . . . . 6 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (𝐶 · Σ𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚)) = Σ𝑚𝐴 ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑚))
77 sumfc 15061 . . . . . . 7 Σ𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = Σ𝑘𝐴 𝐵
7877oveq2i 7150 . . . . . 6 (𝐶 · Σ𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚)) = (𝐶 · Σ𝑘𝐴 𝐵)
79 sumfc 15061 . . . . . 6 Σ𝑚𝐴 ((𝑘𝐴 ↦ (𝐶 · 𝐵))‘𝑚) = Σ𝑘𝐴 (𝐶 · 𝐵)
8076, 78, 793eqtr3g 2859 . . . . 5 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (𝐶 · Σ𝑘𝐴 𝐵) = Σ𝑘𝐴 (𝐶 · 𝐵))
8180expr 460 . . . 4 ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto𝐴 → (𝐶 · Σ𝑘𝐴 𝐵) = Σ𝑘𝐴 (𝐶 · 𝐵)))
8281exlimdv 1934 . . 3 ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴 → (𝐶 · Σ𝑘𝐴 𝐵) = Σ𝑘𝐴 (𝐶 · 𝐵)))
8382expimpd 457 . 2 (𝜑 → (((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) → (𝐶 · Σ𝑘𝐴 𝐵) = Σ𝑘𝐴 (𝐶 · 𝐵)))
84 fsummulc2.1 . . 3 (𝜑𝐴 ∈ Fin)
85 fz1f1o 15062 . . 3 (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)))
8684, 85syl 17 . 2 (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)))
8711, 83, 86mpjaod 857 1 (𝜑 → (𝐶 · Σ𝑘𝐴 𝐵) = Σ𝑘𝐴 (𝐶 · 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2112  ∀wral 3109  ∅c0 4246   ↦ cmpt 5113   ∘ ccom 5527  ⟶wf 6324  –1-1-onto→wf1o 6327  ‘cfv 6328  (class class class)co 7139  Fincfn 8496  ℂcc 10528  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535  ℕcn 11629  ℤ≥cuz 12235  ...cfz 12889  seqcseq 13368  ♯chash 13690  Σcsu 15037 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-sup 8894  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-rp 12382  df-fz 12890  df-fzo 13033  df-seq 13369  df-exp 13430  df-hash 13691  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-sum 15038 This theorem is referenced by:  fsummulc1  15135  fsumneg  15137  fsum2mul  15139  incexc2  15188  pwdif  15218  mertens  15237  binomrisefac  15391  fsumkthpow  15405  eirrlem  15552  pwp1fsum  15735  csbren  24006  trirn  24007  itg1addlem4  24306  itg1addlem5  24307  itg1mulc  24311  elqaalem3  24920  advlogexp  25249  fsumharmonic  25600  basellem8  25676  muinv  25781  fsumdvdsmul  25783  logfaclbnd  25809  dchrsum2  25855  sumdchr2  25857  rplogsumlem2  26072  rpvmasumlem  26074  dchrmusum2  26081  dchrvmasumlem1  26082  dchrvmasum2lem  26083  dchrvmasumlem2  26085  dchrvmasumiflem1  26088  rpvmasum2  26099  dchrisum0lem2  26105  mudivsum  26117  mulogsum  26119  mulog2sumlem1  26121  mulog2sumlem2  26122  mulog2sumlem3  26123  vmalogdivsum2  26125  logsqvma  26129  selberglem1  26132  selberglem2  26133  selberg  26135  selberg3lem1  26144  selberg4lem1  26147  selberg4  26148  selbergr  26155  selberg3r  26156  selberg34r  26158  pntsval2  26163  pntrlog2bndlem2  26165  pntrlog2bndlem3  26166  pntrlog2bndlem4  26167  pntrlog2bndlem6  26170  pntpbnd2  26174  pntlemk  26193  axsegconlem9  26722  ax5seglem1  26725  ax5seglem2  26726  ax5seglem9  26734  hgt750lemf  32032  hgt750lemb  32035  knoppndvlem11  33969  3factsumint4  39305  lcmineqlem6  39315  jm2.22  39923  dvnprodlem2  42576  stoweidlem26  42655  stirlinglem12  42714  fourierdlem83  42818  etransclem46  42909  altgsumbcALT  44742  aacllem  45316
 Copyright terms: Public domain W3C validator