Metamath Proof Explorer


Theorem nn0nepnf

Description: No standard nonnegative integer equals positive infinity. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion nn0nepnf A0A+∞

Proof

Step Hyp Ref Expression
1 pnfnre +∞
2 1 neli ¬+∞
3 nn0re +∞0+∞
4 2 3 mto ¬+∞0
5 eleq1 A=+∞A0+∞0
6 4 5 mtbiri A=+∞¬A0
7 6 necon2ai A0A+∞