Theorem basendxltplendx

Description: The index value of the Base slot is less than the index value of the le slot. (Contributed by AV, 30-Oct-2024)

	Ref	Expression
Assertion	basendxltplendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<{\le }_{\mathrm{ndx}}$$

Proof

Step	Hyp	Ref	Expression
1		1lt10	$$⊢1<10$$
2		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
3		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
4	1 2 3	3brtr4i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<{\le }_{\mathrm{ndx}}$$