Description: Index value of the Euclidean function slot. Use ndxarg . (Contributed by Thierry Arnoux, 22-Mar-2025) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eufndx | |- ( EuclF ` ndx ) = ; 2 1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-euf | |- EuclF = Slot ; 2 1 |
|
| 2 | 2nn0 | |- 2 e. NN0 |
|
| 3 | 1nn | |- 1 e. NN |
|
| 4 | 2 3 | decnncl | |- ; 2 1 e. NN |
| 5 | 1 4 | ndxarg | |- ( EuclF ` ndx ) = ; 2 1 |