mmtheorems56 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10752

Statement List for Metamath Proof Explorer - 5501-5600 - Page 56 of 108

Type	Label	Description
Statement
Definition	df-xr 5501	Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of [Gleason] p. 173.
⊢ ℝ* = (ℝ ∪ { +∞, -∞})
Definition	df-ltxr 5502	Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. The clipping of <ℝ makes our definition independent of the complex number construction, since the postulates don't presuppose that <ℝ is a relation on ℝ.
⊢ < = ((( <ℝ ∩ (ℝ × ℝ)) ∪ {⟨ -∞, +∞⟩}) ∪ ((ℝ × { +∞}) ∪ ({ -∞} × ℝ)))
Definition	df-le 5503	Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloet 5530 relates it to 'less than' for reals.
⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
Theorem	xrex 5504	The set of extended reals exists.
⊢ ℝ* ∈ V
Theorem	pnfxr 5505	Plus infinity belongs to the set of extended reals.
⊢ +∞ ∈ ℝ*
Theorem	mnfxr 5506	Minus infinity belongs to the set of extended reals.
⊢ -∞ ∈ ℝ*
Theorem	ltxrt 5507	The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → (A < B ↔ ((((A ∈ ℝ ⋀ B ∈ ℝ) ⋀ A <ℝ B) ⋁ (A = -∞ ⋀ B = +∞)) ⋁ ((A ∈ ℝ ⋀ B = +∞) ⋁ (A = -∞ ⋀ B ∈ ℝ)))))
Theorem	pnfnre 5508	Plus infinity is not a real number.
⊢ +∞ ∉ ℝ
Theorem	mnfnre 5509	Minus infinity is not a real number.
⊢ -∞ ∉ ℝ
Theorem	ressxr 5510	The standard reals are a subset of the extended reals.
⊢ ℝ ⊆ ℝ*
Theorem	rexrt 5511	A standard real is an extended real.
⊢ (A ∈ ℝ → A ∈ ℝ*)
Theorem	ltxrltt 5512	The standard less-than <ℝ and the extended real less-than < are identical when restricted to the non-extended reals ℝ.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A < B ↔ A <ℝ B))
Theorem	xrlenltt 5513	'Less than or equal to' expressed in terms of 'less than', for extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → (A ≤ B ↔ ¬ B < A))
Theorem	xrltnlet 5514	'Less than' expressed in terms of 'less than or equal to', for extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → (A < B ↔ ¬ B ≤ A))
Restate the ordering postulates with extended real "less than"
Theorem	axlttri 5515	Ordering on reals satisfies strict trichotomy. Axiom 22 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axlttri 5299 with ordering on the extended reals.)
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A < B ↔ ¬ (A = B ⋁ B < A)))
Theorem	axlttrn 5516	Ordering on reals is transitive. Axiom 23 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axlttrn 5300 with ordering on the extended reals.)
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ C ∈ ℝ) → ((A < B ⋀ B < C) → A < C))
Theorem	axltadd 5517	Ordering property of addition on reals. Axiom 24 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axltadd 5301 with ordering on the extended reals.)
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ C ∈ ℝ) → (A < B → (C + A) < (C + B)))
Theorem	axmulgt0 5518	The product of two positive reals is positive. Axiom 25 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axmulgt0 5302 with ordering on the extended reals.)
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → ((0 < A ⋀ 0 < B) → 0 < (A · B)))
Theorem	axsup 5519	A non-empty, bounded-above set of reals has a supremum. Axiom 27 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axsup 5303 with ordering on the extended reals.)
⊢ ((A ⊆ ℝ ⋀ A ≠ ∅ ⋀ ∃x ∈ ℝ ∀y ∈ A y < x) → ∃x ∈ ℝ (∀y ∈ A ¬ x < y ⋀ ∀y ∈ ℝ (y < x → ∃z ∈ A y < z)))
Ordering on reals
Theorem	lttrt 5520	Alias for axlttrn 5516, for naming consistency with lttr 5597.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ C ∈ ℝ) → ((A < B ⋀ B < C) → A < C))
Theorem	mulgt0t 5521	Alias for axmulgt0 5518, for naming consistency with mulgt0 5618.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → ((0 < A ⋀ 0 < B) → 0 < (A · B)))
Theorem	lenltt 5522	'Less than or equal to' expressed in terms of 'less than'.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A ≤ B ↔ ¬ B < A))
Theorem	ltnlet 5523	'Less than' expressed in terms of 'less than or equal to'.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A < B ↔ ¬ B ≤ A))
Theorem	ltso 5524	'Less than' is a strict ordering. Note: do not shorten this with ltsor 5273, and do not use ltsor 5273 in complex number proofs, in order to maintain a portable derivation of all complex number proofs directly from postulates.
⊢ < Or ℝ
Theorem	lttri2t 5525	Consequence of trichotomy.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A ≠ B ↔ (A < B ⋁ B < A)))
Theorem	lttri3t 5526	Trichotomy law for 'less than'.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A = B ↔ (¬ A < B ⋀ ¬ B < A)))
Theorem	lttri4t 5527	Trichotomy law for 'less than'.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A < B ⋁ A = B ⋁ B < A))
Theorem	ltnet 5528	'Less than' implies not equal.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ A < B) → B ≠ A)
Theorem	letri3t 5529	Trichotomy law.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A = B ↔ (A ≤ B ⋀ B ≤ A)))
Theorem	leloet 5530	'Less than or equal to' expressed in terms of 'less than' or 'equals'.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A ≤ B ↔ (A < B ⋁ A = B)))
Theorem	eqleltt 5531	Equality in terms of 'less than or equal to', 'less than'.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A = B ↔ (A ≤ B ⋀ ¬ A < B)))
Theorem	ltlet 5532	'Less than' implies 'less than or equal to'.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A < B → A ≤ B))
Theorem	leltnet 5533	'Less than or equal to' implies 'less than' is not 'equals'.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → (A < B ↔ B ≠ A))
Theorem	ltlent 5534	'Less than' expressed in terms of 'less than or equal to'.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A < B ↔ (A ≤ B ⋀ B ≠ A)))
Theorem	lelttrt 5535	Transitive law.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ C ∈ ℝ) → ((A ≤ B ⋀ B < C) → A < C))
Theorem	ltletrt 5536	Transitive law.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ C ∈ ℝ) → ((A < B ⋀ B ≤ C) → A < C))
Theorem	letrt 5537	Transitive law.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ C ∈ ℝ) → ((A ≤ B ⋀ B ≤ C) → A ≤ C))
Theorem	letrd 5538	Transitive law deduction for 'less than or equal to'.
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → C ∈ ℝ)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → B ≤ C)    ⇒   ⊢ (φ → A ≤ C)
Theorem	lelttrd 5539	Transitive law deduction for 'less than or equal to', 'less than'.
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → C ∈ ℝ)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → B < C)    ⇒   ⊢ (φ → A < C)
Theorem	ltletrd 5540	Transitive law deduction for 'less than', 'less than or equal to'.
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → C ∈ ℝ)    &   ⊢ (φ → A < B)    &   ⊢ (φ → B ≤ C)    ⇒   ⊢ (φ → A < C)
Theorem	lttrd 5541	Transitive law deduction for 'less than'.
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → C ∈ ℝ)    &   ⊢ (φ → A < B)    &   ⊢ (φ → B < C)    ⇒   ⊢ (φ → A < C)
Theorem	ltnrt 5542	'Less than' is irreflexive.
⊢ (A ∈ ℝ → ¬ A < A)
Theorem	leidt 5543	'Less than or equal to' is reflexive.
⊢ (A ∈ ℝ → A ≤ A)
Theorem	ltnsymt 5544	'Less than' is not symmetric.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → (A < B → ¬ B < A))
Theorem	ltnsym2t 5545	'Less than' is antisymmetric and irreflexive.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ) → ¬ (A < B ⋀ B < A))
Theorem	pm2.61ltle 5546	Ordering elimination by cases.
⊢ ((φ ⋀ A < B) → ψ)    &   ⊢ ((φ ⋀ B ≤ A) → ψ)    &   ⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    ⇒   ⊢ (φ → ψ)
Ordering on the extended reals
Theorem	elxr 5547	Membership in the set of extended reals.
⊢ (A ∈ ℝ* ↔ (A ∈ ℝ ⋁ A = +∞ ⋁ A = -∞))
Theorem	pnfnemnf 5548	Plus and minus infinity are distinguished elements of ℝ*.
⊢ +∞ ≠ -∞
Theorem	renepnft 5549	No (finite) real equals plus infinity.
⊢ (A ∈ ℝ → A ≠ +∞)
Theorem	renemnft 5550	No real equals minus infinity.
⊢ (A ∈ ℝ → A ≠ -∞)
Theorem	renfdisj 5551	The reals and the infinities are disjoint.
⊢ (ℝ ∩ { +∞, -∞}) = ∅
Theorem	ssxr 5552	The three (non-exclusive) possibilities implied by a subset of extended reals.
⊢ (A ⊆ ℝ* → (A ⊆ ℝ ⋁ +∞ ∈ A ⋁ -∞ ∈ A))
Theorem	xrltnrt 5553	The extended real 'less than' is irreflexive.
⊢ (A ∈ ℝ* → ¬ A < A)
Theorem	ltpnft 5554	Any (finite) real is less than plus infinity.
⊢ (A ∈ ℝ → A < +∞)
Theorem	mnfltt 5555	Minus infinity is less than any (finite) real.
⊢ (A ∈ ℝ → -∞ < A)
Theorem	mnfltpnf 5556	Minus infinity is less than plus infinity.
⊢ -∞ < +∞
Theorem	mnfltxrt 5557	Minus infinity is less than an extended real that is either real or plus infinity.
⊢ ((A ∈ ℝ ⋁ A = +∞) → -∞ < A)
Theorem	pnfnltt 5558	No extended real is greater than plus infinity.
⊢ (A ∈ ℝ* → ¬ +∞ < A)
Theorem	nltmnft 5559	No extended real is less than minus infinity.
⊢ (A ∈ ℝ* → ¬ A < -∞)
Theorem	pnfget 5560	Plus infinity is an upper bound for extended reals.
⊢ (A ∈ ℝ* → A ≤ +∞)
Theorem	mnflet 5561	Minus infinity is less than or equal to any extended real.
⊢ (A ∈ ℝ* → -∞ ≤ A)
Theorem	xrltnsymt 5562	Ordering on the extended reals is not symmetric.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → (A < B → ¬ B < A))
Theorem	xrltnsym2t 5563	'Less than' is antisymmetric and irreflexive for extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → ¬ (A < B ⋀ B < A))
Theorem	xrlttrit 5564	Ordering on the extended reals satisfies strict trichotomy.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → (A < B ↔ ¬ (A = B ⋁ B < A)))
Theorem	xrlttrt 5565	Ordering on the extended reals is transitive.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ* ⋀ C ∈ ℝ*) → ((A < B ⋀ B < C) → A < C))
Theorem	xrltso 5566	'Less than' is a strict ordering on the extended reals.
⊢ < Or ℝ*
Theorem	xrlttri2t 5567	Trichotomy law for 'less than' for extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → (A ≠ B ↔ (A < B ⋁ B < A)))
Theorem	xrlttri3t 5568	Trichotomy law for 'less than' for extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → (A = B ↔ (¬ A < B ⋀ ¬ B < A)))
Theorem	xrleloet 5569	'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → (A ≤ B ↔ (A < B ⋁ A = B)))
Theorem	xrleltnet 5570	'Less than or equal to' implies 'less than' is not 'equals', for extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ* ⋀ A ≤ B) → (A < B ↔ B ≠ A))
Theorem	xrltlet 5571	'Less than' implies 'less than or equal' for extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → (A < B → A ≤ B))
Theorem	xrleidt 5572	'Less than or equal to' is reflexive for extended reals.
⊢ (A ∈ ℝ* → A ≤ A)
Theorem	xrletrit 5573	Trichotomy law for extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ*) → (A ≤ B ⋁ B ≤ A))
Theorem	xrlelttrt 5574	Transitive law for ordering on extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ* ⋀ C ∈ ℝ*) → ((A ≤ B ⋀ B < C) → A < C))
Theorem	xrltletrt 5575	Transitive law for ordering on extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ* ⋀ C ∈ ℝ*) → ((A < B ⋀ B ≤ C) → A < C))
Theorem	xrletrt 5576	Transitive law for ordering on extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ* ⋀ C ∈ ℝ*) → ((A ≤ B ⋀ B ≤ C) → A ≤ C))
Theorem	xrltnet 5577	'Less than' implies not equal for extended reals.
⊢ ((A ∈ ℝ* ⋀ B ∈ ℝ* ⋀ A < B) → B ≠ A)
Theorem	nltpnftt 5578	An extended real is not less than plus infinity iff they are equal.
⊢ (A ∈ ℝ* → (A = +∞ ↔ ¬ A < +∞))
Theorem	ngtmnftt 5579	An extended real is not greater than minus infinity iff they are equal.
⊢ (A ∈ ℝ* → (A = -∞ ↔ ¬ -∞ < A))
Theorem	xrrebndt 5580	An extended real is real iff it is strictly bounded by infinities.
⊢ (A ∈ ℝ* → (A ∈ ℝ ↔ ( -∞ < A ⋀ A < +∞)))
Theorem	xrret 5581	A way of proving that an extended real is real.
⊢ (((A ∈ ℝ* ⋀ B ∈ ℝ) ⋀ ( -∞ < A ⋀ A ≤ B)) → A ∈ ℝ)
Theorem	xrre2t 5582	An extended real between two others is real.
⊢ (((A ∈ ℝ* ⋀ B ∈ ℝ* ⋀ C ∈ ℝ*) ⋀ (A < B ⋀ B < C)) → B ∈ ℝ)
Ordering on reals (cont.)
Theorem	eqlet 5583	Equality implies 'less than or equal to'.
⊢ ((A ∈ ℝ ⋀ A = B) → A ≤ B)
Theorem	lttri2 5584	Consequence of trichotomy.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A ≠ B ↔ (A < B ⋁ B < A))
Theorem	lttri3 5585	Consequence of trichotomy.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A = B ↔ (¬ A < B ⋀ ¬ B < A))
Theorem	letri3 5586	Consequence of trichotomy.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A = B ↔ (A ≤ B ⋀ B ≤ A))
Theorem	leloe 5587	'Less than or equal to' in terms of 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A ≤ B ↔ (A < B ⋁ A = B))
Theorem	ltlen 5588	'Less than' expressed in terms of 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B ↔ (A ≤ B ⋀ B ≠ A))
Theorem	ltnsym 5589	'Less than' is not symmetric.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B → ¬ B < A)
Theorem	lenlt 5590	'Less than or equal to' in terms of 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A ≤ B ↔ ¬ B < A)
Theorem	ltnle 5591	'Less than' in terms of 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B ↔ ¬ B ≤ A)
Theorem	ltle 5592	'Less than' implies 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B → A ≤ B)
Theorem	ltlei 5593	'Less than' implies 'less than or equal to' (inference).
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ A < B    ⇒   ⊢ A ≤ B
Theorem	eqle 5594	Equality implies 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A = B → A ≤ B)
Theorem	ltne 5595	'Less than' implies not equal.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B → B ≠ A)
Theorem	letri 5596	Trichotomy law for 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A ≤ B ⋁ B ≤ A)
Theorem	lttr 5597	'Less than' is transitive. Theorem I.17 of [Apostol] p. 20.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A < B ⋀ B < C) → A < C)
Theorem	lelttr 5598	'Less than or equal to', 'less than' transitive law.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A ≤ B ⋀ B < C) → A < C)
Theorem	ltletr 5599	'Less than', 'less than or equal to' transitive law.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A < B ⋀ B ≤ C) → A < C)
Theorem	letr 5600	'Less than or equal to' is transitive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A ≤ B ⋀ B ≤ C) → A ≤ C)