Theorem slotsbaseefdif

Description: The slots Base and .ef are different. (Contributed by AV, 21-Sep-2020)

	Ref	Expression
Assertion	slotsbaseefdif	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)$$

Proof

Step	Hyp	Ref	Expression
1		basendxnn	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathbb{N}$$
2	1	nnrei	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in ℝ$$
3		baseltedgf	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<\mathrm{ef}\left(\mathrm{ndx}\right)$$
4	2 3	ltneii	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)$$