Step | Hyp | Ref
| Expression |
1 | | ssrab2 4077 |
. . . . 5
โข {๐ฅ โ โ โฃ
(expโ๐ฅ) โ
โ} โ โ |
2 | | ax-resscn 11171 |
. . . . 5
โข โ
โ โ |
3 | 1, 2 | sstri 3991 |
. . . 4
โข {๐ฅ โ โ โฃ
(expโ๐ฅ) โ
โ} โ โ |
4 | 3 | a1i 11 |
. . 3
โข (๐ โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ โ} โ
โ) |
5 | | fveq2 6891 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (expโ๐ฅ) = (expโ๐ฆ)) |
6 | 5 | eleq1d 2817 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ((expโ๐ฅ) โ โ โ (expโ๐ฆ) โ
โ)) |
7 | 6 | elrab 3683 |
. . . . 5
โข (๐ฆ โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ โ} โ (๐ฆ โ โ โง
(expโ๐ฆ) โ
โ)) |
8 | | fveq2 6891 |
. . . . . . 7
โข (๐ฅ = ๐ง โ (expโ๐ฅ) = (expโ๐ง)) |
9 | 8 | eleq1d 2817 |
. . . . . 6
โข (๐ฅ = ๐ง โ ((expโ๐ฅ) โ โ โ (expโ๐ง) โ
โ)) |
10 | 9 | elrab 3683 |
. . . . 5
โข (๐ง โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ โ} โ (๐ง โ โ โง
(expโ๐ง) โ
โ)) |
11 | | fveq2 6891 |
. . . . . . 7
โข (๐ฅ = (๐ฆ + ๐ง) โ (expโ๐ฅ) = (expโ(๐ฆ + ๐ง))) |
12 | 11 | eleq1d 2817 |
. . . . . 6
โข (๐ฅ = (๐ฆ + ๐ง) โ ((expโ๐ฅ) โ โ โ (expโ(๐ฆ + ๐ง)) โ โ)) |
13 | | simpll 764 |
. . . . . . 7
โข (((๐ฆ โ โ โง
(expโ๐ฆ) โ
โ) โง (๐ง โ
โ โง (expโ๐ง)
โ โ)) โ ๐ฆ
โ โ) |
14 | | simprl 768 |
. . . . . . 7
โข (((๐ฆ โ โ โง
(expโ๐ฆ) โ
โ) โง (๐ง โ
โ โง (expโ๐ง)
โ โ)) โ ๐ง
โ โ) |
15 | 13, 14 | readdcld 11248 |
. . . . . 6
โข (((๐ฆ โ โ โง
(expโ๐ฆ) โ
โ) โง (๐ง โ
โ โง (expโ๐ง)
โ โ)) โ (๐ฆ
+ ๐ง) โ
โ) |
16 | 13 | recnd 11247 |
. . . . . . . 8
โข (((๐ฆ โ โ โง
(expโ๐ฆ) โ
โ) โง (๐ง โ
โ โง (expโ๐ง)
โ โ)) โ ๐ฆ
โ โ) |
17 | 14 | recnd 11247 |
. . . . . . . 8
โข (((๐ฆ โ โ โง
(expโ๐ฆ) โ
โ) โง (๐ง โ
โ โง (expโ๐ง)
โ โ)) โ ๐ง
โ โ) |
18 | | efadd 16042 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ
(expโ(๐ฆ + ๐ง)) = ((expโ๐ฆ) ยท (expโ๐ง))) |
19 | 16, 17, 18 | syl2anc 583 |
. . . . . . 7
โข (((๐ฆ โ โ โง
(expโ๐ฆ) โ
โ) โง (๐ง โ
โ โง (expโ๐ง)
โ โ)) โ (expโ(๐ฆ + ๐ง)) = ((expโ๐ฆ) ยท (expโ๐ง))) |
20 | | nnmulcl 12241 |
. . . . . . . 8
โข
(((expโ๐ฆ)
โ โ โง (expโ๐ง) โ โ) โ ((expโ๐ฆ) ยท (expโ๐ง)) โ
โ) |
21 | 20 | ad2ant2l 743 |
. . . . . . 7
โข (((๐ฆ โ โ โง
(expโ๐ฆ) โ
โ) โง (๐ง โ
โ โง (expโ๐ง)
โ โ)) โ ((expโ๐ฆ) ยท (expโ๐ง)) โ โ) |
22 | 19, 21 | eqeltrd 2832 |
. . . . . 6
โข (((๐ฆ โ โ โง
(expโ๐ฆ) โ
โ) โง (๐ง โ
โ โง (expโ๐ง)
โ โ)) โ (expโ(๐ฆ + ๐ง)) โ โ) |
23 | 12, 15, 22 | elrabd 3685 |
. . . . 5
โข (((๐ฆ โ โ โง
(expโ๐ฆ) โ
โ) โง (๐ง โ
โ โง (expโ๐ง)
โ โ)) โ (๐ฆ
+ ๐ง) โ {๐ฅ โ โ โฃ
(expโ๐ฅ) โ
โ}) |
24 | 7, 10, 23 | syl2anb 597 |
. . . 4
โข ((๐ฆ โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ โ} โง ๐ง โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ โ}) โ (๐ฆ + ๐ง) โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ
โ}) |
25 | 24 | adantl 481 |
. . 3
โข ((๐ โง (๐ฆ โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ โ} โง ๐ง โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ โ})) โ
(๐ฆ + ๐ง) โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ
โ}) |
26 | | efnnfsumcl.1 |
. . 3
โข (๐ โ ๐ด โ Fin) |
27 | | fveq2 6891 |
. . . . 5
โข (๐ฅ = ๐ต โ (expโ๐ฅ) = (expโ๐ต)) |
28 | 27 | eleq1d 2817 |
. . . 4
โข (๐ฅ = ๐ต โ ((expโ๐ฅ) โ โ โ (expโ๐ต) โ
โ)) |
29 | | efnnfsumcl.2 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
30 | | efnnfsumcl.3 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ (expโ๐ต) โ โ) |
31 | 28, 29, 30 | elrabd 3685 |
. . 3
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ
โ}) |
32 | | 0re 11221 |
. . . . 5
โข 0 โ
โ |
33 | | 1nn 12228 |
. . . . 5
โข 1 โ
โ |
34 | | fveq2 6891 |
. . . . . . . 8
โข (๐ฅ = 0 โ (expโ๐ฅ) =
(expโ0)) |
35 | | ef0 16039 |
. . . . . . . 8
โข
(expโ0) = 1 |
36 | 34, 35 | eqtrdi 2787 |
. . . . . . 7
โข (๐ฅ = 0 โ (expโ๐ฅ) = 1) |
37 | 36 | eleq1d 2817 |
. . . . . 6
โข (๐ฅ = 0 โ ((expโ๐ฅ) โ โ โ 1 โ
โ)) |
38 | 37 | elrab 3683 |
. . . . 5
โข (0 โ
{๐ฅ โ โ โฃ
(expโ๐ฅ) โ
โ} โ (0 โ โ โง 1 โ โ)) |
39 | 32, 33, 38 | mpbir2an 708 |
. . . 4
โข 0 โ
{๐ฅ โ โ โฃ
(expโ๐ฅ) โ
โ} |
40 | 39 | a1i 11 |
. . 3
โข (๐ โ 0 โ {๐ฅ โ โ โฃ
(expโ๐ฅ) โ
โ}) |
41 | 4, 25, 26, 31, 40 | fsumcllem 15683 |
. 2
โข (๐ โ ฮฃ๐ โ ๐ด ๐ต โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ
โ}) |
42 | | fveq2 6891 |
. . . . 5
โข (๐ฅ = ฮฃ๐ โ ๐ด ๐ต โ (expโ๐ฅ) = (expโฮฃ๐ โ ๐ด ๐ต)) |
43 | 42 | eleq1d 2817 |
. . . 4
โข (๐ฅ = ฮฃ๐ โ ๐ด ๐ต โ ((expโ๐ฅ) โ โ โ
(expโฮฃ๐ โ
๐ด ๐ต) โ โ)) |
44 | 43 | elrab 3683 |
. . 3
โข
(ฮฃ๐ โ
๐ด ๐ต โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ โ} โ
(ฮฃ๐ โ ๐ด ๐ต โ โ โง
(expโฮฃ๐ โ
๐ด ๐ต) โ โ)) |
45 | 44 | simprbi 496 |
. 2
โข
(ฮฃ๐ โ
๐ด ๐ต โ {๐ฅ โ โ โฃ (expโ๐ฅ) โ โ} โ
(expโฮฃ๐ โ
๐ด ๐ต) โ โ) |
46 | 41, 45 | syl 17 |
1
โข (๐ โ (expโฮฃ๐ โ ๐ด ๐ต) โ โ) |