| Step |
Hyp |
Ref |
Expression |
| 1 |
|
oveq1 |
|- ( n = N -> ( n ^ ( x - 1 ) ) = ( N ^ ( x - 1 ) ) ) |
| 2 |
1
|
oveq1d |
|- ( n = N -> ( ( n ^ ( x - 1 ) ) - 1 ) = ( ( N ^ ( x - 1 ) ) - 1 ) ) |
| 3 |
2
|
breq2d |
|- ( n = N -> ( x || ( ( n ^ ( x - 1 ) ) - 1 ) <-> x || ( ( N ^ ( x - 1 ) ) - 1 ) ) ) |
| 4 |
3
|
anbi2d |
|- ( n = N -> ( ( x e/ Prime /\ x || ( ( n ^ ( x - 1 ) ) - 1 ) ) <-> ( x e/ Prime /\ x || ( ( N ^ ( x - 1 ) ) - 1 ) ) ) ) |
| 5 |
4
|
rabbidv |
|- ( n = N -> { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ x || ( ( n ^ ( x - 1 ) ) - 1 ) ) } = { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ x || ( ( N ^ ( x - 1 ) ) - 1 ) ) } ) |
| 6 |
|
df-fppr |
|- FPPr = ( n e. NN |-> { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ x || ( ( n ^ ( x - 1 ) ) - 1 ) ) } ) |
| 7 |
|
fvex |
|- ( ZZ>= ` 4 ) e. _V |
| 8 |
7
|
rabex |
|- { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ x || ( ( N ^ ( x - 1 ) ) - 1 ) ) } e. _V |
| 9 |
5 6 8
|
fvmpt |
|- ( N e. NN -> ( FPPr ` N ) = { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ x || ( ( N ^ ( x - 1 ) ) - 1 ) ) } ) |