Metamath Proof Explorer


Theorem plendxnmulrndx

Description: The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. Formerly part of proof for opsrmulr . (Contributed by AV, 1-Nov-2024)

Ref Expression
Assertion plendxnmulrndx ndxndx

Proof

Step Hyp Ref Expression
1 3re 3
2 3lt10 3<10
3 1 2 gtneii 103
4 plendx ndx=10
5 mulrndx ndx=3
6 4 5 neeq12i ndxndx103
7 3 6 mpbir ndxndx