Step | Hyp | Ref
| Expression |
1 | | peano2nn 12172 |
. . . . 5
โข (๐ โ โ โ (๐ + 1) โ
โ) |
2 | 1 | nnnn0d 12480 |
. . . 4
โข (๐ โ โ โ (๐ + 1) โ
โ0) |
3 | | derang.d |
. . . . 5
โข ๐ท = (๐ฅ โ Fin โฆ (โฏโ{๐ โฃ (๐:๐ฅโ1-1-ontoโ๐ฅ โง โ๐ฆ โ ๐ฅ (๐โ๐ฆ) โ ๐ฆ)})) |
4 | | subfac.n |
. . . . 5
โข ๐ = (๐ โ โ0 โฆ (๐ทโ(1...๐))) |
5 | 3, 4 | subfacval 33807 |
. . . 4
โข ((๐ + 1) โ โ0
โ (๐โ(๐ + 1)) = (๐ทโ(1...(๐ + 1)))) |
6 | 2, 5 | syl 17 |
. . 3
โข (๐ โ โ โ (๐โ(๐ + 1)) = (๐ทโ(1...(๐ + 1)))) |
7 | | fzfid 13885 |
. . . . 5
โข (๐ โ โ โ
(1...(๐ + 1)) โ
Fin) |
8 | 3 | derangval 33801 |
. . . . 5
โข
((1...(๐ + 1))
โ Fin โ (๐ทโ(1...(๐ + 1))) = (โฏโ{๐ โฃ (๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)})) |
9 | 7, 8 | syl 17 |
. . . 4
โข (๐ โ โ โ (๐ทโ(1...(๐ + 1))) = (โฏโ{๐ โฃ (๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)})) |
10 | | subfacp1lem.a |
. . . . 5
โข ๐ด = {๐ โฃ (๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)} |
11 | 10 | fveq2i 6850 |
. . . 4
โข
(โฏโ๐ด) =
(โฏโ{๐ โฃ
(๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)}) |
12 | 9, 11 | eqtr4di 2795 |
. . 3
โข (๐ โ โ โ (๐ทโ(1...(๐ + 1))) = (โฏโ๐ด)) |
13 | | nnuz 12813 |
. . . . . . . . . . 11
โข โ =
(โคโฅโ1) |
14 | 1, 13 | eleqtrdi 2848 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ + 1) โ
(โคโฅโ1)) |
15 | | eluzfz1 13455 |
. . . . . . . . . 10
โข ((๐ + 1) โ
(โคโฅโ1) โ 1 โ (1...(๐ + 1))) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
โข (๐ โ โ โ 1 โ
(1...(๐ +
1))) |
17 | | f1of 6789 |
. . . . . . . . . 10
โข (๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โ ๐:(1...(๐ + 1))โถ(1...(๐ + 1))) |
18 | 17 | adantr 482 |
. . . . . . . . 9
โข ((๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ) โ ๐:(1...(๐ + 1))โถ(1...(๐ + 1))) |
19 | | ffvelcdm 7037 |
. . . . . . . . . 10
โข ((๐:(1...(๐ + 1))โถ(1...(๐ + 1)) โง 1 โ (1...(๐ + 1))) โ (๐โ1) โ (1...(๐ + 1))) |
20 | 19 | expcom 415 |
. . . . . . . . 9
โข (1 โ
(1...(๐ + 1)) โ (๐:(1...(๐ + 1))โถ(1...(๐ + 1)) โ (๐โ1) โ (1...(๐ + 1)))) |
21 | 16, 18, 20 | syl2im 40 |
. . . . . . . 8
โข (๐ โ โ โ ((๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ) โ (๐โ1) โ (1...(๐ + 1)))) |
22 | 21 | ss2abdv 4025 |
. . . . . . 7
โข (๐ โ โ โ {๐ โฃ (๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)} โ {๐ โฃ (๐โ1) โ (1...(๐ + 1))}) |
23 | | fveq1 6846 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐โ1) = (๐โ1)) |
24 | 23 | eleq1d 2823 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐โ1) โ (1...(๐ + 1)) โ (๐โ1) โ (1...(๐ + 1)))) |
25 | 24 | cbvabv 2810 |
. . . . . . 7
โข {๐ โฃ (๐โ1) โ (1...(๐ + 1))} = {๐ โฃ (๐โ1) โ (1...(๐ + 1))} |
26 | 22, 10, 25 | 3sstr4g 3994 |
. . . . . 6
โข (๐ โ โ โ ๐ด โ {๐ โฃ (๐โ1) โ (1...(๐ + 1))}) |
27 | | ssabral 4024 |
. . . . . 6
โข (๐ด โ {๐ โฃ (๐โ1) โ (1...(๐ + 1))} โ โ๐ โ ๐ด (๐โ1) โ (1...(๐ + 1))) |
28 | 26, 27 | sylib 217 |
. . . . 5
โข (๐ โ โ โ
โ๐ โ ๐ด (๐โ1) โ (1...(๐ + 1))) |
29 | | rabid2 3439 |
. . . . 5
โข (๐ด = {๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))} โ โ๐ โ ๐ด (๐โ1) โ (1...(๐ + 1))) |
30 | 28, 29 | sylibr 233 |
. . . 4
โข (๐ โ โ โ ๐ด = {๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) |
31 | 30 | fveq2d 6851 |
. . 3
โข (๐ โ โ โ
(โฏโ๐ด) =
(โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...(๐ + 1))})) |
32 | 6, 12, 31 | 3eqtrd 2781 |
. 2
โข (๐ โ โ โ (๐โ(๐ + 1)) = (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))})) |
33 | | elfz1end 13478 |
. . . 4
โข ((๐ + 1) โ โ โ
(๐ + 1) โ (1...(๐ + 1))) |
34 | 1, 33 | sylib 217 |
. . 3
โข (๐ โ โ โ (๐ + 1) โ (1...(๐ + 1))) |
35 | | eleq1 2826 |
. . . . . . 7
โข (๐ฅ = 1 โ (๐ฅ โ (1...(๐ + 1)) โ 1 โ (1...(๐ + 1)))) |
36 | | oveq2 7370 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ (1...๐ฅ) = (1...1)) |
37 | | 1z 12540 |
. . . . . . . . . . . . . 14
โข 1 โ
โค |
38 | | fzsn 13490 |
. . . . . . . . . . . . . 14
โข (1 โ
โค โ (1...1) = {1}) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . 13
โข (1...1) =
{1} |
40 | 36, 39 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ (1...๐ฅ) = {1}) |
41 | 40 | eleq2d 2824 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ ((๐โ1) โ (1...๐ฅ) โ (๐โ1) โ {1})) |
42 | | fvex 6860 |
. . . . . . . . . . . 12
โข (๐โ1) โ
V |
43 | 42 | elsn 4606 |
. . . . . . . . . . 11
โข ((๐โ1) โ {1} โ
(๐โ1) =
1) |
44 | 41, 43 | bitrdi 287 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ ((๐โ1) โ (1...๐ฅ) โ (๐โ1) = 1)) |
45 | 44 | rabbidv 3418 |
. . . . . . . . 9
โข (๐ฅ = 1 โ {๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)} = {๐ โ ๐ด โฃ (๐โ1) = 1}) |
46 | 45 | fveq2d 6851 |
. . . . . . . 8
โข (๐ฅ = 1 โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = (โฏโ{๐ โ ๐ด โฃ (๐โ1) = 1})) |
47 | | oveq1 7369 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ (๐ฅ โ 1) = (1 โ 1)) |
48 | | 1m1e0 12232 |
. . . . . . . . . 10
โข (1
โ 1) = 0 |
49 | 47, 48 | eqtrdi 2793 |
. . . . . . . . 9
โข (๐ฅ = 1 โ (๐ฅ โ 1) = 0) |
50 | 49 | oveq1d 7377 |
. . . . . . . 8
โข (๐ฅ = 1 โ ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) = (0 ยท ((๐โ๐) + (๐โ(๐ โ 1))))) |
51 | 46, 50 | eqeq12d 2753 |
. . . . . . 7
โข (๐ฅ = 1 โ
((โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) = 1}) = (0 ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) |
52 | 35, 51 | imbi12d 345 |
. . . . . 6
โข (๐ฅ = 1 โ ((๐ฅ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) โ (1 โ (1...(๐ + 1)) โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) = 1}) = (0 ยท
((๐โ๐) + (๐โ(๐ โ 1))))))) |
53 | 52 | imbi2d 341 |
. . . . 5
โข (๐ฅ = 1 โ ((๐ โ โ โ (๐ฅ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) โ (๐ โ โ โ (1 โ (1...(๐ + 1)) โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) = 1}) = (0 ยท
((๐โ๐) + (๐โ(๐ โ 1)))))))) |
54 | | eleq1 2826 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ฅ โ (1...(๐ + 1)) โ ๐ โ (1...(๐ + 1)))) |
55 | | oveq2 7370 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ (1...๐ฅ) = (1...๐)) |
56 | 55 | eleq2d 2824 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ ((๐โ1) โ (1...๐ฅ) โ (๐โ1) โ (1...๐))) |
57 | 56 | rabbidv 3418 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ {๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)} = {๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) |
58 | 57 | fveq2d 6851 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)})) |
59 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (๐ฅ โ 1) = (๐ โ 1)) |
60 | 59 | oveq1d 7377 |
. . . . . . . 8
โข (๐ฅ = ๐ โ ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) |
61 | 58, 60 | eqeq12d 2753 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) |
62 | 54, 61 | imbi12d 345 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ฅ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) โ (๐ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))))) |
63 | 62 | imbi2d 341 |
. . . . 5
โข (๐ฅ = ๐ โ ((๐ โ โ โ (๐ฅ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) โ (๐ โ โ โ (๐ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))))) |
64 | | eleq1 2826 |
. . . . . . 7
โข (๐ฅ = (๐ + 1) โ (๐ฅ โ (1...(๐ + 1)) โ (๐ + 1) โ (1...(๐ + 1)))) |
65 | | oveq2 7370 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ + 1) โ (1...๐ฅ) = (1...(๐ + 1))) |
66 | 65 | eleq2d 2824 |
. . . . . . . . . 10
โข (๐ฅ = (๐ + 1) โ ((๐โ1) โ (1...๐ฅ) โ (๐โ1) โ (1...(๐ + 1)))) |
67 | 66 | rabbidv 3418 |
. . . . . . . . 9
โข (๐ฅ = (๐ + 1) โ {๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)} = {๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) |
68 | 67 | fveq2d 6851 |
. . . . . . . 8
โข (๐ฅ = (๐ + 1) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))})) |
69 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ฅ = (๐ + 1) โ (๐ฅ โ 1) = ((๐ + 1) โ 1)) |
70 | 69 | oveq1d 7377 |
. . . . . . . 8
โข (๐ฅ = (๐ + 1) โ ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) |
71 | 68, 70 | eqeq12d 2753 |
. . . . . . 7
โข (๐ฅ = (๐ + 1) โ ((โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) |
72 | 64, 71 | imbi12d 345 |
. . . . . 6
โข (๐ฅ = (๐ + 1) โ ((๐ฅ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) โ ((๐ + 1) โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))))) |
73 | 72 | imbi2d 341 |
. . . . 5
โข (๐ฅ = (๐ + 1) โ ((๐ โ โ โ (๐ฅ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) โ (๐ โ โ โ ((๐ + 1) โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))))) |
74 | | eleq1 2826 |
. . . . . . 7
โข (๐ฅ = (๐ + 1) โ (๐ฅ โ (1...(๐ + 1)) โ (๐ + 1) โ (1...(๐ + 1)))) |
75 | | oveq2 7370 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ + 1) โ (1...๐ฅ) = (1...(๐ + 1))) |
76 | 75 | eleq2d 2824 |
. . . . . . . . . 10
โข (๐ฅ = (๐ + 1) โ ((๐โ1) โ (1...๐ฅ) โ (๐โ1) โ (1...(๐ + 1)))) |
77 | 76 | rabbidv 3418 |
. . . . . . . . 9
โข (๐ฅ = (๐ + 1) โ {๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)} = {๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) |
78 | 77 | fveq2d 6851 |
. . . . . . . 8
โข (๐ฅ = (๐ + 1) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))})) |
79 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ฅ = (๐ + 1) โ (๐ฅ โ 1) = ((๐ + 1) โ 1)) |
80 | 79 | oveq1d 7377 |
. . . . . . . 8
โข (๐ฅ = (๐ + 1) โ ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) |
81 | 78, 80 | eqeq12d 2753 |
. . . . . . 7
โข (๐ฅ = (๐ + 1) โ ((โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) |
82 | 74, 81 | imbi12d 345 |
. . . . . 6
โข (๐ฅ = (๐ + 1) โ ((๐ฅ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) โ ((๐ + 1) โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))))) |
83 | 82 | imbi2d 341 |
. . . . 5
โข (๐ฅ = (๐ + 1) โ ((๐ โ โ โ (๐ฅ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐ฅ)}) = ((๐ฅ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) โ (๐ โ โ โ ((๐ + 1) โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))))) |
84 | | hash0 14274 |
. . . . . . 7
โข
(โฏโโ
) = 0 |
85 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ = 1 โ (๐โ๐ฆ) = (๐โ1)) |
86 | | id 22 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ = 1 โ ๐ฆ = 1) |
87 | 85, 86 | neeq12d 3006 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = 1 โ ((๐โ๐ฆ) โ ๐ฆ โ (๐โ1) โ 1)) |
88 | 87 | rspcv 3580 |
. . . . . . . . . . . . . 14
โข (1 โ
(1...(๐ + 1)) โ
(โ๐ฆ โ
(1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ โ (๐โ1) โ 1)) |
89 | 16, 88 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(โ๐ฆ โ
(1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ โ (๐โ1) โ 1)) |
90 | 89 | adantld 492 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ) โ (๐โ1) โ 1)) |
91 | 90 | ss2abdv 4025 |
. . . . . . . . . . 11
โข (๐ โ โ โ {๐ โฃ (๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)} โ {๐ โฃ (๐โ1) โ 1}) |
92 | | df-ne 2945 |
. . . . . . . . . . . . 13
โข ((๐โ1) โ 1 โ ยฌ
(๐โ1) =
1) |
93 | 23 | neeq1d 3004 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((๐โ1) โ 1 โ (๐โ1) โ 1)) |
94 | 92, 93 | bitr3id 285 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (ยฌ (๐โ1) = 1 โ (๐โ1) โ 1)) |
95 | 94 | cbvabv 2810 |
. . . . . . . . . . 11
โข {๐ โฃ ยฌ (๐โ1) = 1} = {๐ โฃ (๐โ1) โ 1} |
96 | 91, 10, 95 | 3sstr4g 3994 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ด โ {๐ โฃ ยฌ (๐โ1) = 1}) |
97 | | ssabral 4024 |
. . . . . . . . . 10
โข (๐ด โ {๐ โฃ ยฌ (๐โ1) = 1} โ โ๐ โ ๐ด ยฌ (๐โ1) = 1) |
98 | 96, 97 | sylib 217 |
. . . . . . . . 9
โข (๐ โ โ โ
โ๐ โ ๐ด ยฌ (๐โ1) = 1) |
99 | | rabeq0 4349 |
. . . . . . . . 9
โข ({๐ โ ๐ด โฃ (๐โ1) = 1} = โ
โ โ๐ โ ๐ด ยฌ (๐โ1) = 1) |
100 | 98, 99 | sylibr 233 |
. . . . . . . 8
โข (๐ โ โ โ {๐ โ ๐ด โฃ (๐โ1) = 1} = โ
) |
101 | 100 | fveq2d 6851 |
. . . . . . 7
โข (๐ โ โ โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) = 1}) =
(โฏโโ
)) |
102 | | nnnn0 12427 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ0) |
103 | 3, 4 | subfacf 33809 |
. . . . . . . . . . . 12
โข ๐:โ0โถโ0 |
104 | 103 | ffvelcdmi 7039 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (๐โ๐) โ
โ0) |
105 | 102, 104 | syl 17 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐โ๐) โ
โ0) |
106 | | nnm1nn0 12461 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
107 | 103 | ffvelcdmi 7039 |
. . . . . . . . . . 11
โข ((๐ โ 1) โ
โ0 โ (๐โ(๐ โ 1)) โ
โ0) |
108 | 106, 107 | syl 17 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐โ(๐ โ 1)) โ
โ0) |
109 | 105, 108 | nn0addcld 12484 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐โ๐) + (๐โ(๐ โ 1))) โ
โ0) |
110 | 109 | nn0cnd 12482 |
. . . . . . . 8
โข (๐ โ โ โ ((๐โ๐) + (๐โ(๐ โ 1))) โ
โ) |
111 | 110 | mul02d 11360 |
. . . . . . 7
โข (๐ โ โ โ (0
ยท ((๐โ๐) + (๐โ(๐ โ 1)))) = 0) |
112 | 84, 101, 111 | 3eqtr4a 2803 |
. . . . . 6
โข (๐ โ โ โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) = 1}) = (0 ยท
((๐โ๐) + (๐โ(๐ โ 1))))) |
113 | 112 | a1d 25 |
. . . . 5
โข (๐ โ โ โ (1 โ
(1...(๐ + 1)) โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) = 1}) = (0 ยท
((๐โ๐) + (๐โ(๐ โ 1)))))) |
114 | | simplr 768 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ๐ โ
โ) |
115 | 114, 13 | eleqtrdi 2848 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ๐ โ
(โคโฅโ1)) |
116 | | peano2fzr 13461 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ1) โง (๐ + 1) โ (1...(๐ + 1))) โ ๐ โ (1...(๐ + 1))) |
117 | 115, 116 | sylancom 589 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ๐ โ (1...(๐ + 1))) |
118 | 117 | ex 414 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + 1) โ (1...(๐ + 1)) โ ๐ โ (1...(๐ + 1)))) |
119 | 118 | imim1d 82 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) โ ((๐ + 1) โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))))) |
120 | | oveq1 7369 |
. . . . . . . . . . 11
โข
((โฏโ{๐
โ ๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) โ ((โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) + (โฏโ{๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)})) = (((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) + (โฏโ{๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)}))) |
121 | | elfzp1 13498 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(โคโฅโ1) โ ((๐โ1) โ (1...(๐ + 1)) โ ((๐โ1) โ (1...๐) โจ (๐โ1) = (๐ + 1)))) |
122 | 115, 121 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ((๐โ1) โ (1...(๐ + 1)) โ ((๐โ1) โ (1...๐) โจ (๐โ1) = (๐ + 1)))) |
123 | 122 | rabbidv 3418 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ {๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))} = {๐ โ ๐ด โฃ ((๐โ1) โ (1...๐) โจ (๐โ1) = (๐ + 1))}) |
124 | | unrab 4270 |
. . . . . . . . . . . . . . 15
โข ({๐ โ ๐ด โฃ (๐โ1) โ (1...๐)} โช {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)}) = {๐ โ ๐ด โฃ ((๐โ1) โ (1...๐) โจ (๐โ1) = (๐ + 1))} |
125 | 123, 124 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ {๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))} = ({๐ โ ๐ด โฃ (๐โ1) โ (1...๐)} โช {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)})) |
126 | 125 | fveq2d 6851 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) =
(โฏโ({๐ โ
๐ด โฃ (๐โ1) โ (1...๐)} โช {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)}))) |
127 | | fzfi 13884 |
. . . . . . . . . . . . . . . . 17
โข
(1...(๐ + 1)) โ
Fin |
128 | | deranglem 33800 |
. . . . . . . . . . . . . . . . 17
โข
((1...(๐ + 1))
โ Fin โ {๐
โฃ (๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)} โ Fin) |
129 | 127, 128 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
โข {๐ โฃ (๐:(1...(๐ + 1))โ1-1-ontoโ(1...(๐ + 1)) โง โ๐ฆ โ (1...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)} โ Fin |
130 | 10, 129 | eqeltri 2834 |
. . . . . . . . . . . . . . 15
โข ๐ด โ Fin |
131 | | ssrab2 4042 |
. . . . . . . . . . . . . . 15
โข {๐ โ ๐ด โฃ (๐โ1) โ (1...๐)} โ ๐ด |
132 | | ssfi 9124 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ Fin โง {๐ โ ๐ด โฃ (๐โ1) โ (1...๐)} โ ๐ด) โ {๐ โ ๐ด โฃ (๐โ1) โ (1...๐)} โ Fin) |
133 | 130, 131,
132 | mp2an 691 |
. . . . . . . . . . . . . 14
โข {๐ โ ๐ด โฃ (๐โ1) โ (1...๐)} โ Fin |
134 | | ssrab2 4042 |
. . . . . . . . . . . . . . 15
โข {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)} โ ๐ด |
135 | | ssfi 9124 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ Fin โง {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)} โ ๐ด) โ {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)} โ Fin) |
136 | 130, 134,
135 | mp2an 691 |
. . . . . . . . . . . . . 14
โข {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)} โ Fin |
137 | | inrab 4271 |
. . . . . . . . . . . . . . 15
โข ({๐ โ ๐ด โฃ (๐โ1) โ (1...๐)} โฉ {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)}) = {๐ โ ๐ด โฃ ((๐โ1) โ (1...๐) โง (๐โ1) = (๐ + 1))} |
138 | | fzp1disj 13507 |
. . . . . . . . . . . . . . . . . 18
โข
((1...๐) โฉ
{(๐ + 1)}) =
โ
|
139 | 42 | elsn 4606 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐โ1) โ {(๐ + 1)} โ (๐โ1) = (๐ + 1)) |
140 | | inelcm 4429 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐โ1) โ (1...๐) โง (๐โ1) โ {(๐ + 1)}) โ ((1...๐) โฉ {(๐ + 1)}) โ โ
) |
141 | 139, 140 | sylan2br 596 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐โ1) โ (1...๐) โง (๐โ1) = (๐ + 1)) โ ((1...๐) โฉ {(๐ + 1)}) โ โ
) |
142 | 141 | necon2bi 2975 |
. . . . . . . . . . . . . . . . . 18
โข
(((1...๐) โฉ
{(๐ + 1)}) = โ
โ
ยฌ ((๐โ1) โ
(1...๐) โง (๐โ1) = (๐ + 1))) |
143 | 138, 142 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข ยฌ
((๐โ1) โ
(1...๐) โง (๐โ1) = (๐ + 1)) |
144 | 143 | rgenw 3069 |
. . . . . . . . . . . . . . . 16
โข
โ๐ โ
๐ด ยฌ ((๐โ1) โ (1...๐) โง (๐โ1) = (๐ + 1)) |
145 | | rabeq0 4349 |
. . . . . . . . . . . . . . . 16
โข ({๐ โ ๐ด โฃ ((๐โ1) โ (1...๐) โง (๐โ1) = (๐ + 1))} = โ
โ โ๐ โ ๐ด ยฌ ((๐โ1) โ (1...๐) โง (๐โ1) = (๐ + 1))) |
146 | 144, 145 | mpbir 230 |
. . . . . . . . . . . . . . 15
โข {๐ โ ๐ด โฃ ((๐โ1) โ (1...๐) โง (๐โ1) = (๐ + 1))} = โ
|
147 | 137, 146 | eqtri 2765 |
. . . . . . . . . . . . . 14
โข ({๐ โ ๐ด โฃ (๐โ1) โ (1...๐)} โฉ {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)}) = โ
|
148 | | hashun 14289 |
. . . . . . . . . . . . . 14
โข (({๐ โ ๐ด โฃ (๐โ1) โ (1...๐)} โ Fin โง {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)} โ Fin โง ({๐ โ ๐ด โฃ (๐โ1) โ (1...๐)} โฉ {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)}) = โ
) โ
(โฏโ({๐ โ
๐ด โฃ (๐โ1) โ (1...๐)} โช {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)})) = ((โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) + (โฏโ{๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)}))) |
149 | 133, 136,
147, 148 | mp3an 1462 |
. . . . . . . . . . . . 13
โข
(โฏโ({๐
โ ๐ด โฃ (๐โ1) โ (1...๐)} โช {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)})) = ((โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) + (โฏโ{๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)})) |
150 | 126, 149 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) =
((โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...๐)}) + (โฏโ{๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)}))) |
151 | | nncn 12168 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โ) |
152 | 151 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ๐ โ
โ) |
153 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . 16
โข 1 โ
โ |
154 | 153 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ 1 โ
โ) |
155 | 152, 154,
154 | addsubd 11540 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ((๐ + 1) โ 1) = ((๐ โ 1) +
1)) |
156 | 155 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ (((๐ + 1) โ 1) ยท
((๐โ๐) + (๐โ(๐ โ 1)))) = (((๐ โ 1) + 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) |
157 | | subcl 11407 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
1) โ โ) |
158 | 152, 153,
157 | sylancl 587 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ (๐ โ 1) โ
โ) |
159 | 109 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ((๐โ๐) + (๐โ(๐ โ 1))) โ
โ0) |
160 | 159 | nn0cnd 12482 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ((๐โ๐) + (๐โ(๐ โ 1))) โ
โ) |
161 | 158, 154,
160 | adddird 11187 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ (((๐ โ 1) + 1) ยท
((๐โ๐) + (๐โ(๐ โ 1)))) = (((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) + (1 ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) |
162 | 160 | mulid2d 11180 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ (1 ยท
((๐โ๐) + (๐โ(๐ โ 1)))) = ((๐โ๐) + (๐โ(๐ โ 1)))) |
163 | | exmidne 2954 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐โ(๐ + 1)) = 1 โจ (๐โ(๐ + 1)) โ 1) |
164 | | orcom 869 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐โ(๐ + 1)) = 1 โจ (๐โ(๐ + 1)) โ 1) โ ((๐โ(๐ + 1)) โ 1 โจ (๐โ(๐ + 1)) = 1)) |
165 | 163, 164 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐โ(๐ + 1)) โ 1 โจ (๐โ(๐ + 1)) = 1) |
166 | 165 | biantru 531 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐โ1) = (๐ + 1) โ ((๐โ1) = (๐ + 1) โง ((๐โ(๐ + 1)) โ 1 โจ (๐โ(๐ + 1)) = 1))) |
167 | | andi 1007 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐โ1) = (๐ + 1) โง ((๐โ(๐ + 1)) โ 1 โจ (๐โ(๐ + 1)) = 1)) โ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โจ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1))) |
168 | 166, 167 | bitri 275 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐โ1) = (๐ + 1) โ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โจ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1))) |
169 | 168 | rabbii 3416 |
. . . . . . . . . . . . . . . . . . 19
โข {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)} = {๐ โ ๐ด โฃ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โจ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1))} |
170 | | unrab 4270 |
. . . . . . . . . . . . . . . . . . 19
โข ({๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โช {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)}) = {๐ โ ๐ด โฃ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โจ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1))} |
171 | 169, 170 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . 18
โข {๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)} = ({๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โช {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)}) |
172 | 171 | fveq2i 6850 |
. . . . . . . . . . . . . . . . 17
โข
(โฏโ{๐
โ ๐ด โฃ (๐โ1) = (๐ + 1)}) = (โฏโ({๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โช {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)})) |
173 | | ssrab2 4042 |
. . . . . . . . . . . . . . . . . . 19
โข {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โ ๐ด |
174 | | ssfi 9124 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ Fin โง {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โ ๐ด) โ {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โ Fin) |
175 | 130, 173,
174 | mp2an 691 |
. . . . . . . . . . . . . . . . . 18
โข {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โ Fin |
176 | | ssrab2 4042 |
. . . . . . . . . . . . . . . . . . 19
โข {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)} โ ๐ด |
177 | | ssfi 9124 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ Fin โง {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)} โ ๐ด) โ {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)} โ Fin) |
178 | 130, 176,
177 | mp2an 691 |
. . . . . . . . . . . . . . . . . 18
โข {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)} โ Fin |
179 | | inrab 4271 |
. . . . . . . . . . . . . . . . . . 19
โข ({๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โฉ {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)}) = {๐ โ ๐ด โฃ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โง ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1))} |
180 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1) โ (๐โ(๐ + 1)) = 1) |
181 | 180 | necon3ai 2969 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐โ(๐ + 1)) โ 1 โ ยฌ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)) |
182 | 181 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โ ยฌ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)) |
183 | | imnan 401 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โ ยฌ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)) โ ยฌ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โง ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1))) |
184 | 182, 183 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . 21
โข ยฌ
(((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โง ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)) |
185 | 184 | rgenw 3069 |
. . . . . . . . . . . . . . . . . . . 20
โข
โ๐ โ
๐ด ยฌ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โง ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)) |
186 | | rabeq0 4349 |
. . . . . . . . . . . . . . . . . . . 20
โข ({๐ โ ๐ด โฃ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โง ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1))} = โ
โ โ๐ โ ๐ด ยฌ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โง ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1))) |
187 | 185, 186 | mpbir 230 |
. . . . . . . . . . . . . . . . . . 19
โข {๐ โ ๐ด โฃ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โง ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1))} = โ
|
188 | 179, 187 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
โข ({๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โฉ {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)}) = โ
|
189 | | hashun 14289 |
. . . . . . . . . . . . . . . . . 18
โข (({๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โ Fin โง {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)} โ Fin โง ({๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โฉ {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)}) = โ
) โ
(โฏโ({๐ โ
๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โช {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)})) = ((โฏโ{๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)}) + (โฏโ{๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)}))) |
190 | 175, 178,
188, 189 | mp3an 1462 |
. . . . . . . . . . . . . . . . 17
โข
(โฏโ({๐
โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} โช {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)})) = ((โฏโ{๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)}) + (โฏโ{๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)})) |
191 | 172, 190 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
โข
(โฏโ{๐
โ ๐ด โฃ (๐โ1) = (๐ + 1)}) = ((โฏโ{๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)}) + (โฏโ{๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)})) |
192 | | simpll 766 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ๐ โ โ) |
193 | | nnne0 12194 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ๐ โ 0) |
194 | | 0p1e1 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (0 + 1) =
1 |
195 | 194 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ + 1) = (0 + 1) โ (๐ + 1) = 1) |
196 | | 0cn 11154 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข 0 โ
โ |
197 | | addcan2 11347 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โ โ โง 0 โ
โ โง 1 โ โ) โ ((๐ + 1) = (0 + 1) โ ๐ = 0)) |
198 | 196, 153,
197 | mp3an23 1454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ ((๐ + 1) = (0 + 1) โ ๐ = 0)) |
199 | 151, 198 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ ((๐ + 1) = (0 + 1) โ ๐ = 0)) |
200 | 195, 199 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ((๐ + 1) = 1 โ ๐ = 0)) |
201 | 200 | necon3bbid 2982 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (ยฌ
(๐ + 1) = 1 โ ๐ โ 0)) |
202 | 193, 201 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ยฌ
(๐ + 1) =
1) |
203 | 202 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ยฌ (๐ + 1) = 1) |
204 | 14 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + 1) โ
(โคโฅโ1)) |
205 | | elfzp12 13527 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ + 1) โ
(โคโฅโ1) โ ((๐ + 1) โ (1...(๐ + 1)) โ ((๐ + 1) = 1 โจ (๐ + 1) โ ((1 + 1)...(๐ + 1))))) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + 1) โ (1...(๐ + 1)) โ ((๐ + 1) = 1 โจ (๐ + 1) โ ((1 + 1)...(๐ + 1))))) |
207 | 206 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ ((๐ + 1) = 1 โจ (๐ + 1) โ ((1 + 1)...(๐ + 1)))) |
208 | 207 | ord 863 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ (ยฌ (๐ + 1) = 1 โ (๐ + 1) โ ((1 + 1)...(๐ + 1)))) |
209 | 203, 208 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ (๐ + 1) โ ((1 + 1)...(๐ + 1))) |
210 | | df-2 12223 |
. . . . . . . . . . . . . . . . . . . 20
โข 2 = (1 +
1) |
211 | 210 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . 19
โข
(2...(๐ + 1)) = ((1
+ 1)...(๐ +
1)) |
212 | 209, 211 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ (๐ + 1) โ (2...(๐ + 1))) |
213 | | ovex 7395 |
. . . . . . . . . . . . . . . . . 18
โข (๐ + 1) โ V |
214 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
โข
((2...(๐ + 1))
โ {(๐ + 1)}) =
((2...(๐ + 1)) โ
{(๐ + 1)}) |
215 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = โ โ (๐โ1) = (โโ1)) |
216 | 215 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = โ โ ((๐โ1) = (๐ + 1) โ (โโ1) = (๐ + 1))) |
217 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = โ โ (๐โ(๐ + 1)) = (โโ(๐ + 1))) |
218 | 217 | neeq1d 3004 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = โ โ ((๐โ(๐ + 1)) โ 1 โ (โโ(๐ + 1)) โ 1)) |
219 | 216, 218 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = โ โ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1) โ ((โโ1) = (๐ + 1) โง (โโ(๐ + 1)) โ 1))) |
220 | 219 | cbvrabv 3420 |
. . . . . . . . . . . . . . . . . 18
โข {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)} = {โ โ ๐ด โฃ ((โโ1) = (๐ + 1) โง (โโ(๐ + 1)) โ 1)} |
221 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
โข (( I
โพ ((2...(๐ + 1))
โ {(๐ + 1)})) โช
{โจ1, (๐ + 1)โฉ,
โจ(๐ + 1), 1โฉ}) =
(( I โพ ((2...(๐ + 1))
โ {(๐ + 1)})) โช
{โจ1, (๐ + 1)โฉ,
โจ(๐ + 1),
1โฉ}) |
222 | | f1oeq1 6777 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ (๐:(2...(๐ + 1))โ1-1-ontoโ(2...(๐ + 1)) โ ๐:(2...(๐ + 1))โ1-1-ontoโ(2...(๐ + 1)))) |
223 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ง = ๐ฆ โ (๐โ๐ง) = (๐โ๐ฆ)) |
224 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ง = ๐ฆ โ ๐ง = ๐ฆ) |
225 | 223, 224 | neeq12d 3006 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ง = ๐ฆ โ ((๐โ๐ง) โ ๐ง โ (๐โ๐ฆ) โ ๐ฆ)) |
226 | 225 | cbvralvw 3228 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(โ๐ง โ
(2...(๐ + 1))(๐โ๐ง) โ ๐ง โ โ๐ฆ โ (2...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ) |
227 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = ๐ โ (๐โ๐ฆ) = (๐โ๐ฆ)) |
228 | 227 | neeq1d 3004 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = ๐ โ ((๐โ๐ฆ) โ ๐ฆ โ (๐โ๐ฆ) โ ๐ฆ)) |
229 | 228 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ (โ๐ฆ โ (2...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ โ โ๐ฆ โ (2...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)) |
230 | 226, 229 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ (โ๐ง โ (2...(๐ + 1))(๐โ๐ง) โ ๐ง โ โ๐ฆ โ (2...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)) |
231 | 222, 230 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = ๐ โ ((๐:(2...(๐ + 1))โ1-1-ontoโ(2...(๐ + 1)) โง โ๐ง โ (2...(๐ + 1))(๐โ๐ง) โ ๐ง) โ (๐:(2...(๐ + 1))โ1-1-ontoโ(2...(๐ + 1)) โง โ๐ฆ โ (2...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ))) |
232 | 231 | cbvabv 2810 |
. . . . . . . . . . . . . . . . . 18
โข {๐ โฃ (๐:(2...(๐ + 1))โ1-1-ontoโ(2...(๐ + 1)) โง โ๐ง โ (2...(๐ + 1))(๐โ๐ง) โ ๐ง)} = {๐ โฃ (๐:(2...(๐ + 1))โ1-1-ontoโ(2...(๐ + 1)) โง โ๐ฆ โ (2...(๐ + 1))(๐โ๐ฆ) โ ๐ฆ)} |
233 | 3, 4, 10, 192, 212, 213, 214, 220, 221, 232 | subfacp1lem5 33818 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ
(โฏโ{๐ โ
๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)}) = (๐โ๐)) |
234 | 217 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = โ โ ((๐โ(๐ + 1)) = 1 โ (โโ(๐ + 1)) = 1)) |
235 | 216, 234 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = โ โ (((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1) โ ((โโ1) = (๐ + 1) โง (โโ(๐ + 1)) = 1))) |
236 | 235 | cbvrabv 3420 |
. . . . . . . . . . . . . . . . . 18
โข {๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)} = {โ โ ๐ด โฃ ((โโ1) = (๐ + 1) โง (โโ(๐ + 1)) = 1)} |
237 | | f1oeq1 6777 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ (๐:((2...(๐ + 1)) โ {(๐ + 1)})โ1-1-ontoโ((2...(๐ + 1)) โ {(๐ + 1)}) โ ๐:((2...(๐ + 1)) โ {(๐ + 1)})โ1-1-ontoโ((2...(๐ + 1)) โ {(๐ + 1)}))) |
238 | 225 | cbvralvw 3228 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(โ๐ง โ
((2...(๐ + 1)) โ
{(๐ + 1)})(๐โ๐ง) โ ๐ง โ โ๐ฆ โ ((2...(๐ + 1)) โ {(๐ + 1)})(๐โ๐ฆ) โ ๐ฆ) |
239 | 228 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ (โ๐ฆ โ ((2...(๐ + 1)) โ {(๐ + 1)})(๐โ๐ฆ) โ ๐ฆ โ โ๐ฆ โ ((2...(๐ + 1)) โ {(๐ + 1)})(๐โ๐ฆ) โ ๐ฆ)) |
240 | 238, 239 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ (โ๐ง โ ((2...(๐ + 1)) โ {(๐ + 1)})(๐โ๐ง) โ ๐ง โ โ๐ฆ โ ((2...(๐ + 1)) โ {(๐ + 1)})(๐โ๐ฆ) โ ๐ฆ)) |
241 | 237, 240 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = ๐ โ ((๐:((2...(๐ + 1)) โ {(๐ + 1)})โ1-1-ontoโ((2...(๐ + 1)) โ {(๐ + 1)}) โง โ๐ง โ ((2...(๐ + 1)) โ {(๐ + 1)})(๐โ๐ง) โ ๐ง) โ (๐:((2...(๐ + 1)) โ {(๐ + 1)})โ1-1-ontoโ((2...(๐ + 1)) โ {(๐ + 1)}) โง โ๐ฆ โ ((2...(๐ + 1)) โ {(๐ + 1)})(๐โ๐ฆ) โ ๐ฆ))) |
242 | 241 | cbvabv 2810 |
. . . . . . . . . . . . . . . . . 18
โข {๐ โฃ (๐:((2...(๐ + 1)) โ {(๐ + 1)})โ1-1-ontoโ((2...(๐ + 1)) โ {(๐ + 1)}) โง โ๐ง โ ((2...(๐ + 1)) โ {(๐ + 1)})(๐โ๐ง) โ ๐ง)} = {๐ โฃ (๐:((2...(๐ + 1)) โ {(๐ + 1)})โ1-1-ontoโ((2...(๐ + 1)) โ {(๐ + 1)}) โง โ๐ฆ โ ((2...(๐ + 1)) โ {(๐ + 1)})(๐โ๐ฆ) โ ๐ฆ)} |
243 | 3, 4, 10, 192, 212, 213, 214, 236, 242 | subfacp1lem3 33816 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ
(โฏโ{๐ โ
๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)}) = (๐โ(๐ โ 1))) |
244 | 233, 243 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ
((โฏโ{๐ โ
๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) โ 1)}) + (โฏโ{๐ โ ๐ด โฃ ((๐โ1) = (๐ + 1) โง (๐โ(๐ + 1)) = 1)})) = ((๐โ๐) + (๐โ(๐ โ 1)))) |
245 | 191, 244 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) = (๐ + 1)}) = ((๐โ๐) + (๐โ(๐ โ 1)))) |
246 | 162, 245 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ (1 ยท
((๐โ๐) + (๐โ(๐ โ 1)))) = (โฏโ{๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)})) |
247 | 246 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ (((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) + (1 ยท ((๐โ๐) + (๐โ(๐ โ 1))))) = (((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) + (โฏโ{๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)}))) |
248 | 156, 161,
247 | 3eqtrd 2781 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ (((๐ + 1) โ 1) ยท
((๐โ๐) + (๐โ(๐ โ 1)))) = (((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) + (โฏโ{๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)}))) |
249 | 150, 248 | eqeq12d 2753 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ
((โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) โ ((โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) + (โฏโ{๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)})) = (((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) + (โฏโ{๐ โ ๐ด โฃ (๐โ1) = (๐ + 1)})))) |
250 | 120, 249 | syl5ibr 246 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ + 1) โ (1...(๐ + 1))) โ
((โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) |
251 | 250 | ex 414 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + 1) โ (1...(๐ + 1)) โ
((โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))))) |
252 | 251 | a2d 29 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ + 1) โ (1...(๐ + 1)) โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) โ ((๐ + 1) โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))))) |
253 | 119, 252 | syld 47 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) โ ((๐ + 1) โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))))) |
254 | 253 | expcom 415 |
. . . . . 6
โข (๐ โ โ โ (๐ โ โ โ ((๐ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) โ ((๐ + 1) โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))))) |
255 | 254 | a2d 29 |
. . . . 5
โข (๐ โ โ โ ((๐ โ โ โ (๐ โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...๐)}) = ((๐ โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) โ (๐ โ โ โ ((๐ + 1) โ (1...(๐ + 1)) โ (โฏโ{๐ โ ๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))))) |
256 | 53, 63, 73, 83, 113, 255 | nnind 12178 |
. . . 4
โข ((๐ + 1) โ โ โ
(๐ โ โ โ
((๐ + 1) โ (1...(๐ + 1)) โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))))) |
257 | 1, 256 | mpcom 38 |
. . 3
โข (๐ โ โ โ ((๐ + 1) โ (1...(๐ + 1)) โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1)))))) |
258 | 34, 257 | mpd 15 |
. 2
โข (๐ โ โ โ
(โฏโ{๐ โ
๐ด โฃ (๐โ1) โ (1...(๐ + 1))}) = (((๐ + 1) โ 1) ยท ((๐โ๐) + (๐โ(๐ โ 1))))) |
259 | | nncn 12168 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ) |
260 | | pncan 11414 |
. . . 4
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
261 | 259, 153,
260 | sylancl 587 |
. . 3
โข (๐ โ โ โ ((๐ + 1) โ 1) = ๐) |
262 | 261 | oveq1d 7377 |
. 2
โข (๐ โ โ โ (((๐ + 1) โ 1) ยท
((๐โ๐) + (๐โ(๐ โ 1)))) = (๐ ยท ((๐โ๐) + (๐โ(๐ โ 1))))) |
263 | 32, 258, 262 | 3eqtrd 2781 |
1
โข (๐ โ โ โ (๐โ(๐ + 1)) = (๐ ยท ((๐โ๐) + (๐โ(๐ โ 1))))) |