|  Home | Metamath
Proof Explorer Theorem List (p. 112 of 494) | < Previous Next > | 
| Bad symbols? Try the GIF version. | ||
| Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List | ||
| Color key: |  Metamath Proof Explorer (1-30938) |  Hilbert Space Explorer (30939-32461) |  Users' Mathboxes (32462-49379) | 
| Type | Label | Description | 
|---|---|---|
| Statement | ||
| Definition | df-0r 11101 | Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers df-c 11162, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) | 
| ⊢ 0R = [〈1P, 1P〉] ~R | ||
| Definition | df-1r 11102 | Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 11162, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) | 
| ⊢ 1R = [〈(1P +P 1P), 1P〉] ~R | ||
| Definition | df-m1r 11103 | Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers df-c 11162, and is intended to be used only by the construction. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) | 
| ⊢ -1R = [〈1P, (1P +P 1P)〉] ~R | ||
| Theorem | enrer 11104 | The equivalence relation for signed reals is an equivalence relation. Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) (New usage is discouraged.) | 
| ⊢ ~R Er (P × P) | ||
| Theorem | nrex1 11105 | The class of signed reals is a set. Note that a shorter proof is possible using qsex 8817 (and not requiring enrer 11104), but it would add a dependency on ax-rep 5278. (Contributed by Mario Carneiro, 17-Nov-2014.) Extract proof from that of axcnex 11188. (Revised by BJ, 4-Feb-2023.) (New usage is discouraged.) | 
| ⊢ R ∈ V | ||
| Theorem | enrbreq 11106 | Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) | 
| ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → (〈𝐴, 𝐵〉 ~R 〈𝐶, 𝐷〉 ↔ (𝐴 +P 𝐷) = (𝐵 +P 𝐶))) | ||
| Theorem | enreceq 11107 | Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.) (New usage is discouraged.) | 
| ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([〈𝐴, 𝐵〉] ~R = [〈𝐶, 𝐷〉] ~R ↔ (𝐴 +P 𝐷) = (𝐵 +P 𝐶))) | ||
| Theorem | enrex 11108 | The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) | 
| ⊢ ~R ∈ V | ||
| Theorem | ltrelsr 11109 | Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) | 
| ⊢ <R ⊆ (R × R) | ||
| Theorem | addcmpblnr 11110 | Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) | 
| ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → 〈(𝐴 +P 𝐹), (𝐵 +P 𝐺)〉 ~R 〈(𝐶 +P 𝑅), (𝐷 +P 𝑆)〉)) | ||
| Theorem | mulcmpblnrlem 11111 | Lemma used in lemma showing compatibility of multiplication. (Contributed by NM, 4-Sep-1995.) (New usage is discouraged.) | 
| ⊢ (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆))))) | ||
| Theorem | mulcmpblnr 11112 | Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.) (New usage is discouraged.) | 
| ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → 〈((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)), ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹))〉 ~R 〈((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)), ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))〉)) | ||
| Theorem | prsrlem1 11113* | Decomposing signed reals into positive reals. Lemma for addsrpr 11116 and mulsrpr 11117. (Contributed by Jim Kingdon, 30-Dec-2019.) | 
| ⊢ (((𝐴 ∈ ((P × P) / ~R ) ∧ 𝐵 ∈ ((P × P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧ 𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧ (𝐴 = [〈𝑠, 𝑓〉] ~R ∧ 𝐵 = [〈𝑔, ℎ〉] ~R ))) → ((((𝑤 ∈ P ∧ 𝑣 ∈ P) ∧ (𝑠 ∈ P ∧ 𝑓 ∈ P)) ∧ ((𝑢 ∈ P ∧ 𝑡 ∈ P) ∧ (𝑔 ∈ P ∧ ℎ ∈ P))) ∧ ((𝑤 +P 𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔)))) | ||
| Theorem | addsrmo 11114* | There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.) | 
| ⊢ ((𝐴 ∈ ((P × P) / ~R ) ∧ 𝐵 ∈ ((P × P) / ~R )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧ 𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧ 𝑧 = [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉] ~R )) | ||
| Theorem | mulsrmo 11115* | There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.) | 
| ⊢ ((𝐴 ∈ ((P × P) / ~R ) ∧ 𝐵 ∈ ((P × P) / ~R )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧ 𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧ 𝑧 = [〈((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑡)), ((𝑤 ·P 𝑡) +P (𝑣 ·P 𝑢))〉] ~R )) | ||
| Theorem | addsrpr 11116 | Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) | 
| ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([〈𝐴, 𝐵〉] ~R +R [〈𝐶, 𝐷〉] ~R ) = [〈(𝐴 +P 𝐶), (𝐵 +P 𝐷)〉] ~R ) | ||
| Theorem | mulsrpr 11117 | Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) | 
| ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([〈𝐴, 𝐵〉] ~R ·R [〈𝐶, 𝐷〉] ~R ) = [〈((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))〉] ~R ) | ||
| Theorem | ltsrpr 11118 | Ordering of signed reals in terms of positive reals. (Contributed by NM, 20-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) | 
| ⊢ ([〈𝐴, 𝐵〉] ~R <R [〈𝐶, 𝐷〉] ~R ↔ (𝐴 +P 𝐷)<P (𝐵 +P 𝐶)) | ||
| Theorem | gt0srpr 11119 | Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) | 
| ⊢ (0R <R [〈𝐴, 𝐵〉] ~R ↔ 𝐵<P 𝐴) | ||
| Theorem | 0nsr 11120 | The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) | 
| ⊢ ¬ ∅ ∈ R | ||
| Theorem | 0r 11121 | The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) | 
| ⊢ 0R ∈ R | ||
| Theorem | 1sr 11122 | The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) | 
| ⊢ 1R ∈ R | ||
| Theorem | m1r 11123 | The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) | 
| ⊢ -1R ∈ R | ||
| Theorem | addclsr 11124 | Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 +R 𝐵) ∈ R) | ||
| Theorem | mulclsr 11125 | Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 ·R 𝐵) ∈ R) | ||
| Theorem | dmaddsr 11126 | Domain of addition on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) | 
| ⊢ dom +R = (R × R) | ||
| Theorem | dmmulsr 11127 | Domain of multiplication on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) | 
| ⊢ dom ·R = (R × R) | ||
| Theorem | addcomsr 11128 | Addition of signed reals is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) | 
| ⊢ (𝐴 +R 𝐵) = (𝐵 +R 𝐴) | ||
| Theorem | addasssr 11129 | Addition of signed reals is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) | 
| ⊢ ((𝐴 +R 𝐵) +R 𝐶) = (𝐴 +R (𝐵 +R 𝐶)) | ||
| Theorem | mulcomsr 11130 | Multiplication of signed reals is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) | 
| ⊢ (𝐴 ·R 𝐵) = (𝐵 ·R 𝐴) | ||
| Theorem | mulasssr 11131 | Multiplication of signed reals is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ·R 𝐵) ·R 𝐶) = (𝐴 ·R (𝐵 ·R 𝐶)) | ||
| Theorem | distrsr 11132 | Multiplication of signed reals is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) | 
| ⊢ (𝐴 ·R (𝐵 +R 𝐶)) = ((𝐴 ·R 𝐵) +R (𝐴 ·R 𝐶)) | ||
| Theorem | m1p1sr 11133 | Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) | 
| ⊢ (-1R +R 1R) = 0R | ||
| Theorem | m1m1sr 11134 | Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) | 
| ⊢ (-1R ·R -1R) = 1R | ||
| Theorem | ltsosr 11135 | Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.) (New usage is discouraged.) | 
| ⊢ <R Or R | ||
| Theorem | 0lt1sr 11136 | 0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.) | 
| ⊢ 0R <R 1R | ||
| Theorem | 1ne0sr 11137 | 1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.) | 
| ⊢ ¬ 1R = 0R | ||
| Theorem | 0idsr 11138 | The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.) | 
| ⊢ (𝐴 ∈ R → (𝐴 +R 0R) = 𝐴) | ||
| Theorem | 1idsr 11139 | 1 is an identity element for multiplication. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) | 
| ⊢ (𝐴 ∈ R → (𝐴 ·R 1R) = 𝐴) | ||
| Theorem | 00sr 11140 | A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.) | 
| ⊢ (𝐴 ∈ R → (𝐴 ·R 0R) = 0R) | ||
| Theorem | ltasr 11141 | Ordering property of addition. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) | 
| ⊢ (𝐶 ∈ R → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵))) | ||
| Theorem | pn0sr 11142 | A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) | 
| ⊢ (𝐴 ∈ R → (𝐴 +R (𝐴 ·R -1R)) = 0R) | ||
| Theorem | negexsr 11143* | Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) | 
| ⊢ (𝐴 ∈ R → ∃𝑥 ∈ R (𝐴 +R 𝑥) = 0R) | ||
| Theorem | recexsrlem 11144* | The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) | 
| ⊢ (0R <R 𝐴 → ∃𝑥 ∈ R (𝐴 ·R 𝑥) = 1R) | ||
| Theorem | addgt0sr 11145 | The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) | 
| ⊢ ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 +R 𝐵)) | ||
| Theorem | mulgt0sr 11146 | The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) | 
| ⊢ ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 ·R 𝐵)) | ||
| Theorem | sqgt0sr 11147 | The square of a nonzero signed real is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ R ∧ 𝐴 ≠ 0R) → 0R <R (𝐴 ·R 𝐴)) | ||
| Theorem | recexsr 11148* | The reciprocal of a nonzero signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ R ∧ 𝐴 ≠ 0R) → ∃𝑥 ∈ R (𝐴 ·R 𝑥) = 1R) | ||
| Theorem | mappsrpr 11149 | Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) | 
| ⊢ 𝐶 ∈ R ⇒ ⊢ ((𝐶 +R -1R) <R (𝐶 +R [〈𝐴, 1P〉] ~R ) ↔ 𝐴 ∈ P) | ||
| Theorem | ltpsrpr 11150 | Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) | 
| ⊢ 𝐶 ∈ R ⇒ ⊢ ((𝐶 +R [〈𝐴, 1P〉] ~R ) <R (𝐶 +R [〈𝐵, 1P〉] ~R ) ↔ 𝐴<P 𝐵) | ||
| Theorem | map2psrpr 11151* | Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) | 
| ⊢ 𝐶 ∈ R ⇒ ⊢ ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥 ∈ P (𝐶 +R [〈𝑥, 1P〉] ~R ) = 𝐴) | ||
| Theorem | supsrlem 11152* | Lemma for supremum theorem. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) | 
| ⊢ 𝐵 = {𝑤 ∣ (𝐶 +R [〈𝑤, 1P〉] ~R ) ∈ 𝐴} & ⊢ 𝐶 ∈ R ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) | ||
| Theorem | supsr 11153* | A nonempty, bounded set of signed reals has a supremum. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) | ||
| Syntax | cc 11154 | Class of complex numbers. | 
| class ℂ | ||
| Syntax | cr 11155 | Class of real numbers. | 
| class ℝ | ||
| Syntax | cc0 11156 | Extend class notation to include the complex number 0. | 
| class 0 | ||
| Syntax | c1 11157 | Extend class notation to include the complex number 1. | 
| class 1 | ||
| Syntax | ci 11158 | Extend class notation to include the complex number i. | 
| class i | ||
| Syntax | caddc 11159 | Addition on complex numbers. | 
| class + | ||
| Syntax | cltrr 11160 | 'Less than' predicate (defined over real subset of complex numbers). | 
| class <ℝ | ||
| Syntax | cmul 11161 | Multiplication on complex numbers. The token · is a center dot. | 
| class · | ||
| Definition | df-c 11162 | Define the set of complex numbers. The 23 axioms for complex numbers start at axresscn 11189. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) | 
| ⊢ ℂ = (R × R) | ||
| Definition | df-0 11163 | Define the complex number 0. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) | 
| ⊢ 0 = 〈0R, 0R〉 | ||
| Definition | df-1 11164 | Define the complex number 1. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) | 
| ⊢ 1 = 〈1R, 0R〉 | ||
| Definition | df-i 11165 | Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) | 
| ⊢ i = 〈0R, 1R〉 | ||
| Definition | df-r 11166 | Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) | 
| ⊢ ℝ = (R × {0R}) | ||
| Definition | df-add 11167* | Define addition over complex numbers. (Contributed by NM, 28-May-1995.) (New usage is discouraged.) | 
| ⊢ + = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))} | ||
| Definition | df-mul 11168* | Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) | 
| ⊢ · = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))〉))} | ||
| Definition | df-lt 11169* | Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr 11301. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) | 
| ⊢ <ℝ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = 〈𝑧, 0R〉 ∧ 𝑦 = 〈𝑤, 0R〉) ∧ 𝑧 <R 𝑤))} | ||
| Theorem | opelcn 11170 | Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) | 
| ⊢ (〈𝐴, 𝐵〉 ∈ ℂ ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R)) | ||
| Theorem | opelreal 11171 | Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) | 
| ⊢ (〈𝐴, 0R〉 ∈ ℝ ↔ 𝐴 ∈ R) | ||
| Theorem | elreal 11172* | Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) | 
| ⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R 〈𝑥, 0R〉 = 𝐴) | ||
| Theorem | elreal2 11173 | Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) | 
| ⊢ (𝐴 ∈ ℝ ↔ ((1st ‘𝐴) ∈ R ∧ 𝐴 = 〈(1st ‘𝐴), 0R〉)) | ||
| Theorem | 0ncn 11174 | The empty set is not a complex number. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) | 
| ⊢ ¬ ∅ ∈ ℂ | ||
| Theorem | ltrelre 11175 | 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) | 
| ⊢ <ℝ ⊆ (ℝ × ℝ) | ||
| Theorem | addcnsr 11176 | Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) (New usage is discouraged.) | 
| ⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (〈𝐴, 𝐵〉 + 〈𝐶, 𝐷〉) = 〈(𝐴 +R 𝐶), (𝐵 +R 𝐷)〉) | ||
| Theorem | mulcnsr 11177 | Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) | 
| ⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (〈𝐴, 𝐵〉 · 〈𝐶, 𝐷〉) = 〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉) | ||
| Theorem | eqresr 11178 | Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) | 
| ⊢ 𝐴 ∈ V ⇒ ⊢ (〈𝐴, 0R〉 = 〈𝐵, 0R〉 ↔ 𝐴 = 𝐵) | ||
| Theorem | addresr 11179 | Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (〈𝐴, 0R〉 + 〈𝐵, 0R〉) = 〈(𝐴 +R 𝐵), 0R〉) | ||
| Theorem | mulresr 11180 | Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (〈𝐴, 0R〉 · 〈𝐵, 0R〉) = 〈(𝐴 ·R 𝐵), 0R〉) | ||
| Theorem | ltresr 11181 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) | 
| ⊢ (〈𝐴, 0R〉 <ℝ 〈𝐵, 0R〉 ↔ 𝐴 <R 𝐵) | ||
| Theorem | ltresr2 11182 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (1st ‘𝐴) <R (1st ‘𝐵))) | ||
| Theorem | dfcnqs 11183 | Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 8824, which shows that the coset of the converse membership relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that ℂ is a quotient set, even though it is not (compare df-c 11162), and allows to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.) | 
| ⊢ ℂ = ((R × R) / ◡ E ) | ||
| Theorem | addcnsrec 11184 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 11183 and mulcnsrec 11185. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.) | 
| ⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([〈𝐴, 𝐵〉]◡ E + [〈𝐶, 𝐷〉]◡ E ) = [〈(𝐴 +R 𝐶), (𝐵 +R 𝐷)〉]◡ E ) | ||
| Theorem | mulcnsrec 11185 | Technical trick to permit re-use of some equivalence class lemmas for
     operation laws.  The trick involves ecid 8823,
