Metamath Proof Explorer

Theorem pnfnlt

Description: No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005)

Ref Expression
Assertion pnfnlt ${⊢}{A}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{A}$

Proof

Step Hyp Ref Expression
1 pnfnre ${⊢}\mathrm{+\infty }\notin ℝ$
2 1 neli ${⊢}¬\mathrm{+\infty }\in ℝ$
3 2 intnanr ${⊢}¬\left(\mathrm{+\infty }\in ℝ\wedge {A}\in ℝ\right)$
4 3 intnanr ${⊢}¬\left(\left(\mathrm{+\infty }\in ℝ\wedge {A}\in ℝ\right)\wedge \mathrm{+\infty }{<}_{ℝ}{A}\right)$
5 pnfnemnf ${⊢}\mathrm{+\infty }\ne \mathrm{-\infty }$
6 5 neii ${⊢}¬\mathrm{+\infty }=\mathrm{-\infty }$
7 6 intnanr ${⊢}¬\left(\mathrm{+\infty }=\mathrm{-\infty }\wedge {A}=\mathrm{+\infty }\right)$
8 4 7 pm3.2ni ${⊢}¬\left(\left(\left(\mathrm{+\infty }\in ℝ\wedge {A}\in ℝ\right)\wedge \mathrm{+\infty }{<}_{ℝ}{A}\right)\vee \left(\mathrm{+\infty }=\mathrm{-\infty }\wedge {A}=\mathrm{+\infty }\right)\right)$
9 2 intnanr ${⊢}¬\left(\mathrm{+\infty }\in ℝ\wedge {A}=\mathrm{+\infty }\right)$
10 6 intnanr ${⊢}¬\left(\mathrm{+\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)$
11 9 10 pm3.2ni ${⊢}¬\left(\left(\mathrm{+\infty }\in ℝ\wedge {A}=\mathrm{+\infty }\right)\vee \left(\mathrm{+\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)\right)$
12 8 11 pm3.2ni ${⊢}¬\left(\left(\left(\left(\mathrm{+\infty }\in ℝ\wedge {A}\in ℝ\right)\wedge \mathrm{+\infty }{<}_{ℝ}{A}\right)\vee \left(\mathrm{+\infty }=\mathrm{-\infty }\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(\mathrm{+\infty }\in ℝ\wedge {A}=\mathrm{+\infty }\right)\vee \left(\mathrm{+\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)\right)\right)$
13 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
14 ltxr ${⊢}\left(\mathrm{+\infty }\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left(\mathrm{+\infty }<{A}↔\left(\left(\left(\left(\mathrm{+\infty }\in ℝ\wedge {A}\in ℝ\right)\wedge \mathrm{+\infty }{<}_{ℝ}{A}\right)\vee \left(\mathrm{+\infty }=\mathrm{-\infty }\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(\mathrm{+\infty }\in ℝ\wedge {A}=\mathrm{+\infty }\right)\vee \left(\mathrm{+\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)\right)\right)\right)$
15 13 14 mpan ${⊢}{A}\in {ℝ}^{*}\to \left(\mathrm{+\infty }<{A}↔\left(\left(\left(\left(\mathrm{+\infty }\in ℝ\wedge {A}\in ℝ\right)\wedge \mathrm{+\infty }{<}_{ℝ}{A}\right)\vee \left(\mathrm{+\infty }=\mathrm{-\infty }\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(\mathrm{+\infty }\in ℝ\wedge {A}=\mathrm{+\infty }\right)\vee \left(\mathrm{+\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)\right)\right)\right)$
16 12 15 mtbiri ${⊢}{A}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{A}$