Description: Value of the Euler phi function at 1. (Contributed by Mario Carneiro, 23-Feb-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | phi1 | |- ( phi ` 1 ) = 1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1nn | |- 1 e. NN |
|
| 2 | phicl2 | |- ( 1 e. NN -> ( phi ` 1 ) e. ( 1 ... 1 ) ) |
|
| 3 | 1 2 | ax-mp | |- ( phi ` 1 ) e. ( 1 ... 1 ) |
| 4 | 1z | |- 1 e. ZZ |
|
| 5 | fzsn | |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } ) |
|
| 6 | 4 5 | ax-mp | |- ( 1 ... 1 ) = { 1 } |
| 7 | 3 6 | eleqtri | |- ( phi ` 1 ) e. { 1 } |
| 8 | elsni | |- ( ( phi ` 1 ) e. { 1 } -> ( phi ` 1 ) = 1 ) |
|
| 9 | 7 8 | ax-mp | |- ( phi ` 1 ) = 1 |