![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > gsummpt1n0 | Structured version Visualization version Unicode version |
Description: If only one summand in a finite group sum is not zero, the whole sum equals this summand. More general version of gsummptif1n0 17609. (Contributed by AV, 11-Oct-2019.) |
Ref | Expression |
---|---|
gsummpt1n0.0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
gsummpt1n0.g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
gsummpt1n0.i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
gsummpt1n0.x |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
gsummpt1n0.f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
gsummpt1n0.a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
gsummpt1n0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2452 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | gsummpt1n0.0 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | gsummpt1n0.g |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | gsummpt1n0.i |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | gsummpt1n0.x |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | gsummpt1n0.a |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 6 | r19.21bi 2757 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 2 | mndidcl 16565 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3, 8 | syl 17 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | adantr 471 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 7, 10 | ifcld 3892 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | gsummpt1n0.f |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 11, 12 | fmptd 6030 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 12 | oveq1i 6286 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | eldifsni 4067 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
16 | 15 | adantl 472 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | ifnefalse 3861 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | 16, 17 | syl 17 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 18, 4 | suppss2 6937 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 14, 19 | syl5eqss 3444 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 1, 2, 3, 4, 5, 13, 20 | gsumpt 17605 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | rspcsbela 3763 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
23 | 5, 6, 22 | syl2anc 671 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | iftrue 3855 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
25 | csbeq1 3334 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
26 | 24, 25 | eqtrd 2486 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
27 | nfcv 2593 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
28 | nfv 1765 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() | |
29 | nfcsb1v 3347 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
30 | nfcv 2593 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
31 | 28, 29, 30 | nfif 3878 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | eqeq1 2456 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
33 | csbeq1a 3340 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
34 | 32, 33 | ifbieq1d 3872 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
35 | 27, 31, 34 | cbvmpt 4466 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 12, 35 | eqtri 2474 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | 26, 36 | fvmptg 5930 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
38 | 5, 23, 37 | syl2anc 671 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
39 | 21, 38 | eqtrd 2486 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-8 1893 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-rep 4487 ax-sep 4497 ax-nul 4506 ax-pow 4554 ax-pr 4612 ax-un 6571 ax-inf2 8133 ax-cnex 9582 ax-resscn 9583 ax-1cn 9584 ax-icn 9585 ax-addcl 9586 ax-addrcl 9587 ax-mulcl 9588 ax-mulrcl 9589 ax-mulcom 9590 ax-addass 9591 ax-mulass 9592 ax-distr 9593 ax-i2m1 9594 ax-1ne0 9595 ax-1rid 9596 ax-rnegex 9597 ax-rrecex 9598 ax-cnre 9599 ax-pre-lttri 9600 ax-pre-lttrn 9601 ax-pre-ltadd 9602 ax-pre-mulgt0 9603 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 987 df-3an 988 df-tru 1451 df-fal 1454 df-ex 1668 df-nf 1672 df-sb 1802 df-eu 2304 df-mo 2305 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3015 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-pss 3388 df-nul 3700 df-if 3850 df-pw 3921 df-sn 3937 df-pr 3939 df-tp 3941 df-op 3943 df-uni 4169 df-int 4205 df-iun 4250 df-iin 4251 df-br 4375 df-opab 4434 df-mpt 4435 df-tr 4470 df-eprel 4723 df-id 4727 df-po 4733 df-so 4734 df-fr 4771 df-se 4772 df-we 4773 df-xp 4818 df-rel 4819 df-cnv 4820 df-co 4821 df-dm 4822 df-rn 4823 df-res 4824 df-ima 4825 df-pred 5359 df-ord 5405 df-on 5406 df-lim 5407 df-suc 5408 df-iota 5525 df-fun 5563 df-fn 5564 df-f 5565 df-f1 5566 df-fo 5567 df-f1o 5568 df-fv 5569 df-isom 5570 df-riota 6238 df-ov 6279 df-oprab 6280 df-mpt2 6281 df-om 6681 df-1st 6781 df-2nd 6782 df-supp 6903 df-wrecs 7015 df-recs 7077 df-rdg 7115 df-1o 7169 df-oadd 7173 df-er 7350 df-en 7557 df-dom 7558 df-sdom 7559 df-fin 7560 df-fsupp 7871 df-oi 8012 df-card 8360 df-pnf 9664 df-mnf 9665 df-xr 9666 df-ltxr 9667 df-le 9668 df-sub 9849 df-neg 9850 df-nn 10599 df-2 10657 df-n0 10860 df-z 10928 df-uz 11150 df-fz 11776 df-fzo 11909 df-seq 12208 df-hash 12510 df-ndx 15135 df-slot 15136 df-base 15137 df-sets 15138 df-ress 15139 df-plusg 15214 df-0g 15351 df-gsum 15352 df-mre 15503 df-mrc 15504 df-acs 15506 df-mgm 16499 df-sgrp 16538 df-mnd 16548 df-submnd 16594 df-mulg 16687 df-cntz 16982 df-cmn 17443 |
This theorem is referenced by: gsummptif1n0 17609 gsummoncoe1 18909 scmatscm 19549 idpm2idmp 19836 mp2pm2mplem4 19844 monmat2matmon 19859 |
Copyright terms: Public domain | W3C validator |