Step | Hyp | Ref
| Expression |
1 | | iccssxr 13354 |
. . 3
โข
(0[,]+โ) โ โ* |
2 | | esumpinfval.1 |
. . . 4
โข (๐ โ ๐ด โ ๐) |
3 | | esumpinfval.0 |
. . . . 5
โข
โฒ๐๐ |
4 | | esumpinfval.2 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) |
5 | 4 | ex 414 |
. . . . 5
โข (๐ โ (๐ โ ๐ด โ ๐ต โ (0[,]+โ))) |
6 | 3, 5 | ralrimi 3243 |
. . . 4
โข (๐ โ โ๐ โ ๐ด ๐ต โ (0[,]+โ)) |
7 | | nfcv 2908 |
. . . . 5
โข
โฒ๐๐ด |
8 | 7 | esumcl 32669 |
. . . 4
โข ((๐ด โ ๐ โง โ๐ โ ๐ด ๐ต โ (0[,]+โ)) โ
ฮฃ*๐ โ
๐ด๐ต โ (0[,]+โ)) |
9 | 2, 6, 8 | syl2anc 585 |
. . 3
โข (๐ โ ฮฃ*๐ โ ๐ด๐ต โ (0[,]+โ)) |
10 | 1, 9 | sselid 3947 |
. 2
โข (๐ โ ฮฃ*๐ โ ๐ด๐ต โ
โ*) |
11 | | nfrab1 3429 |
. . . . 5
โข
โฒ๐{๐ โ ๐ด โฃ ๐ต = +โ} |
12 | | ssrab2 4042 |
. . . . . 6
โข {๐ โ ๐ด โฃ ๐ต = +โ} โ ๐ด |
13 | 12 | a1i 11 |
. . . . 5
โข (๐ โ {๐ โ ๐ด โฃ ๐ต = +โ} โ ๐ด) |
14 | | 0xr 11209 |
. . . . . . . 8
โข 0 โ
โ* |
15 | | pnfxr 11216 |
. . . . . . . 8
โข +โ
โ โ* |
16 | | 0lepnf 13060 |
. . . . . . . 8
โข 0 โค
+โ |
17 | | ubicc2 13389 |
. . . . . . . 8
โข ((0
โ โ* โง +โ โ โ* โง 0
โค +โ) โ +โ โ (0[,]+โ)) |
18 | 14, 15, 16, 17 | mp3an 1462 |
. . . . . . 7
โข +โ
โ (0[,]+โ) |
19 | 18 | a1i 11 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ด) โง ๐ต = +โ) โ +โ โ
(0[,]+โ)) |
20 | | 0e0iccpnf 13383 |
. . . . . . 7
โข 0 โ
(0[,]+โ) |
21 | 20 | a1i 11 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ด) โง ยฌ ๐ต = +โ) โ 0 โ
(0[,]+โ)) |
22 | 19, 21 | ifclda 4526 |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ if(๐ต = +โ, +โ, 0) โ
(0[,]+โ)) |
23 | | eldif 3925 |
. . . . . . . 8
โข (๐ โ (๐ด โ {๐ โ ๐ด โฃ ๐ต = +โ}) โ (๐ โ ๐ด โง ยฌ ๐ โ {๐ โ ๐ด โฃ ๐ต = +โ})) |
24 | | rabid 3430 |
. . . . . . . . . 10
โข (๐ โ {๐ โ ๐ด โฃ ๐ต = +โ} โ (๐ โ ๐ด โง ๐ต = +โ)) |
25 | 24 | simplbi2 502 |
. . . . . . . . 9
โข (๐ โ ๐ด โ (๐ต = +โ โ ๐ โ {๐ โ ๐ด โฃ ๐ต = +โ})) |
26 | 25 | con3dimp 410 |
. . . . . . . 8
โข ((๐ โ ๐ด โง ยฌ ๐ โ {๐ โ ๐ด โฃ ๐ต = +โ}) โ ยฌ ๐ต = +โ) |
27 | 23, 26 | sylbi 216 |
. . . . . . 7
โข (๐ โ (๐ด โ {๐ โ ๐ด โฃ ๐ต = +โ}) โ ยฌ ๐ต = +โ) |
28 | 27 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ (๐ด โ {๐ โ ๐ด โฃ ๐ต = +โ})) โ ยฌ ๐ต = +โ) |
29 | 28 | iffalsed 4502 |
. . . . 5
โข ((๐ โง ๐ โ (๐ด โ {๐ โ ๐ด โฃ ๐ต = +โ})) โ if(๐ต = +โ, +โ, 0) =
0) |
30 | 3, 11, 7, 13, 2, 22, 29 | esumss 32711 |
. . . 4
โข (๐ โ ฮฃ*๐ โ {๐ โ ๐ด โฃ ๐ต = +โ}if(๐ต = +โ, +โ, 0) =
ฮฃ*๐ โ
๐ดif(๐ต = +โ, +โ, 0)) |
31 | | eqidd 2738 |
. . . . . 6
โข (๐ โ {๐ โ ๐ด โฃ ๐ต = +โ} = {๐ โ ๐ด โฃ ๐ต = +โ}) |
32 | 24 | simprbi 498 |
. . . . . . . 8
โข (๐ โ {๐ โ ๐ด โฃ ๐ต = +โ} โ ๐ต = +โ) |
33 | 32 | iftrued 4499 |
. . . . . . 7
โข (๐ โ {๐ โ ๐ด โฃ ๐ต = +โ} โ if(๐ต = +โ, +โ, 0) =
+โ) |
34 | 33 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ {๐ โ ๐ด โฃ ๐ต = +โ}) โ if(๐ต = +โ, +โ, 0) =
+โ) |
35 | 3, 31, 34 | esumeq12dvaf 32670 |
. . . . 5
โข (๐ โ ฮฃ*๐ โ {๐ โ ๐ด โฃ ๐ต = +โ}if(๐ต = +โ, +โ, 0) =
ฮฃ*๐ โ
{๐ โ ๐ด โฃ ๐ต = +โ}+โ) |
36 | 2, 13 | ssexd 5286 |
. . . . . 6
โข (๐ โ {๐ โ ๐ด โฃ ๐ต = +โ} โ V) |
37 | | nfcv 2908 |
. . . . . . 7
โข
โฒ๐+โ |
38 | 11, 37 | esumcst 32702 |
. . . . . 6
โข (({๐ โ ๐ด โฃ ๐ต = +โ} โ V โง +โ โ
(0[,]+โ)) โ ฮฃ*๐ โ {๐ โ ๐ด โฃ ๐ต = +โ}+โ =
((โฏโ{๐ โ
๐ด โฃ ๐ต = +โ}) ยทe
+โ)) |
39 | 36, 18, 38 | sylancl 587 |
. . . . 5
โข (๐ โ ฮฃ*๐ โ {๐ โ ๐ด โฃ ๐ต = +โ}+โ =
((โฏโ{๐ โ
๐ด โฃ ๐ต = +โ}) ยทe
+โ)) |
40 | | hashxrcl 14264 |
. . . . . . 7
โข ({๐ โ ๐ด โฃ ๐ต = +โ} โ V โ
(โฏโ{๐ โ
๐ด โฃ ๐ต = +โ}) โ
โ*) |
41 | 36, 40 | syl 17 |
. . . . . 6
โข (๐ โ (โฏโ{๐ โ ๐ด โฃ ๐ต = +โ}) โ
โ*) |
42 | | esumpinfval.3 |
. . . . . . . 8
โข (๐ โ โ๐ โ ๐ด ๐ต = +โ) |
43 | | rabn0 4350 |
. . . . . . . 8
โข ({๐ โ ๐ด โฃ ๐ต = +โ} โ โ
โ
โ๐ โ ๐ด ๐ต = +โ) |
44 | 42, 43 | sylibr 233 |
. . . . . . 7
โข (๐ โ {๐ โ ๐ด โฃ ๐ต = +โ} โ โ
) |
45 | | hashgt0 14295 |
. . . . . . 7
โข (({๐ โ ๐ด โฃ ๐ต = +โ} โ V โง {๐ โ ๐ด โฃ ๐ต = +โ} โ โ
) โ 0 <
(โฏโ{๐ โ
๐ด โฃ ๐ต = +โ})) |
46 | 36, 44, 45 | syl2anc 585 |
. . . . . 6
โข (๐ โ 0 <
(โฏโ{๐ โ
๐ด โฃ ๐ต = +โ})) |
47 | | xmulpnf1 13200 |
. . . . . 6
โข
(((โฏโ{๐
โ ๐ด โฃ ๐ต = +โ}) โ
โ* โง 0 < (โฏโ{๐ โ ๐ด โฃ ๐ต = +โ})) โ ((โฏโ{๐ โ ๐ด โฃ ๐ต = +โ}) ยทe +โ)
= +โ) |
48 | 41, 46, 47 | syl2anc 585 |
. . . . 5
โข (๐ โ ((โฏโ{๐ โ ๐ด โฃ ๐ต = +โ}) ยทe +โ)
= +โ) |
49 | 35, 39, 48 | 3eqtrd 2781 |
. . . 4
โข (๐ โ ฮฃ*๐ โ {๐ โ ๐ด โฃ ๐ต = +โ}if(๐ต = +โ, +โ, 0) =
+โ) |
50 | 30, 49 | eqtr3d 2779 |
. . 3
โข (๐ โ ฮฃ*๐ โ ๐ดif(๐ต = +โ, +โ, 0) =
+โ) |
51 | | breq1 5113 |
. . . . 5
โข (+โ
= if(๐ต = +โ,
+โ, 0) โ (+โ โค ๐ต โ if(๐ต = +โ, +โ, 0) โค ๐ต)) |
52 | | breq1 5113 |
. . . . 5
โข (0 =
if(๐ต = +โ, +โ,
0) โ (0 โค ๐ต โ
if(๐ต = +โ, +โ,
0) โค ๐ต)) |
53 | | pnfge 13058 |
. . . . . . . 8
โข (+โ
โ โ* โ +โ โค +โ) |
54 | 15, 53 | ax-mp 5 |
. . . . . . 7
โข +โ
โค +โ |
55 | | breq2 5114 |
. . . . . . 7
โข (๐ต = +โ โ (+โ
โค ๐ต โ +โ โค
+โ)) |
56 | 54, 55 | mpbiri 258 |
. . . . . 6
โข (๐ต = +โ โ +โ โค
๐ต) |
57 | 56 | adantl 483 |
. . . . 5
โข (((๐ โง ๐ โ ๐ด) โง ๐ต = +โ) โ +โ โค ๐ต) |
58 | 4 | adantr 482 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ด) โง ยฌ ๐ต = +โ) โ ๐ต โ (0[,]+โ)) |
59 | | iccgelb 13327 |
. . . . . . 7
โข ((0
โ โ* โง +โ โ โ* โง
๐ต โ (0[,]+โ))
โ 0 โค ๐ต) |
60 | 14, 15, 59 | mp3an12 1452 |
. . . . . 6
โข (๐ต โ (0[,]+โ) โ 0
โค ๐ต) |
61 | 58, 60 | syl 17 |
. . . . 5
โข (((๐ โง ๐ โ ๐ด) โง ยฌ ๐ต = +โ) โ 0 โค ๐ต) |
62 | 51, 52, 57, 61 | ifbothda 4529 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ if(๐ต = +โ, +โ, 0) โค ๐ต) |
63 | 3, 7, 2, 22, 4, 62 | esumlef 32701 |
. . 3
โข (๐ โ ฮฃ*๐ โ ๐ดif(๐ต = +โ, +โ, 0) โค
ฮฃ*๐ โ
๐ด๐ต) |
64 | 50, 63 | eqbrtrrd 5134 |
. 2
โข (๐ โ +โ โค
ฮฃ*๐ โ
๐ด๐ต) |
65 | | xgepnf 13091 |
. . 3
โข
(ฮฃ*๐ โ ๐ด๐ต โ โ* โ (+โ
โค ฮฃ*๐
โ ๐ด๐ต โ ฮฃ*๐ โ ๐ด๐ต = +โ)) |
66 | 65 | biimpd 228 |
. 2
โข
(ฮฃ*๐ โ ๐ด๐ต โ โ* โ (+โ
โค ฮฃ*๐
โ ๐ด๐ต โ ฮฃ*๐ โ ๐ด๐ต = +โ)) |
67 | 10, 64, 66 | sylc 65 |
1
โข (๐ โ ฮฃ*๐ โ ๐ด๐ต = +โ) |