HomeHome Intuitionistic Logic Explorer
Theorem List (p. 67 of 75)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 6601-6700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Axiomax-cnre 6601* A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom for real and complex numbers, justified by theorem axcnre 6574. For naming consistency, use cnre 6626 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
(A ℂ → x y A = (x + (i · y)))
 
Axiomax-pre-ltirr 6602 Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6602. (Contributed by Jim Kingdon, 12-Jan-2020.)
(A ℝ → ¬ A < A)
 
Axiomax-pre-ltwlin 6603 Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6576. (Contributed by Jim Kingdon, 12-Jan-2020.)
((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))
 
Axiomax-pre-lttrn 6604 Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 6577. (Contributed by NM, 13-Oct-2005.)
((A B 𝐶 ℝ) → ((A < B B < 𝐶) → A < 𝐶))
 
Axiomax-pre-apti 6605 Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 6578. (Contributed by Jim Kingdon, 29-Jan-2020.)
((A B ¬ (A < B B < A)) → A = B)
 
Axiomax-pre-ltadd 6606 Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 6579. (Contributed by NM, 13-Oct-2005.)
((A B 𝐶 ℝ) → (A < B → (𝐶 + A) < (𝐶 + B)))
 
Axiomax-pre-mulgt0 6607 The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 6580. (Contributed by NM, 13-Oct-2005.)
((A B ℝ) → ((0 < A 0 < B) → 0 < (A · B)))
 
3.2  Derive the basic properties from the field axioms
 
3.2.1  Some deductions from the field axioms for complex numbers
 
Theoremcnex 6608 Alias for ax-cnex 6581. (Contributed by Mario Carneiro, 17-Nov-2014.)
V
 
Theoremaddcl 6609 Alias for ax-addcl 6586, for naming consistency with addcli 6634. Use this theorem instead of ax-addcl 6586 or axaddcl 6559. (Contributed by NM, 10-Mar-2008.)
((A B ℂ) → (A + B) ℂ)
 
Theoremreaddcl 6610 Alias for ax-addrcl 6587, for naming consistency with readdcli 6643. (Contributed by NM, 10-Mar-2008.)
((A B ℝ) → (A + B) ℝ)
 
Theoremmulcl 6611 Alias for ax-mulcl 6588, for naming consistency with mulcli 6635. (Contributed by NM, 10-Mar-2008.)
((A B ℂ) → (A · B) ℂ)
 
Theoremremulcl 6612 Alias for ax-mulrcl 6589, for naming consistency with remulcli 6644. (Contributed by NM, 10-Mar-2008.)
((A B ℝ) → (A · B) ℝ)
 
Theoremmulcom 6613 Alias for ax-mulcom 6591, for naming consistency with mulcomi 6636. (Contributed by NM, 10-Mar-2008.)
((A B ℂ) → (A · B) = (B · A))
 
Theoremaddass 6614 Alias for ax-addass 6592, for naming consistency with addassi 6638. (Contributed by NM, 10-Mar-2008.)
((A B 𝐶 ℂ) → ((A + B) + 𝐶) = (A + (B + 𝐶)))
 
Theoremmulass 6615 Alias for ax-mulass 6593, for naming consistency with mulassi 6639. (Contributed by NM, 10-Mar-2008.)
((A B 𝐶 ℂ) → ((A · B) · 𝐶) = (A · (B · 𝐶)))
 
Theoremadddi 6616 Alias for ax-distr 6594, for naming consistency with adddii 6640. (Contributed by NM, 10-Mar-2008.)
((A B 𝐶 ℂ) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))
 
Theoremrecn 6617 A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
(A ℝ → A ℂ)
 
Theoremreex 6618 The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
V
 
Theoremreelprrecn 6619 Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
{ℝ, ℂ}
 
Theoremcnelprrecn 6620 Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
{ℝ, ℂ}
 
Theoremadddir 6621 Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
((A B 𝐶 ℂ) → ((A + B) · 𝐶) = ((A · 𝐶) + (B · 𝐶)))
 
Theorem0cn 6622 0 is a complex number. (Contributed by NM, 19-Feb-2005.)
0
 
Theorem0cnd 6623 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
(φ → 0 ℂ)
 
Theoremc0ex 6624 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
0 V
 
Theorem1ex 6625 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
1 V
 
