Beginning of Section SurComplex
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
tag.
Definition. We define
SNo_pair to be
pair_tag {2} of type
set → set → set.
Axiom. (
SNo_pair_0) We take the following as an axiom:
Definition. We define
CSNo to be
CD_carr {2} SNo of type
set → prop.
Axiom. (
CSNo_I) We take the following as an axiom:
Axiom. (
CSNo_E) We take the following as an axiom:
Axiom. (
SNo_CSNo) We take the following as an axiom:
Axiom. (
CSNo_0) We take the following as an axiom:
Axiom. (
CSNo_1) We take the following as an axiom:
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {2}
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo.
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo.
Notation. We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat.
Definition. We define
CSNo_Re to be
CD_proj0 {2} SNo of type
set → set.
Definition. We define
CSNo_Im to be
CD_proj1 {2} SNo of type
set → set.
Axiom. (
CSNo_Re1) We take the following as an axiom:
∀z, CSNo z → SNo (Re z) ∧ ∃y, SNo y ∧ z = pa (Re z) y
Axiom. (
CSNo_Re2) We take the following as an axiom:
∀x y, SNo x → SNo y → Re (pa x y) = x
Axiom. (
CSNo_Im1) We take the following as an axiom:
∀z, CSNo z → SNo (Im z) ∧ z = pa (Re z) (Im z)
Axiom. (
CSNo_Im2) We take the following as an axiom:
∀x y, SNo x → SNo y → Im (pa x y) = y
Axiom. (
CSNo_ReR) We take the following as an axiom:
Axiom. (
CSNo_ImR) We take the following as an axiom:
Axiom. (
CSNo_ReIm) We take the following as an axiom:
∀z, CSNo z → z = pa (Re z) (Im z)
Axiom. (
CSNo_ReIm_split) We take the following as an axiom:
∀z w, CSNo z → CSNo w → Re z = Re w → Im z = Im w → z = w
Definition. We define
CSNoLev to be
λz ⇒ SNoLev (Re z) ∪ SNoLev (Im z) of type
set → set.
Let conj : set → set ≝ λx ⇒ x
Definition. We define
minus_CSNo to be
CD_minus {2} SNo minus_SNo of type
set → set.
Definition. We define
conj_CSNo to be
CD_conj {2} SNo minus_SNo conj of type
set → set.
Definition. We define
add_CSNo to be
CD_add {2} SNo add_SNo of type
set → set → set.
Definition. We define
mul_CSNo to be
CD_mul {2} SNo minus_SNo conj add_SNo mul_SNo of type
set → set → set.
Definition. We define
exp_CSNo_nat to be
CD_exp_nat {2} SNo minus_SNo conj add_SNo mul_SNo of type
set → set → set.
Definition. We define
abs_sqr_CSNo to be
λz ⇒ Re z ^ 2 + Im z ^ 2 of type
set → set.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
minus_CSNo.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
conj_CSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_CSNo.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_CSNo.
Notation. We use
:^: as an infix operator with priority 355 and which associates to the right corresponding to applying term
exp_CSNo_nat.
Axiom. (
add_CSNo_CRe) We take the following as an axiom:
∀z w, CSNo z → CSNo w → Re (plus' z w) = Re z + Re w
Axiom. (
add_CSNo_CIm) We take the following as an axiom:
∀z w, CSNo z → CSNo w → Im (plus' z w) = Im z + Im w
Axiom. (
mul_CSNo_CRe) We take the following as an axiom:
∀z w, CSNo z → CSNo w → Re (mult' z w) = Re z * Re w + - (Im w * Im z)
Axiom. (
mul_CSNo_CIm) We take the following as an axiom:
∀z w, CSNo z → CSNo w → Im (mult' z w) = Im w * Re z + Im z * Re w
Axiom. (
SNo_Re) We take the following as an axiom:
∀x, SNo x → Re x = x
Axiom. (
SNo_Im) We take the following as an axiom:
∀x, SNo x → Im x = 0
Axiom. (
Re_0) We take the following as an axiom:
Re 0 = 0
Axiom. (
Im_0) We take the following as an axiom:
Im 0 = 0
Axiom. (
Re_1) We take the following as an axiom:
Re 1 = 1
Axiom. (
Im_1) We take the following as an axiom:
Im 1 = 0
Axiom. (
Re_i) We take the following as an axiom:
Re i = 0
Axiom. (
Im_i) We take the following as an axiom:
Im i = 1
Axiom. (
conj_CSNo_0) We take the following as an axiom:
Axiom. (
conj_CSNo_1) We take the following as an axiom:
Axiom. (
conj_CSNo_i) We take the following as an axiom:
Axiom. (
add_CSNo_add_SNo) We take the following as an axiom:
∀x y, SNo x → SNo y → x + y = x + y
Axiom. (
mul_CSNo_mul_SNo) We take the following as an axiom:
∀x y, SNo x → SNo y → x ⨯ y = x * y
Axiom. (
add_CSNo_0L) We take the following as an axiom:
Axiom. (
add_CSNo_0R) We take the following as an axiom:
Axiom. (
mul_CSNo_0R) We take the following as an axiom:
Axiom. (
mul_CSNo_0L) We take the following as an axiom:
Axiom. (
mul_CSNo_1R) We take the following as an axiom:
Axiom. (
mul_CSNo_1L) We take the following as an axiom:
Axiom. (
exp_CSNo_nat_S) We take the following as an axiom:
∀z n, nat_p n → z(ordsucc n) = z ⨯ zn
Axiom. (
add_SNo_rotate_4_0312) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) + (z + w) = (x + w) + (y + z)
Axiom. (
sqrt_SNo_nonneg_mon_strict) We take the following as an axiom:
∀x y, SNo x → SNo y → 0 ≤ x → x < y → sqrt_SNo_nonneg x < sqrt_SNo_nonneg y
Axiom. (
sqrt_SNo_nonneg_mon) We take the following as an axiom:
∀x y, SNo x → SNo y → 0 ≤ x → x ≤ y → sqrt_SNo_nonneg x ≤ sqrt_SNo_nonneg y
Axiom. (
sqrt_SNo_nonneg_mul_SNo) We take the following as an axiom:
∀x y, SNo x → SNo y → 0 ≤ x → 0 ≤ y → sqrt_SNo_nonneg (x * y) = sqrt_SNo_nonneg x * sqrt_SNo_nonneg y
End of Section SurComplex
Beginning of Section Complex
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_CSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_CSNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_CSNo.
Notation. We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt.
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe.
Definition. We define
complex to be
{pa (u 0) (u 1)|u ∈ real ⨯ real} of type
set.
Axiom. (
complex_I) We take the following as an axiom:
Axiom. (
complex_E) We take the following as an axiom:
∀z ∈ complex, ∀p : prop, (∀x y ∈ real, z = pa x y → p) → p
Axiom. (
complex_0) We take the following as an axiom:
Axiom. (
complex_1) We take the following as an axiom:
Axiom. (
complex_i) We take the following as an axiom:
Axiom. (
complex_Re_eq) We take the following as an axiom:
∀x y ∈ real, Re (pa x y) = x
Axiom. (
complex_Im_eq) We take the following as an axiom:
∀x y ∈ real, Im (pa x y) = y
Axiom. (
real_Re_eq) We take the following as an axiom:
Axiom. (
real_Im_eq) We take the following as an axiom:
Axiom. (
mul_i_real_eq) We take the following as an axiom:
∀x ∈ real, i * x = pa 0 x
Axiom. (
real_Re_i_eq) We take the following as an axiom:
∀x ∈ real, Re (i * x) = 0
Axiom. (
real_Im_i_eq) We take the following as an axiom:
∀x ∈ real, Im (i * x) = x
Axiom. (
complex_eta) We take the following as an axiom:
Beginning of Section ComplexDiv
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo.
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo.
Notation. We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat.
End of Section ComplexDiv
End of Section Complex