Metamath Proof Explorer


Theorem topnfbey

Description: Nothing seems to be impossible to Prof. Lirpa. After years of intensive research, he managed to find a proof that when given a chance to reach infinity, one could indeed go beyond, thus giving formal soundness to Buzz Lightyear's motto "To infinity... and beyond!" (Contributed by Prof. Loof Lirpa, 1-Apr-2020) (Revised by Thierry Arnoux, 2-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion topnfbey B0+∞+∞<B

Proof

Step Hyp Ref Expression
1 noel ¬B
2 pnfxr +∞*
3 xrltnr +∞*¬+∞<+∞
4 2 3 ax-mp ¬+∞<+∞
5 zre +∞+∞
6 ltpnf +∞+∞<+∞
7 5 6 syl +∞+∞<+∞
8 4 7 mto ¬+∞
9 8 intnan ¬0+∞
10 fzf :×𝒫
11 10 fdmi dom=×
12 11 ndmov ¬0+∞0+∞=
13 9 12 ax-mp 0+∞=
14 13 eleq2i B0+∞B
15 1 14 mtbir ¬B0+∞
16 15 pm2.21i B0+∞+∞<B