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