Step | Hyp | Ref
| Expression |
1 | | elfzuz2 10028 |
. . . . . . . . 9
โข (๐พ โ (1...๐) โ ๐ โ
(โคโฅโ1)) |
2 | | nnuz 9562 |
. . . . . . . . 9
โข โ =
(โคโฅโ1) |
3 | 1, 2 | eleqtrrdi 2271 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ ๐ โ โ) |
4 | 3 | nnnn0d 9228 |
. . . . . . 7
โข (๐พ โ (1...๐) โ ๐ โ
โ0) |
5 | 4 | faccld 10715 |
. . . . . 6
โข (๐พ โ (1...๐) โ (!โ๐) โ โ) |
6 | 5 | nncnd 8932 |
. . . . 5
โข (๐พ โ (1...๐) โ (!โ๐) โ โ) |
7 | | fznn0sub 10056 |
. . . . . . . . . 10
โข (๐พ โ (1...๐) โ (๐ โ ๐พ) โ
โ0) |
8 | | nn0p1nn 9214 |
. . . . . . . . . 10
โข ((๐ โ ๐พ) โ โ0 โ ((๐ โ ๐พ) + 1) โ โ) |
9 | 7, 8 | syl 14 |
. . . . . . . . 9
โข (๐พ โ (1...๐) โ ((๐ โ ๐พ) + 1) โ โ) |
10 | 9 | nnnn0d 9228 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ ((๐ โ ๐พ) + 1) โ
โ0) |
11 | 10 | faccld 10715 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ((๐ โ ๐พ) + 1)) โ โ) |
12 | | elfznn 10053 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ ๐พ โ โ) |
13 | | nnm1nn0 9216 |
. . . . . . . 8
โข (๐พ โ โ โ (๐พ โ 1) โ
โ0) |
14 | | faccl 10714 |
. . . . . . . 8
โข ((๐พ โ 1) โ
โ0 โ (!โ(๐พ โ 1)) โ
โ) |
15 | 12, 13, 14 | 3syl 17 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ(๐พ โ 1)) โ
โ) |
16 | 11, 15 | nnmulcld 8967 |
. . . . . 6
โข (๐พ โ (1...๐) โ ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ
โ) |
17 | 16 | nncnd 8932 |
. . . . 5
โข (๐พ โ (1...๐) โ ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) โ
โ) |
18 | 9 | nncnd 8932 |
. . . . 5
โข (๐พ โ (1...๐) โ ((๐ โ ๐พ) + 1) โ โ) |
19 | 12 | nncnd 8932 |
. . . . 5
โข (๐พ โ (1...๐) โ ๐พ โ โ) |
20 | 16 | nnap0d 8964 |
. . . . 5
โข (๐พ โ (1...๐) โ ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) # 0) |
21 | 12 | nnap0d 8964 |
. . . . 5
โข (๐พ โ (1...๐) โ ๐พ # 0) |
22 | 6, 17, 18, 19, 20, 21 | divmuldivapd 8788 |
. . . 4
โข (๐พ โ (1...๐) โ (((!โ๐) / ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1)))) ยท (((๐ โ ๐พ) + 1) / ๐พ)) = (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) ยท ๐พ))) |
23 | | elfzel2 10022 |
. . . . . . . . . 10
โข (๐พ โ (1...๐) โ ๐ โ โค) |
24 | 23 | zcnd 9375 |
. . . . . . . . 9
โข (๐พ โ (1...๐) โ ๐ โ โ) |
25 | | 1cnd 7972 |
. . . . . . . . 9
โข (๐พ โ (1...๐) โ 1 โ โ) |
26 | 24, 19, 25 | subsubd 8295 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ (๐ โ (๐พ โ 1)) = ((๐ โ ๐พ) + 1)) |
27 | 26 | fveq2d 5519 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ(๐ โ (๐พ โ 1))) = (!โ((๐ โ ๐พ) + 1))) |
28 | 27 | oveq1d 5889 |
. . . . . 6
โข (๐พ โ (1...๐) โ ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1))) =
((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1)))) |
29 | 28 | oveq2d 5890 |
. . . . 5
โข (๐พ โ (1...๐) โ ((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1)))) = ((!โ๐) / ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))))) |
30 | 26 | oveq1d 5889 |
. . . . 5
โข (๐พ โ (1...๐) โ ((๐ โ (๐พ โ 1)) / ๐พ) = (((๐ โ ๐พ) + 1) / ๐พ)) |
31 | 29, 30 | oveq12d 5892 |
. . . 4
โข (๐พ โ (1...๐) โ (((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1)))) ยท ((๐ โ (๐พ โ 1)) / ๐พ)) = (((!โ๐) / ((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1)))) ยท (((๐ โ ๐พ) + 1) / ๐พ))) |
32 | | facp1 10709 |
. . . . . . . . 9
โข ((๐ โ ๐พ) โ โ0 โ
(!โ((๐ โ ๐พ) + 1)) = ((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1))) |
33 | 7, 32 | syl 14 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ (!โ((๐ โ ๐พ) + 1)) = ((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1))) |
34 | 33 | eqcomd 2183 |
. . . . . . 7
โข (๐พ โ (1...๐) โ ((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1)) = (!โ((๐ โ ๐พ) + 1))) |
35 | | facnn2 10713 |
. . . . . . . 8
โข (๐พ โ โ โ
(!โ๐พ) =
((!โ(๐พ โ 1))
ยท ๐พ)) |
36 | 12, 35 | syl 14 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ๐พ) = ((!โ(๐พ โ 1)) ยท ๐พ)) |
37 | 34, 36 | oveq12d 5892 |
. . . . . 6
โข (๐พ โ (1...๐) โ (((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1)) ยท (!โ๐พ)) = ((!โ((๐ โ ๐พ) + 1)) ยท ((!โ(๐พ โ 1)) ยท ๐พ))) |
38 | 7 | faccld 10715 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ (!โ(๐ โ ๐พ)) โ โ) |
39 | 38 | nncnd 8932 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ(๐ โ ๐พ)) โ โ) |
40 | 12 | nnnn0d 9228 |
. . . . . . . . 9
โข (๐พ โ (1...๐) โ ๐พ โ
โ0) |
41 | 40 | faccld 10715 |
. . . . . . . 8
โข (๐พ โ (1...๐) โ (!โ๐พ) โ โ) |
42 | 41 | nncnd 8932 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ๐พ) โ โ) |
43 | 39, 42, 18 | mul32d 8109 |
. . . . . 6
โข (๐พ โ (1...๐) โ (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1)) = (((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1)) ยท (!โ๐พ))) |
44 | 11 | nncnd 8932 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ((๐ โ ๐พ) + 1)) โ โ) |
45 | 15 | nncnd 8932 |
. . . . . . 7
โข (๐พ โ (1...๐) โ (!โ(๐พ โ 1)) โ
โ) |
46 | 44, 45, 19 | mulassd 7980 |
. . . . . 6
โข (๐พ โ (1...๐) โ (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) ยท ๐พ) = ((!โ((๐ โ ๐พ) + 1)) ยท ((!โ(๐พ โ 1)) ยท ๐พ))) |
47 | 37, 43, 46 | 3eqtr4d 2220 |
. . . . 5
โข (๐พ โ (1...๐) โ (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1)) = (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) ยท ๐พ)) |
48 | 47 | oveq2d 5890 |
. . . 4
โข (๐พ โ (1...๐) โ (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1))) = (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ((๐ โ ๐พ) + 1)) ยท (!โ(๐พ โ 1))) ยท ๐พ))) |
49 | 22, 31, 48 | 3eqtr4d 2220 |
. . 3
โข (๐พ โ (1...๐) โ (((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1)))) ยท ((๐ โ (๐พ โ 1)) / ๐พ)) = (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1)))) |
50 | 6, 18 | mulcomd 7978 |
. . . 4
โข (๐พ โ (1...๐) โ ((!โ๐) ยท ((๐ โ ๐พ) + 1)) = (((๐ โ ๐พ) + 1) ยท (!โ๐))) |
51 | 38, 41 | nnmulcld 8967 |
. . . . . 6
โข (๐พ โ (1...๐) โ ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) โ โ) |
52 | 51 | nncnd 8932 |
. . . . 5
โข (๐พ โ (1...๐) โ ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) โ โ) |
53 | 52, 18 | mulcomd 7978 |
. . . 4
โข (๐พ โ (1...๐) โ (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1)) = (((๐ โ ๐พ) + 1) ยท ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
54 | 50, 53 | oveq12d 5892 |
. . 3
โข (๐พ โ (1...๐) โ (((!โ๐) ยท ((๐ โ ๐พ) + 1)) / (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ โ ๐พ) + 1))) = ((((๐ โ ๐พ) + 1) ยท (!โ๐)) / (((๐ โ ๐พ) + 1) ยท ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))))) |
55 | 51 | nnap0d 8964 |
. . . 4
โข (๐พ โ (1...๐) โ ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) # 0) |
56 | 9 | nnap0d 8964 |
. . . 4
โข (๐พ โ (1...๐) โ ((๐ โ ๐พ) + 1) # 0) |
57 | 6, 52, 18, 55, 56 | divcanap5d 8773 |
. . 3
โข (๐พ โ (1...๐) โ ((((๐ โ ๐พ) + 1) ยท (!โ๐)) / (((๐ โ ๐พ) + 1) ยท ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) = ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
58 | 49, 54, 57 | 3eqtrrd 2215 |
. 2
โข (๐พ โ (1...๐) โ ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))) = (((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1)))) ยท ((๐ โ (๐พ โ 1)) / ๐พ))) |
59 | | 0p1e1 9032 |
. . . . . 6
โข (0 + 1) =
1 |
60 | 59 | oveq1i 5884 |
. . . . 5
โข ((0 +
1)...๐) = (1...๐) |
61 | | 0z 9263 |
. . . . . 6
โข 0 โ
โค |
62 | | fzp1ss 10072 |
. . . . . 6
โข (0 โ
โค โ ((0 + 1)...๐) โ (0...๐)) |
63 | 61, 62 | ax-mp 5 |
. . . . 5
โข ((0 +
1)...๐) โ (0...๐) |
64 | 60, 63 | eqsstrri 3188 |
. . . 4
โข
(1...๐) โ
(0...๐) |
65 | 64 | sseli 3151 |
. . 3
โข (๐พ โ (1...๐) โ ๐พ โ (0...๐)) |
66 | | bcval2 10729 |
. . 3
โข (๐พ โ (0...๐) โ (๐C๐พ) = ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
67 | 65, 66 | syl 14 |
. 2
โข (๐พ โ (1...๐) โ (๐C๐พ) = ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
68 | | ax-1cn 7903 |
. . . . . . . 8
โข 1 โ
โ |
69 | | npcan 8165 |
. . . . . . . 8
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ โ
1) + 1) = ๐) |
70 | 24, 68, 69 | sylancl 413 |
. . . . . . 7
โข (๐พ โ (1...๐) โ ((๐ โ 1) + 1) = ๐) |
71 | | peano2zm 9290 |
. . . . . . . 8
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
72 | | uzid 9541 |
. . . . . . . 8
โข ((๐ โ 1) โ โค
โ (๐ โ 1) โ
(โคโฅโ(๐ โ 1))) |
73 | | peano2uz 9582 |
. . . . . . . 8
โข ((๐ โ 1) โ
(โคโฅโ(๐ โ 1)) โ ((๐ โ 1) + 1) โ
(โคโฅโ(๐ โ 1))) |
74 | 23, 71, 72, 73 | 4syl 18 |
. . . . . . 7
โข (๐พ โ (1...๐) โ ((๐ โ 1) + 1) โ
(โคโฅโ(๐ โ 1))) |
75 | 70, 74 | eqeltrrd 2255 |
. . . . . 6
โข (๐พ โ (1...๐) โ ๐ โ (โคโฅโ(๐ โ 1))) |
76 | | fzss2 10063 |
. . . . . 6
โข (๐ โ
(โคโฅโ(๐ โ 1)) โ (0...(๐ โ 1)) โ (0...๐)) |
77 | 75, 76 | syl 14 |
. . . . 5
โข (๐พ โ (1...๐) โ (0...(๐ โ 1)) โ (0...๐)) |
78 | | elfzmlbm 10130 |
. . . . 5
โข (๐พ โ (1...๐) โ (๐พ โ 1) โ (0...(๐ โ 1))) |
79 | 77, 78 | sseldd 3156 |
. . . 4
โข (๐พ โ (1...๐) โ (๐พ โ 1) โ (0...๐)) |
80 | | bcval2 10729 |
. . . 4
โข ((๐พ โ 1) โ (0...๐) โ (๐C(๐พ โ 1)) = ((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1))))) |
81 | 79, 80 | syl 14 |
. . 3
โข (๐พ โ (1...๐) โ (๐C(๐พ โ 1)) = ((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1))))) |
82 | 81 | oveq1d 5889 |
. 2
โข (๐พ โ (1...๐) โ ((๐C(๐พ โ 1)) ยท ((๐ โ (๐พ โ 1)) / ๐พ)) = (((!โ๐) / ((!โ(๐ โ (๐พ โ 1))) ยท (!โ(๐พ โ 1)))) ยท ((๐ โ (๐พ โ 1)) / ๐พ))) |
83 | 58, 67, 82 | 3eqtr4d 2220 |
1
โข (๐พ โ (1...๐) โ (๐C๐พ) = ((๐C(๐พ โ 1)) ยท ((๐ โ (๐พ โ 1)) / ๐พ))) |