Step | Hyp | Ref
| Expression |
1 | | nn0cn 12428 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
2 | | ax-1cn 11114 |
. . . . . . . . 9
โข 1 โ
โ |
3 | | addass 11143 |
. . . . . . . . 9
โข ((๐ โ โ โง 1 โ
โ โง 1 โ โ) โ ((๐ + 1) + 1) = (๐ + (1 + 1))) |
4 | 2, 2, 3 | mp3an23 1454 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ + 1) + 1) = (๐ + (1 + 1))) |
5 | 1, 4 | syl 17 |
. . . . . . 7
โข (๐ โ โ0
โ ((๐ + 1) + 1) =
(๐ + (1 +
1))) |
6 | | df-2 12221 |
. . . . . . . . . 10
โข 2 = (1 +
1) |
7 | 6 | oveq2i 7369 |
. . . . . . . . 9
โข (๐ + 2) = (๐ + (1 + 1)) |
8 | 7 | eqcomi 2742 |
. . . . . . . 8
โข (๐ + (1 + 1)) = (๐ + 2) |
9 | 8 | a1i 11 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ + (1 + 1)) =
(๐ + 2)) |
10 | 5, 9 | eqtrd 2773 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ + 1) + 1) =
(๐ + 2)) |
11 | 10 | fveq2d 6847 |
. . . . 5
โข (๐ โ โ0
โ (!โ((๐ + 1) +
1)) = (!โ(๐ +
2))) |
12 | | peano2nn0 12458 |
. . . . . 6
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
13 | | facp1 14184 |
. . . . . 6
โข ((๐ + 1) โ โ0
โ (!โ((๐ + 1) +
1)) = ((!โ(๐ + 1))
ยท ((๐ + 1) +
1))) |
14 | 12, 13 | syl 17 |
. . . . 5
โข (๐ โ โ0
โ (!โ((๐ + 1) +
1)) = ((!โ(๐ + 1))
ยท ((๐ + 1) +
1))) |
15 | 11, 14 | eqtr3d 2775 |
. . . 4
โข (๐ โ โ0
โ (!โ(๐ + 2)) =
((!โ(๐ + 1)) ยท
((๐ + 1) +
1))) |
16 | 10 | oveq2d 7374 |
. . . 4
โข (๐ โ โ0
โ ((!โ(๐ + 1))
ยท ((๐ + 1) + 1)) =
((!โ(๐ + 1)) ยท
(๐ + 2))) |
17 | 15, 16 | eqtrd 2773 |
. . 3
โข (๐ โ โ0
โ (!โ(๐ + 2)) =
((!โ(๐ + 1)) ยท
(๐ + 2))) |
18 | | facp1 14184 |
. . . 4
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
19 | 18 | oveq1d 7373 |
. . 3
โข (๐ โ โ0
โ ((!โ(๐ + 1))
ยท (๐ + 2)) =
(((!โ๐) ยท
(๐ + 1)) ยท (๐ + 2))) |
20 | 17, 19 | eqtrd 2773 |
. 2
โข (๐ โ โ0
โ (!โ(๐ + 2)) =
(((!โ๐) ยท
(๐ + 1)) ยท (๐ + 2))) |
21 | | faccl 14189 |
. . . 4
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
22 | | nncn 12166 |
. . . 4
โข
((!โ๐) โ
โ โ (!โ๐)
โ โ) |
23 | 21, 22 | syl 17 |
. . 3
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
24 | | nn0cn 12428 |
. . . 4
โข ((๐ + 1) โ โ0
โ (๐ + 1) โ
โ) |
25 | 12, 24 | syl 17 |
. . 3
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
26 | | 2cn 12233 |
. . . . 5
โข 2 โ
โ |
27 | | addcl 11138 |
. . . . 5
โข ((๐ โ โ โง 2 โ
โ) โ (๐ + 2)
โ โ) |
28 | 26, 27 | mpan2 690 |
. . . 4
โข (๐ โ โ โ (๐ + 2) โ
โ) |
29 | 1, 28 | syl 17 |
. . 3
โข (๐ โ โ0
โ (๐ + 2) โ
โ) |
30 | | mulass 11144 |
. . 3
โข
(((!โ๐) โ
โ โง (๐ + 1)
โ โ โง (๐ +
2) โ โ) โ (((!โ๐) ยท (๐ + 1)) ยท (๐ + 2)) = ((!โ๐) ยท ((๐ + 1) ยท (๐ + 2)))) |
31 | 23, 25, 29, 30 | syl3anc 1372 |
. 2
โข (๐ โ โ0
โ (((!โ๐)
ยท (๐ + 1)) ยท
(๐ + 2)) = ((!โ๐) ยท ((๐ + 1) ยท (๐ + 2)))) |
32 | 20, 31 | eqtrd 2773 |
1
โข (๐ โ โ0
โ (!โ(๐ + 2)) =
((!โ๐) ยท
((๐ + 1) ยท (๐ + 2)))) |