Step | Hyp | Ref
| Expression |
1 | | f1eq2 6739 |
. . . . . . . . 9
โข (๐ฅ = โ
โ (๐:๐ฅโ1-1โ๐ต โ ๐:โ
โ1-1โ๐ต)) |
2 | | f1fn 6744 |
. . . . . . . . . . . 12
โข (๐:โ
โ1-1โ๐ต โ ๐ Fn โ
) |
3 | | fn0 6637 |
. . . . . . . . . . . 12
โข (๐ Fn โ
โ ๐ = โ
) |
4 | 2, 3 | sylib 217 |
. . . . . . . . . . 11
โข (๐:โ
โ1-1โ๐ต โ ๐ = โ
) |
5 | | f10 6822 |
. . . . . . . . . . . 12
โข
โ
:โ
โ1-1โ๐ต |
6 | | f1eq1 6738 |
. . . . . . . . . . . 12
โข (๐ = โ
โ (๐:โ
โ1-1โ๐ต โ โ
:โ
โ1-1โ๐ต)) |
7 | 5, 6 | mpbiri 258 |
. . . . . . . . . . 11
โข (๐ = โ
โ ๐:โ
โ1-1โ๐ต) |
8 | 4, 7 | impbii 208 |
. . . . . . . . . 10
โข (๐:โ
โ1-1โ๐ต โ ๐ = โ
) |
9 | | velsn 4607 |
. . . . . . . . . 10
โข (๐ โ {โ
} โ ๐ = โ
) |
10 | 8, 9 | bitr4i 278 |
. . . . . . . . 9
โข (๐:โ
โ1-1โ๐ต โ ๐ โ {โ
}) |
11 | 1, 10 | bitrdi 287 |
. . . . . . . 8
โข (๐ฅ = โ
โ (๐:๐ฅโ1-1โ๐ต โ ๐ โ {โ
})) |
12 | 11 | abbi1dv 2873 |
. . . . . . 7
โข (๐ฅ = โ
โ {๐ โฃ ๐:๐ฅโ1-1โ๐ต} = {โ
}) |
13 | 12 | fveq2d 6851 |
. . . . . 6
โข (๐ฅ = โ
โ
(โฏโ{๐ โฃ
๐:๐ฅโ1-1โ๐ต}) =
(โฏโ{โ
})) |
14 | | 0ex 5269 |
. . . . . . 7
โข โ
โ V |
15 | | hashsng 14276 |
. . . . . . 7
โข (โ
โ V โ (โฏโ{โ
}) = 1) |
16 | 14, 15 | ax-mp 5 |
. . . . . 6
โข
(โฏโ{โ
}) = 1 |
17 | 13, 16 | eqtrdi 2793 |
. . . . 5
โข (๐ฅ = โ
โ
(โฏโ{๐ โฃ
๐:๐ฅโ1-1โ๐ต}) = 1) |
18 | | fveq2 6847 |
. . . . . . . . 9
โข (๐ฅ = โ
โ
(โฏโ๐ฅ) =
(โฏโโ
)) |
19 | | hash0 14274 |
. . . . . . . . 9
โข
(โฏโโ
) = 0 |
20 | 18, 19 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ฅ = โ
โ
(โฏโ๐ฅ) =
0) |
21 | 20 | fveq2d 6851 |
. . . . . . 7
โข (๐ฅ = โ
โ
(!โ(โฏโ๐ฅ))
= (!โ0)) |
22 | | fac0 14183 |
. . . . . . 7
โข
(!โ0) = 1 |
23 | 21, 22 | eqtrdi 2793 |
. . . . . 6
โข (๐ฅ = โ
โ
(!โ(โฏโ๐ฅ))
= 1) |
24 | 20 | oveq2d 7378 |
. . . . . 6
โข (๐ฅ = โ
โ
((โฏโ๐ต)C(โฏโ๐ฅ)) = ((โฏโ๐ต)C0)) |
25 | 23, 24 | oveq12d 7380 |
. . . . 5
โข (๐ฅ = โ
โ
((!โ(โฏโ๐ฅ)) ยท ((โฏโ๐ต)C(โฏโ๐ฅ))) = (1 ยท ((โฏโ๐ต)C0))) |
26 | 17, 25 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = โ
โ
((โฏโ{๐ โฃ
๐:๐ฅโ1-1โ๐ต}) = ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ))) โ 1 = (1 ยท
((โฏโ๐ต)C0)))) |
27 | 26 | imbi2d 341 |
. . 3
โข (๐ฅ = โ
โ ((๐ต โ Fin โ
(โฏโ{๐ โฃ
๐:๐ฅโ1-1โ๐ต}) = ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ)))) โ (๐ต โ Fin โ 1 = (1 ยท
((โฏโ๐ต)C0))))) |
28 | | f1eq2 6739 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (๐:๐ฅโ1-1โ๐ต โ ๐:๐ฆโ1-1โ๐ต)) |
29 | 28 | abbidv 2806 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ {๐ โฃ ๐:๐ฅโ1-1โ๐ต} = {๐ โฃ ๐:๐ฆโ1-1โ๐ต}) |
30 | 29 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (โฏโ{๐ โฃ ๐:๐ฅโ1-1โ๐ต}) = (โฏโ{๐ โฃ ๐:๐ฆโ1-1โ๐ต})) |
31 | | 2fveq3 6852 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (!โ(โฏโ๐ฅ)) =
(!โ(โฏโ๐ฆ))) |
32 | | fveq2 6847 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (โฏโ๐ฅ) = (โฏโ๐ฆ)) |
33 | 32 | oveq2d 7378 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ((โฏโ๐ต)C(โฏโ๐ฅ)) = ((โฏโ๐ต)C(โฏโ๐ฆ))) |
34 | 31, 33 | oveq12d 7380 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ))) = ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ)))) |
35 | 30, 34 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((โฏโ{๐ โฃ ๐:๐ฅโ1-1โ๐ต}) = ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ))) โ (โฏโ{๐ โฃ ๐:๐ฆโ1-1โ๐ต}) = ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ))))) |
36 | 35 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ต โ Fin โ (โฏโ{๐ โฃ ๐:๐ฅโ1-1โ๐ต}) = ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ)))) โ (๐ต โ Fin โ (โฏโ{๐ โฃ ๐:๐ฆโ1-1โ๐ต}) = ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ)))))) |
37 | | f1eq2 6739 |
. . . . . . 7
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (๐:๐ฅโ1-1โ๐ต โ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต)) |
38 | 37 | abbidv 2806 |
. . . . . 6
โข (๐ฅ = (๐ฆ โช {๐ง}) โ {๐ โฃ ๐:๐ฅโ1-1โ๐ต} = {๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) |
39 | 38 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (โฏโ{๐ โฃ ๐:๐ฅโ1-1โ๐ต}) = (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต})) |
40 | | 2fveq3 6852 |
. . . . . 6
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (!โ(โฏโ๐ฅ)) =
(!โ(โฏโ(๐ฆ
โช {๐ง})))) |
41 | | fveq2 6847 |
. . . . . . 7
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (โฏโ๐ฅ) = (โฏโ(๐ฆ โช {๐ง}))) |
42 | 41 | oveq2d 7378 |
. . . . . 6
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((โฏโ๐ต)C(โฏโ๐ฅ)) = ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง})))) |
43 | 40, 42 | oveq12d 7380 |
. . . . 5
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ))) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง}))))) |
44 | 39, 43 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((โฏโ{๐ โฃ ๐:๐ฅโ1-1โ๐ต}) = ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ))) โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง})))))) |
45 | 44 | imbi2d 341 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((๐ต โ Fin โ (โฏโ{๐ โฃ ๐:๐ฅโ1-1โ๐ต}) = ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ)))) โ (๐ต โ Fin โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง}))))))) |
46 | | f1eq2 6739 |
. . . . . . 7
โข (๐ฅ = ๐ด โ (๐:๐ฅโ1-1โ๐ต โ ๐:๐ดโ1-1โ๐ต)) |
47 | 46 | abbidv 2806 |
. . . . . 6
โข (๐ฅ = ๐ด โ {๐ โฃ ๐:๐ฅโ1-1โ๐ต} = {๐ โฃ ๐:๐ดโ1-1โ๐ต}) |
48 | 47 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = ๐ด โ (โฏโ{๐ โฃ ๐:๐ฅโ1-1โ๐ต}) = (โฏโ{๐ โฃ ๐:๐ดโ1-1โ๐ต})) |
49 | | 2fveq3 6852 |
. . . . . 6
โข (๐ฅ = ๐ด โ (!โ(โฏโ๐ฅ)) =
(!โ(โฏโ๐ด))) |
50 | | fveq2 6847 |
. . . . . . 7
โข (๐ฅ = ๐ด โ (โฏโ๐ฅ) = (โฏโ๐ด)) |
51 | 50 | oveq2d 7378 |
. . . . . 6
โข (๐ฅ = ๐ด โ ((โฏโ๐ต)C(โฏโ๐ฅ)) = ((โฏโ๐ต)C(โฏโ๐ด))) |
52 | 49, 51 | oveq12d 7380 |
. . . . 5
โข (๐ฅ = ๐ด โ ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ))) = ((!โ(โฏโ๐ด)) ยท
((โฏโ๐ต)C(โฏโ๐ด)))) |
53 | 48, 52 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = ๐ด โ ((โฏโ{๐ โฃ ๐:๐ฅโ1-1โ๐ต}) = ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ))) โ (โฏโ{๐ โฃ ๐:๐ดโ1-1โ๐ต}) = ((!โ(โฏโ๐ด)) ยท
((โฏโ๐ต)C(โฏโ๐ด))))) |
54 | 53 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ด โ ((๐ต โ Fin โ (โฏโ{๐ โฃ ๐:๐ฅโ1-1โ๐ต}) = ((!โ(โฏโ๐ฅ)) ยท
((โฏโ๐ต)C(โฏโ๐ฅ)))) โ (๐ต โ Fin โ (โฏโ{๐ โฃ ๐:๐ดโ1-1โ๐ต}) = ((!โ(โฏโ๐ด)) ยท
((โฏโ๐ต)C(โฏโ๐ด)))))) |
55 | | hashcl 14263 |
. . . . . 6
โข (๐ต โ Fin โ
(โฏโ๐ต) โ
โ0) |
56 | | bcn0 14217 |
. . . . . 6
โข
((โฏโ๐ต)
โ โ0 โ ((โฏโ๐ต)C0) = 1) |
57 | 55, 56 | syl 17 |
. . . . 5
โข (๐ต โ Fin โ
((โฏโ๐ต)C0) =
1) |
58 | 57 | oveq2d 7378 |
. . . 4
โข (๐ต โ Fin โ (1 ยท
((โฏโ๐ต)C0)) = (1
ยท 1)) |
59 | | 1t1e1 12322 |
. . . 4
โข (1
ยท 1) = 1 |
60 | 58, 59 | eqtr2di 2794 |
. . 3
โข (๐ต โ Fin โ 1 = (1
ยท ((โฏโ๐ต)C0))) |
61 | | abn0 4345 |
. . . . . . . . . . . . 13
โข ({๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต} โ โ
โ โ๐ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต) |
62 | | f1domg 8919 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ Fin โ (๐:(๐ฆ โช {๐ง})โ1-1โ๐ต โ (๐ฆ โช {๐ง}) โผ ๐ต)) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (๐:(๐ฆ โช {๐ง})โ1-1โ๐ต โ (๐ฆ โช {๐ง}) โผ ๐ต)) |
64 | | hashunsng 14299 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง โ V โ ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1))) |
65 | 64 | elv 3454 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1)) |
66 | 65 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1)) |
67 | 66 | breq1d 5120 |
. . . . . . . . . . . . . . . 16
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ(๐ฆ โช {๐ง})) โค (โฏโ๐ต) โ ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต))) |
68 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ๐ฆ โ Fin) |
69 | | snfi 8995 |
. . . . . . . . . . . . . . . . . 18
โข {๐ง} โ Fin |
70 | | unfi 9123 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ Fin โง {๐ง} โ Fin) โ (๐ฆ โช {๐ง}) โ Fin) |
71 | 68, 69, 70 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (๐ฆ โช {๐ง}) โ Fin) |
72 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ๐ต โ Fin) |
73 | | hashdom 14286 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฆ โช {๐ง}) โ Fin โง ๐ต โ Fin) โ ((โฏโ(๐ฆ โช {๐ง})) โค (โฏโ๐ต) โ (๐ฆ โช {๐ง}) โผ ๐ต)) |
74 | 71, 72, 73 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ(๐ฆ โช {๐ง})) โค (โฏโ๐ต) โ (๐ฆ โช {๐ง}) โผ ๐ต)) |
75 | | hashcl 14263 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ โ Fin โ
(โฏโ๐ฆ) โ
โ0) |
76 | 75 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ๐ฆ) โ
โ0) |
77 | | nn0p1nn 12459 |
. . . . . . . . . . . . . . . . . . 19
โข
((โฏโ๐ฆ)
โ โ0 โ ((โฏโ๐ฆ) + 1) โ โ) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ๐ฆ) + 1) โ โ) |
79 | 78 | nnred 12175 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ๐ฆ) + 1) โ โ) |
80 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ๐ต) โ
โ0) |
81 | 80 | nn0red 12481 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ๐ต) โ โ) |
82 | 79, 81 | lenltd 11308 |
. . . . . . . . . . . . . . . 16
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (((โฏโ๐ฆ) + 1) โค (โฏโ๐ต) โ ยฌ (โฏโ๐ต) < ((โฏโ๐ฆ) + 1))) |
83 | 67, 74, 82 | 3bitr3d 309 |
. . . . . . . . . . . . . . 15
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((๐ฆ โช {๐ง}) โผ ๐ต โ ยฌ (โฏโ๐ต) < ((โฏโ๐ฆ) + 1))) |
84 | 63, 83 | sylibd 238 |
. . . . . . . . . . . . . 14
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (๐:(๐ฆ โช {๐ง})โ1-1โ๐ต โ ยฌ (โฏโ๐ต) < ((โฏโ๐ฆ) + 1))) |
85 | 84 | exlimdv 1937 |
. . . . . . . . . . . . 13
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โ๐ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต โ ยฌ (โฏโ๐ต) < ((โฏโ๐ฆ) + 1))) |
86 | 61, 85 | biimtrid 241 |
. . . . . . . . . . . 12
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ({๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต} โ โ
โ ยฌ
(โฏโ๐ต) <
((โฏโ๐ฆ) +
1))) |
87 | 86 | necon4ad 2963 |
. . . . . . . . . . 11
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ๐ต) < ((โฏโ๐ฆ) + 1) โ {๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต} = โ
)) |
88 | 87 | imp 408 |
. . . . . . . . . 10
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ {๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต} = โ
) |
89 | 88 | fveq2d 6851 |
. . . . . . . . 9
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) =
(โฏโโ
)) |
90 | | hashcl 14263 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โช {๐ง}) โ Fin โ (โฏโ(๐ฆ โช {๐ง})) โ
โ0) |
91 | 71, 90 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ(๐ฆ โช {๐ง})) โ
โ0) |
92 | 91 | faccld 14191 |
. . . . . . . . . . . 12
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (!โ(โฏโ(๐ฆ โช {๐ง}))) โ โ) |
93 | 92 | nncnd 12176 |
. . . . . . . . . . 11
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (!โ(โฏโ(๐ฆ โช {๐ง}))) โ โ) |
94 | 93 | adantr 482 |
. . . . . . . . . 10
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ (!โ(โฏโ(๐ฆ โช {๐ง}))) โ โ) |
95 | 94 | mul01d 11361 |
. . . . . . . . 9
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ
((!โ(โฏโ(๐ฆ
โช {๐ง}))) ยท 0) =
0) |
96 | 19, 89, 95 | 3eqtr4a 2803 |
. . . . . . . 8
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท 0)) |
97 | 66 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1)) |
98 | 97 | oveq2d 7378 |
. . . . . . . . . 10
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง}))) = ((โฏโ๐ต)C((โฏโ๐ฆ) + 1))) |
99 | 80 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ (โฏโ๐ต) โ
โ0) |
100 | 78 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ ((โฏโ๐ฆ) + 1) โ
โ) |
101 | 100 | nnzd 12533 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ ((โฏโ๐ฆ) + 1) โ
โค) |
102 | | animorr 978 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ (((โฏโ๐ฆ) + 1) < 0 โจ
(โฏโ๐ต) <
((โฏโ๐ฆ) +
1))) |
103 | | bcval4 14214 |
. . . . . . . . . . 11
โข
(((โฏโ๐ต)
โ โ0 โง ((โฏโ๐ฆ) + 1) โ โค โง
(((โฏโ๐ฆ) + 1)
< 0 โจ (โฏโ๐ต) < ((โฏโ๐ฆ) + 1))) โ ((โฏโ๐ต)C((โฏโ๐ฆ) + 1)) = 0) |
104 | 99, 101, 102, 103 | syl3anc 1372 |
. . . . . . . . . 10
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ ((โฏโ๐ต)C((โฏโ๐ฆ) + 1)) = 0) |
105 | 98, 104 | eqtrd 2777 |
. . . . . . . . 9
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง}))) = 0) |
106 | 105 | oveq2d 7378 |
. . . . . . . 8
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ
((!โ(โฏโ(๐ฆ
โช {๐ง}))) ยท
((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง})))) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท 0)) |
107 | 96, 106 | eqtr4d 2780 |
. . . . . . 7
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง}))))) |
108 | 107 | a1d 25 |
. . . . . 6
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง (โฏโ๐ต) < ((โฏโ๐ฆ) + 1)) โ ((โฏโ{๐ โฃ ๐:๐ฆโ1-1โ๐ต}) = ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ))) โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง})))))) |
109 | | oveq2 7370 |
. . . . . . 7
โข
((โฏโ{๐
โฃ ๐:๐ฆโ1-1โ๐ต}) = ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ))) โ (((โฏโ๐ต) โ (โฏโ๐ฆ)) ยท (โฏโ{๐ โฃ ๐:๐ฆโ1-1โ๐ต})) = (((โฏโ๐ต) โ (โฏโ๐ฆ)) ยท ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ))))) |
110 | 68 | adantr 482 |
. . . . . . . . 9
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ๐ฆ โ Fin) |
111 | 72 | adantr 482 |
. . . . . . . . 9
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ๐ต โ Fin) |
112 | | simplrr 777 |
. . . . . . . . 9
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ยฌ ๐ง โ ๐ฆ) |
113 | | simpr 486 |
. . . . . . . . 9
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) |
114 | 110, 111,
112, 113 | hashf1lem2 14362 |
. . . . . . . 8
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = (((โฏโ๐ต) โ (โฏโ๐ฆ)) ยท (โฏโ{๐ โฃ ๐:๐ฆโ1-1โ๐ต}))) |
115 | 80 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (โฏโ๐ต) โ
โ0) |
116 | 115 | faccld 14191 |
. . . . . . . . . . . . 13
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ(โฏโ๐ต)) โ
โ) |
117 | 116 | nncnd 12176 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ(โฏโ๐ต)) โ
โ) |
118 | 76 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (โฏโ๐ฆ) โ
โ0) |
119 | | peano2nn0 12460 |
. . . . . . . . . . . . . . . 16
โข
((โฏโ๐ฆ)
โ โ0 โ ((โฏโ๐ฆ) + 1) โ
โ0) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ฆ) + 1) โ
โ0) |
121 | | nn0sub2 12571 |
. . . . . . . . . . . . . . 15
โข
((((โฏโ๐ฆ)
+ 1) โ โ0 โง (โฏโ๐ต) โ โ0 โง
((โฏโ๐ฆ) + 1)
โค (โฏโ๐ต))
โ ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)) โ โ0) |
122 | 120, 115,
113, 121 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1)) โ
โ0) |
123 | 122 | faccld 14191 |
. . . . . . . . . . . . 13
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) โ
โ) |
124 | 123 | nncnd 12176 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) โ
โ) |
125 | 123 | nnne0d 12210 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) โ
0) |
126 | 117, 124,
125 | divcld 11938 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)))) โ โ) |
127 | 120 | faccld 14191 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ฆ) + 1)) โ
โ) |
128 | 127 | nncnd 12176 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ฆ) + 1)) โ
โ) |
129 | 127 | nnne0d 12210 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ฆ) + 1)) โ 0) |
130 | 126, 128,
129 | divcan2d 11940 |
. . . . . . . . . 10
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ((โฏโ๐ฆ) + 1)) ยท
(((!โ(โฏโ๐ต)) / (!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1)))) /
(!โ((โฏโ๐ฆ)
+ 1)))) = ((!โ(โฏโ๐ต)) / (!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))))) |
131 | 115 | nn0cnd 12482 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (โฏโ๐ต) โ โ) |
132 | 118 | nn0cnd 12482 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (โฏโ๐ฆ) โ โ) |
133 | 131, 132 | subcld 11519 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ต) โ (โฏโ๐ฆ)) โ โ) |
134 | | ax-1cn 11116 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
135 | | npcan 11417 |
. . . . . . . . . . . . . 14
โข
((((โฏโ๐ต)
โ (โฏโ๐ฆ))
โ โ โง 1 โ โ) โ ((((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 1) + 1) =
((โฏโ๐ต) โ
(โฏโ๐ฆ))) |
136 | 133, 134,
135 | sylancl 587 |
. . . . . . . . . . . . 13
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 1) + 1) =
((โฏโ๐ต) โ
(โฏโ๐ฆ))) |
137 | | 1cnd 11157 |
. . . . . . . . . . . . . . . 16
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ 1 โ โ) |
138 | 131, 132,
137 | subsub4d 11550 |
. . . . . . . . . . . . . . 15
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 1) = ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) |
139 | 138, 122 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 1) โ
โ0) |
140 | | nn0p1nn 12459 |
. . . . . . . . . . . . . 14
โข
((((โฏโ๐ต)
โ (โฏโ๐ฆ))
โ 1) โ โ0 โ ((((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 1) + 1) โ
โ) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 1) + 1) โ
โ) |
142 | 136, 141 | eqeltrrd 2839 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ต) โ (โฏโ๐ฆ)) โ โ) |
143 | 142 | nnne0d 12210 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 0) |
144 | 126, 133,
143 | divcan2d 11940 |
. . . . . . . . . 10
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (((โฏโ๐ต) โ (โฏโ๐ฆ)) ยท (((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)))) / ((โฏโ๐ต) โ (โฏโ๐ฆ)))) = ((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1))))) |
145 | 130, 144 | eqtr4d 2780 |
. . . . . . . . 9
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ((โฏโ๐ฆ) + 1)) ยท
(((!โ(โฏโ๐ต)) / (!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1)))) /
(!โ((โฏโ๐ฆ)
+ 1)))) = (((โฏโ๐ต) โ (โฏโ๐ฆ)) ยท (((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)))) / ((โฏโ๐ต) โ (โฏโ๐ฆ))))) |
146 | 66 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1)) |
147 | 146 | fveq2d 6851 |
. . . . . . . . . 10
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ(โฏโ(๐ฆ โช {๐ง}))) = (!โ((โฏโ๐ฆ) + 1))) |
148 | | nn0uz 12812 |
. . . . . . . . . . . . . . 15
โข
โ0 = (โคโฅโ0) |
149 | 120, 148 | eleqtrdi 2848 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ฆ) + 1) โ
(โคโฅโ0)) |
150 | 115 | nn0zd 12532 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (โฏโ๐ต) โ โค) |
151 | | elfz5 13440 |
. . . . . . . . . . . . . 14
โข
((((โฏโ๐ฆ)
+ 1) โ (โคโฅโ0) โง (โฏโ๐ต) โ โค) โ
(((โฏโ๐ฆ) + 1)
โ (0...(โฏโ๐ต)) โ ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต))) |
152 | 149, 150,
151 | syl2anc 585 |
. . . . . . . . . . . . 13
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (((โฏโ๐ฆ) + 1) โ
(0...(โฏโ๐ต))
โ ((โฏโ๐ฆ) +
1) โค (โฏโ๐ต))) |
153 | 113, 152 | mpbird 257 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ฆ) + 1) โ (0...(โฏโ๐ต))) |
154 | | bcval2 14212 |
. . . . . . . . . . . 12
โข
(((โฏโ๐ฆ)
+ 1) โ (0...(โฏโ๐ต)) โ ((โฏโ๐ต)C((โฏโ๐ฆ) + 1)) = ((!โ(โฏโ๐ต)) /
((!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) ยท
(!โ((โฏโ๐ฆ)
+ 1))))) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ต)C((โฏโ๐ฆ) + 1)) = ((!โ(โฏโ๐ต)) /
((!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) ยท
(!โ((โฏโ๐ฆ)
+ 1))))) |
156 | 146 | oveq2d 7378 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง}))) = ((โฏโ๐ต)C((โฏโ๐ฆ) + 1))) |
157 | 117, 124,
128, 125, 129 | divdiv1d 11969 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)))) / (!โ((โฏโ๐ฆ) + 1))) = ((!โ(โฏโ๐ต)) /
((!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) ยท
(!โ((โฏโ๐ฆ)
+ 1))))) |
158 | 155, 156,
157 | 3eqtr4d 2787 |
. . . . . . . . . 10
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง}))) = (((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)))) / (!โ((โฏโ๐ฆ) + 1)))) |
159 | 147, 158 | oveq12d 7380 |
. . . . . . . . 9
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง})))) = ((!โ((โฏโ๐ฆ) + 1)) ยท
(((!โ(โฏโ๐ต)) / (!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1)))) /
(!โ((โฏโ๐ฆ)
+ 1))))) |
160 | 118, 148 | eleqtrdi 2848 |
. . . . . . . . . . . . . . 15
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (โฏโ๐ฆ) โ
(โคโฅโ0)) |
161 | | peano2fzr 13461 |
. . . . . . . . . . . . . . 15
โข
(((โฏโ๐ฆ)
โ (โคโฅโ0) โง ((โฏโ๐ฆ) + 1) โ
(0...(โฏโ๐ต)))
โ (โฏโ๐ฆ)
โ (0...(โฏโ๐ต))) |
162 | 160, 153,
161 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (โฏโ๐ฆ) โ (0...(โฏโ๐ต))) |
163 | | bcval2 14212 |
. . . . . . . . . . . . . 14
โข
((โฏโ๐ฆ)
โ (0...(โฏโ๐ต)) โ ((โฏโ๐ต)C(โฏโ๐ฆ)) = ((!โ(โฏโ๐ต)) /
((!โ((โฏโ๐ต) โ (โฏโ๐ฆ))) ยท (!โ(โฏโ๐ฆ))))) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ต)C(โฏโ๐ฆ)) = ((!โ(โฏโ๐ต)) /
((!โ((โฏโ๐ต) โ (โฏโ๐ฆ))) ยท (!โ(โฏโ๐ฆ))))) |
165 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . 18
โข
((โฏโ๐ฆ)
โ (0...(โฏโ๐ต)) โ (โฏโ๐ฆ) โค (โฏโ๐ต)) |
166 | 162, 165 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (โฏโ๐ฆ) โค (โฏโ๐ต)) |
167 | | nn0sub2 12571 |
. . . . . . . . . . . . . . . . 17
โข
(((โฏโ๐ฆ)
โ โ0 โง (โฏโ๐ต) โ โ0 โง
(โฏโ๐ฆ) โค
(โฏโ๐ต)) โ
((โฏโ๐ต) โ
(โฏโ๐ฆ)) โ
โ0) |
168 | 118, 115,
166, 167 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ต) โ (โฏโ๐ฆ)) โ
โ0) |
169 | 168 | faccld 14191 |
. . . . . . . . . . . . . . 15
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ต) โ (โฏโ๐ฆ))) โ
โ) |
170 | 169 | nncnd 12176 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ต) โ (โฏโ๐ฆ))) โ
โ) |
171 | 118 | faccld 14191 |
. . . . . . . . . . . . . . 15
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ(โฏโ๐ฆ)) โ
โ) |
172 | 171 | nncnd 12176 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ(โฏโ๐ฆ)) โ
โ) |
173 | 169 | nnne0d 12210 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ต) โ (โฏโ๐ฆ))) โ 0) |
174 | 171 | nnne0d 12210 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ(โฏโ๐ฆ)) โ 0) |
175 | 117, 170,
172, 173, 174 | divdiv1d 11969 |
. . . . . . . . . . . . 13
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ (โฏโ๐ฆ)))) / (!โ(โฏโ๐ฆ))) =
((!โ(โฏโ๐ต)) / ((!โ((โฏโ๐ต) โ (โฏโ๐ฆ))) ยท
(!โ(โฏโ๐ฆ))))) |
176 | 164, 175 | eqtr4d 2780 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ๐ต)C(โฏโ๐ฆ)) = (((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ (โฏโ๐ฆ)))) / (!โ(โฏโ๐ฆ)))) |
177 | 176 | oveq2d 7378 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ))) = ((!โ(โฏโ๐ฆ)) ยท
(((!โ(โฏโ๐ต)) / (!โ((โฏโ๐ต) โ (โฏโ๐ฆ)))) /
(!โ(โฏโ๐ฆ))))) |
178 | | facnn2 14189 |
. . . . . . . . . . . . . . 15
โข
(((โฏโ๐ต)
โ (โฏโ๐ฆ))
โ โ โ (!โ((โฏโ๐ต) โ (โฏโ๐ฆ))) = ((!โ(((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 1)) ยท
((โฏโ๐ต) โ
(โฏโ๐ฆ)))) |
179 | 142, 178 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ต) โ (โฏโ๐ฆ))) =
((!โ(((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 1)) ยท ((โฏโ๐ต) โ (โฏโ๐ฆ)))) |
180 | 138 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ(((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 1)) =
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)))) |
181 | 180 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ(((โฏโ๐ต) โ (โฏโ๐ฆ)) โ 1)) ยท
((โฏโ๐ต) โ
(โฏโ๐ฆ))) =
((!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) ยท ((โฏโ๐ต) โ (โฏโ๐ฆ)))) |
182 | 179, 181 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (!โ((โฏโ๐ต) โ (โฏโ๐ฆ))) =
((!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) ยท ((โฏโ๐ต) โ (โฏโ๐ฆ)))) |
183 | 182 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ (โฏโ๐ฆ)))) = ((!โ(โฏโ๐ต)) /
((!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) ยท ((โฏโ๐ต) โ (โฏโ๐ฆ))))) |
184 | 117, 170,
173 | divcld 11938 |
. . . . . . . . . . . . 13
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ (โฏโ๐ฆ)))) โ โ) |
185 | 184, 172,
174 | divcan2d 11940 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ(โฏโ๐ฆ)) ยท
(((!โ(โฏโ๐ต)) / (!โ((โฏโ๐ต) โ (โฏโ๐ฆ)))) /
(!โ(โฏโ๐ฆ)))) = ((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ (โฏโ๐ฆ))))) |
186 | 117, 124,
133, 125, 143 | divdiv1d 11969 |
. . . . . . . . . . . 12
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)))) / ((โฏโ๐ต) โ (โฏโ๐ฆ))) = ((!โ(โฏโ๐ต)) /
((!โ((โฏโ๐ต) โ ((โฏโ๐ฆ) + 1))) ยท ((โฏโ๐ต) โ (โฏโ๐ฆ))))) |
187 | 183, 185,
186 | 3eqtr4d 2787 |
. . . . . . . . . . 11
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ(โฏโ๐ฆ)) ยท
(((!โ(โฏโ๐ต)) / (!โ((โฏโ๐ต) โ (โฏโ๐ฆ)))) /
(!โ(โฏโ๐ฆ)))) = (((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)))) / ((โฏโ๐ต) โ (โฏโ๐ฆ)))) |
188 | 177, 187 | eqtrd 2777 |
. . . . . . . . . 10
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ))) = (((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)))) / ((โฏโ๐ต) โ (โฏโ๐ฆ)))) |
189 | 188 | oveq2d 7378 |
. . . . . . . . 9
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ (((โฏโ๐ต) โ (โฏโ๐ฆ)) ยท ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ)))) = (((โฏโ๐ต) โ (โฏโ๐ฆ)) ยท (((!โ(โฏโ๐ต)) /
(!โ((โฏโ๐ต)
โ ((โฏโ๐ฆ)
+ 1)))) / ((โฏโ๐ต) โ (โฏโ๐ฆ))))) |
190 | 145, 159,
189 | 3eqtr4d 2787 |
. . . . . . . 8
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง})))) = (((โฏโ๐ต) โ (โฏโ๐ฆ)) ยท ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ))))) |
191 | 114, 190 | eqeq12d 2753 |
. . . . . . 7
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง})))) โ (((โฏโ๐ต) โ (โฏโ๐ฆ)) ยท
(โฏโ{๐ โฃ
๐:๐ฆโ1-1โ๐ต})) = (((โฏโ๐ต) โ (โฏโ๐ฆ)) ยท ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ)))))) |
192 | 109, 191 | syl5ibr 246 |
. . . . . 6
โข (((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โง ((โฏโ๐ฆ) + 1) โค (โฏโ๐ต)) โ ((โฏโ{๐ โฃ ๐:๐ฆโ1-1โ๐ต}) = ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ))) โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง})))))) |
193 | 108, 192,
81, 79 | ltlecasei 11270 |
. . . . 5
โข ((๐ต โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ{๐ โฃ ๐:๐ฆโ1-1โ๐ต}) = ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ))) โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง})))))) |
194 | 193 | expcom 415 |
. . . 4
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (๐ต โ Fin โ ((โฏโ{๐ โฃ ๐:๐ฆโ1-1โ๐ต}) = ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ))) โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง}))))))) |
195 | 194 | a2d 29 |
. . 3
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ ((๐ต โ Fin โ (โฏโ{๐ โฃ ๐:๐ฆโ1-1โ๐ต}) = ((!โ(โฏโ๐ฆ)) ยท
((โฏโ๐ต)C(โฏโ๐ฆ)))) โ (๐ต โ Fin โ (โฏโ{๐ โฃ ๐:(๐ฆ โช {๐ง})โ1-1โ๐ต}) = ((!โ(โฏโ(๐ฆ โช {๐ง}))) ยท ((โฏโ๐ต)C(โฏโ(๐ฆ โช {๐ง}))))))) |
196 | 27, 36, 45, 54, 60, 195 | findcard2s 9116 |
. 2
โข (๐ด โ Fin โ (๐ต โ Fin โ
(โฏโ{๐ โฃ
๐:๐ดโ1-1โ๐ต}) = ((!โ(โฏโ๐ด)) ยท
((โฏโ๐ต)C(โฏโ๐ด))))) |
197 | 196 | imp 408 |
1
โข ((๐ด โ Fin โง ๐ต โ Fin) โ
(โฏโ{๐ โฃ
๐:๐ดโ1-1โ๐ต}) = ((!โ(โฏโ๐ด)) ยท
((โฏโ๐ต)C(โฏโ๐ด)))) |