Step | Hyp | Ref
| Expression |
1 | | 2cn 12233 |
. . . . . . . . 9
โข 2 โ
โ |
2 | | nn0cn 12428 |
. . . . . . . . 9
โข (๐ฅ โ โ0
โ ๐ฅ โ
โ) |
3 | | mulcl 11140 |
. . . . . . . . 9
โข ((2
โ โ โง ๐ฅ
โ โ) โ (2 ยท ๐ฅ) โ โ) |
4 | 1, 2, 3 | sylancr 588 |
. . . . . . . 8
โข (๐ฅ โ โ0
โ (2 ยท ๐ฅ)
โ โ) |
5 | | ax-1cn 11114 |
. . . . . . . . 9
โข 1 โ
โ |
6 | | addass 11143 |
. . . . . . . . 9
โข (((2
ยท ๐ฅ) โ โ
โง 2 โ โ โง 1 โ โ) โ (((2 ยท ๐ฅ) + 2) + 1) = ((2 ยท ๐ฅ) + (2 + 1))) |
7 | 1, 5, 6 | mp3an23 1454 |
. . . . . . . 8
โข ((2
ยท ๐ฅ) โ โ
โ (((2 ยท ๐ฅ) +
2) + 1) = ((2 ยท ๐ฅ) +
(2 + 1))) |
8 | 4, 7 | syl 17 |
. . . . . . 7
โข (๐ฅ โ โ0
โ (((2 ยท ๐ฅ) +
2) + 1) = ((2 ยท ๐ฅ) +
(2 + 1))) |
9 | | df-3 12222 |
. . . . . . . . 9
โข 3 = (2 +
1) |
10 | 9 | a1i 11 |
. . . . . . . 8
โข (๐ฅ โ โ0
โ 3 = (2 + 1)) |
11 | 10 | oveq2d 7374 |
. . . . . . 7
โข (๐ฅ โ โ0
โ ((2 ยท ๐ฅ) + 3)
= ((2 ยท ๐ฅ) + (2 +
1))) |
12 | 8, 11 | eqtr4d 2776 |
. . . . . 6
โข (๐ฅ โ โ0
โ (((2 ยท ๐ฅ) +
2) + 1) = ((2 ยท ๐ฅ) +
3)) |
13 | 12 | fveq2d 6847 |
. . . . 5
โข (๐ฅ โ โ0
โ (!โ(((2 ยท ๐ฅ) + 2) + 1)) = (!โ((2 ยท ๐ฅ) + 3))) |
14 | | 2nn0 12435 |
. . . . . . . 8
โข 2 โ
โ0 |
15 | | nn0mulcl 12454 |
. . . . . . . 8
โข ((2
โ โ0 โง ๐ฅ โ โ0) โ (2
ยท ๐ฅ) โ
โ0) |
16 | 14, 15 | mpan 689 |
. . . . . . 7
โข (๐ฅ โ โ0
โ (2 ยท ๐ฅ)
โ โ0) |
17 | | nn0addcl 12453 |
. . . . . . . 8
โข (((2
ยท ๐ฅ) โ
โ0 โง 2 โ โ0) โ ((2 ยท
๐ฅ) + 2) โ
โ0) |
18 | 14, 17 | mpan2 690 |
. . . . . . 7
โข ((2
ยท ๐ฅ) โ
โ0 โ ((2 ยท ๐ฅ) + 2) โ
โ0) |
19 | 16, 18 | syl 17 |
. . . . . 6
โข (๐ฅ โ โ0
โ ((2 ยท ๐ฅ) + 2)
โ โ0) |
20 | | facp1 14184 |
. . . . . 6
โข (((2
ยท ๐ฅ) + 2) โ
โ0 โ (!โ(((2 ยท ๐ฅ) + 2) + 1)) = ((!โ((2 ยท ๐ฅ) + 2)) ยท (((2 ยท
๐ฅ) + 2) +
1))) |
21 | 19, 20 | syl 17 |
. . . . 5
โข (๐ฅ โ โ0
โ (!โ(((2 ยท ๐ฅ) + 2) + 1)) = ((!โ((2 ยท ๐ฅ) + 2)) ยท (((2 ยท
๐ฅ) + 2) +
1))) |
22 | 13, 21 | eqtr3d 2775 |
. . . 4
โข (๐ฅ โ โ0
โ (!โ((2 ยท ๐ฅ) + 3)) = ((!โ((2 ยท ๐ฅ) + 2)) ยท (((2 ยท
๐ฅ) + 2) +
1))) |
23 | 12 | oveq2d 7374 |
. . . 4
โข (๐ฅ โ โ0
โ ((!โ((2 ยท ๐ฅ) + 2)) ยท (((2 ยท ๐ฅ) + 2) + 1)) = ((!โ((2
ยท ๐ฅ) + 2)) ยท
((2 ยท ๐ฅ) +
3))) |
24 | 22, 23 | eqtrd 2773 |
. . 3
โข (๐ฅ โ โ0
โ (!โ((2 ยท ๐ฅ) + 3)) = ((!โ((2 ยท ๐ฅ) + 2)) ยท ((2 ยท
๐ฅ) + 3))) |
25 | | addass 11143 |
. . . . . . . . . . 11
โข (((2
ยท ๐ฅ) โ โ
โง 1 โ โ โง 1 โ โ) โ (((2 ยท ๐ฅ) + 1) + 1) = ((2 ยท ๐ฅ) + (1 + 1))) |
26 | 5, 5, 25 | mp3an23 1454 |
. . . . . . . . . 10
โข ((2
ยท ๐ฅ) โ โ
โ (((2 ยท ๐ฅ) +
1) + 1) = ((2 ยท ๐ฅ) +
(1 + 1))) |
27 | 4, 26 | syl 17 |
. . . . . . . . 9
โข (๐ฅ โ โ0
โ (((2 ยท ๐ฅ) +
1) + 1) = ((2 ยท ๐ฅ) +
(1 + 1))) |
28 | | df-2 12221 |
. . . . . . . . . . 11
โข 2 = (1 +
1) |
29 | 28 | a1i 11 |
. . . . . . . . . 10
โข (๐ฅ โ โ0
โ 2 = (1 + 1)) |
30 | 29 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ฅ โ โ0
โ ((2 ยท ๐ฅ) + 2)
= ((2 ยท ๐ฅ) + (1 +
1))) |
31 | 27, 30 | eqtr4d 2776 |
. . . . . . . 8
โข (๐ฅ โ โ0
โ (((2 ยท ๐ฅ) +
1) + 1) = ((2 ยท ๐ฅ) +
2)) |
32 | 31 | fveq2d 6847 |
. . . . . . 7
โข (๐ฅ โ โ0
โ (!โ(((2 ยท ๐ฅ) + 1) + 1)) = (!โ((2 ยท ๐ฅ) + 2))) |
33 | | peano2nn0 12458 |
. . . . . . . . 9
โข ((2
ยท ๐ฅ) โ
โ0 โ ((2 ยท ๐ฅ) + 1) โ
โ0) |
34 | 16, 33 | syl 17 |
. . . . . . . 8
โข (๐ฅ โ โ0
โ ((2 ยท ๐ฅ) + 1)
โ โ0) |
35 | | facp1 14184 |
. . . . . . . 8
โข (((2
ยท ๐ฅ) + 1) โ
โ0 โ (!โ(((2 ยท ๐ฅ) + 1) + 1)) = ((!โ((2 ยท ๐ฅ) + 1)) ยท (((2 ยท
๐ฅ) + 1) +
1))) |
36 | 34, 35 | syl 17 |
. . . . . . 7
โข (๐ฅ โ โ0
โ (!โ(((2 ยท ๐ฅ) + 1) + 1)) = ((!โ((2 ยท ๐ฅ) + 1)) ยท (((2 ยท
๐ฅ) + 1) +
1))) |
37 | 32, 36 | eqtr3d 2775 |
. . . . . 6
โข (๐ฅ โ โ0
โ (!โ((2 ยท ๐ฅ) + 2)) = ((!โ((2 ยท ๐ฅ) + 1)) ยท (((2 ยท
๐ฅ) + 1) +
1))) |
38 | 31 | oveq2d 7374 |
. . . . . 6
โข (๐ฅ โ โ0
โ ((!โ((2 ยท ๐ฅ) + 1)) ยท (((2 ยท ๐ฅ) + 1) + 1)) = ((!โ((2
ยท ๐ฅ) + 1)) ยท
((2 ยท ๐ฅ) +
2))) |
39 | 37, 38 | eqtrd 2773 |
. . . . 5
โข (๐ฅ โ โ0
โ (!โ((2 ยท ๐ฅ) + 2)) = ((!โ((2 ยท ๐ฅ) + 1)) ยท ((2 ยท
๐ฅ) + 2))) |
40 | 39 | oveq1d 7373 |
. . . 4
โข (๐ฅ โ โ0
โ ((!โ((2 ยท ๐ฅ) + 2)) ยท ((2 ยท ๐ฅ) + 3)) = (((!โ((2
ยท ๐ฅ) + 1)) ยท
((2 ยท ๐ฅ) + 2))
ยท ((2 ยท ๐ฅ) +
3))) |
41 | 40 | eqeq2d 2744 |
. . 3
โข (๐ฅ โ โ0
โ ((!โ((2 ยท ๐ฅ) + 3)) = ((!โ((2 ยท ๐ฅ) + 2)) ยท ((2 ยท
๐ฅ) + 3)) โ
(!โ((2 ยท ๐ฅ) +
3)) = (((!โ((2 ยท ๐ฅ) + 1)) ยท ((2 ยท ๐ฅ) + 2)) ยท ((2 ยท
๐ฅ) + 3)))) |
42 | 24, 41 | mpbid 231 |
. 2
โข (๐ฅ โ โ0
โ (!โ((2 ยท ๐ฅ) + 3)) = (((!โ((2 ยท ๐ฅ) + 1)) ยท ((2 ยท
๐ฅ) + 2)) ยท ((2
ยท ๐ฅ) +
3))) |
43 | | faccl 14189 |
. . . . 5
โข (((2
ยท ๐ฅ) + 1) โ
โ0 โ (!โ((2 ยท ๐ฅ) + 1)) โ โ) |
44 | 34, 43 | syl 17 |
. . . 4
โข (๐ฅ โ โ0
โ (!โ((2 ยท ๐ฅ) + 1)) โ โ) |
45 | | nncn 12166 |
. . . 4
โข
((!โ((2 ยท ๐ฅ) + 1)) โ โ โ (!โ((2
ยท ๐ฅ) + 1)) โ
โ) |
46 | 44, 45 | syl 17 |
. . 3
โข (๐ฅ โ โ0
โ (!โ((2 ยท ๐ฅ) + 1)) โ โ) |
47 | | addcl 11138 |
. . . 4
โข (((2
ยท ๐ฅ) โ โ
โง 2 โ โ) โ ((2 ยท ๐ฅ) + 2) โ โ) |
48 | 4, 1, 47 | sylancl 587 |
. . 3
โข (๐ฅ โ โ0
โ ((2 ยท ๐ฅ) + 2)
โ โ) |
49 | | 3cn 12239 |
. . . 4
โข 3 โ
โ |
50 | | addcl 11138 |
. . . 4
โข (((2
ยท ๐ฅ) โ โ
โง 3 โ โ) โ ((2 ยท ๐ฅ) + 3) โ โ) |
51 | 4, 49, 50 | sylancl 587 |
. . 3
โข (๐ฅ โ โ0
โ ((2 ยท ๐ฅ) + 3)
โ โ) |
52 | | mulass 11144 |
. . 3
โข
(((!โ((2 ยท ๐ฅ) + 1)) โ โ โง ((2 ยท
๐ฅ) + 2) โ โ
โง ((2 ยท ๐ฅ) + 3)
โ โ) โ (((!โ((2 ยท ๐ฅ) + 1)) ยท ((2 ยท ๐ฅ) + 2)) ยท ((2 ยท
๐ฅ) + 3)) = ((!โ((2
ยท ๐ฅ) + 1)) ยท
(((2 ยท ๐ฅ) + 2)
ยท ((2 ยท ๐ฅ) +
3)))) |
53 | 46, 48, 51, 52 | syl3anc 1372 |
. 2
โข (๐ฅ โ โ0
โ (((!โ((2 ยท ๐ฅ) + 1)) ยท ((2 ยท ๐ฅ) + 2)) ยท ((2 ยท
๐ฅ) + 3)) = ((!โ((2
ยท ๐ฅ) + 1)) ยท
(((2 ยท ๐ฅ) + 2)
ยท ((2 ยท ๐ฅ) +
3)))) |
54 | 42, 53 | eqtrd 2773 |
1
โข (๐ฅ โ โ0
โ (!โ((2 ยท ๐ฅ) + 3)) = ((!โ((2 ยท ๐ฅ) + 1)) ยท (((2 ยท
๐ฅ) + 2) ยท ((2
ยท ๐ฅ) +
3)))) |