| Step |
Hyp |
Ref |
Expression |
| 1 |
|
3nn |
|- 3 e. NN |
| 2 |
|
prmonn2 |
|- ( 3 e. NN -> ( #p ` 3 ) = if ( 3 e. Prime , ( ( #p ` ( 3 - 1 ) ) x. 3 ) , ( #p ` ( 3 - 1 ) ) ) ) |
| 3 |
1 2
|
ax-mp |
|- ( #p ` 3 ) = if ( 3 e. Prime , ( ( #p ` ( 3 - 1 ) ) x. 3 ) , ( #p ` ( 3 - 1 ) ) ) |
| 4 |
|
3prm |
|- 3 e. Prime |
| 5 |
4
|
iftruei |
|- if ( 3 e. Prime , ( ( #p ` ( 3 - 1 ) ) x. 3 ) , ( #p ` ( 3 - 1 ) ) ) = ( ( #p ` ( 3 - 1 ) ) x. 3 ) |
| 6 |
|
3m1e2 |
|- ( 3 - 1 ) = 2 |
| 7 |
6
|
fveq2i |
|- ( #p ` ( 3 - 1 ) ) = ( #p ` 2 ) |
| 8 |
|
prmo2 |
|- ( #p ` 2 ) = 2 |
| 9 |
7 8
|
eqtri |
|- ( #p ` ( 3 - 1 ) ) = 2 |
| 10 |
9
|
oveq1i |
|- ( ( #p ` ( 3 - 1 ) ) x. 3 ) = ( 2 x. 3 ) |
| 11 |
|
3cn |
|- 3 e. CC |
| 12 |
|
2cn |
|- 2 e. CC |
| 13 |
|
3t2e6 |
|- ( 3 x. 2 ) = 6 |
| 14 |
11 12 13
|
mulcomli |
|- ( 2 x. 3 ) = 6 |
| 15 |
10 14
|
eqtri |
|- ( ( #p ` ( 3 - 1 ) ) x. 3 ) = 6 |
| 16 |
5 15
|
eqtri |
|- if ( 3 e. Prime , ( ( #p ` ( 3 - 1 ) ) x. 3 ) , ( #p ` ( 3 - 1 ) ) ) = 6 |
| 17 |
3 16
|
eqtri |
|- ( #p ` 3 ) = 6 |