Step | Hyp | Ref
| Expression |
1 | | elfzuz2 13452 |
. . . . . . . . 9
โข (๐พ โ (1...๐) โ ๐ โ
(โคโฅโ1)) |
2 | | nnuz 12811 |
. . . . . . . . 9
โข โ =
(โคโฅโ1) |
3 | 1, 2 | eleqtrrdi 2845 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ ๐ โ โ) |
4 | 3 | nnnn0d 12478 |
. . . . . . 7
โข (๐พ โ (1...๐) โ ๐ โ
โ0) |
5 | 4 | faccld 14190 |
. . . . . 6
โข (๐พ โ (1...๐) โ (!โ๐) โ โ) |
6 | 5 | nncnd 12174 |
. . . . 5
โข (๐พ โ (1...๐) โ (!โ๐) โ โ) |
7 | | fznn0sub 13479 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (๐ โ ๐พ) โ
โ0) |
8 | | nn0p1nn 12457 |
. . . . . . 7
โข ((๐ โ ๐พ) โ โ0 โ ((๐ โ ๐พ) + 1) โ โ) |
9 | 7, 8 | syl 17 |
. . . . . 6
โข (๐พ โ (1...๐) โ ((๐ โ ๐พ) + 1) โ โ) |
10 | 9 | nncnd 12174 |
. . . . 5
โข (๐พ โ (1...๐) โ ((๐ โ ๐พ) + 1) โ โ) |
11 | 9 | nnnn0d 12478 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ ((๐ โ ๐พ) + 1) โ
โ0) |
12 | 11 | faccld 14190 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ((๐ โ ๐พ) + 1)) โ โ) |
13 | | elfznn 13476 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ ๐พ โ โ) |
14 | | nnm1nn0 12459 |
. . . . . . . 8
โข (๐พ โ โ โ (๐พ โ 1) โ
โ0) |
15 | | faccl 14189 |
. . . . . . . 8
โข ((๐พ โ 1) โ
โ0 โ (!โ(๐พ โ 1)) โ
โ) |
16 | 13, 14, 15 | 3syl 18 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ(๐พ โ 1)) โ
โ) |
17 | 12, 16 | nnmulcld 12211 |
. . . . . 6
โข (๐พ โ (1...๐) โ ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ
โ) |
18 | | nncn 12166 |
. . . . . . 7
โข
(((!โ((๐
โ ๐พ) + 1)) ยท
(!โ(๐พ โ 1)))
โ โ โ ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ
โ) |
19 | | nnne0 12192 |
. . . . . . 7
โข
(((!โ((๐
โ ๐พ) + 1)) ยท
(!โ(๐พ โ 1)))
โ โ โ ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ 0) |
20 | 18, 19 | jca 513 |
. . . . . 6
โข
(((!โ((๐
โ ๐พ) + 1)) ยท
(!โ(๐พ โ 1)))
โ โ โ (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ โ โง
((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ
0)) |
21 | 17, 20 | syl 17 |
. . . . 5
โข (๐พ โ (1...๐) โ (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ โ โง
((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ
0)) |
22 | 13 | nncnd 12174 |
. . . . . 6
โข (๐พ โ (1...๐) โ ๐พ โ โ) |
23 | 13 | nnne0d 12208 |
. . . . . 6
โข (๐พ โ (1...๐) โ ๐พ โ 0) |
24 | 22, 23 | jca 513 |
. . . . 5
โข (๐พ โ (1...๐) โ (๐พ โ โ โง ๐พ โ 0)) |
25 | | divmuldiv 11860 |
. . . . 5
โข
((((!โ๐)
โ โ โง ((๐
โ ๐พ) + 1) โ
โ) โง ((((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ โ โง
((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ 0) โง
(๐พ โ โ โง
๐พ โ 0))) โ
(((!โ๐) /
((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1)))) ยท (((๐ โ ๐พ) + 1) / ๐พ)) = (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) ยท ๐พ))) |
26 | 6, 10, 21, 24, 25 | syl22anc 838 |
. . . 4
โข (๐พ โ (1...๐) โ (((!โ๐) / ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1)))) ยท (((๐ โ ๐พ) + 1) / ๐พ)) = (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) ยท ๐พ))) |
27 | | elfzel2 13445 |
. . . . . . . . . 10
โข (๐พ โ (1...๐) โ ๐ โ โค) |
28 | 27 | zcnd 12613 |
. . . . . . . . 9
โข (๐พ โ (1...๐) โ ๐ โ โ) |
29 | | 1cnd 11155 |
. . . . . . . . 9
โข (๐พ โ (1...๐) โ 1 โ โ) |
30 | 28, 22, 29 | subsubd 11545 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ (๐ โ (๐พ โ 1)) = ((๐ โ ๐พ) + 1)) |
31 | 30 | fveq2d 6847 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ(๐ โ (๐พ โ 1))) = (!โ((๐ โ ๐พ) + 1))) |
32 | 31 | oveq1d 7373 |
. . . . . 6
โข (๐พ โ (1...๐) โ ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1))) =
((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1)))) |
33 | 32 | oveq2d 7374 |
. . . . 5
โข (๐พ โ (1...๐) โ ((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1)))) = ((!โ๐) / ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))))) |
34 | 30 | oveq1d 7373 |
. . . . 5
โข (๐พ โ (1...๐) โ ((๐ โ (๐พ โ 1)) / ๐พ) = (((๐ โ ๐พ) + 1) / ๐พ)) |
35 | 33, 34 | oveq12d 7376 |
. . . 4
โข (๐พ โ (1...๐) โ (((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1)))) ยท ((๐ โ (๐พ โ 1)) / ๐พ)) = (((!โ๐) / ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1)))) ยท (((๐ โ ๐พ) + 1) / ๐พ))) |
36 | | facp1 14184 |
. . . . . . . . 9
โข ((๐ โ ๐พ) โ โ0 โ
(!โ((๐ โ ๐พ) + 1)) = ((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1))) |
37 | 7, 36 | syl 17 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ (!โ((๐ โ ๐พ) + 1)) = ((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1))) |
38 | 37 | eqcomd 2739 |
. . . . . . 7
โข (๐พ โ (1...๐) โ ((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1)) = (!โ((๐ โ ๐พ) + 1))) |
39 | | facnn2 14188 |
. . . . . . . 8
โข (๐พ โ โ โ
(!โ๐พ) =
((!โ(๐พ โ 1))
ยท ๐พ)) |
40 | 13, 39 | syl 17 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ๐พ) = ((!โ(๐พ โ 1)) ยท ๐พ)) |
41 | 38, 40 | oveq12d 7376 |
. . . . . 6
โข (๐พ โ (1...๐) โ (((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1)) ยท (!โ๐พ)) = ((!โ((๐ โ ๐พ) + 1)) ยท ((!โ(๐พ โ 1)) ยท ๐พ))) |
42 | 7 | faccld 14190 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ (!โ(๐ โ ๐พ)) โ โ) |
43 | 42 | nncnd 12174 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ(๐ โ ๐พ)) โ โ) |
44 | 13 | nnnn0d 12478 |
. . . . . . . . 9
โข (๐พ โ (1...๐) โ ๐พ โ
โ0) |
45 | 44 | faccld 14190 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ (!โ๐พ) โ โ) |
46 | 45 | nncnd 12174 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ๐พ) โ โ) |
47 | 43, 46, 10 | mul32d 11370 |
. . . . . 6
โข (๐พ โ (1...๐) โ (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1)) = (((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1)) ยท (!โ๐พ))) |
48 | 12 | nncnd 12174 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ((๐ โ ๐พ) + 1)) โ โ) |
49 | 16 | nncnd 12174 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ(๐พ โ 1)) โ
โ) |
50 | 48, 49, 22 | mulassd 11183 |
. . . . . 6
โข (๐พ โ (1...๐) โ (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) ยท ๐พ) = ((!โ((๐ โ ๐พ) + 1)) ยท ((!โ(๐พ โ 1)) ยท ๐พ))) |
51 | 41, 47, 50 | 3eqtr4d 2783 |
. . . . 5
โข (๐พ โ (1...๐) โ (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1)) = (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) ยท ๐พ)) |
52 | 51 | oveq2d 7374 |
. . . 4
โข (๐พ โ (1...๐) โ (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1))) = (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) ยท ๐พ))) |
53 | 26, 35, 52 | 3eqtr4d 2783 |
. . 3
โข (๐พ โ (1...๐) โ (((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1)))) ยท ((๐ โ (๐พ โ 1)) / ๐พ)) = (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1)))) |
54 | 6, 10 | mulcomd 11181 |
. . . 4
โข (๐พ โ (1...๐) โ ((!โ๐) ยท ((๐ โ ๐พ) + 1)) = (((๐ โ ๐พ) + 1) ยท (!โ๐))) |
55 | 42, 45 | nnmulcld 12211 |
. . . . . 6
โข (๐พ โ (1...๐) โ ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) โ โ) |
56 | 55 | nncnd 12174 |
. . . . 5
โข (๐พ โ (1...๐) โ ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) โ โ) |
57 | 56, 10 | mulcomd 11181 |
. . . 4
โข (๐พ โ (1...๐) โ (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1)) = (((๐ โ ๐พ) + 1) ยท ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
58 | 54, 57 | oveq12d 7376 |
. . 3
โข (๐พ โ (1...๐) โ (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1))) = ((((๐ โ ๐พ) + 1) ยท (!โ๐)) / (((๐ โ ๐พ) + 1) ยท ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))))) |
59 | 55 | nnne0d 12208 |
. . . 4
โข (๐พ โ (1...๐) โ ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) โ 0) |
60 | 9 | nnne0d 12208 |
. . . 4
โข (๐พ โ (1...๐) โ ((๐ โ ๐พ) + 1) โ 0) |
61 | 6, 56, 10, 59, 60 | divcan5d 11962 |
. . 3
โข (๐พ โ (1...๐) โ ((((๐ โ ๐พ) + 1) ยท (!โ๐)) / (((๐ โ ๐พ) + 1) ยท ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) = ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
62 | 53, 58, 61 | 3eqtrrd 2778 |
. 2
โข (๐พ โ (1...๐) โ ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))) = (((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1)))) ยท ((๐ โ (๐พ โ 1)) / ๐พ))) |
63 | | fz1ssfz0 13543 |
. . . 4
โข
(1...๐) โ
(0...๐) |
64 | 63 | sseli 3941 |
. . 3
โข (๐พ โ (1...๐) โ ๐พ โ (0...๐)) |
65 | | bcval2 14211 |
. . 3
โข (๐พ โ (0...๐) โ (๐C๐พ) = ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
66 | 64, 65 | syl 17 |
. 2
โข (๐พ โ (1...๐) โ (๐C๐พ) = ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
67 | | ax-1cn 11114 |
. . . . . . . 8
โข 1 โ
โ |
68 | | npcan 11415 |
. . . . . . . 8
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ โ
1) + 1) = ๐) |
69 | 28, 67, 68 | sylancl 587 |
. . . . . . 7
โข (๐พ โ (1...๐) โ ((๐ โ 1) + 1) = ๐) |
70 | | peano2zm 12551 |
. . . . . . . 8
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
71 | | uzid 12783 |
. . . . . . . 8
โข ((๐ โ 1) โ โค
โ (๐ โ 1) โ
(โคโฅโ(๐ โ 1))) |
72 | | peano2uz 12831 |
. . . . . . . 8
โข ((๐ โ 1) โ
(โคโฅโ(๐ โ 1)) โ ((๐ โ 1) + 1) โ
(โคโฅโ(๐ โ 1))) |
73 | 27, 70, 71, 72 | 4syl 19 |
. . . . . . 7
โข (๐พ โ (1...๐) โ ((๐ โ 1) + 1) โ
(โคโฅโ(๐ โ 1))) |
74 | 69, 73 | eqeltrrd 2835 |
. . . . . 6
โข (๐พ โ (1...๐) โ ๐ โ (โคโฅโ(๐ โ 1))) |
75 | | fzss2 13487 |
. . . . . 6
โข (๐ โ
(โคโฅโ(๐ โ 1)) โ (0...(๐ โ 1)) โ (0...๐)) |
76 | 74, 75 | syl 17 |
. . . . 5
โข (๐พ โ (1...๐) โ (0...(๐ โ 1)) โ (0...๐)) |
77 | | elfzmlbm 13557 |
. . . . 5
โข (๐พ โ (1...๐) โ (๐พ โ 1) โ (0...(๐ โ 1))) |
78 | 76, 77 | sseldd 3946 |
. . . 4
โข (๐พ โ (1...๐) โ (๐พ โ 1) โ (0...๐)) |
79 | | bcval2 14211 |
. . . 4
โข ((๐พ โ 1) โ (0...๐) โ (๐C(๐พ โ 1)) = ((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1))))) |
80 | 78, 79 | syl 17 |
. . 3
โข (๐พ โ (1...๐) โ (๐C(๐พ โ 1)) = ((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1))))) |
81 | 80 | oveq1d 7373 |
. 2
โข (๐พ โ (1...๐) โ ((๐C(๐พ โ 1)) ยท ((๐ โ (๐พ โ 1)) / ๐พ)) = (((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1)))) ยท ((๐ โ (๐พ โ 1)) / ๐พ))) |
82 | 62, 66, 81 | 3eqtr4d 2783 |
1
โข (๐พ โ (1...๐) โ (๐C๐พ) = ((๐C(๐พ โ 1)) ยท ((๐ โ (๐พ โ 1)) / ๐พ))) |