Theoremcnre 6626* Alias for ax-cnre 6601, for naming consistency. (Contributed by NM, 3-Jan-2013.)
(A ℂ → x y A = (x + (i · y)))
 
Theoremmulid1 6627 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
(A ℂ → (A · 1) = A)
 
Theoremmulid2 6628 Identity law for multiplication. Note: see mulid1 6627 for commuted version. (Contributed by NM, 8-Oct-1999.)
(A ℂ → (1 · A) = A)
 
Theorem1re 6629 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
1
 
Theorem0re 6630 0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
0
 
Theorem0red 6631 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
(φ → 0 ℝ)
 
Theoremmulid1i 6632 Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
A        (A · 1) = A
 
Theoremmulid2i 6633 Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
A        (1 · A) = A
 
Theoremaddcli 6634 Closure law for addition. (Contributed by NM, 23-Nov-1994.)
A     &   B        (A + B)
 
Theoremmulcli 6635 Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
A     &   B        (A · B)
 
Theoremmulcomi 6636 Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
A     &   B        (A · B) = (B · A)
 
Theoremmulcomli 6637 Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
A     &   B     &   (A · B) = 𝐶       (B · A) = 𝐶
 
Theoremaddassi 6638 Associative law for addition. (Contributed by NM, 23-Nov-1994.)
A     &   B     &   𝐶        ((A + B) + 𝐶) = (A + (B + 𝐶))
 
Theoremmulassi 6639 Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
A     &   B     &   𝐶        ((A · B) · 𝐶) = (A · (B · 𝐶))
 
Theoremadddii 6640 Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
A     &   B     &   𝐶        (A · (B + 𝐶)) = ((A · B) + (A · 𝐶))
 
Theoremadddiri 6641 Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
A     &   B     &   𝐶        ((A + B) · 𝐶) = ((A · 𝐶) + (B · 𝐶))
 
Theoremrecni 6642 A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
A        A
 
Theoremreaddcli 6643 Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
A     &   B        (A + B)
 
Theoremremulcli 6644 Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
A     &   B        (A · B)
 
Theorem1red 6645 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
(φ → 1 ℝ)
 
Theorem1cnd 6646 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
(φ → 1 ℂ)
 
Theoremmulid1d 6647 Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℂ)       (φ → (A · 1) = A)
 
Theoremmulid2d 6648 Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℂ)       (φ → (1 · A) = A)
 
Theoremaddcld 6649 Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (A + B) ℂ)
 
Theoremmulcld 6650 Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (A · B) ℂ)
 
Theoremmulcomd 6651 Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (A · B) = (B · A))
 
Theoremaddassd 6652 Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)       (φ → ((A + B) + 𝐶) = (A + (B + 𝐶)))
 
Theoremmulassd 6653 Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)       (φ → ((A · B) · 𝐶) = (A · (B · 𝐶)))
 
Theoremadddid 6654 Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)       (φ → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))
 
Theoremadddird 6655 Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)       (φ → ((A + B) · 𝐶) = ((A · 𝐶) + (B · 𝐶)))
 
Theoremrecnd 6656 Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
(φA ℝ)       (φA ℂ)
 
Theoremreaddcld 6657 Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℝ)    &   (φB ℝ)       (φ → (A + B) ℝ)
 
Theoremremulcld 6658 Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℝ)    &   (φB ℝ)       (φ → (A · B) ℝ)
 
3.2.2  Infinity and the extended real number system
 
Syntaxcpnf 6659 Plus infinity.
class +∞
 
Syntaxcmnf 6660 Minus infinity.
class -∞
 
Syntaxcxr 6661 The set of extended reals (includes plus and minus infinity).
class *
 
Syntaxclt 6662 'Less than' predicate (extended to include the extended reals).
class <
 
Syntaxcle 6663 Extend wff notation to include the 'less than or equal to' relation.
class
 
Definitiondf-pnf 6664 Define plus infinity. Note that the definition is arbitrary, requiring only that +∞ be a set not in and different from -∞ (df-mnf 6665). We use 𝒫 to make it independent of the construction of , and Cantor's Theorem will show that it is different from any member of and therefore . See pnfnre 6669 and mnfnre 6670, and we'll also be able to prove +∞ ≠ -∞.

A simpler possibility is to define +∞ as and -∞ as {ℂ}, but that approach requires the Axiom of Regularity to show that +∞ and -∞ are different from each other and from all members of . (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)

+∞ = 𝒫
 
