nltmnf - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nltmnf		Structured version Visualization version GIF version

Theorem nltmnf 12847

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

**Assertion**
Ref	Expression
nltmnf	⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)

**Proof of Theorem nltmnf**
Step	Hyp	Ref	Expression
1		mnfnre 11002	. . . . . . 7 ⊢ -∞ ∉ ℝ
2	1	neli 3052	. . . . . 6 ⊢ ¬ -∞ ∈ ℝ
3	2	intnan 486	. . . . 5 ⊢ ¬ (𝐴 ∈ ℝ ∧ -∞ ∈ ℝ)
4	3	intnanr 487	. . . 4 ⊢ ¬ ((𝐴 ∈ ℝ ∧ -∞ ∈ ℝ) ∧ 𝐴 <_ℝ -∞)
5		pnfnemnf 11014	. . . . . 6 ⊢ +∞ ≠ -∞
6	5	nesymi 3002	. . . . 5 ⊢ ¬ -∞ = +∞
7	6	intnan 486	. . . 4 ⊢ ¬ (𝐴 = -∞ ∧ -∞ = +∞)
8	4, 7	pm3.2ni 877	. . 3 ⊢ ¬ (((𝐴 ∈ ℝ ∧ -∞ ∈ ℝ) ∧ 𝐴 <_ℝ -∞) ∨ (𝐴 = -∞ ∧ -∞ = +∞))
9	6	intnan 486	. . . 4 ⊢ ¬ (𝐴 ∈ ℝ ∧ -∞ = +∞)
10	2	intnan 486	. . . 4 ⊢ ¬ (𝐴 = -∞ ∧ -∞ ∈ ℝ)
11	9, 10	pm3.2ni 877	. . 3 ⊢ ¬ ((𝐴 ∈ ℝ ∧ -∞ = +∞) ∨ (𝐴 = -∞ ∧ -∞ ∈ ℝ))
12	8, 11	pm3.2ni 877	. 2 ⊢ ¬ ((((𝐴 ∈ ℝ ∧ -∞ ∈ ℝ) ∧ 𝐴 <_ℝ -∞) ∨ (𝐴 = -∞ ∧ -∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ -∞ = +∞) ∨ (𝐴 = -∞ ∧ -∞ ∈ ℝ)))
13		mnfxr 11016	. . 3 ⊢ -∞ ∈ ℝ^*
14		ltxr 12833	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ -∞ ∈ ℝ^*) → (𝐴 < -∞ ↔ ((((𝐴 ∈ ℝ ∧ -∞ ∈ ℝ) ∧ 𝐴 <_ℝ -∞) ∨ (𝐴 = -∞ ∧ -∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ -∞ = +∞) ∨ (𝐴 = -∞ ∧ -∞ ∈ ℝ)))))
15	13, 14	mpan2 687	. 2 ⊢ (𝐴 ∈ ℝ^* → (𝐴 < -∞ ↔ ((((𝐴 ∈ ℝ ∧ -∞ ∈ ℝ) ∧ 𝐴 <_ℝ -∞) ∨ (𝐴 = -∞ ∧ -∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ -∞ = +∞) ∨ (𝐴 = -∞ ∧ -∞ ∈ ℝ)))))
16	12, 15	mtbiri 326	1 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 = wceq 1541 ∈ wcel 2109 class class class wbr 5078 ℝcr 10854 <_ℝ cltrr 10859 +∞cpnf 10990 -∞cmnf 10991 ℝ^*cxr 10992 < clt 10993

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7579 ax-cnex 10911 ax-resscn 10912

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3432 df-sbc 3720 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4567 df-pr 4569 df-op 4573 df-uni 4845 df-br 5079 df-opab 5141 df-mpt 5162 df-id 5488 df-xp 5594 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-rn 5599 df-res 5600 df-ima 5601 df-iota 6388 df-fun 6432 df-fn 6433 df-f 6434 df-f1 6435 df-fo 6436 df-f1o 6437 df-fv 6438 df-er 8472 df-en 8708 df-dom 8709 df-sdom 8710 df-pnf 10995 df-mnf 10996 df-xr 10997 df-ltxr 10998

This theorem is referenced by: mnfle 12852 xrltnsym 12853 xrlttr 12856 qbtwnxr 12916 xltnegi 12932 xmullem2 12981 xmulasslem2 12998 xlemul1a 13004 xrsupexmnf 13021 xrsupsslem 13023 xrinfmsslem 13024 xrsup0 13039 reltxrnmnf 13058 infmremnf 13059 mnfnei 22353 blssioo 23939 deg1add 25249 icorempo 35501 relowlssretop 35513 supxrgere 42826 supxrgelem 42830 infxrunb2 42861 iccpartiltu 44826

W3C validator