which shows that the coset of
     the converse membership relation (which is not an equivalence relation)
     leaves a set unchanged.  See also dfcnqs 11183. Note: This is the last lemma (from which the axioms will be derived) in the construction of real and complex numbers. The construction starts at cnpi 10885. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.) | 
| ⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([〈𝐴, 𝐵〉]◡ E · [〈𝐶, 𝐷〉]◡ E ) = [〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉]◡ E ) | ||
| Theorem | axaddf 11186 | Addition is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axaddcl 11192. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 11235. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) | 
| ⊢ + :(ℂ × ℂ)⟶ℂ | ||
| Theorem | axmulf 11187 | Multiplication is an operation on the complex numbers. This is the construction-dependent version of ax-mulf 11236 and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific mulcl 11240. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) | 
| ⊢ · :(ℂ × ℂ)⟶ℂ | ||
| Theorem | axcnex 11188 | The complex numbers form a set. This axiom is redundant in the presence of the other axioms (see cnexALT 13029), but the proof requires the axiom of replacement, while the derivation from the construction here does not. Thus, we can avoid ax-rep 5278 in later theorems by invoking Axiom ax-cnex 11212 instead of cnexALT 13029. Use cnex 11237 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) | 
| ⊢ ℂ ∈ V | ||
| Theorem | axresscn 11189 | The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 11213. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.) | 
| ⊢ ℝ ⊆ ℂ | ||
| Theorem | ax1cn 11190 | 1 is a complex number. Axiom 2 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 11214. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.) | 
| ⊢ 1 ∈ ℂ | ||
| Theorem | axicn 11191 | i is a complex number. Axiom 3 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 11215. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.) | 
| ⊢ i ∈ ℂ | ||
| Theorem | axaddcl 11192 | Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcl 11216 be used later. Instead, in most cases use addcl 11238. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
| Theorem | axaddrcl 11193 | Closure law for addition in the real subfield of complex numbers. Axiom 5 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl 11217 be used later. Instead, in most cases use readdcl 11239. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
| Theorem | axmulcl 11194 | Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcl 11218 be used later. Instead, in most cases use mulcl 11240. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
| Theorem | axmulrcl 11195 | Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 11219 be used later. Instead, in most cases use remulcl 11241. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) | 
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
| Theorem | axmulcom 11196 | Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcom 11220 be used later. Instead, use mulcom 11242. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
| Theorem | axaddass 11197 | Addition of complex numbers is associative. This theorem transfers the associative laws for the real and imaginary signed real components of complex number pairs, to complex number addition itself. Axiom 9 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addass 11221 be used later. Instead, use addass 11243. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
| Theorem | axmulass 11198 | Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 11222. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
| Theorem | axdistr 11199 | Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 11223 be used later. Instead, use adddi 11245. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) | 
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
| Theorem | axi2m1 11200 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 11224. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) | 
| ⊢ ((i · i) + 1) = 0 | ||
| < Previous Next > | 
| Copyright terms: Public domain | < Previous Next > |