Definitiondf-mnf 6665 Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that -∞ be a set not in and different from +∞ (see mnfnre 6670). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
-∞ = 𝒫 +∞
 
Definitiondf-xr 6666 Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 13-Oct-2005.)
* = (ℝ ∪ {+∞, -∞})
 
Definitiondf-ltxr 6667* Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. Note that in our postulates for complex numbers, < is primitive and not necessarily a relation on . (Contributed by NM, 13-Oct-2005.)
< = ({⟨x, y⟩ ∣ (x y x < y)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
 
Definitiondf-le 6668 Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.)
≤ = ((ℝ* × ℝ*) ∖ < )
 
Theorempnfnre 6669 Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
+∞ ∉ ℝ
 
Theoremmnfnre 6670 Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
-∞ ∉ ℝ
 
Theoremressxr 6671 The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
ℝ ⊆ ℝ*
 
Theoremrexpssxrxp 6672 The Cartesian product of standard reals are a subset of the Cartesian product of extended reals (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
(ℝ × ℝ) ⊆ (ℝ* × ℝ*)
 
Theoremrexr 6673 A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
(A ℝ → A *)
 
Theorem0xr 6674 Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
0 *
 
Theoremrenepnf 6675 No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
(A ℝ → A ≠ +∞)
 
Theoremrenemnf 6676 No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
(A ℝ → A ≠ -∞)
 
Theoremrexrd 6677 A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)       (φA *)
 
Theoremrenepnfd 6678 No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)       (φA ≠ +∞)
 
Theoremrenemnfd 6679 No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)       (φA ≠ -∞)
 
Theoremrexri 6680 A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
A        A *
 
Theoremrenfdisj 6681 The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
(ℝ ∩ {+∞, -∞}) = ∅
 
Theoremltrelxr 6682 'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
< ⊆ (ℝ* × ℝ*)
 
Theoremltrel 6683 'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
Rel <
 
Theoremlerelxr 6684 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
≤ ⊆ (ℝ* × ℝ*)
 
Theoremlerel 6685 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
Rel ≤
 
Theoremxrlenlt 6686 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
((A * B *) → (AB ↔ ¬ B < A))
 
Theoremltxrlt 6687 The standard less-than < and the extended real less-than < are identical when restricted to the non-extended reals . (Contributed by NM, 13-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
((A B ℝ) → (A < BA < B))
 
3.2.3  Restate the ordering postulates with extended real "less than"
 
Theoremaxltirr 6688 Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 6602 with ordering on the extended reals. New proofs should use ltnr 6697 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
(A ℝ → ¬ A < A)
 
Theoremaxltwlin 6689 Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 6603 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))
 
Theoremaxlttrn 6690 Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 6604 with ordering on the extended reals. New proofs should use lttr 6694 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
((A B 𝐶 ℝ) → ((A < B B < 𝐶) → A < 𝐶))
 
Theoremaxltadd 6691 Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 6606 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
((A B 𝐶 ℝ) → (A < B → (𝐶 + A) < (𝐶 + B)))
 
Theoremaxapti 6692 Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 6605 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.)
((A B ¬ (A < B B < A)) → A = B)
 
Theoremaxmulgt0 6693 The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 6607 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
((A B ℝ) → ((0 < A 0 < B) → 0 < (A · B)))
 
3.2.4  Ordering on reals
 
Theoremlttr 6694 Alias for axlttrn 6690, for naming consistency with lttri 6724. New proofs should generally use this instead of ax-pre-lttrn 6604. (Contributed by NM, 10-Mar-2008.)
((A B 𝐶 ℝ) → ((A < B B < 𝐶) → A < 𝐶))
 
Theoremmulgt0 6695 The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.)
(((A 0 < A) (B 0 < B)) → 0 < (A · B))
 
Theoremlenlt 6696 'Less than or equal to' expressed in terms of 'less than'. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-May-1999.)
((A B ℝ) → (AB ↔ ¬ B < A))
 
Theoremltnr 6697 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
(A ℝ → ¬ A < A)
 
Theoremltso 6698 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
< Or ℝ
 
Theoremgtso 6699 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
< Or ℝ
 
Theoremlttri3 6700 Tightness of real apartness. (Contributed by NM, 5-May-1999.)
((A B ℝ) → (A = B ↔ (¬ A < B ¬ B < A)))
    < Previous  Next >

Page List
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-7411
  Copyright terms: Public domain < Previous  Next >