Step | Hyp | Ref
| Expression |
1 | | sum0 11380 |
. . . 4
![sum_ sum_](csigma.gif) ![0 0](0.gif) |
2 | | fsumf1o.3 |
. . . . . . . 8
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
3 | | f1oeq2 5446 |
. . . . . . . 8
![( (](lp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![F F](_cf.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
4 | 2, 3 | syl5ibcom 155 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | 4 | imp 124 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![(/) (/)](varnothing.gif)
![F F](_cf.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
6 | | f1ofo 5464 |
. . . . . 6
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![F F](_cf.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![-onto-> -onto->](onto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
7 | | fo00 5493 |
. . . . . . 7
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![-onto-> -onto->](onto.gif)
![( (](lp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | 7 | simprbi 275 |
. . . . . 6
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![-onto-> -onto->](onto.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
9 | 5, 6, 8 | 3syl 17 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![(/) (/)](varnothing.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
10 | 9 | sumeq1d 11358 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![(/) (/)](varnothing.gif)
![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif)
![B B](_cb.gif) ![) )](rp.gif) |
11 | | simpr 110 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![(/) (/)](varnothing.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
12 | 11 | sumeq1d 11358 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![(/) (/)](varnothing.gif)
![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) |
13 | | sum0 11380 |
. . . . 5
![sum_ sum_](csigma.gif) ![0 0](0.gif) |
14 | 12, 13 | eqtrdi 2226 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![(/) (/)](varnothing.gif)
![sum_ sum_](csigma.gif) ![0 0](0.gif) ![) )](rp.gif) |
15 | 1, 10, 14 | 3eqtr4a 2236 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![(/) (/)](varnothing.gif)
![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) |
16 | 15 | ex 115 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![sum_
sum_](csigma.gif)
![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | | 2fveq3 5516 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | | simprl 529 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
19 | | simprr 531 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![f
f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) |
20 | | f1of 5457 |
. . . . . . . . . . . 12
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![-->
-->](longrightarrow.gif) ![A A](_ca.gif) ![) )](rp.gif) |
21 | 2, 20 | syl 14 |
. . . . . . . . . . 11
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![) )](rp.gif) |
22 | 21 | ffvelcdmda 5647 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A A](_ca.gif) ![) )](rp.gif) |
23 | | fsumf1o.5 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
24 | 23 | fmpttd 5667 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
25 | 24 | ffvelcdmda 5647 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![m m](_m.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
26 | 22, 25 | syldan 282 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
27 | 26 | adantlr 477 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
28 | 2 | adantr 276 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
29 | | f1oco 5480 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![`
`](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![( (](lp.gif)
![f f](_f.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![`
`](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
30 | 28, 19, 29 | syl2anc 411 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![)
)](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
31 | | f1of 5457 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![`
`](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![) )](rp.gif) |
32 | 30, 31 | syl 14 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![)
)](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![) )](rp.gif) |
33 | | fvco3 5583 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![)
)](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![)
)](rp.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
34 | 32, 33 | sylan 283 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | | f1of 5457 |
. . . . . . . . . . . 12
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![`
`](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
36 | 35 | ad2antll 491 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![f
f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
37 | | fvco3 5583 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 36, 37 | sylan 283 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 38 | fveq2d 5515 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
40 | 34, 39 | eqtrd 2210 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | 17, 18, 19, 27, 40 | fsum3 11379 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![f f](_f.gif) ![)
)](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![)
)](rp.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | | eqid 2177 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
43 | | fsumf1o.1 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) |
44 | | fsumf1o.4 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![G G](_cg.gif) ![) )](rp.gif) |
45 | 21 | ffvelcdmda 5647 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![A A](_ca.gif) ![) )](rp.gif) |
46 | 44, 45 | eqeltrrd 2255 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![A A](_ca.gif) ![) )](rp.gif) |
47 | 43 | eleq1d 2246 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![) )](rp.gif) ![) )](rp.gif) |
48 | 23 | ralrimiva 2550 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![A. A.](forall.gif)
![CC CC](bbc.gif) ![) )](rp.gif) |
49 | 48 | adantr 276 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![A. A.](forall.gif)
![CC CC](bbc.gif) ![) )](rp.gif) |
50 | 47, 49, 46 | rspcdva 2846 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
51 | 42, 43, 46, 50 | fvmptd3 5605 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![G G](_cg.gif) ![D D](_cd.gif) ![) )](rp.gif) |
52 | 44 | fveq2d 5515 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![G G](_cg.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | | simpr 110 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
54 | | eqid 2177 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) |
55 | 54 | fvmpt2 5595 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![D D](_cd.gif) ![) )](rp.gif) |
56 | 53, 50, 55 | syl2anc 411 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![D D](_cd.gif) ![) )](rp.gif) |
57 | 51, 52, 56 | 3eqtr4rd 2221 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | 57 | ralrimiva 2550 |
. . . . . . . . . 10
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
59 | | nffvmpt1 5522 |
. . . . . . . . . . . 12
![F/_ F/_](_finvbar.gif) ![n n](_n.gif) ![(
(](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) |
60 | 59 | nfeq1 2329 |
. . . . . . . . . . 11
![F/ F/](finv.gif) ![n n](_n.gif) ![(
(](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![)
)](rp.gif) |
61 | | fveq2 5511 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) |
62 | | 2fveq3 5516 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
63 | 61, 62 | eqeq12d 2192 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
64 | 60, 63 | rspc 2835 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
65 | 58, 64 | mpan9 281 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
66 | 65 | adantlr 477 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | 66 | sumeq2dv 11360 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![sum_ sum_](csigma.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
68 | | fveq2 5511 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
69 | 24 | adantr 276 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
70 | 69 | ffvelcdmda 5647 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
71 | 68, 18, 30, 70, 34 | fsum3 11379 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![f f](_f.gif) ![)
)](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![n n](_n.gif) ![)
)](rp.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
72 | 41, 67, 71 | 3eqtr4rd 2221 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![sum_ sum_](csigma.gif)
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) |
73 | | sumfct 11366 |
. . . . . . . 8
![( (](lp.gif) ![A. A.](forall.gif)
![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![sum_
sum_](csigma.gif) ![B B](_cb.gif) ![) )](rp.gif) |
74 | 48, 73 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![sum_
sum_](csigma.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![sum_ sum_](csigma.gif)
![B B](_cb.gif) ![)
)](rp.gif) |
75 | 74 | adantr 276 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![sum_ sum_](csigma.gif)
![B B](_cb.gif) ![) )](rp.gif) |
76 | 50 | ralrimiva 2550 |
. . . . . . . 8
![( (](lp.gif) ![A. A.](forall.gif)
![CC CC](bbc.gif) ![) )](rp.gif) |
77 | | sumfct 11366 |
. . . . . . . 8
![( (](lp.gif) ![A. A.](forall.gif)
![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![sum_
sum_](csigma.gif)
![D D](_cd.gif) ![) )](rp.gif) |
78 | 76, 77 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![sum_
sum_](csigma.gif)
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) |
79 | 78 | adantr 276 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![sum_ sum_](csigma.gif)
![D D](_cd.gif) ![) )](rp.gif) |
80 | 72, 75, 79 | 3eqtr3d 2218 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) |
81 | 80 | expr 375 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
♯![` `](backtick.gif) ![C C](_cc.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
82 | 81 | exlimdv 1819 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
♯![` `](backtick.gif) ![C C](_cc.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f
f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
83 | 82 | expimpd 363 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![sum_ sum_](csigma.gif)
![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![)
)](rp.gif) ![) )](rp.gif) |
84 | | fsumf1o.2 |
. . 3
![( (](lp.gif) ![Fin Fin](_fin.gif) ![) )](rp.gif) |
85 | | fz1f1o 11367 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![E. E.](exists.gif) ![f
f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | 84, 85 | syl 14 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | 16, 83, 86 | mpjaod 718 |
1
![( (](lp.gif) ![sum_
sum_](csigma.gif)
![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) |