Metamath Proof Explorer


Theorem basendxnmulrndxOLD

Description: Obsolete proof of basendxnmulrndx as of 28-Oct-2024. The slot for the base set is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 16-Feb-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion basendxnmulrndxOLD Basendxndx

Proof

Step Hyp Ref Expression
1 df-base Base=Slot1
2 1nn 1
3 1 2 ndxarg Basendx=1
4 1re 1
5 1lt3 1<3
6 4 5 ltneii 13
7 mulrndx ndx=3
8 6 7 neeqtrri 1ndx
9 3 8 eqnetri Basendxndx