Home | Intuitionistic Logic Explorer Theorem List (p. 77 of 133) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | caucvgsrlemcau 7601* | Lemma for caucvgsr 7610. Defining the Cauchy condition in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.) |
⊢ (𝜑 → 𝐹:N⟶R) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) & ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚)) & ⊢ 𝐺 = (𝑥 ∈ N ↦ (℩𝑦 ∈ P (𝐹‘𝑥) = [〈(𝑦 +P 1P), 1P〉] ~R )) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐺‘𝑛)<P ((𝐺‘𝑘) +P 〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉) ∧ (𝐺‘𝑘)<P ((𝐺‘𝑛) +P 〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉)))) | ||
Theorem | caucvgsrlembound 7602* | Lemma for caucvgsr 7610. Defining the boundedness condition in terms of positive reals. (Contributed by Jim Kingdon, 25-Jun-2021.) |
⊢ (𝜑 → 𝐹:N⟶R) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) & ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚)) & ⊢ 𝐺 = (𝑥 ∈ N ↦ (℩𝑦 ∈ P (𝐹‘𝑥) = [〈(𝑦 +P 1P), 1P〉] ~R )) ⇒ ⊢ (𝜑 → ∀𝑚 ∈ N 1P<P (𝐺‘𝑚)) | ||
Theorem | caucvgsrlemgt1 7603* | Lemma for caucvgsr 7610. A Cauchy sequence whose terms are greater than one converges. (Contributed by Jim Kingdon, 22-Jun-2021.) |
⊢ (𝜑 → 𝐹:N⟶R) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) & ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N 𝑖 → ((𝐹‘𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑖) +R 𝑥))))) | ||
Theorem | caucvgsrlemoffval 7604* | Lemma for caucvgsr 7610. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
⊢ (𝜑 → 𝐹:N⟶R) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚)) & ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R))) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ((𝐺‘𝐽) +R 𝐴) = ((𝐹‘𝐽) +R 1R)) | ||
Theorem | caucvgsrlemofff 7605* | Lemma for caucvgsr 7610. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
⊢ (𝜑 → 𝐹:N⟶R) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚)) & ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R))) ⇒ ⊢ (𝜑 → 𝐺:N⟶R) | ||
Theorem | caucvgsrlemoffcau 7606* | Lemma for caucvgsr 7610. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
⊢ (𝜑 → 𝐹:N⟶R) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚)) & ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R))) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) | ||
Theorem | caucvgsrlemoffgt1 7607* | Lemma for caucvgsr 7610. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
⊢ (𝜑 → 𝐹:N⟶R) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚)) & ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R))) ⇒ ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐺‘𝑚)) | ||
Theorem | caucvgsrlemoffres 7608* | Lemma for caucvgsr 7610. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
⊢ (𝜑 → 𝐹:N⟶R) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚)) & ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥))))) | ||
Theorem | caucvgsrlembnd 7609* | Lemma for caucvgsr 7610. A Cauchy sequence with a lower bound converges. (Contributed by Jim Kingdon, 19-Jun-2021.) |
⊢ (𝜑 → 𝐹:N⟶R) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥))))) | ||
Theorem | caucvgsr 7610* |
A Cauchy sequence of signed reals with a modulus of convergence
converges to a signed real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies). The HoTT book
theorem has a modulus of
convergence (that is, a rate of convergence) specified by (11.2.9) in
HoTT whereas this theorem fixes the rate of convergence to say that
all terms after the nth term must be within 1 / 𝑛 of the nth term
(it should later be able to prove versions of this theorem with a
different fixed rate or a modulus of convergence supplied as a
hypothesis).
This is similar to caucvgprpr 7520 but is for signed reals rather than positive reals. Here is an outline of how we prove it: 1. Choose a lower bound for the sequence (see caucvgsrlembnd 7609). 2. Offset each element of the sequence so that each element of the resulting sequence is greater than one (greater than zero would not suffice, because the limit as well as the elements of the sequence need to be positive) (see caucvgsrlemofff 7605). 3. Since a signed real (element of R) which is greater than zero can be mapped to a positive real (element of P), perform that mapping on each element of the sequence and invoke caucvgprpr 7520 to get a limit (see caucvgsrlemgt1 7603). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 7603). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7608). (Contributed by Jim Kingdon, 20-Jun-2021.) |
⊢ (𝜑 → 𝐹:N⟶R) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥))))) | ||
Theorem | ltpsrprg 7611 | Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [〈𝐴, 1P〉] ~R ) <R (𝐶 +R [〈𝐵, 1P〉] ~R ) ↔ 𝐴<P 𝐵)) | ||
Theorem | mappsrprg 7612 | Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) |
⊢ ((𝐴 ∈ P ∧ 𝐶 ∈ R) → (𝐶 +R -1R) <R (𝐶 +R [〈𝐴, 1P〉] ~R )) | ||
Theorem | map2psrprg 7613* | Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) |
⊢ (𝐶 ∈ R → ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥 ∈ P (𝐶 +R [〈𝑥, 1P〉] ~R ) = 𝐴)) | ||
Theorem | suplocsrlemb 7614* | Lemma for suplocsr 7617. The set 𝐵 is located. (Contributed by Jim Kingdon, 18-Jan-2024.) |
⊢ 𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [〈𝑤, 1P〉] ~R ) ∈ 𝐴} & ⊢ (𝜑 → 𝐴 ⊆ R) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) & ⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦))) ⇒ ⊢ (𝜑 → ∀𝑢 ∈ P ∀𝑣 ∈ P (𝑢<P 𝑣 → (∃𝑞 ∈ 𝐵 𝑢<P 𝑞 ∨ ∀𝑞 ∈ 𝐵 𝑞<P 𝑣))) | ||
Theorem | suplocsrlempr 7615* | Lemma for suplocsr 7617. The set 𝐵 has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.) |
⊢ 𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [〈𝑤, 1P〉] ~R ) ∈ 𝐴} & ⊢ (𝜑 → 𝐴 ⊆ R) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) & ⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦))) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ P (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))) | ||
Theorem | suplocsrlem 7616* | Lemma for suplocsr 7617. The set 𝐴 has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.) |
⊢ 𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [〈𝑤, 1P〉] ~R ) ∈ 𝐴} & ⊢ (𝜑 → 𝐴 ⊆ R) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) & ⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) | ||
Theorem | suplocsr 7617* | An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.) |
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) & ⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) | ||
Syntax | cc 7618 | Class of complex numbers. |
class ℂ | ||
Syntax | cr 7619 | Class of real numbers. |
class ℝ | ||
Syntax | cc0 7620 | Extend class notation to include the complex number 0. |
class 0 | ||
Syntax | c1 7621 | Extend class notation to include the complex number 1. |
class 1 | ||
Syntax | ci 7622 | Extend class notation to include the complex number i. |
class i | ||
Syntax | caddc 7623 | Addition on complex numbers. |
class + | ||
Syntax | cltrr 7624 | 'Less than' predicate (defined over real subset of complex numbers). |
class <ℝ | ||
Syntax | cmul 7625 | Multiplication on complex numbers. The token · is a center dot. |
class · | ||
Definition | df-c 7626 | Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ ℂ = (R × R) | ||
Definition | df-0 7627 | Define the complex number 0. (Contributed by NM, 22-Feb-1996.) |
⊢ 0 = 〈0R, 0R〉 | ||
Definition | df-1 7628 | Define the complex number 1. (Contributed by NM, 22-Feb-1996.) |
⊢ 1 = 〈1R, 0R〉 | ||
Definition | df-i 7629 | Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.) |
⊢ i = 〈0R, 1R〉 | ||
Definition | df-r 7630 | Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ ℝ = (R × {0R}) | ||
Definition | df-add 7631* | Define addition over complex numbers. (Contributed by NM, 28-May-1995.) |
⊢ + = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))} | ||
Definition | df-mul 7632* | Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) |
⊢ · = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))〉))} | ||
Definition | df-lt 7633* | Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ <ℝ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = 〈𝑧, 0R〉 ∧ 𝑦 = 〈𝑤, 0R〉) ∧ 𝑧 <R 𝑤))} | ||
Theorem | opelcn 7634 | Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) |
⊢ (〈𝐴, 𝐵〉 ∈ ℂ ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R)) | ||
Theorem | opelreal 7635 | Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ (〈𝐴, 0R〉 ∈ ℝ ↔ 𝐴 ∈ R) | ||
Theorem | elreal 7636* | Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) |
⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R 〈𝑥, 0R〉 = 𝐴) | ||
Theorem | elrealeu 7637* | The real number mapping in elreal 7636 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.) |
⊢ (𝐴 ∈ ℝ ↔ ∃!𝑥 ∈ R 〈𝑥, 0R〉 = 𝐴) | ||
Theorem | elreal2 7638 | Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) |
⊢ (𝐴 ∈ ℝ ↔ ((1st ‘𝐴) ∈ R ∧ 𝐴 = 〈(1st ‘𝐴), 0R〉)) | ||
Theorem | 0ncn 7639 | 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. See also cnm 7640 which is a related property. (Contributed by NM, 2-May-1996.) |
⊢ ¬ ∅ ∈ ℂ | ||
Theorem | cnm 7640* | A complex number is an inhabited set. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by Jim Kingdon, 23-Oct-2023.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | ltrelre 7641 | 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ <ℝ ⊆ (ℝ × ℝ) | ||
Theorem | addcnsr 7642 | Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (〈𝐴, 𝐵〉 + 〈𝐶, 𝐷〉) = 〈(𝐴 +R 𝐶), (𝐵 +R 𝐷)〉) | ||
Theorem | mulcnsr 7643 | Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (〈𝐴, 𝐵〉 · 〈𝐶, 𝐷〉) = 〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉) | ||
Theorem | eqresr 7644 | Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (〈𝐴, 0R〉 = 〈𝐵, 0R〉 ↔ 𝐴 = 𝐵) | ||
Theorem | addresr 7645 | Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (〈𝐴, 0R〉 + 〈𝐵, 0R〉) = 〈(𝐴 +R 𝐵), 0R〉) | ||
Theorem | mulresr 7646 | Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (〈𝐴, 0R〉 · 〈𝐵, 0R〉) = 〈(𝐴 ·R 𝐵), 0R〉) | ||
Theorem | ltresr 7647 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
⊢ (〈𝐴, 0R〉 <ℝ 〈𝐵, 0R〉 ↔ 𝐴 <R 𝐵) | ||
Theorem | ltresr2 7648 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (1st ‘𝐴) <R (1st ‘𝐵))) | ||
Theorem | dfcnqs 7649 | Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 6494, which shows that the coset of the converse epsilon 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 7626), and allows us 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.) |
⊢ ℂ = ((R × R) / ◡ E ) | ||
Theorem | addcnsrec 7650 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7649 and mulcnsrec 7651. (Contributed by NM, 13-Aug-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([〈𝐴, 𝐵〉]◡ E + [〈𝐶, 𝐷〉]◡ E ) = [〈(𝐴 +R 𝐶), (𝐵 +R 𝐷)〉]◡ E ) | ||
Theorem | mulcnsrec 7651 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6493, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7649. (Contributed by NM, 13-Aug-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([〈𝐴, 𝐵〉]◡ E · [〈𝐶, 𝐷〉]◡ E ) = [〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉]◡ E ) | ||
Theorem | addvalex 7652 | Existence of a sum. This is dependent on how we define + so once we proceed to real number axioms we will replace it with theorems such as addcl 7745. (Contributed by Jim Kingdon, 14-Jul-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 + 𝐵) ∈ V) | ||
Theorem | pitonnlem1 7653* | Lemma for pitonn 7656. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.) |
⊢ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈1o, 1o〉] ~Q }, {𝑢 ∣ [〈1o, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 = 1 | ||
Theorem | pitonnlem1p1 7654 | Lemma for pitonn 7656. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.) |
⊢ (𝐴 ∈ P → [〈(𝐴 +P (1P +P 1P)), (1P +P 1P)〉] ~R = [〈(𝐴 +P 1P), 1P〉] ~R ) | ||
Theorem | pitonnlem2 7655* | Lemma for pitonn 7656. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.) |
⊢ (𝐾 ∈ N → (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉] ~Q }, {𝑢 ∣ [〈𝐾, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 + 1) = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈(𝐾 +N 1o), 1o〉] ~Q }, {𝑢 ∣ [〈(𝐾 +N 1o), 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) | ||
Theorem | pitonn 7656* | Mapping from N to ℕ. (Contributed by Jim Kingdon, 22-Apr-2020.) |
⊢ (𝑁 ∈ N → 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉] ~Q }, {𝑢 ∣ [〈𝑁, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) | ||
Theorem | pitoregt0 7657* | Embedding from N to ℝ yields a number greater than zero. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ (𝑁 ∈ N → 0 <ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉] ~Q }, {𝑢 ∣ [〈𝑁, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) | ||
Theorem | pitore 7658* | Embedding from N to ℝ. Similar to pitonn 7656 but separate in the sense that we have not proved nnssre 8724 yet. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ (𝑁 ∈ N → 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉] ~Q }, {𝑢 ∣ [〈𝑁, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 ∈ ℝ) | ||
Theorem | recnnre 7659* | Embedding the reciprocal of a natural number into ℝ. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ (𝑁 ∈ N → 〈[〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑁, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑁, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 ∈ ℝ) | ||
Theorem | peano1nnnn 7660* | One is an element of ℕ. This is a counterpart to 1nn 8731 designed for real number axioms which involve natural numbers (notably, axcaucvg 7708). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ 1 ∈ 𝑁 | ||
Theorem | peano2nnnn 7661* | A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 8732 designed for real number axioms which involve to natural numbers (notably, axcaucvg 7708). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ (𝐴 ∈ 𝑁 → (𝐴 + 1) ∈ 𝑁) | ||
Theorem | ltrennb 7662* | Ordering of natural numbers with <N or <ℝ. (Contributed by Jim Kingdon, 13-Jul-2021.) |
⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → (𝐽 <N 𝐾 ↔ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐽, 1o〉] ~Q }, {𝑢 ∣ [〈𝐽, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 <ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉] ~Q }, {𝑢 ∣ [〈𝐾, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉)) | ||
Theorem | ltrenn 7663* | Ordering of natural numbers with <N or <ℝ. (Contributed by Jim Kingdon, 12-Jul-2021.) |
⊢ (𝐽 <N 𝐾 → 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐽, 1o〉] ~Q }, {𝑢 ∣ [〈𝐽, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 <ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉] ~Q }, {𝑢 ∣ [〈𝐾, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) | ||
Theorem | recidpipr 7664* | Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.) |
⊢ (𝑁 ∈ N → (〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉] ~Q }, {𝑢 ∣ [〈𝑁, 1o〉] ~Q <Q 𝑢}〉 ·P 〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑁, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑁, 1o〉] ~Q ) <Q 𝑢}〉) = 1P) | ||
Theorem | recidpirqlemcalc 7665 | Lemma for recidpirq 7666. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.) |
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → (𝐴 ·P 𝐵) = 1P) ⇒ ⊢ (𝜑 → ((((𝐴 +P 1P) ·P (𝐵 +P 1P)) +P (1P ·P 1P)) +P 1P) = ((((𝐴 +P 1P) ·P 1P) +P (1P ·P (𝐵 +P 1P))) +P (1P +P 1P))) | ||
Theorem | recidpirq 7666* | A real number times its reciprocal is one, where reciprocal is expressed with *Q. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ (𝑁 ∈ N → (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉] ~Q }, {𝑢 ∣ [〈𝑁, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 · 〈[〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑁, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑁, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) = 1) | ||
Theorem | axcnex 7667 | The complex numbers form a set. Use cnex 7744 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
⊢ ℂ ∈ V | ||
Theorem | axresscn 7668 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 7712. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.) |
⊢ ℝ ⊆ ℂ | ||
Theorem | ax1cn 7669 | 1 is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 7713. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.) |
⊢ 1 ∈ ℂ | ||
Theorem | ax1re 7670 |
1 is a real number. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-1re 7714.
In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 7713 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
⊢ 1 ∈ ℝ | ||
Theorem | axicn 7671 | i is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 7715. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.) |
⊢ i ∈ ℂ | ||
Theorem | axaddcl 7672 | Closure law for addition of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcl 7716 be used later. Instead, in most cases use addcl 7745. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | axaddrcl 7673 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl 7717 be used later. Instead, in most cases use readdcl 7746. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | axmulcl 7674 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcl 7718 be used later. Instead, in most cases use mulcl 7747. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | axmulrcl 7675 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 7719 be used later. Instead, in most cases use remulcl 7748. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Theorem | axaddf 7676 | 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 7672. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 7742. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) |
⊢ + :(ℂ × ℂ)⟶ℂ | ||
Theorem | axmulf 7677 | Multiplication 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 axmulcl 7674. This construction-dependent theorem should not be referenced directly; instead, use ax-mulf 7743. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) |
⊢ · :(ℂ × ℂ)⟶ℂ | ||
Theorem | axaddcom 7678 |
Addition commutes. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly, nor should the proven axiom ax-addcom 7720 be used later.
Instead, use addcom 7899.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | axmulcom 7679 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcom 7721 be used later. Instead, use mulcom 7749. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | axaddass 7680 | 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 for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addass 7722 be used later. Instead, use addass 7750. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | axmulass 7681 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 7723. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | axdistr 7682 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 7724 be used later. Instead, use adddi 7752. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | axi2m1 7683 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 7725. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
⊢ ((i · i) + 1) = 0 | ||
Theorem | ax0lt1 7684 |
0 is less than 1. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-0lt1 7726.
The version of this axiom in the Metamath Proof Explorer reads 1 ≠ 0; here we change it to 0 <ℝ 1. The proof of 0 <ℝ 1 from 1 ≠ 0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ 0 <ℝ 1 | ||
Theorem | ax1rid 7685 | 1 is an identity element for real multiplication. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 7727. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
Theorem | ax0id 7686 |
0 is an identity element for real addition. Axiom for
real and
complex numbers, derived from set theory. This construction-dependent
theorem should not be referenced directly; instead, use ax-0id 7728.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | ||
Theorem | axrnegex 7687* | Existence of negative of real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex 7729. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Theorem | axprecex 7688* |
Existence of positive reciprocal of positive real number. Axiom for
real and complex numbers, derived from set theory. This
construction-dependent theorem should not be referenced directly;
instead, use ax-precex 7730.
In treatments which assume excluded middle, the 0 <ℝ 𝐴 condition is generally replaced by 𝐴 ≠ 0, and it may not be necessary to state that the reciproacal is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃𝑥 ∈ ℝ (0 <ℝ 𝑥 ∧ (𝐴 · 𝑥) = 1)) | ||
Theorem | axcnre 7689* | 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, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre 7731. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | axpre-ltirr 7690 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 7732. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴) | ||
Theorem | axpre-ltwlin 7691 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 7733. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵))) | ||
Theorem | axpre-lttrn 7692 | Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 7734. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) | ||
Theorem | axpre-apti 7693 |
Apartness of reals is tight. Axiom for real and complex numbers,
derived from set theory. This construction-dependent theorem should not
be referenced directly; instead, use ax-pre-apti 7735.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵) | ||
Theorem | axpre-ltadd 7694 | Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 7736. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | ||
Theorem | axpre-mulgt0 7695 | The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 7737. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵))) | ||
Theorem | axpre-mulext 7696 |
Strong extensionality of multiplication (expressed in terms of
<ℝ). Axiom for real and
complex numbers, derived from set theory.
This construction-dependent theorem should not be referenced directly;
instead, use ax-pre-mulext 7738.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴))) | ||
Theorem | rereceu 7697* | The reciprocal from axprecex 7688 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) | ||
Theorem | recriota 7698* | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) |
⊢ (𝑁 ∈ N → (℩𝑟 ∈ ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉] ~Q }, {𝑢 ∣ [〈𝑁, 1o〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 · 𝑟) = 1) = 〈[〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑁, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑁, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) | ||
Theorem | axarch 7699* |
Archimedean axiom. The Archimedean property is more naturally stated
once we have defined ℕ. Unless we find
another way to state it,
we'll just use the right hand side of dfnn2 8722 in stating what we mean by
"natural number" in the context of this axiom.
This construction-dependent theorem should not be referenced directly; instead, use ax-arch 7739. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛) | ||
Theorem | peano5nnnn 7700* | Peano's inductive postulate. This is a counterpart to peano5nni 8723 designed for real number axioms which involve natural numbers (notably, axcaucvg 7708). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ ((1 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝑧 + 1) ∈ 𝐴) → 𝑁 ⊆ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |