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 13089

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 11217	. . . . . . 7 ⊢ -∞ ∉ ℝ
2	1	neli 3031	. . . . . 6 ⊢ ¬ -∞ ∈ ℝ
3	2	intnan 486	. . . . 5 ⊢ ¬ (𝐴 ∈ ℝ ∧ -∞ ∈ ℝ)
4	3	intnanr 487	. . . 4 ⊢ ¬ ((𝐴 ∈ ℝ ∧ -∞ ∈ ℝ) ∧ 𝐴 <_ℝ -∞)
5		pnfnemnf 11229	. . . . . 6 ⊢ +∞ ≠ -∞
6	5	nesymi 2982	. . . . 5 ⊢ ¬ -∞ = +∞
7	6	intnan 486	. . . 4 ⊢ ¬ (𝐴 = -∞ ∧ -∞ = +∞)
8	4, 7	pm3.2ni 880	. . 3 ⊢ ¬ (((𝐴 ∈ ℝ ∧ -∞ ∈ ℝ) ∧ 𝐴 <_ℝ -∞) ∨ (𝐴 = -∞ ∧ -∞ = +∞))
9	6	intnan 486	. . . 4 ⊢ ¬ (𝐴 ∈ ℝ ∧ -∞ = +∞)
10	2	intnan 486	. . . 4 ⊢ ¬ (𝐴 = -∞ ∧ -∞ ∈ ℝ)
11	9, 10	pm3.2ni 880	. . 3 ⊢ ¬ ((𝐴 ∈ ℝ ∧ -∞ = +∞) ∨ (𝐴 = -∞ ∧ -∞ ∈ ℝ))
12	8, 11	pm3.2ni 880	. 2 ⊢ ¬ ((((𝐴 ∈ ℝ ∧ -∞ ∈ ℝ) ∧ 𝐴 <_ℝ -∞) ∨ (𝐴 = -∞ ∧ -∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ -∞ = +∞) ∨ (𝐴 = -∞ ∧ -∞ ∈ ℝ)))
13		mnfxr 11231	. . 3 ⊢ -∞ ∈ ℝ^*
14		ltxr 13075	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ -∞ ∈ ℝ^*) → (𝐴 < -∞ ↔ ((((𝐴 ∈ ℝ ∧ -∞ ∈ ℝ) ∧ 𝐴 <_ℝ -∞) ∨ (𝐴 = -∞ ∧ -∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ -∞ = +∞) ∨ (𝐴 = -∞ ∧ -∞ ∈ ℝ)))))
15	13, 14	mpan2 691	. 2 ⊢ (𝐴 ∈ ℝ^* → (𝐴 < -∞ ↔ ((((𝐴 ∈ ℝ ∧ -∞ ∈ ℝ) ∧ 𝐴 <_ℝ -∞) ∨ (𝐴 = -∞ ∧ -∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ -∞ = +∞) ∨ (𝐴 = -∞ ∧ -∞ ∈ ℝ)))))
16	12, 15	mtbiri 327	1 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 class class class wbr 5107 ℝcr 11067 <_ℝ cltrr 11072 +∞cpnf 11205 -∞cmnf 11206 ℝ^*cxr 11207 < clt 11208

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-br 5108 df-opab 5170 df-mpt 5189 df-id 5533 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213

This theorem is referenced by: mnfle 13095 xrltnsym 13097 xrlttr 13100 qbtwnxr 13160 xltnegi 13176 xmullem2 13225 xmulasslem2 13242 xlemul1a 13248 xrsupexmnf 13265 xrsupsslem 13267 xrinfmsslem 13268 xrsup0 13283 reltxrnmnf 13303 infmremnf 13304 mnfnei 23108 blssioo 24683 deg1add 26008 icorempo 37339 relowlssretop 37351 supxrgere 45329 supxrgelem 45333 infxrunb2 45364 iccpartiltu 47423

W3C validator