| Step |
Hyp |
Ref |
Expression |
| 1 |
|
6nn |
|- 6 e. NN |
| 2 |
|
prmonn2 |
|- ( 6 e. NN -> ( #p ` 6 ) = if ( 6 e. Prime , ( ( #p ` ( 6 - 1 ) ) x. 6 ) , ( #p ` ( 6 - 1 ) ) ) ) |
| 3 |
1 2
|
ax-mp |
|- ( #p ` 6 ) = if ( 6 e. Prime , ( ( #p ` ( 6 - 1 ) ) x. 6 ) , ( #p ` ( 6 - 1 ) ) ) |
| 4 |
|
6nprm |
|- -. 6 e. Prime |
| 5 |
4
|
iffalsei |
|- if ( 6 e. Prime , ( ( #p ` ( 6 - 1 ) ) x. 6 ) , ( #p ` ( 6 - 1 ) ) ) = ( #p ` ( 6 - 1 ) ) |
| 6 |
3 5
|
eqtri |
|- ( #p ` 6 ) = ( #p ` ( 6 - 1 ) ) |
| 7 |
|
6m1e5 |
|- ( 6 - 1 ) = 5 |
| 8 |
7
|
fveq2i |
|- ( #p ` ( 6 - 1 ) ) = ( #p ` 5 ) |
| 9 |
|
prmo5 |
|- ( #p ` 5 ) = ; 3 0 |
| 10 |
8 9
|
eqtri |
|- ( #p ` ( 6 - 1 ) ) = ; 3 0 |
| 11 |
6 10
|
eqtri |
|- ( #p ` 6 ) = ; 3 0 |