Beginning of Section Tags
Variable tagn : set
Hypothesis tagn_nat : nat_p tagn
Hypothesis tagn_1 : 1 ∈ tagn
Theorem. (not_TransSet_Sing_tagn)
¬ TransSet {tagn}
In Proofgold the corresponding term root is 774f46... and proposition id is 749b5c...
Proof:
Assume H1: TransSet {tagn}.
We prove the intermediate claim L1: 0 ∈ {tagn}.
Apply H1 tagn (SingI tagn) to the current goal.
We will prove 0 ∈ tagn.
An exact proof term for the current goal is nat_trans tagn tagn_nat 1 tagn_1 0 In_0_1.
Apply In_no2cycle 0 1 In_0_1 to the current goal.
We will prove 1 ∈ 0.
rewrite the current goal using SingE tagn 0 L1 (from left to right) at position 2.
We will prove 1 ∈ tagn.
An exact proof term for the current goal is tagn_1.
∎
Theorem. (not_ordinal_Sing_tagn)
¬ ordinal {tagn}
In Proofgold the corresponding term root is 14d4ad... and proposition id is caf993...
Proof:
Assume H1.
Apply H1 to the current goal.
Assume H2 _.
An exact proof term for the current goal is not_TransSet_Sing_tagn H2.
∎
End of Section Tags
Beginning of Section ExtendedSNo
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 ExtendedSNoElt_ to be λn x ⇒ ∀v ∈ ⋃ x, ordinal v ∨ ∃i ∈ n, v = {i} of type set → set → prop.
In Proofgold the corresponding term root is 13321a... and object id is 8abcfe...
Theorem. (extension_SNoElt_mon)
∀M N, M ⊆ N → ∀x, ExtendedSNoElt_ M x → ExtendedSNoElt_ N x
In Proofgold the corresponding term root is 96f031... and proposition id is 11c5b8...
Proof:
Let M and N be given.
Assume HMN.
Let x be given.
Assume Hx.
Let v be given.
Assume Hv.
Apply Hx v Hv to the current goal.
Assume H1: ordinal v.
We will prove ordinal v ∨ ∃i ∈ N, v = {i}.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
Assume H.
Apply H to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ M.
Assume H1: v = {i}.
We will prove ordinal v ∨ ∃i ∈ N, v = {i}.
Apply orIR to the current goal.
We use i to witness the existential quantifier.
Apply andI to the current goal.
We will prove i ∈ N.
An exact proof term for the current goal is HMN i Hi.
An exact proof term for the current goal is H1.
∎
Theorem. (Sing_nat_fresh_extension)
∀n, nat_p n → 1 ∈ n → ∀x, ExtendedSNoElt_ n x → ∀u ∈ x, {n} ∉ u
In Proofgold the corresponding term root is 18d72f... and proposition id is a0507f...
Proof:
Let n be given.
Assume Hn.
Assume Hn1: 1 ∈ n.
Let x be given.
Assume Hx.
Let u be given.
Assume Hu.
Assume H1: {n} ∈ u.
We prove the intermediate claim L1: {n} ∈ ⋃ x.
An exact proof term for the current goal is UnionI x {n} u H1 Hu.
Apply Hx {n} L1 to the current goal.
An exact proof term for the current goal is not_ordinal_Sing_tagn n Hn Hn1.
Assume H.
Apply H to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ n.
Assume H2: {n} = {i}.
Apply In_irref i to the current goal.
rewrite the current goal using Sing_inj n i H2 (from right to left) at position 2.
An exact proof term for the current goal is Hi.
∎
Theorem. (SNo_ExtendedSNoElt_2)
∀x, SNo x → ExtendedSNoElt_ 2 x
In Proofgold the corresponding term root is 16e5e3... and proposition id is 778d84...
Proof:
Let x be given.
Assume Hx.
Let v be given.
Assume Hv.
We will prove ordinal v ∨ ∃i ∈ 2, v = {i}.
Apply UnionE_impred x v Hv to the current goal.
Let u be given.
Assume H1: v ∈ u.
Assume H2: u ∈ x.
Apply SNoLev_ x Hx to the current goal.
Assume H3: x ⊆ SNoElts_ (SNoLev x).
Assume _.
Apply binunionE (SNoLev x) {beta '|beta ∈ SNoLev x} u (H3 u H2) to the current goal.
Assume H4: u ∈ SNoLev x.
We prove the intermediate claim Luo: ordinal u.
An exact proof term for the current goal is ordinal_Hered (SNoLev x) (SNoLev_ordinal x Hx) u H4.
We will prove ordinal v ∨ ∃i ∈ 2, v = {i}.
Apply orIL to the current goal.
An exact proof term for the current goal is ordinal_Hered u Luo v H1.
Assume H4: u ∈ {beta '|beta ∈ SNoLev x}.
Apply ReplE_impred (SNoLev x) tag u H4 to the current goal.
Let beta be given.
Assume Hb: beta ∈ SNoLev x.
Assume Hub: u = beta '.
We prove the intermediate claim Lv: v ∈ beta '.
rewrite the current goal using Hub (from right to left).
An exact proof term for the current goal is H1.
Apply binunionE beta {{1}} v Lv to the current goal.
Assume H5: v ∈ beta.
We prove the intermediate claim Lbo: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (SNoLev x) (SNoLev_ordinal x Hx) beta Hb.
We will prove ordinal v ∨ ∃i ∈ 2, v = {i}.
Apply orIL to the current goal.
An exact proof term for the current goal is ordinal_Hered beta Lbo v H5.
Assume H5: v ∈ {{1}}.
We will prove ordinal v ∨ ∃i ∈ 2, v = {i}.
Apply orIR to the current goal.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is In_1_2.
We will prove v = {1}.
An exact proof term for the current goal is SingE {1} v H5.
∎
End of Section ExtendedSNo
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.
Theorem. (complex_tag_fresh)
∀x, SNo x → ∀u ∈ x, {2} ∉ u
In Proofgold the corresponding term root is 3d8064... and proposition id is e01e5b...
Proof:
Let x be given.
Assume Hx.
Apply Sing_nat_fresh_extension 2 nat_2 In_1_2 x to the current goal.
We will prove ExtendedSNoElt_ 2 x.
An exact proof term for the current goal is SNo_ExtendedSNoElt_2 x Hx.
∎
Definition. We define SNo_pair to be pair_tag {2} of type set → set → set.
In Proofgold the corresponding term root is 7a69f6... and object id is 23fbcd...
Theorem. (SNo_pair_0)
∀x, SNo_pair x 0 = x
In Proofgold the corresponding term root is 1cb458... and proposition id is f7bb55...
Proof:
An exact proof term for the current goal is pair_tag_0 {2} SNo complex_tag_fresh.
∎
Theorem. (SNo_pair_prop_1)
∀x1 y1 x2 y2, SNo x1 → SNo x2 → SNo_pair x1 y1 = SNo_pair x2 y2 → x1 = x2
In Proofgold the corresponding term root is 070aac... and proposition id is b7a761...
Proof:
An exact proof term for the current goal is pair_tag_prop_1 {2} SNo complex_tag_fresh.
∎
Theorem. (SNo_pair_prop_2)
∀x1 y1 x2 y2, SNo x1 → SNo y1 → SNo x2 → SNo y2 → SNo_pair x1 y1 = SNo_pair x2 y2 → y1 = y2
In Proofgold the corresponding term root is 3e9308... and proposition id is f4146d...
Proof:
An exact proof term for the current goal is pair_tag_prop_2 {2} SNo complex_tag_fresh.
∎
Definition. We define CSNo to be CD_carr {2} SNo of type set → prop.
In Proofgold the corresponding term root is 4235a7... and object id is a08f56...
Theorem. (CSNo_I)
∀x y, SNo x → SNo y → CSNo (SNo_pair x y)
In Proofgold the corresponding term root is cad32d... and proposition id is dd6f38...
Proof:
An exact proof term for the current goal is CD_carr_I {2} SNo complex_tag_fresh.
∎
Theorem. (CSNo_E)
∀z, CSNo z → ∀p : set → prop, (∀x y, SNo x → SNo y → z = SNo_pair x y → p (SNo_pair x y)) → p z
In Proofgold the corresponding term root is cc5af4... and proposition id is 58f9bd...
Proof:
An exact proof term for the current goal is CD_carr_E {2} SNo complex_tag_fresh.
∎
Theorem. (SNo_CSNo)
∀x, SNo x → CSNo x
In Proofgold the corresponding term root is 9b0483... and proposition id is 04d332...
Proof:
An exact proof term for the current goal is CD_carr_0ext {2} SNo complex_tag_fresh SNo_0.
∎
Theorem. (CSNo_0)
CSNo 0
In Proofgold the corresponding term root is 77c1b5... and proposition id is fc59ef...
Proof:
Apply SNo_CSNo to the current goal.
An exact proof term for the current goal is SNo_0.
∎
Theorem. (CSNo_1)
CSNo 1
In Proofgold the corresponding term root is 8cf686... and proposition id is 14c184...
Proof:
Apply SNo_CSNo to the current goal.
An exact proof term for the current goal is SNo_1.
∎
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {2}
Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.
Theorem. (CSNo_ExtendedSNoElt_3)
∀z, CSNo z → ExtendedSNoElt_ 3 z
In Proofgold the corresponding term root is 5700d1... and proposition id is 4b578b...
Proof:
Let z be given.
Assume Hz.
Apply CSNo_E z Hz to the current goal.
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hzxy: z = SNo_pair x y.
Let v be given.
Assume Hv: v ∈ ⋃ (SNo_pair x y).
Apply UnionE_impred (SNo_pair x y) v Hv to the current goal.
Let u be given.
Assume H1: v ∈ u.
Assume H2: u ∈ SNo_pair x y.
Apply binunionE x {w ''|w ∈ y} u H2 to the current goal.
Assume H3: u ∈ x.
We prove the intermediate claim L1: v ∈ ⋃ x.
An exact proof term for the current goal is UnionI x v u H1 H3.
We will prove ordinal v ∨ ∃i ∈ 3, v = {i}.
An exact proof term for the current goal is extension_SNoElt_mon 2 3 (ordsuccI1 2) x (SNo_ExtendedSNoElt_2 x Hx) v L1.
Assume H3: u ∈ {w ''|w ∈ y}.
Apply ReplE_impred y ctag u H3 to the current goal.
Let w be given.
Assume Hw: w ∈ y.
Assume H4: u = w ''.
We prove the intermediate claim L2: v ∈ w ''.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H1.
Apply binunionE w {{2}} v L2 to the current goal.
Assume H5: v ∈ w.
We prove the intermediate claim L3: v ∈ ⋃ y.
An exact proof term for the current goal is UnionI y v w H5 Hw.
An exact proof term for the current goal is extension_SNoElt_mon 2 3 (ordsuccI1 2) y (SNo_ExtendedSNoElt_2 y Hy) v L3.
Assume H5: v ∈ {{2}}.
We will prove ordinal v ∨ ∃i ∈ 3, v = {i}.
Apply orIR to the current goal.
We use 2 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 2 ∈ 3.
An exact proof term for the current goal is In_2_3.
We will prove v = {2}.
An exact proof term for the current goal is SingE {2} v H5.
∎
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 Complex_i to be SNo_pair 0 1 of type set.
In Proofgold the corresponding term root is ace1d5... and object id is 04654a...
Definition. We define CSNo_Re to be CD_proj0 {2} SNo of type set → set.
In Proofgold the corresponding term root is a3c3be... and object id is 39e73f...
Definition. We define CSNo_Im to be CD_proj1 {2} SNo of type set → set.
In Proofgold the corresponding term root is 9a1a1e... and object id is 784bb4...
Let i ≝ Complex_i
Let Re : set → set ≝ CSNo_Re
Let Im : set → set ≝ CSNo_Im
Let pa : set → set → set ≝ SNo_pair
Theorem. (CSNo_Re1)
∀z, CSNo z → SNo (Re z) ∧ ∃y, SNo y ∧ z = pa (Re z) y
In Proofgold the corresponding term root is 107683... and proposition id is 6e4a86...
Proof:
An exact proof term for the current goal is CD_proj0_1 {2} SNo complex_tag_fresh.
∎
Theorem. (CSNo_Re2)
∀x y, SNo x → SNo y → Re (pa x y) = x
In Proofgold the corresponding term root is d6dd63... and proposition id is c7769d...
Proof:
An exact proof term for the current goal is CD_proj0_2 {2} SNo complex_tag_fresh.
∎
Theorem. (CSNo_Im1)
∀z, CSNo z → SNo (Im z) ∧ z = pa (Re z) (Im z)
In Proofgold the corresponding term root is e5de1d... and proposition id is 63974e...
Proof:
An exact proof term for the current goal is CD_proj1_1 {2} SNo complex_tag_fresh.
∎
Theorem. (CSNo_Im2)
∀x y, SNo x → SNo y → Im (pa x y) = y
In Proofgold the corresponding term root is 01dd37... and proposition id is 71ee31...
Proof:
An exact proof term for the current goal is CD_proj1_2 {2} SNo complex_tag_fresh.
∎
Theorem. (CSNo_ReR)
∀z, CSNo z → SNo (Re z)
In Proofgold the corresponding term root is 6ff298... and proposition id is 39509b...
Proof:
An exact proof term for the current goal is CD_proj0R {2} SNo complex_tag_fresh.
∎
Theorem. (CSNo_ImR)
∀z, CSNo z → SNo (Im z)
In Proofgold the corresponding term root is c1dc53... and proposition id is f2d16d...
Proof:
An exact proof term for the current goal is CD_proj1R {2} SNo complex_tag_fresh.
∎
Theorem. (CSNo_ReIm)
∀z, CSNo z → z = pa (Re z) (Im z)
In Proofgold the corresponding term root is 06dc6f... and proposition id is 1fdc97...
Proof:
An exact proof term for the current goal is CD_proj0proj1_eta {2} SNo complex_tag_fresh.
∎
Theorem. (CSNo_ReIm_split)
∀z w, CSNo z → CSNo w → Re z = Re w → Im z = Im w → z = w
In Proofgold the corresponding term root is b4ba0e... and proposition id is 5191fd...
Proof:
An exact proof term for the current goal is CD_proj0proj1_split {2} SNo complex_tag_fresh.
∎
Definition. We define CSNoLev to be λz ⇒ SNoLev (Re z) ∪ SNoLev (Im z) of type set → set.
In Proofgold the corresponding term root is f29582... and object id is 5ebbe9...
Theorem. (CSNoLev_ordinal)
∀z, CSNo z → ordinal (CSNoLev z)
In Proofgold the corresponding term root is 143261... and proposition id is 973671...
Proof:
Let z be given.
Assume Hz.
Apply CSNo_E z Hz to the current goal.
Let x and y be given.
Assume Hx Hy.
Assume Hzxy: z = pa x y.
We will prove ordinal (SNoLev (Re (pa x y)) ∪ SNoLev (Im (pa x y))).
rewrite the current goal using CSNo_Re2 x y Hx Hy (from left to right).
rewrite the current goal using CSNo_Im2 x y Hx Hy (from left to right).
We will prove ordinal (SNoLev x ∪ SNoLev y).
An exact proof term for the current goal is ordinal_binunion (SNoLev x) (SNoLev y) (SNoLev_ordinal x Hx) (SNoLev_ordinal y Hy).
∎
Let conj : set → set ≝ λx ⇒ x
Definition. We define minus_CSNo to be CD_minus {2} SNo minus_SNo of type set → set.
In Proofgold the corresponding term root is 84edf6... and object id is d06e08...
Definition. We define conj_CSNo to be CD_conj {2} SNo minus_SNo conj of type set → set.
In Proofgold the corresponding term root is f0317b... and object id is 35fddb...
Definition. We define add_CSNo to be CD_add {2} SNo add_SNo of type set → set → set.
In Proofgold the corresponding term root is 1c8cce... and object id is 756300...
Definition. We define mul_CSNo to be CD_mul {2} SNo minus_SNo conj add_SNo mul_SNo of type set → set → set.
In Proofgold the corresponding term root is fbcd2a... and object id is 46d4cd...
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.
In Proofgold the corresponding term root is 1ff646... and object id is dce27b...
Definition. We define abs_sqr_CSNo to be λz ⇒ Re z ^ 2 + Im z ^ 2 of type set → set.
In Proofgold the corresponding term root is 8363b8... and object id is 5fbf97...
Definition. We define recip_CSNo to be λz ⇒ pa (Re z :/: abs_sqr_CSNo z) (- (Im z :/: abs_sqr_CSNo z)) of type set → set.
In Proofgold the corresponding term root is 6e6e74... and object id is 42648e...
Let plus' ≝ add_CSNo
Let mult' ≝ mul_CSNo
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.
Definition. We define div_CSNo to be λz w ⇒ z ⨯ recip_CSNo w of type set → set → set.
In Proofgold the corresponding term root is 3a99f0... and object id is 51b5b9...
Theorem. (CSNo_Complex_i)
CSNo i
In Proofgold the corresponding term root is c1ad38... and proposition id is 92db43...
Proof:
We will prove CSNo (pa 0 1).
Apply CSNo_I to the current goal.
An exact proof term for the current goal is SNo_0.
An exact proof term for the current goal is SNo_1.
∎
Theorem. (CSNo_minus_CSNo)
∀z, CSNo z → CSNo (minus_CSNo z)
In Proofgold the corresponding term root is ed113e... and proposition id is 876b1c...
Proof:
An exact proof term for the current goal is CD_minus_CD {2} SNo complex_tag_fresh minus_SNo SNo_minus_SNo.
∎
Theorem. (minus_CSNo_CRe)
∀z, CSNo z → Re (:-: z) = - Re z
In Proofgold the corresponding term root is 3d4fc3... and proposition id is 8a656a...
Proof:
An exact proof term for the current goal is CD_minus_proj0 {2} SNo complex_tag_fresh minus_SNo SNo_minus_SNo.
∎
Theorem. (minus_CSNo_CIm)
∀z, CSNo z → Im (:-: z) = - Im z
In Proofgold the corresponding term root is e7712f... and proposition id is 901983...
Proof:
An exact proof term for the current goal is CD_minus_proj1 {2} SNo complex_tag_fresh minus_SNo SNo_minus_SNo.
∎
Theorem. (CSNo_conj_CSNo)
∀z, CSNo z → CSNo (conj_CSNo z)
In Proofgold the corresponding term root is 131b13... and proposition id is e9cc63...
Proof:
An exact proof term for the current goal is CD_conj_CD {2} SNo complex_tag_fresh minus_SNo SNo_minus_SNo conj (λx H ⇒ H).
∎
Theorem. (conj_CSNo_CRe)
∀z, CSNo z → Re (z ') = Re z
In Proofgold the corresponding term root is c50c46... and proposition id is a8772e...
Proof:
An exact proof term for the current goal is CD_conj_proj0 {2} SNo complex_tag_fresh minus_SNo SNo_minus_SNo conj (λx H ⇒ H).
∎
Theorem. (conj_CSNo_CIm)
∀z, CSNo z → Im (z ') = - Im z
In Proofgold the corresponding term root is ad25ad... and proposition id is d3861c...
Proof:
An exact proof term for the current goal is CD_conj_proj1 {2} SNo complex_tag_fresh minus_SNo SNo_minus_SNo conj (λx H ⇒ H).
∎
Theorem. (CSNo_add_CSNo)
∀z w, CSNo z → CSNo w → CSNo (add_CSNo z w)
In Proofgold the corresponding term root is 03ed30... and proposition id is 9bf062...
Proof:
An exact proof term for the current goal is CD_add_CD {2} SNo complex_tag_fresh add_SNo SNo_add_SNo.
∎
Theorem. (CSNo_add_CSNo_3)
∀z w v, CSNo z → CSNo w → CSNo v → CSNo (z + w + v)
In Proofgold the corresponding term root is 2bfa20... and proposition id is 8b5121...
Proof:
Let z, w and v be given.
Assume Hz Hw Hv.
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
∎
Theorem. (add_CSNo_CRe)
∀z w, CSNo z → CSNo w → Re (plus' z w) = Re z + Re w
In Proofgold the corresponding term root is c9a95c... and proposition id is c220af...
Proof:
An exact proof term for the current goal is CD_add_proj0 {2} SNo complex_tag_fresh add_SNo SNo_add_SNo.
∎
Theorem. (add_CSNo_CIm)
∀z w, CSNo z → CSNo w → Im (plus' z w) = Im z + Im w
In Proofgold the corresponding term root is 5e4827... and proposition id is 568f7b...
Proof:
An exact proof term for the current goal is CD_add_proj1 {2} SNo complex_tag_fresh add_SNo SNo_add_SNo.
∎
Theorem. (CSNo_mul_CSNo)
∀z w, CSNo z → CSNo w → CSNo (z ⨯ w)
In Proofgold the corresponding term root is 960670... and proposition id is 866107...
Proof:
An exact proof term for the current goal is CD_mul_CD {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_minus_SNo (λx H ⇒ H) SNo_add_SNo SNo_mul_SNo.
∎
Theorem. (CSNo_mul_CSNo_3)
∀z w v, CSNo z → CSNo w → CSNo v → CSNo (z ⨯ w ⨯ v)
In Proofgold the corresponding term root is 71c203... and proposition id is fb3c1b...
Proof:
Let z, w and v be given.
Assume Hz Hw Hv.
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
∎
Theorem. (mul_CSNo_CRe)
∀z w, CSNo z → CSNo w → Re (mult' z w) = Re z * Re w + - (Im w * Im z)
In Proofgold the corresponding term root is 06f6e3... and proposition id is ea0bfe...
Proof:
An exact proof term for the current goal is CD_mul_proj0 {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_minus_SNo (λx H ⇒ H) SNo_add_SNo SNo_mul_SNo.
∎
Theorem. (mul_CSNo_CIm)
∀z w, CSNo z → CSNo w → Im (mult' z w) = Im w * Re z + Im z * Re w
In Proofgold the corresponding term root is c8110c... and proposition id is 5587f2...
Proof:
An exact proof term for the current goal is CD_mul_proj1 {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_minus_SNo (λx H ⇒ H) SNo_add_SNo SNo_mul_SNo.
∎
Theorem. (SNo_Re)
∀x, SNo x → Re x = x
In Proofgold the corresponding term root is 50191e... and proposition id is a39bef...
Proof:
An exact proof term for the current goal is CD_proj0_F {2} SNo complex_tag_fresh SNo_0.
∎
Theorem. (SNo_Im)
∀x, SNo x → Im x = 0
In Proofgold the corresponding term root is e827aa... and proposition id is 021995...
Proof:
An exact proof term for the current goal is CD_proj1_F {2} SNo complex_tag_fresh SNo_0.
∎
Theorem. (Re_0)
Re 0 = 0
In Proofgold the corresponding term root is cd467c... and proposition id is e48eab...
Proof:
An exact proof term for the current goal is SNo_Re 0 SNo_0.
∎
Theorem. (Im_0)
Im 0 = 0
In Proofgold the corresponding term root is 3d0622... and proposition id is cec939...
Proof:
An exact proof term for the current goal is SNo_Im 0 SNo_0.
∎
Theorem. (Re_1)
Re 1 = 1
In Proofgold the corresponding term root is df187f... and proposition id is 5672d2...
Proof:
An exact proof term for the current goal is SNo_Re 1 SNo_1.
∎
Theorem. (Im_1)
Im 1 = 0
In Proofgold the corresponding term root is ca8804... and proposition id is 389106...
Proof:
An exact proof term for the current goal is SNo_Im 1 SNo_1.
∎
Theorem. (Re_i)
Re i = 0
In Proofgold the corresponding term root is 016d84... and proposition id is 64299d...
Proof:
An exact proof term for the current goal is CSNo_Re2 0 1 SNo_0 SNo_1.
∎
Theorem. (Im_i)
Im i = 1
In Proofgold the corresponding term root is a6da12... and proposition id is 6d4781...
Proof:
An exact proof term for the current goal is CSNo_Im2 0 1 SNo_0 SNo_1.
∎
Theorem. (conj_CSNo_id_SNo)
∀x, SNo x → x ' = x
In Proofgold the corresponding term root is 119723... and proposition id is baaa35...
Proof:
An exact proof term for the current goal is CD_conj_F_eq {2} SNo complex_tag_fresh minus_SNo SNo_0 minus_SNo_0 conj.
∎
Theorem. (conj_CSNo_0)
0 ' = 0
In Proofgold the corresponding term root is 4e40f8... and proposition id is ee56ed...
Proof:
An exact proof term for the current goal is conj_CSNo_id_SNo 0 SNo_0.
∎
Theorem. (conj_CSNo_1)
1 ' = 1
In Proofgold the corresponding term root is 632854... and proposition id is f32e05...
Proof:
An exact proof term for the current goal is conj_CSNo_id_SNo 1 SNo_1.
∎
Theorem. (conj_CSNo_i)
i ' = :-: i
In Proofgold the corresponding term root is b17555... and proposition id is 3ef34f...
Proof:
Apply CSNo_ReIm_split (i ') (:-: i) (CSNo_conj_CSNo i CSNo_Complex_i) (CSNo_minus_CSNo i CSNo_Complex_i) to the current goal.
We will prove Re (i ') = Re (:-: i).
rewrite the current goal using conj_CSNo_CRe i CSNo_Complex_i (from left to right).
rewrite the current goal using minus_CSNo_CRe i CSNo_Complex_i (from left to right).
We will prove Re i = - Re i.
rewrite the current goal using Re_i (from left to right).
Use symmetry.
An exact proof term for the current goal is minus_SNo_0.
We will prove Im (i ') = Im (:-: i).
rewrite the current goal using minus_CSNo_CIm i CSNo_Complex_i (from left to right).
An exact proof term for the current goal is conj_CSNo_CIm i CSNo_Complex_i.
∎
Theorem. (minus_CSNo_minus_SNo)
∀x, SNo x → :-: x = - x
In Proofgold the corresponding term root is c7c7a2... and proposition id is b2e3bc...
Proof:
An exact proof term for the current goal is CD_minus_F_eq {2} SNo complex_tag_fresh minus_SNo SNo_0 minus_SNo_0.
∎
Theorem. (minus_CSNo_0)
:-: 0 = 0
In Proofgold the corresponding term root is 733a71... and proposition id is 781e00...
Proof:
rewrite the current goal using minus_CSNo_minus_SNo 0 SNo_0 (from left to right).
An exact proof term for the current goal is minus_SNo_0.
∎
Theorem. (add_CSNo_add_SNo)
∀x y, SNo x → SNo y → x + y = x + y
In Proofgold the corresponding term root is 9bf667... and proposition id is 78adb6...
Proof:
An exact proof term for the current goal is CD_add_F_eq {2} SNo complex_tag_fresh add_SNo SNo_0 (add_SNo_0L 0 SNo_0).
∎
Theorem. (mul_CSNo_mul_SNo)
∀x y, SNo x → SNo y → x ⨯ y = x * y
In Proofgold the corresponding term root is d07924... and proposition id is 35fd7f...
Proof:
An exact proof term for the current goal is CD_mul_F_eq {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_0 (λx H ⇒ H) SNo_mul_SNo minus_SNo_0 add_SNo_0R mul_SNo_zeroL mul_SNo_zeroR.
∎
Theorem. (minus_CSNo_invol)
∀z, CSNo z → :-: :-: z = z
In Proofgold the corresponding term root is 718eca... and proposition id is 1133eb...
Proof:
An exact proof term for the current goal is CD_minus_invol {2} SNo complex_tag_fresh minus_SNo SNo_minus_SNo minus_SNo_invol.
∎
Theorem. (conj_CSNo_invol)
∀z, CSNo z → z ' ' = z
In Proofgold the corresponding term root is 80a94e... and proposition id is 01ed39...
Proof:
An exact proof term for the current goal is CD_conj_invol {2} SNo complex_tag_fresh minus_SNo conj SNo_minus_SNo (λx H ⇒ H) minus_SNo_invol (λx _ q H ⇒ H).
∎
Theorem. (conj_minus_CSNo)
∀z, CSNo z → (:-: z) ' = :-: (z ')
In Proofgold the corresponding term root is e285c3... and proposition id is f32597...
Proof:
An exact proof term for the current goal is CD_conj_minus {2} SNo complex_tag_fresh minus_SNo conj SNo_minus_SNo (λx H ⇒ H) (λx _ q H ⇒ H).
∎
Theorem. (minus_add_CSNo)
∀z w, CSNo z → CSNo w → :-: (z + w) = :-: z + :-: w
In Proofgold the corresponding term root is 7d8b27... and proposition id is f2c713...
Proof:
An exact proof term for the current goal is CD_minus_add {2} SNo complex_tag_fresh minus_SNo add_SNo SNo_minus_SNo SNo_add_SNo minus_add_SNo_distr.
∎
Theorem. (conj_add_CSNo)
∀z w, CSNo z → CSNo w → (z + w) ' = z ' + w '
In Proofgold the corresponding term root is af649d... and proposition id is 884e86...
Proof:
An exact proof term for the current goal is CD_conj_add {2} SNo complex_tag_fresh minus_SNo conj add_SNo SNo_minus_SNo (λx H ⇒ H) SNo_add_SNo minus_add_SNo_distr (λx y _ _ q H ⇒ H).
∎
Theorem. (add_CSNo_com)
∀z w, CSNo z → CSNo w → z + w = w + z
In Proofgold the corresponding term root is 4b7106... and proposition id is 7214c5...
Proof:
An exact proof term for the current goal is CD_add_com {2} SNo complex_tag_fresh add_SNo add_SNo_com.
∎
Theorem. (add_CSNo_assoc)
∀z w v, CSNo z → CSNo w → CSNo v → (z + w) + v = z + (w + v)
In Proofgold the corresponding term root is d8944b... and proposition id is 76142e...
Proof:
We prove the intermediate claim L1: ∀x y z, SNo x → SNo y → SNo z → (x + y) + z = x + (y + z).
Let x, y and z be given.
Assume Hx Hy Hz.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc x y z Hx Hy Hz.
Apply CD_add_assoc {2} SNo complex_tag_fresh add_SNo SNo_add_SNo L1 to the current goal.
∎
Theorem. (add_CSNo_0L)
∀z, CSNo z → add_CSNo 0 z = z
In Proofgold the corresponding term root is 192e4f... and proposition id is f071aa...
Proof:
An exact proof term for the current goal is CD_add_0L {2} SNo complex_tag_fresh add_SNo SNo_0 add_SNo_0L.
∎
Theorem. (add_CSNo_0R)
∀z, CSNo z → add_CSNo z 0 = z
In Proofgold the corresponding term root is 5d190c... and proposition id is f422cd...
Proof:
An exact proof term for the current goal is CD_add_0R {2} SNo complex_tag_fresh add_SNo SNo_0 add_SNo_0R.
∎
Theorem. (add_CSNo_minus_CSNo_linv)
∀z, CSNo z → add_CSNo (minus_CSNo z) z = 0
In Proofgold the corresponding term root is 02ca9b... and proposition id is b8f406...
Proof:
An exact proof term for the current goal is CD_add_minus_linv {2} SNo complex_tag_fresh minus_SNo add_SNo SNo_minus_SNo add_SNo_minus_SNo_linv.
∎
Theorem. (add_CSNo_minus_CSNo_rinv)
∀z, CSNo z → add_CSNo z (minus_CSNo z) = 0
In Proofgold the corresponding term root is a39e67... and proposition id is cef63c...
Proof:
An exact proof term for the current goal is CD_add_minus_rinv {2} SNo complex_tag_fresh minus_SNo add_SNo SNo_minus_SNo add_SNo_minus_SNo_rinv.
∎
Theorem. (mul_CSNo_0R)
∀z, CSNo z → z ⨯ 0 = 0
In Proofgold the corresponding term root is cc1bfb... and proposition id is a20c54...
Proof:
An exact proof term for the current goal is CD_mul_0R {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_0 minus_SNo_0 (λq H ⇒ H) (add_SNo_0L 0 SNo_0) mul_SNo_zeroL mul_SNo_zeroR.
∎
Theorem. (mul_CSNo_0L)
∀z, CSNo z → 0 ⨯ z = 0
In Proofgold the corresponding term root is a0f420... and proposition id is 491817...
Proof:
An exact proof term for the current goal is CD_mul_0L {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_0 (λx H ⇒ H) minus_SNo_0 (add_SNo_0L 0 SNo_0) mul_SNo_zeroL mul_SNo_zeroR.
∎
Theorem. (mul_CSNo_1R)
∀z, CSNo z → z ⨯ 1 = z
In Proofgold the corresponding term root is 0cbbac... and proposition id is ddbaab...
Proof:
An exact proof term for the current goal is CD_mul_1R {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_0 SNo_1 minus_SNo_0 (λq H ⇒ H) (λq H ⇒ H) add_SNo_0L add_SNo_0R mul_SNo_zeroL mul_SNo_oneR.
∎
Theorem. (mul_CSNo_1L)
∀z, CSNo z → 1 ⨯ z = z
In Proofgold the corresponding term root is 2c05ca... and proposition id is 88f311...
Proof:
An exact proof term for the current goal is CD_mul_1L {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_0 SNo_1 (λx H ⇒ H) minus_SNo_0 add_SNo_0R mul_SNo_zeroL mul_SNo_zeroR mul_SNo_oneL mul_SNo_oneR.
∎
Theorem. (conj_mul_CSNo)
∀z w, CSNo z → CSNo w → (z ⨯ w) ' = w ' ⨯ z '
In Proofgold the corresponding term root is d18a4e... and proposition id is 43023c...
Proof:
An exact proof term for the current goal is CD_conj_mul {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_minus_SNo (λz H ⇒ H) SNo_add_SNo SNo_mul_SNo minus_SNo_invol (λx _ q H ⇒ H) (λx _ q H ⇒ H) (λx y _ _ q H ⇒ H) minus_add_SNo_distr add_SNo_com mul_SNo_com mul_SNo_minus_distrR mul_SNo_minus_distrL.
∎
Theorem. (mul_CSNo_distrL)
∀z w u, CSNo z → CSNo w → CSNo u → z ⨯ (w + u) = z ⨯ w + z ⨯ u
In Proofgold the corresponding term root is 4300b1... and proposition id is 146a23...
Proof:
We prove the intermediate claim L1: ∀x y z, SNo x → SNo y → SNo z → (x + y) + z = x + (y + z).
Let x, y and z be given.
Assume Hx Hy Hz.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc x y z Hx Hy Hz.
An exact proof term for the current goal is CD_add_mul_distrL {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_minus_SNo (λx H ⇒ H) SNo_add_SNo SNo_mul_SNo minus_add_SNo_distr (λx y _ _ q H ⇒ H) L1 add_SNo_com mul_SNo_distrL mul_SNo_distrR.
∎
Theorem. (mul_CSNo_distrR)
∀z w u, CSNo z → CSNo w → CSNo u → (z + w) ⨯ u = z ⨯ u + w ⨯ u
In Proofgold the corresponding term root is 6eb197... and proposition id is 7fab8b...
Proof:
We prove the intermediate claim L1: ∀x y z, SNo x → SNo y → SNo z → (x + y) + z = x + (y + z).
Let x, y and z be given.
Assume Hx Hy Hz.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc x y z Hx Hy Hz.
An exact proof term for the current goal is CD_add_mul_distrR {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_minus_SNo (λx H ⇒ H) SNo_add_SNo SNo_mul_SNo minus_add_SNo_distr L1 add_SNo_com mul_SNo_distrL mul_SNo_distrR.
∎
Theorem. (minus_mul_CSNo_distrR)
∀z w, CSNo z → CSNo w → z ⨯ (:-: w) = :-: z ⨯ w
In Proofgold the corresponding term root is 11bf1c... and proposition id is 79b3b3...
Proof:
An exact proof term for the current goal is CD_minus_mul_distrR {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_minus_SNo (λx H ⇒ H) SNo_add_SNo SNo_mul_SNo (λx _ q H ⇒ H) minus_add_SNo_distr mul_SNo_minus_distrR mul_SNo_minus_distrL.
∎
Theorem. (minus_mul_CSNo_distrL)
∀z w, CSNo z → CSNo w → (:-: z) ⨯ w = :-: z ⨯ w
In Proofgold the corresponding term root is 995a36... and proposition id is 1b56a5...
Proof:
An exact proof term for the current goal is CD_minus_mul_distrL {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_minus_SNo (λx H ⇒ H) SNo_add_SNo SNo_mul_SNo minus_add_SNo_distr mul_SNo_minus_distrR mul_SNo_minus_distrL.
∎
Theorem. (exp_CSNo_nat_0)
∀z, z0 = 1
In Proofgold the corresponding term root is 4ac193... and proposition id is c694c7...
Proof:
An exact proof term for the current goal is CD_exp_nat_0 {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo.
∎
Theorem. (exp_CSNo_nat_S)
∀z n, nat_p n → z(ordsucc n) = z ⨯ zn
In Proofgold the corresponding term root is cc896c... and proposition id is ce5d58...
Proof:
An exact proof term for the current goal is CD_exp_nat_S {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo.
∎
Theorem. (exp_CSNo_nat_1)
∀z, CSNo z → z1 = z
In Proofgold the corresponding term root is 00324b... and proposition id is 4f5719...
Proof:
An exact proof term for the current goal is CD_exp_nat_1 {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_0 SNo_1 minus_SNo_0 (λq H ⇒ H) (λq H ⇒ H) add_SNo_0L add_SNo_0R mul_SNo_zeroL mul_SNo_oneR.
∎
Theorem. (exp_CSNo_nat_2)
∀z, CSNo z → z2 = z ⨯ z
In Proofgold the corresponding term root is 3de725... and proposition id is b58c27...
Proof:
An exact proof term for the current goal is CD_exp_nat_2 {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_0 SNo_1 minus_SNo_0 (λq H ⇒ H) (λq H ⇒ H) add_SNo_0L add_SNo_0R mul_SNo_zeroL mul_SNo_oneR.
∎
Theorem. (CSNo_exp_CSNo_nat)
∀z, CSNo z → ∀n, nat_p n → CSNo (zn)
In Proofgold the corresponding term root is 11b0c7... and proposition id is 0d7167...
Proof:
An exact proof term for the current goal is CD_exp_nat_CD {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_minus_SNo (λx H ⇒ H) SNo_add_SNo SNo_mul_SNo SNo_0 SNo_1.
∎
Theorem. (add_SNo_rotate_4_0312)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) + (z + w) = (x + w) + (y + z)
In Proofgold the corresponding term root is a00d0b... and proposition id is 1932b8...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_SNo_com z w Hz Hw (from left to right).
We will prove (x + y) + (w + z) = (x + w) + (y + z).
An exact proof term for the current goal is add_SNo_com_4_inner_mid x y w z Hx Hy Hw Hz.
∎
Theorem. (mul_CSNo_com)
∀z w, CSNo z → CSNo w → z ⨯ w = w ⨯ z
In Proofgold the corresponding term root is d89de4... and proposition id is 8f3381...
Proof:
Let z and w be given.
Assume Hz Hw.
We prove the intermediate claim Lzw: CSNo (mult' z w).
An exact proof term for the current goal is CSNo_mul_CSNo z w Hz Hw.
We prove the intermediate claim Lwz: CSNo (mult' w z).
An exact proof term for the current goal is CSNo_mul_CSNo w z Hw Hz.
We prove the intermediate claim LRezR: SNo (Re z).
An exact proof term for the current goal is CSNo_ReR z Hz.
We prove the intermediate claim LRewR: SNo (Re w).
An exact proof term for the current goal is CSNo_ReR w Hw.
We prove the intermediate claim LImzR: SNo (Im z).
An exact proof term for the current goal is CSNo_ImR z Hz.
We prove the intermediate claim LImwR: SNo (Im w).
An exact proof term for the current goal is CSNo_ImR w Hw.
Apply CSNo_ReIm_split (mult' z w) (mult' w z) Lzw Lwz to the current goal.
We will prove Re (mult' z w) = Re (mult' w z).
Use transitivity with Re z * Re w + - (Im w * Im z), and Re w * Re z + - (Im z * Im w).
An exact proof term for the current goal is mul_CSNo_CRe z w Hz Hw.
Use f_equal.
An exact proof term for the current goal is mul_SNo_com (Re z) (Re w) LRezR LRewR.
Use f_equal.
An exact proof term for the current goal is mul_SNo_com (Im w) (Im z) LImwR LImzR.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_CRe w z Hw Hz.
We will prove Im (mult' z w) = Im (mult' w z).
Use transitivity with Im w * Re z + Im z * Re w, and Im z * Re w + Im w * Re z.
An exact proof term for the current goal is mul_CSNo_CIm z w Hz Hw.
An exact proof term for the current goal is add_SNo_com (Im w * Re z) (Im z * Re w) (SNo_mul_SNo (Im w) (Re z) LImwR LRezR) (SNo_mul_SNo (Im z) (Re w) LImzR LRewR).
Use symmetry.
An exact proof term for the current goal is mul_CSNo_CIm w z Hw Hz.
∎
Theorem. (mul_CSNo_assoc)
∀z w v, CSNo z → CSNo w → CSNo v → z ⨯ (w ⨯ v) = (z ⨯ w) ⨯ v
In Proofgold the corresponding term root is 227f96... and proposition id is 9f937c...
Proof:
Let z, w and v be given.
Assume Hz Hw Hv.
We prove the intermediate claim Lwv: CSNo (mult' w v).
An exact proof term for the current goal is CSNo_mul_CSNo w v Hw Hv.
We prove the intermediate claim Lzw: CSNo (mult' z w).
An exact proof term for the current goal is CSNo_mul_CSNo z w Hz Hw.
We prove the intermediate claim Lzwv1: CSNo (mult' z (mult' w v)).
An exact proof term for the current goal is CSNo_mul_CSNo z (mult' w v) Hz Lwv.
We prove the intermediate claim Lzwv2: CSNo (mult' (mult' z w) v).
An exact proof term for the current goal is CSNo_mul_CSNo (mult' z w) v Lzw Hv.
We prove the intermediate claim LRezR: SNo (Re z).
An exact proof term for the current goal is CSNo_ReR z Hz.
We prove the intermediate claim LRewR: SNo (Re w).
An exact proof term for the current goal is CSNo_ReR w Hw.
We prove the intermediate claim LRevR: SNo (Re v).
An exact proof term for the current goal is CSNo_ReR v Hv.
We prove the intermediate claim LImzR: SNo (Im z).
An exact proof term for the current goal is CSNo_ImR z Hz.
We prove the intermediate claim LImwR: SNo (Im w).
An exact proof term for the current goal is CSNo_ImR w Hw.
We prove the intermediate claim LImvR: SNo (Im v).
An exact proof term for the current goal is CSNo_ImR v Hv.
Apply CSNo_ReIm_split (mult' z (mult' w v)) (mult' (mult' z w) v) Lzwv1 Lzwv2 to the current goal.
We will prove Re (mult' z (mult' w v)) = Re (mult' (mult' z w) v).
Use transitivity with Re z * Re (mult' w v) + - (Im (mult' w v) * Im z), (Re z * Re w * Re v + - (Re z * Im v * Im w)) + (- Im v * Re w * Im z + - Im w * Re v * Im z), (Re z * Re w * Re v + - Im w * Re v * Im z) + (- (Re z * Im v * Im w) + - Im v * Re w * Im z), and Re (mult' z w) * Re v + - (Im v * Im (mult' z w)).
An exact proof term for the current goal is mul_CSNo_CRe z (mult' w v) Hz Lwv.
Use f_equal.
We will prove Re z * Re (mult' w v) = Re z * Re w * Re v + - (Re z * Im v * Im w).
Use transitivity with Re z * (Re w * Re v + - (Im v * Im w)), and Re z * Re w * Re v + Re z * (- (Im v * Im w)).
Use f_equal.
An exact proof term for the current goal is mul_CSNo_CRe w v Hw Hv.
Apply mul_SNo_distrL (Re z) (Re w * Re v) (- (Im v * Im w)) LRezR (SNo_mul_SNo (Re w) (Re v) LRewR LRevR) to the current goal.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is SNo_mul_SNo (Im v) (Im w) LImvR LImwR.
Use f_equal.
We will prove Re z * (- (Im v * Im w)) = - (Re z * Im v * Im w).
An exact proof term for the current goal is mul_SNo_minus_distrR (Re z) (Im v * Im w) LRezR (SNo_mul_SNo (Im v) (Im w) LImvR LImwR).
We will prove - (Im (mult' w v) * Im z) = - Im v * Re w * Im z + - Im w * Re v * Im z.
Use transitivity with and - (Im v * Re w * Im z + Im w * Re v * Im z).
Use f_equal.
We will prove Im (mult' w v) * Im z = Im v * Re w * Im z + Im w * Re v * Im z.
Use transitivity with (Im v * Re w + Im w * Re v) * Im z, and (Im v * Re w) * Im z + (Im w * Re v) * Im z.
Use f_equal.
An exact proof term for the current goal is mul_CSNo_CIm w v Hw Hv.
We will prove (Im v * Re w + Im w * Re v) * Im z = (Im v * Re w) * Im z + (Im w * Re v) * Im z.
An exact proof term for the current goal is mul_SNo_distrR (Im v * Re w) (Im w * Re v) (Im z) (SNo_mul_SNo (Im v) (Re w) LImvR LRewR) (SNo_mul_SNo (Im w) (Re v) LImwR LRevR) LImzR.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_SNo_assoc (Im v) (Re w) (Im z) ?? ?? ??.
Use symmetry.
An exact proof term for the current goal is mul_SNo_assoc (Im w) (Re v) (Im z) ?? ?? ??.
We will prove - (Im v * Re w * Im z + Im w * Re v * Im z) = - Im v * Re w * Im z + - Im w * Re v * Im z.
Apply minus_add_SNo_distr to the current goal.
An exact proof term for the current goal is SNo_mul_SNo_3 (Im v) (Re w) (Im z) LImvR LRewR LImzR.
An exact proof term for the current goal is SNo_mul_SNo_3 (Im w) (Re v) (Im z) LImwR LRevR LImzR.
Apply add_SNo_rotate_4_0312 to the current goal.
An exact proof term for the current goal is SNo_mul_SNo_3 (Re z) (Re w) (Re v) LRezR LRewR LRevR.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is SNo_mul_SNo_3 (Re z) (Im v) (Im w) LRezR LImvR LImwR.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is SNo_mul_SNo_3 (Im v) (Re w) (Im z) LImvR LRewR LImzR.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is SNo_mul_SNo_3 (Im w) (Re v) (Im z) LImwR LRevR LImzR.
We will prove (Re z * Re w * Re v + - Im w * Re v * Im z) + (- (Re z * Im v * Im w) + - Im v * Re w * Im z) = (Re (mult' z w) * Re v) + - (Im v * Im (mult' z w)).
Use f_equal.
We will prove Re z * Re w * Re v + - Im w * Re v * Im z = Re (mult' z w) * Re v.
Use transitivity with (Re z * Re w) * Re v + (- (Im w * Im z)) * Re v, and (Re z * Re w + - (Im w * Im z)) * Re v.
Use f_equal.
We will prove Re z * Re w * Re v = (Re z * Re w) * Re v.
An exact proof term for the current goal is mul_SNo_assoc (Re z) (Re w) (Re v) LRezR LRewR LRevR.
We will prove - (Im w * Re v * Im z) = (- (Im w * Im z)) * Re v.
Use transitivity with and - ((Im w * Im z) * Re v).
Use f_equal.
Use transitivity with and (Im w * Im z * Re v).
Use f_equal.
An exact proof term for the current goal is mul_SNo_com (Re v) (Im z) ?? ??.
An exact proof term for the current goal is mul_SNo_assoc (Im w) (Im z) (Re v) ?? ?? ??.
Use symmetry.
We will prove (- (Im w * Im z)) * Re v = - ((Im w * Im z) * Re v).
An exact proof term for the current goal is mul_SNo_minus_distrL (Im w * Im z) (Re v) (SNo_mul_SNo (Im w) (Im z) LImwR LImzR) LRevR.
Use symmetry.
An exact proof term for the current goal is mul_SNo_distrR (Re z * Re w) (- (Im w * Im z)) (Re v) (SNo_mul_SNo (Re z) (Re w) LRezR LRewR) (SNo_minus_SNo (Im w * Im z) (SNo_mul_SNo (Im w) (Im z) LImwR LImzR)) LRevR.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_CRe z w Hz Hw.
We will prove - (Re z * Im v * Im w) + - Im v * Re w * Im z = - (Im v * Im (mult' z w)).
Use transitivity with and - (Re z * Im v * Im w + Im v * Re w * Im z).
Use symmetry.
Apply minus_add_SNo_distr to the current goal.
An exact proof term for the current goal is SNo_mul_SNo_3 (Re z) (Im v) (Im w) ?? ?? ??.
An exact proof term for the current goal is SNo_mul_SNo_3 (Im v) (Re w) (Im z) ?? ?? ??.
Use f_equal.
We will prove Re z * Im v * Im w + Im v * Re w * Im z = Im v * Im (mult' z w).
rewrite the current goal using mul_SNo_com_3_0_1 (Re z) (Im v) (Im w) ?? ?? ?? (from left to right).
Use transitivity with and Im v * (Re z * Im w + Re w * Im z).
Use symmetry.
An exact proof term for the current goal is mul_SNo_distrL (Im v) (Re z * Im w) (Re w * Im z) ?? (SNo_mul_SNo (Re z) (Im w) ?? ??) (SNo_mul_SNo (Re w) (Im z) ?? ??).
We will prove Im v * (Re z * Im w + Re w * Im z) = Im v * Im (mult' z w).
Use f_equal.
Use symmetry.
We will prove Im (mult' z w) = Re z * Im w + Re w * Im z.
rewrite the current goal using mul_SNo_com (Re z) (Im w) ?? ?? (from left to right).
rewrite the current goal using mul_SNo_com (Re w) (Im z) ?? ?? (from left to right).
An exact proof term for the current goal is mul_CSNo_CIm z w Hz Hw.
We will prove (Re (mult' z w) * Re v) + - (Im v * Im (mult' z w)) = Re (mult' (mult' z w) v).
Use symmetry.
An exact proof term for the current goal is mul_CSNo_CRe (mult' z w) v Lzw Hv.
We will prove Im (mult' z (mult' w v)) = Im (mult' (mult' z w) v).
Use transitivity with Im (mult' w v) * Re z + Im z * Re (mult' w v), (Im v * Re w + Im w * Re v) * Re z + Im z * (Re w * Re v + - (Im v * Im w)), (Im v * Re w * Re z + Im w * Re v * Re z) + (Im z * Re w * Re v + - (Im z * Im v * Im w)), (Im v * Re w * Re z + - (Im z * Im v * Im w)) + (Im w * Re v * Re z + Im z * Re w * Re v), Im v * (Re z * Re w + - (Im w * Im z)) + (Im w * Re z + Im z * Re w) * Re v, and Im v * Re (mult' z w) + Im (mult' z w) * Re v.
We will prove Im (mult' z (mult' w v)) = Im (mult' w v) * Re z + Im z * Re (mult' w v).
An exact proof term for the current goal is mul_CSNo_CIm z (mult' w v) Hz Lwv.
We will prove Im (mult' w v) * Re z + Im z * Re (mult' w v) = (Im v * Re w + Im w * Re v) * Re z + Im z * (Re w * Re v + - (Im v * Im w)).
Use f_equal.
Use f_equal.
An exact proof term for the current goal is mul_CSNo_CIm w v ?? ??.
Use f_equal.
An exact proof term for the current goal is mul_CSNo_CRe w v ?? ??.
We will prove (Im v * Re w + Im w * Re v) * Re z + Im z * (Re w * Re v + - (Im v * Im w)) = (Im v * Re w * Re z + Im w * Re v * Re z) + (Im z * Re w * Re v + - (Im z * Im v * Im w)).
Use f_equal.
Use transitivity with and (Im v * Re w) * Re z + (Im w * Re v) * Re z.
An exact proof term for the current goal is mul_SNo_distrR (Im v * Re w) (Im w * Re v) (Re z) (SNo_mul_SNo (Im v) (Re w) ?? ??) (SNo_mul_SNo (Im w) (Re v) ?? ??) ??.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_SNo_assoc (Im v) (Re w) (Re z) ?? ?? ??.
Use symmetry.
An exact proof term for the current goal is mul_SNo_assoc (Im w) (Re v) (Re z) ?? ?? ??.
Use transitivity with and Im z * Re w * Re v + Im z * (- (Im v * Im w)).
Apply mul_SNo_distrL (Im z) (Re w * Re v) (- (Im v * Im w)) ?? (SNo_mul_SNo (Re w) (Re v) ?? ??) to the current goal.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is SNo_mul_SNo (Im v) (Im w) ?? ??.
Use f_equal.
We will prove Im z * (- (Im v * Im w)) = - Im z * Im v * Im w.
An exact proof term for the current goal is mul_SNo_minus_distrR (Im z) (Im v * Im w) ?? (SNo_mul_SNo (Im v) (Im w) ?? ??).
We will prove (Im v * Re w * Re z + Im w * Re v * Re z) + (Im z * Re w * Re v + - (Im z * Im v * Im w)) = (Im v * Re w * Re z + - (Im z * Im v * Im w)) + (Im w * Re v * Re z + Im z * Re w * Re v).
Apply add_SNo_rotate_4_0312 to the current goal.
Apply SNo_mul_SNo_3 to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply SNo_mul_SNo_3 to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply SNo_mul_SNo_3 to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply SNo_minus_SNo to the current goal.
Apply SNo_mul_SNo_3 to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Use f_equal.
We will prove Im v * Re w * Re z + - (Im z * Im v * Im w) = Im v * (Re z * Re w + - (Im w * Im z)).
rewrite the current goal using mul_SNo_com (Re w) (Re z) ?? ?? (from left to right).
rewrite the current goal using mul_SNo_com (Im w) (Im z) ?? ?? (from left to right).
rewrite the current goal using mul_SNo_com_3_0_1 (Im z) (Im v) (Im w) ?? ?? ?? (from left to right).
We will prove Im v * Re z * Re w + - (Im v * Im z * Im w) = Im v * (Re z * Re w + - (Im z * Im w)).
rewrite the current goal using mul_SNo_minus_distrR (Im v) (Im z * Im w) ?? (SNo_mul_SNo (Im z) (Im w) ?? ??) (from right to left).
Use symmetry.
We will prove Im v * (Re z * Re w + - (Im z * Im w)) = Im v * Re z * Re w + Im v * (- Im z * Im w).
An exact proof term for the current goal is mul_SNo_distrL (Im v) (Re z * Re w) (- (Im z * Im w)) ?? (SNo_mul_SNo (Re z) (Re w) ?? ??) (SNo_minus_SNo (Im z * Im w) (SNo_mul_SNo (Im z) (Im w) ?? ??)).
We will prove Im w * Re v * Re z + Im z * Re w * Re v = (Im w * Re z + Im z * Re w) * Re v.
rewrite the current goal using mul_SNo_com (Re v) (Re z) ?? ?? (from left to right).
rewrite the current goal using mul_SNo_assoc (Im w) (Re z) (Re v) ?? ?? ?? (from left to right).
rewrite the current goal using mul_SNo_assoc (Im z) (Re w) (Re v) ?? ?? ?? (from left to right).
Use symmetry.
An exact proof term for the current goal is mul_SNo_distrR (Im w * Re z) (Im z * Re w) (Re v) (SNo_mul_SNo (Im w) (Re z) ?? ??) (SNo_mul_SNo (Im z) (Re w) ?? ??) ??.
We will prove Im v * (Re z * Re w + - (Im w * Im z)) + (Im w * Re z + Im z * Re w) * Re v = Im v * Re (mult' z w) + Im (mult' z w) * Re v.
Use f_equal.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_CRe z w Hz Hw.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_CIm z w Hz Hw.
We will prove Im v * Re (mult' z w) + Im (mult' z w) * Re v = Im (mult' (mult' z w) v).
Use symmetry.
An exact proof term for the current goal is mul_CSNo_CIm (mult' z w) v Lzw Hv.
∎
Theorem. (Complex_i_sqr)
i ⨯ i = :-: 1
In Proofgold the corresponding term root is 665bcb... and proposition id is 0ce587...
Proof:
We prove the intermediate claim Lii: CSNo (i ⨯ i).
An exact proof term for the current goal is CSNo_mul_CSNo i i CSNo_Complex_i CSNo_Complex_i.
We prove the intermediate claim Lm1: CSNo (:-: 1).
An exact proof term for the current goal is CSNo_minus_CSNo 1 CSNo_1.
Apply CSNo_ReIm_split (i ⨯ i) (:-: 1) Lii Lm1 to the current goal.
We will prove Re (i ⨯ i) = Re (:-: 1).
rewrite the current goal using mul_CSNo_CRe i i CSNo_Complex_i CSNo_Complex_i (from left to right).
rewrite the current goal using minus_CSNo_CRe 1 CSNo_1 (from left to right).
We will prove Re i * Re i + - Im i * Im i = - Re 1.
rewrite the current goal using Re_i (from left to right).
rewrite the current goal using Im_i (from left to right).
rewrite the current goal using Re_1 (from left to right).
We will prove 0 * 0 + - 1 * 1 = - 1.
rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).
rewrite the current goal using mul_SNo_oneL 1 SNo_1 (from left to right).
We will prove 0 + - 1 = - 1.
An exact proof term for the current goal is add_SNo_0L (- 1) (SNo_minus_SNo 1 SNo_1).
We will prove Im (i ⨯ i) = Im (:-: 1).
rewrite the current goal using mul_CSNo_CIm i i CSNo_Complex_i CSNo_Complex_i (from left to right).
rewrite the current goal using minus_CSNo_CIm 1 CSNo_1 (from left to right).
We will prove Im i * Re i + Im i * Re i = - Im 1.
rewrite the current goal using Re_i (from left to right).
rewrite the current goal using Im_i (from left to right).
rewrite the current goal using Im_1 (from left to right).
We will prove 1 * 0 + 1 * 0 = - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using mul_SNo_zeroR 1 SNo_1 (from left to right).
We will prove 0 + 0 = 0.
An exact proof term for the current goal is add_SNo_0L 0 SNo_0.
∎
Theorem. (SNo_abs_sqr_CSNo)
∀z, CSNo z → SNo (abs_sqr_CSNo z)
In Proofgold the corresponding term root is 3c670d... and proposition id is 487405...
Proof:
Let z be given.
Assume Hz.
We will prove SNo (Re z ^ 2 + Im z ^ 2).
Apply SNo_add_SNo to the current goal.
Apply SNo_exp_SNo_nat to the current goal.
An exact proof term for the current goal is CSNo_ReR z Hz.
An exact proof term for the current goal is nat_2.
Apply SNo_exp_SNo_nat to the current goal.
An exact proof term for the current goal is CSNo_ImR z Hz.
An exact proof term for the current goal is nat_2.
∎
Theorem. (abs_sqr_CSNo_nonneg)
∀z, CSNo z → 0 ≤ abs_sqr_CSNo z
In Proofgold the corresponding term root is 8b1a65... and proposition id is 7810f8...
Proof:
Let z be given.
Assume Hz.
Set x to be the term Re z.
Set y to be the term Im z.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is CSNo_ReR z Hz.
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is CSNo_ImR z Hz.
We prove the intermediate claim Lxx: SNo (x ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat x Lx 2 nat_2.
We prove the intermediate claim Lyy: SNo (y ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat y Ly 2 nat_2.
We will prove 0 ≤ x ^ 2 + y ^ 2.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left) at position 1.
We will prove 0 + 0 ≤ x ^ 2 + y ^ 2.
Apply add_SNo_Le3 0 0 (x ^ 2) (y ^ 2) SNo_0 SNo_0 Lxx Lyy to the current goal.
rewrite the current goal using exp_SNo_nat_2 x Lx (from left to right).
An exact proof term for the current goal is SNo_sqr_nonneg x Lx.
rewrite the current goal using exp_SNo_nat_2 y Ly (from left to right).
An exact proof term for the current goal is SNo_sqr_nonneg y Ly.
∎
Theorem. (abs_sqr_CSNo_zero)
∀z, CSNo z → abs_sqr_CSNo z = 0 → z = 0
In Proofgold the corresponding term root is 717eb1... and proposition id is d8e809...
Proof:
Let z be given.
Assume Hz.
Set x to be the term Re z.
Set y to be the term Im z.
Set s to be the term x ^ 2 + y ^ 2.
Assume H1: s = 0.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is CSNo_ReR z Hz.
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is CSNo_ImR z Hz.
We prove the intermediate claim Lxx: SNo (x ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat x Lx 2 nat_2.
We prove the intermediate claim Lyy: SNo (y ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat y Ly 2 nat_2.
We prove the intermediate claim Ls: SNo s.
An exact proof term for the current goal is SNo_add_SNo (x ^ 2) (y ^ 2) Lxx Lyy.
We will prove z = 0.
Apply CSNo_ReIm_split z 0 Hz CSNo_0 to the current goal.
We will prove Re z = Re 0.
rewrite the current goal using Re_0 (from left to right).
We will prove x = 0.
Apply SNo_zero_or_sqr_pos' x Lx to the current goal.
Assume H2: x = 0.
An exact proof term for the current goal is H2.
Assume H2: 0 < x ^ 2.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using H1 (from right to left) at position 2.
We will prove 0 < s.
Apply SNoLtLe_tra 0 (x ^ 2) s SNo_0 ?? ?? H2 to the current goal.
We will prove x ^ 2 ≤ s.
rewrite the current goal using add_SNo_0R (x ^ 2) ?? (from right to left) at position 1.
We will prove x ^ 2 + 0 ≤ s.
Apply add_SNo_Le2 (x ^ 2) 0 (y ^ 2) ?? SNo_0 ?? to the current goal.
We will prove 0 ≤ y ^ 2.
Apply SNo_sqr_nonneg' y Ly to the current goal.
We will prove Im z = Im 0.
rewrite the current goal using Im_0 (from left to right).
We will prove y = 0.
Apply SNo_zero_or_sqr_pos' y Ly to the current goal.
Assume H2: y = 0.
An exact proof term for the current goal is H2.
Assume H2: 0 < y ^ 2.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using H1 (from right to left) at position 2.
We will prove 0 < s.
Apply SNoLtLe_tra 0 (y ^ 2) s SNo_0 ?? ?? H2 to the current goal.
We will prove y ^ 2 ≤ s.
rewrite the current goal using add_SNo_0L (y ^ 2) ?? (from right to left) at position 1.
We will prove 0 + y ^ 2 ≤ s.
Apply add_SNo_Le1 0 (y ^ 2) (x ^ 2) SNo_0 ?? ?? to the current goal.
We will prove 0 ≤ x ^ 2.
Apply SNo_sqr_nonneg' x Lx to the current goal.
∎
Theorem. (CSNo_recip_CSNo)
∀z, CSNo z → CSNo (recip_CSNo z)
In Proofgold the corresponding term root is fad212... and proposition id is 05a416...
Proof:
Let z be given.
Assume Hz.
Set s to be the term Re z ^ 2 + Im z ^ 2.
We prove the intermediate claim LRezR: SNo (Re z).
An exact proof term for the current goal is CSNo_ReR z Hz.
We prove the intermediate claim LImzR: SNo (Im z).
An exact proof term for the current goal is CSNo_ImR z Hz.
We prove the intermediate claim Ls: SNo s.
An exact proof term for the current goal is SNo_abs_sqr_CSNo z Hz.
We will prove CSNo (pa (Re z :/: s) (- (Im z :/: s))).
Apply CSNo_I to the current goal.
We will prove SNo (Re z :/: s).
Apply SNo_div_SNo to the current goal.
An exact proof term for the current goal is LRezR.
An exact proof term for the current goal is Ls.
We will prove SNo (- (Im z :/: s)).
Apply SNo_minus_SNo to the current goal.
Apply SNo_div_SNo to the current goal.
An exact proof term for the current goal is LImzR.
An exact proof term for the current goal is Ls.
∎
Theorem. (CSNo_relative_recip)
∀z, CSNo z → ∀u, SNo u → (Re z ^ 2 + Im z ^ 2) * u = 1 → z ⨯ (u ⨯ Re z + :-: i ⨯ u ⨯ Im z) = 1
In Proofgold the corresponding term root is dbb71a... and proposition id is d15820...
Proof:
Let z be given.
Assume Hz.
Let u be given.
Assume Hu.
Assume Hur: (Re z ^ 2 + Im z ^ 2) * u = 1.
We will prove z ⨯ (u ⨯ Re z + :-: i ⨯ u ⨯ Im z) = 1.
We prove the intermediate claim LRezR: SNo (Re z).
An exact proof term for the current goal is CSNo_ReR z Hz.
We prove the intermediate claim LImzR: SNo (Im z).
An exact proof term for the current goal is CSNo_ImR z Hz.
We will prove z ⨯ (u ⨯ Re z + :-: i ⨯ u ⨯ Im z) = 1.
rewrite the current goal using mul_CSNo_mul_SNo u (Re z) Hu LRezR (from left to right).
rewrite the current goal using mul_CSNo_mul_SNo u (Im z) Hu LImzR (from left to right).
We will prove z ⨯ (u * Re z + :-: i ⨯ u * Im z) = 1.
We prove the intermediate claim LuRez: SNo (u * Re z).
An exact proof term for the current goal is SNo_mul_SNo u (Re z) ?? ??.
We prove the intermediate claim LuRez': CSNo (u * Re z).
Apply SNo_CSNo to the current goal.
An exact proof term for the current goal is LuRez.
We prove the intermediate claim LuImz: SNo (u * Im z).
An exact proof term for the current goal is SNo_mul_SNo u (Im z) ?? ??.
We prove the intermediate claim LuImz': CSNo (u * Im z).
Apply SNo_CSNo to the current goal.
An exact proof term for the current goal is LuImz.
We prove the intermediate claim LiuImz: CSNo (i ⨯ u * Im z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is CSNo_Complex_i.
An exact proof term for the current goal is LuImz'.
We prove the intermediate claim LmiuImz: CSNo (:-: i ⨯ u * Im z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is LiuImz.
We prove the intermediate claim L1: CSNo (u * Re z + :-: i ⨯ u * Im z).
Apply CSNo_add_CSNo to the current goal.
We will prove CSNo (u * Re z).
An exact proof term for the current goal is LuRez'.
We will prove CSNo (:-: i ⨯ u * Im z).
An exact proof term for the current goal is LmiuImz.
We prove the intermediate claim LRezRez: SNo (Re z * Re z).
An exact proof term for the current goal is SNo_mul_SNo (Re z) (Re z) ?? ??.
We prove the intermediate claim LImzImz: SNo (Im z * Im z).
An exact proof term for the current goal is SNo_mul_SNo (Im z) (Im z) ?? ??.
Apply CSNo_ReIm_split (z ⨯ (u * Re z + :-: i ⨯ u * Im z)) 1 (CSNo_mul_CSNo z (u * Re z + :-: i ⨯ u * Im z) Hz L1) CSNo_1 to the current goal.
We will prove Re (z ⨯ (u * Re z + :-: i ⨯ u * Im z)) = Re 1.
rewrite the current goal using Re_1 (from left to right).
rewrite the current goal using mul_CSNo_CRe z (u * Re z + :-: i ⨯ u * Im z) Hz L1 (from left to right).
We will prove Re z * Re (u * Re z + :-: i ⨯ u * Im z) + - Im (u * Re z + :-: i ⨯ u * Im z) * Im z = 1.
rewrite the current goal using add_CSNo_CRe (u * Re z) (:-: i ⨯ u * Im z) LuRez' LmiuImz (from left to right).
rewrite the current goal using add_CSNo_CIm (u * Re z) (:-: i ⨯ u * Im z) LuRez' LmiuImz (from left to right).
We will prove Re z * (Re (u * Re z) + Re (:-: i ⨯ u * Im z)) + - (Im (u * Re z) + Im (:-: i ⨯ u * Im z)) * Im z = 1.
rewrite the current goal using minus_CSNo_CRe (i ⨯ u * Im z) LiuImz (from left to right).
rewrite the current goal using minus_CSNo_CIm (i ⨯ u * Im z) LiuImz (from left to right).
rewrite the current goal using SNo_Re (u * Re z) LuRez (from left to right).
rewrite the current goal using SNo_Im (u * Re z) LuRez (from left to right).
We will prove Re z * (u * Re z + - Re (i ⨯ u * Im z)) + - (0 + - Im (i ⨯ u * Im z)) * Im z = 1.
rewrite the current goal using mul_CSNo_CRe i (u * Im z) CSNo_Complex_i LuImz' (from left to right).
We will prove Re z * (u * Re z + - (Re i * Re (u * Im z) + - Im (u * Im z) * Im i)) + - (0 + - Im (i ⨯ u * Im z)) * Im z = 1.
rewrite the current goal using mul_CSNo_CIm i (u * Im z) CSNo_Complex_i LuImz' (from left to right).
We will prove Re z * (u * Re z + - (Re i * Re (u * Im z) + - Im (u * Im z) * Im i)) + - (0 + - (Im (u * Im z) * Re i + Im i * Re (u * Im z))) * Im z = 1.
rewrite the current goal using Re_i (from left to right).
rewrite the current goal using Im_i (from left to right).
We will prove Re z * (u * Re z + - (0 * Re (u * Im z) + - Im (u * Im z) * 1)) + - (0 + - (Im (u * Im z) * 0 + 1 * Re (u * Im z))) * Im z = 1.
rewrite the current goal using SNo_Re (u * Im z) LuImz (from left to right).
rewrite the current goal using SNo_Im (u * Im z) LuImz (from left to right).
We will prove Re z * (u * Re z + - (0 * (u * Im z) + - 0 * 1)) + - (0 + - (0 * 0 + 1 * (u * Im z))) * Im z = 1.
rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from left to right).
rewrite the current goal using mul_SNo_zeroL (u * Im z) LuImz (from left to right).
rewrite the current goal using mul_SNo_zeroL 1 SNo_1 (from left to right).
We will prove Re z * (u * Re z + - (0 + - 0)) + - (0 + - (0 + 1 * (u * Im z))) * Im z = 1.
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using add_SNo_0L 0 SNo_0 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using add_SNo_0R (u * Re z) LuRez (from left to right).
We will prove Re z * (u * Re z) + - (0 + - (0 + 1 * (u * Im z))) * Im z = 1.
rewrite the current goal using mul_SNo_oneL (u * Im z) LuImz (from left to right).
We will prove Re z * (u * Re z) + - (0 + - (0 + (u * Im z))) * Im z = 1.
rewrite the current goal using add_SNo_0L (u * Im z) LuImz (from left to right).
rewrite the current goal using add_SNo_0L (- u * Im z) (SNo_minus_SNo (u * Im z) LuImz) (from left to right).
We will prove Re z * (u * Re z) + - (- (u * Im z)) * Im z = 1.
rewrite the current goal using mul_SNo_minus_distrL (- u * Im z) (Im z) (SNo_minus_SNo (u * Im z) LuImz) LImzR (from right to left).
rewrite the current goal using minus_SNo_invol (u * Im z) LuImz (from left to right).
We will prove Re z * (u * Re z) + (u * Im z) * Im z = 1.
rewrite the current goal using mul_SNo_com_3_0_1 (Re z) u (Re z) ?? ?? ?? (from left to right).
rewrite the current goal using mul_SNo_assoc u (Im z) (Im z) ?? ?? ?? (from right to left).
We will prove u * (Re z * Re z) + u * (Im z * Im z) = 1.
rewrite the current goal using mul_SNo_com u (Re z * Re z) ?? ?? (from left to right).
rewrite the current goal using mul_SNo_com u (Im z * Im z) ?? ?? (from left to right).
rewrite the current goal using mul_SNo_distrR (Re z * Re z) (Im z * Im z) u ?? ?? ?? (from right to left).
rewrite the current goal using exp_SNo_nat_2 (Re z) ?? (from right to left).
rewrite the current goal using exp_SNo_nat_2 (Im z) ?? (from right to left).
An exact proof term for the current goal is Hur.
We will prove Im (z ⨯ (u * Re z + :-: i ⨯ u * Im z)) = Im 1.
rewrite the current goal using mul_CSNo_CIm z (u * Re z + :-: i ⨯ u * Im z) Hz L1 (from left to right).
rewrite the current goal using Im_1 (from left to right).
We will prove Im (u * Re z + :-: i ⨯ u * Im z) * Re z + Im z * Re (u * Re z + :-: i ⨯ u * Im z) = 0.
rewrite the current goal using add_CSNo_CRe (u * Re z) (:-: i ⨯ u * Im z) LuRez' LmiuImz (from left to right).
rewrite the current goal using add_CSNo_CIm (u * Re z) (:-: i ⨯ u * Im z) LuRez' LmiuImz (from left to right).
We will prove (Im (u * Re z) + Im (:-: i ⨯ u * Im z)) * Re z + Im z * (Re (u * Re z) + Re (:-: i ⨯ u * Im z)) = 0.
rewrite the current goal using minus_CSNo_CRe (i ⨯ u * Im z) LiuImz (from left to right).
rewrite the current goal using minus_CSNo_CIm (i ⨯ u * Im z) LiuImz (from left to right).
We will prove (Im (u * Re z) + - Im (i ⨯ u * Im z)) * Re z + Im z * (Re (u * Re z) + - Re (i ⨯ u * Im z)) = 0.
rewrite the current goal using SNo_Re (u * Re z) LuRez (from left to right).
rewrite the current goal using SNo_Im (u * Re z) LuRez (from left to right).
We will prove (0 + - Im (i ⨯ u * Im z)) * Re z + Im z * ((u * Re z) + - Re (i ⨯ u * Im z)) = 0.
rewrite the current goal using mul_CSNo_CRe i (u * Im z) CSNo_Complex_i LuImz' (from left to right).
We will prove (0 + - Im (i ⨯ u * Im z)) * Re z + Im z * ((u * Re z) + - (Re i * Re (u * Im z) + - Im (u * Im z) * Im i)) = 0.
rewrite the current goal using mul_CSNo_CIm i (u * Im z) CSNo_Complex_i LuImz' (from left to right).
We will prove (0 + - (Im (u * Im z) * Re i + Im i * Re (u * Im z))) * Re z + Im z * ((u * Re z) + - (Re i * Re (u * Im z) + - Im (u * Im z) * Im i)) = 0.
rewrite the current goal using Re_i (from left to right).
rewrite the current goal using Im_i (from left to right).
We will prove (0 + - (Im (u * Im z) * 0 + 1 * Re (u * Im z))) * Re z + Im z * ((u * Re z) + - (0 * Re (u * Im z) + - Im (u * Im z) * 1)) = 0.
rewrite the current goal using SNo_Re (u * Im z) LuImz (from left to right).
rewrite the current goal using SNo_Im (u * Im z) LuImz (from left to right).
We will prove (0 + - (0 * 0 + 1 * (u * Im z))) * Re z + Im z * ((u * Re z) + - (0 * (u * Im z) + - 0 * 1)) = 0.
rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).
rewrite the current goal using mul_SNo_zeroL (u * Im z) ?? (from left to right).
rewrite the current goal using mul_SNo_zeroL 1 SNo_1 (from left to right).
rewrite the current goal using mul_SNo_oneL (u * Im z) ?? (from left to right).
We will prove (0 + - (0 + u * Im z)) * Re z + Im z * ((u * Re z) + - (0 + - 0)) = 0.
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using add_SNo_0L 0 SNo_0 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using add_SNo_0R (u * Re z) ?? (from left to right).
rewrite the current goal using add_SNo_0L (u * Im z) ?? (from left to right).
We will prove (0 + - (u * Im z)) * Re z + Im z * (u * Re z) = 0.
rewrite the current goal using add_SNo_0L (- (u * Im z)) (SNo_minus_SNo (u * Im z) ??) (from left to right).
We will prove (- (u * Im z)) * Re z + Im z * (u * Re z) = 0.
rewrite the current goal using mul_SNo_minus_distrL (u * Im z) (Re z) ?? ?? (from left to right).
We will prove - (u * Im z) * Re z + Im z * u * Re z = 0.
rewrite the current goal using mul_SNo_assoc u (Im z) (Re z) ?? ?? ?? (from right to left).
rewrite the current goal using mul_SNo_com (Im z) (Re z) ?? ?? (from left to right).
rewrite the current goal using mul_SNo_com_3_0_1 (Im z) u (Re z) ?? ?? ?? (from left to right).
We will prove - u * Re z * Im z + u * Im z * Re z = 0.
rewrite the current goal using mul_SNo_com (Re z) (Im z) ?? ?? (from left to right).
We will prove - u * Im z * Re z + u * Im z * Re z = 0.
An exact proof term for the current goal is add_SNo_minus_SNo_linv (u * Im z * Re z) (SNo_mul_SNo_3 u (Im z) (Re z) ?? ?? ??).
∎
Theorem. (recip_CSNo_invR)
∀z, CSNo z → z ≠ 0 → z ⨯ recip_CSNo z = 1
In Proofgold the corresponding term root is 838352... and proposition id is c71b18...
Proof:
Let z be given.
Assume Hz Hznz.
Set x to be the term Re z.
Set y to be the term Im z.
Set s to be the term x ^ 2 + y ^ 2.
Set u to be the term recip_SNo s.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is CSNo_ReR z Hz.
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is CSNo_ImR z Hz.
We prove the intermediate claim Ls: SNo s.
An exact proof term for the current goal is SNo_abs_sqr_CSNo z Hz.
We prove the intermediate claim LsC: CSNo s.
An exact proof term for the current goal is SNo_CSNo s Ls.
We prove the intermediate claim Lu: SNo u.
An exact proof term for the current goal is SNo_recip_SNo s Ls.
We prove the intermediate claim LuC: CSNo u.
An exact proof term for the current goal is SNo_CSNo u Lu.
We prove the intermediate claim LReuS: SNo (Re u).
An exact proof term for the current goal is CSNo_ReR u LuC.
We prove the intermediate claim LImuS: SNo (Im u).
An exact proof term for the current goal is CSNo_ImR u LuC.
We prove the intermediate claim Luy: CSNo (u ⨯ y).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is LuC.
Apply SNo_CSNo to the current goal.
An exact proof term for the current goal is Ly.
We prove the intermediate claim Lsnz: s ≠ 0.
Assume H1: s = 0.
Apply Hznz to the current goal.
We will prove z = 0.
An exact proof term for the current goal is abs_sqr_CSNo_zero z Hz H1.
We prove the intermediate claim L1: Re (i ⨯ u ⨯ y) = 0.
rewrite the current goal using mul_CSNo_CRe i (u ⨯ y) CSNo_Complex_i ?? (from left to right).
We will prove Re i * Re (u ⨯ y) + - (Im (u ⨯ y) * Im i) = 0.
rewrite the current goal using Re_i (from left to right).
rewrite the current goal using Im_i (from left to right).
We will prove 0 * Re (u ⨯ y) + - (Im (u ⨯ y) * 1) = 0.
rewrite the current goal using mul_SNo_zeroL (Re (u ⨯ y)) (CSNo_ReR (u ⨯ y) (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
rewrite the current goal using mul_SNo_oneR (Im (u ⨯ y)) (CSNo_ImR (u ⨯ y) (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
We will prove 0 + - Im (u ⨯ y) = 0.
rewrite the current goal using mul_CSNo_CIm u y LuC (SNo_CSNo y Ly) (from left to right).
We will prove 0 + - (Im y * Re u + Im u * Re y) = 0.
rewrite the current goal using SNo_Im y Ly (from left to right).
rewrite the current goal using SNo_Im u Lu (from left to right).
We will prove 0 + - (0 * Re u + 0 * Re y) = 0.
rewrite the current goal using mul_SNo_zeroL (Re u) LReuS (from left to right).
rewrite the current goal using mul_SNo_zeroL (Re y) (CSNo_ReR y (SNo_CSNo y Ly)) (from left to right).
We will prove 0 + - (0 + 0) = 0.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is add_SNo_0L 0 SNo_0.
We prove the intermediate claim L2: Im (i ⨯ u ⨯ y) = u * y.
rewrite the current goal using mul_CSNo_CIm i (u ⨯ y) CSNo_Complex_i ?? (from left to right).
We will prove Im (u ⨯ y) * Re i + Im i * Re (u ⨯ y) = u * y.
rewrite the current goal using Re_i (from left to right).
rewrite the current goal using Im_i (from left to right).
We will prove Im (u ⨯ y) * 0 + 1 * Re (u ⨯ y) = u * y.
rewrite the current goal using mul_SNo_zeroR (Im (u ⨯ y)) (CSNo_ImR (u ⨯ y) (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
rewrite the current goal using mul_SNo_oneL (Re (u ⨯ y)) (CSNo_ReR (u ⨯ y) (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
We will prove 0 + Re (u ⨯ y) = u * y.
rewrite the current goal using mul_CSNo_mul_SNo u y Lu Ly (from left to right).
rewrite the current goal using SNo_Re (u * y) (SNo_mul_SNo u y ?? ??) (from left to right).
We will prove 0 + u * y = u * y.
An exact proof term for the current goal is add_SNo_0L (u * y) (SNo_mul_SNo u y ?? ??).
We will prove z ⨯ pa (x :/: s) (- (y :/: s)) = 1.
Use transitivity with and (z ⨯ (u ⨯ x + :-: i ⨯ u ⨯ y)).
We will prove z ⨯ pa (x :/: s) (- (y :/: s)) = z ⨯ (u ⨯ x + :-: i ⨯ u ⨯ y).
Use f_equal.
We will prove pa (x :/: s) (- (y :/: s)) = u ⨯ x + :-: i ⨯ u ⨯ y.
Apply CSNo_ReIm_split (pa (x :/: s) (- (y :/: s))) (u ⨯ x + :-: i ⨯ u ⨯ y) to the current goal.
We will prove CSNo (pa (x :/: s) (- (y :/: s))).
Apply CSNo_I to the current goal.
We will prove SNo (x :/: s).
An exact proof term for the current goal is SNo_div_SNo x s ?? ??.
Apply SNo_minus_SNo to the current goal.
We will prove SNo (y :/: s).
An exact proof term for the current goal is SNo_div_SNo y s ?? ??.
We will prove CSNo (u ⨯ x + :-: i ⨯ u ⨯ y).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is CSNo_mul_CSNo u x LuC (SNo_CSNo x Lx).
Apply CSNo_minus_CSNo to the current goal.
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is CSNo_Complex_i.
An exact proof term for the current goal is CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly).
We will prove Re (pa (x :/: s) (- (y :/: s))) = Re (u ⨯ x + :-: i ⨯ u ⨯ y).
rewrite the current goal using CSNo_Re2 (x :/: s) (- (y :/: s)) (SNo_div_SNo x s Lx Ls) (SNo_minus_SNo (y :/: s) (SNo_div_SNo y s Ly Ls)) (from left to right).
We will prove x :/: s = Re (u ⨯ x + :-: i ⨯ u ⨯ y).
rewrite the current goal using add_CSNo_CRe (u ⨯ x) (:-: i ⨯ u ⨯ y) (CSNo_mul_CSNo u x LuC (SNo_CSNo x Lx)) (CSNo_minus_CSNo (i ⨯ u ⨯ y) (CSNo_mul_CSNo i (u ⨯ y) CSNo_Complex_i (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly)))) (from left to right).
We will prove x :/: s = Re (u ⨯ x) + Re (:-: i ⨯ u ⨯ y).
rewrite the current goal using mul_CSNo_mul_SNo u x Lu Lx (from left to right).
We will prove x :/: s = Re (u * x) + Re (:-: i ⨯ u ⨯ y).
rewrite the current goal using SNo_Re (u * x) (SNo_mul_SNo u x ?? ??) (from left to right).
We will prove x :/: s = u * x + Re (:-: i ⨯ u ⨯ y).
rewrite the current goal using minus_CSNo_CRe (i ⨯ u ⨯ y) (CSNo_mul_CSNo i (u ⨯ y) CSNo_Complex_i (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
We will prove x :/: s = u * x + - Re (i ⨯ u ⨯ y).
rewrite the current goal using L1 (from left to right).
We will prove x :/: s = u * x + - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove x :/: s = u * x + 0.
rewrite the current goal using add_SNo_0R (u * x) (SNo_mul_SNo u x ?? ??) (from left to right).
We will prove x * u = u * x.
An exact proof term for the current goal is mul_SNo_com x u ?? ??.
We will prove Im (pa (x :/: s) (- (y :/: s))) = Im (u ⨯ x + :-: i ⨯ u ⨯ y).
rewrite the current goal using CSNo_Im2 (x :/: s) (- (y :/: s)) (SNo_div_SNo x s Lx Ls) (SNo_minus_SNo (y :/: s) (SNo_div_SNo y s Ly Ls)) (from left to right).
rewrite the current goal using add_CSNo_CIm (u ⨯ x) (:-: i ⨯ u ⨯ y) (CSNo_mul_CSNo u x LuC (SNo_CSNo x Lx)) (CSNo_minus_CSNo (i ⨯ u ⨯ y) (CSNo_mul_CSNo i (u ⨯ y) CSNo_Complex_i (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly)))) (from left to right).
We will prove - (y :/: s) = Im (u ⨯ x) + Im (:-: i ⨯ u ⨯ y).
rewrite the current goal using minus_CSNo_CIm (i ⨯ u ⨯ y) (CSNo_mul_CSNo i (u ⨯ y) CSNo_Complex_i (CSNo_mul_CSNo u y LuC (SNo_CSNo y Ly))) (from left to right).
We will prove - (y :/: s) = Im (u ⨯ x) + - Im (i ⨯ u ⨯ y).
rewrite the current goal using mul_CSNo_mul_SNo u x Lu Lx (from left to right).
rewrite the current goal using SNo_Im (u * x) (SNo_mul_SNo u x ?? ??) (from left to right).
We will prove - (y :/: s) = 0 + - Im (i ⨯ u ⨯ y).
rewrite the current goal using L2 (from left to right).
We will prove - (y :/: s) = 0 + - (u * y).
We will prove - (y * u) = 0 + - (u * y).
rewrite the current goal using add_SNo_0L (- u * y) (SNo_minus_SNo (u * y) (SNo_mul_SNo u y ?? ??)) (from left to right).
Use f_equal.
An exact proof term for the current goal is mul_SNo_com y u ?? ??.
We will prove z ⨯ (u ⨯ x + :-: i ⨯ u ⨯ y) = 1.
Apply CSNo_relative_recip z Hz u Lu to the current goal.
We will prove (x ^ 2 + y ^ 2) * u = 1.
We will prove s * u = 1.
An exact proof term for the current goal is recip_SNo_invR s Ls Lsnz.
∎
Theorem. (recip_CSNo_invL)
∀z, CSNo z → z ≠ 0 → recip_CSNo z ⨯ z = 1
In Proofgold the corresponding term root is a9e4b7... and proposition id is 223581...
Proof:
Let z be given.
Assume Hz Hznz.
rewrite the current goal using mul_CSNo_com (recip_CSNo z) z (CSNo_recip_CSNo z Hz) Hz (from left to right).
An exact proof term for the current goal is recip_CSNo_invR z Hz Hznz.
∎
Theorem. (CSNo_div_CSNo)
∀z w, CSNo z → CSNo w → CSNo (div_CSNo z w)
In Proofgold the corresponding term root is 91055e... and proposition id is ca203c...
Proof:
Let z and w be given.
Assume Hz Hw.
An exact proof term for the current goal is CSNo_mul_CSNo z (recip_CSNo w) Hz (CSNo_recip_CSNo w Hw).
∎
Theorem. (mul_div_CSNo_invL)
∀z w, CSNo z → CSNo w → w ≠ 0 → (div_CSNo z w) ⨯ w = z
In Proofgold the corresponding term root is 9a03b4... and proposition id is 27df05...
Proof:
Let z and w be given.
Assume Hz Hw Hw0.
We will prove (z ⨯ recip_CSNo w) ⨯ w = z.
rewrite the current goal using mul_CSNo_assoc z (recip_CSNo w) w Hz (CSNo_recip_CSNo w Hw) Hw (from right to left).
We will prove z ⨯ (recip_CSNo w ⨯ w) = z.
rewrite the current goal using recip_CSNo_invL w Hw Hw0 (from left to right).
We will prove z ⨯ 1 = z.
An exact proof term for the current goal is mul_CSNo_1R z Hz.
∎
Theorem. (mul_div_CSNo_invR)
∀z w, CSNo z → CSNo w → w ≠ 0 → w ⨯ (div_CSNo z w) = z
In Proofgold the corresponding term root is 442304... and proposition id is ab3599...
Proof:
Let z and w be given.
Assume Hz Hw Hw0.
rewrite the current goal using mul_CSNo_com w (div_CSNo z w) Hw (CSNo_div_CSNo z w Hz Hw) (from left to right).
An exact proof term for the current goal is mul_div_CSNo_invL z w Hz Hw Hw0.
∎
Theorem. (sqrt_SNo_nonneg_sqr_id)
∀x, SNo x → 0 ≤ x → sqrt_SNo_nonneg (x ^ 2) = x
In Proofgold the corresponding term root is 4482ad... and proposition id is 21b2de...
Proof:
Let x be given.
Assume Hx Hxnn.
We prove the intermediate claim Lx2S: SNo (x ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat x Hx 2 nat_2.
We prove the intermediate claim Lx2nn: 0 ≤ x ^ 2.
rewrite the current goal using exp_SNo_nat_2 x Hx (from left to right).
An exact proof term for the current goal is SNo_sqr_nonneg x Hx.
We prove the intermediate claim Lsx2S: SNo (sqrt_SNo_nonneg (x ^ 2)).
An exact proof term for the current goal is SNo_sqrt_SNo_nonneg (x ^ 2) ?? ??.
We prove the intermediate claim Lsx2nn: 0 ≤ sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is sqrt_SNo_nonneg_nonneg (x ^ 2) ?? ??.
We prove the intermediate claim Lsx22xx: sqrt_SNo_nonneg (x ^ 2) * sqrt_SNo_nonneg (x ^ 2) = x * x.
rewrite the current goal using exp_SNo_nat_2 x Hx (from right to left).
An exact proof term for the current goal is sqrt_SNo_nonneg_sqr (x ^ 2) ?? ??.
Apply SNoLeE 0 x SNo_0 Hx Hxnn to the current goal.
Assume H1: 0 < x.
We prove the intermediate claim L1: 0 < sqrt_SNo_nonneg (x ^ 2).
Apply SNoLeE 0 (sqrt_SNo_nonneg (x ^ 2)) SNo_0 ?? ?? to the current goal.
Assume H2: 0 < sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is H2.
Assume H2: 0 = sqrt_SNo_nonneg (x ^ 2).
We will prove False.
Apply SNoLt_irref 0 to the current goal.
rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from right to left) at position 2.
We will prove 0 < 0 * 0.
rewrite the current goal using H2 (from left to right) at positions 2 and 3.
rewrite the current goal using Lsx22xx (from left to right).
We will prove 0 < x * x.
An exact proof term for the current goal is mul_SNo_pos_pos x x ?? ?? ?? ??.
Apply SNoLt_trichotomy_or_impred (sqrt_SNo_nonneg (x ^ 2)) x Lsx2S Hx to the current goal.
Assume H2: sqrt_SNo_nonneg (x ^ 2) < x.
We will prove False.
Apply SNoLt_irref (x * x) to the current goal.
We will prove x * x < x * x.
rewrite the current goal using Lsx22xx (from right to left) at position 1.
We will prove sqrt_SNo_nonneg (x ^ 2) * sqrt_SNo_nonneg (x ^ 2) < x * x.
An exact proof term for the current goal is pos_mul_SNo_Lt2 (sqrt_SNo_nonneg (x ^ 2)) (sqrt_SNo_nonneg (x ^ 2)) x x ?? ?? ?? ?? L1 L1 H2 H2.
Assume H2: sqrt_SNo_nonneg (x ^ 2) = x.
An exact proof term for the current goal is H2.
Assume H2: x < sqrt_SNo_nonneg (x ^ 2).
We will prove False.
Apply SNoLt_irref (x * x) to the current goal.
We will prove x * x < x * x.
rewrite the current goal using Lsx22xx (from right to left) at position 2.
We will prove x * x < sqrt_SNo_nonneg (x ^ 2) * sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is pos_mul_SNo_Lt2 x x (sqrt_SNo_nonneg (x ^ 2)) (sqrt_SNo_nonneg (x ^ 2)) ?? ?? ?? ?? H1 H1 H2 H2.
Assume H1: 0 = x.
rewrite the current goal using exp_SNo_nat_2 x Hx (from left to right).
rewrite the current goal using H1 (from right to left).
We will prove sqrt_SNo_nonneg (0 * 0) = 0.
rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).
We will prove sqrt_SNo_nonneg 0 = 0.
An exact proof term for the current goal is sqrt_SNo_nonneg_0.
∎
Theorem. (sqrt_SNo_nonneg_mon_strict)
∀x y, SNo x → SNo y → 0 ≤ x → x < y → sqrt_SNo_nonneg x < sqrt_SNo_nonneg y
In Proofgold the corresponding term root is 544c39... and proposition id is 02624d...
Proof:
Let x and y be given.
Assume Hx Hy Hxnn Hxy.
We prove the intermediate claim LsxS: SNo (sqrt_SNo_nonneg x).
An exact proof term for the current goal is SNo_sqrt_SNo_nonneg x ?? ??.
We prove the intermediate claim Lsxnn: 0 ≤ sqrt_SNo_nonneg x.
An exact proof term for the current goal is sqrt_SNo_nonneg_nonneg x ?? ??.
We prove the intermediate claim Lynn: 0 ≤ y.
Apply SNoLe_tra 0 x y SNo_0 ?? ?? ?? to the current goal.
We will prove x ≤ y.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hxy.
We prove the intermediate claim LsyS: SNo (sqrt_SNo_nonneg y).
An exact proof term for the current goal is SNo_sqrt_SNo_nonneg y ?? ??.
We prove the intermediate claim Lsynn: 0 ≤ sqrt_SNo_nonneg y.
An exact proof term for the current goal is sqrt_SNo_nonneg_nonneg y ?? ??.
Apply SNoLtLe_or (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg y) ?? ?? to the current goal.
Assume H2.
An exact proof term for the current goal is H2.
Assume H2: sqrt_SNo_nonneg y ≤ sqrt_SNo_nonneg x.
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLtLe_tra x y x Hx Hy Hx Hxy to the current goal.
We will prove y ≤ x.
rewrite the current goal using sqrt_SNo_nonneg_sqr y ?? ?? (from right to left).
rewrite the current goal using sqrt_SNo_nonneg_sqr x ?? ?? (from right to left).
We will prove sqrt_SNo_nonneg y * sqrt_SNo_nonneg y ≤ sqrt_SNo_nonneg x * sqrt_SNo_nonneg x.
Apply nonneg_mul_SNo_Le2 (sqrt_SNo_nonneg y) (sqrt_SNo_nonneg y) (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg x) ?? ?? ?? ?? ?? ?? ?? ?? to the current goal.
∎
Theorem. (sqrt_SNo_nonneg_mon)
∀x y, SNo x → SNo y → 0 ≤ x → x ≤ y → sqrt_SNo_nonneg x ≤ sqrt_SNo_nonneg y
In Proofgold the corresponding term root is 317df1... and proposition id is 30ecc9...
Proof:
Let x and y be given.
Assume Hx Hy Hxnn Hxy.
Apply SNoLeE x y Hx Hy Hxy to the current goal.
Assume H1: x < y.
We will prove sqrt_SNo_nonneg x ≤ sqrt_SNo_nonneg y.
Apply SNoLtLe to the current goal.
We will prove sqrt_SNo_nonneg x < sqrt_SNo_nonneg y.
An exact proof term for the current goal is sqrt_SNo_nonneg_mon_strict x y Hx Hy Hxnn H1.
Assume H1: x = y.
rewrite the current goal using H1 (from left to right).
Apply SNoLe_ref to the current goal.
∎
Theorem. (sqrt_SNo_nonneg_mul_SNo)
∀x y, SNo x → SNo y → 0 ≤ x → 0 ≤ y → sqrt_SNo_nonneg (x * y) = sqrt_SNo_nonneg x * sqrt_SNo_nonneg y
In Proofgold the corresponding term root is c83ae6... and proposition id is c2dc6b...
Proof:
Let x and y be given.
Assume Hx Hy Hxnn Hynn.
We prove the intermediate claim LsxS: SNo (sqrt_SNo_nonneg x).
An exact proof term for the current goal is SNo_sqrt_SNo_nonneg x ?? ??.
We prove the intermediate claim Lsxnn: 0 ≤ sqrt_SNo_nonneg x.
An exact proof term for the current goal is sqrt_SNo_nonneg_nonneg x ?? ??.
We prove the intermediate claim LsyS: SNo (sqrt_SNo_nonneg y).
An exact proof term for the current goal is SNo_sqrt_SNo_nonneg y ?? ??.
We prove the intermediate claim Lsynn: 0 ≤ sqrt_SNo_nonneg y.
An exact proof term for the current goal is sqrt_SNo_nonneg_nonneg y ?? ??.
We prove the intermediate claim LsxsyS: SNo (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L1: (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y) ^ 2 = x * y.
rewrite the current goal using exp_SNo_nat_2 (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y) ?? (from left to right).
We will prove (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y) * (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y) = x * y.
rewrite the current goal using mul_SNo_com_4_inner_mid (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg y) (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg y) ?? ?? ?? ?? (from left to right).
Use f_equal.
An exact proof term for the current goal is sqrt_SNo_nonneg_sqr x ?? ??.
An exact proof term for the current goal is sqrt_SNo_nonneg_sqr y ?? ??.
rewrite the current goal using L1 (from right to left).
Apply sqrt_SNo_nonneg_sqr_id to the current goal.
We will prove SNo (sqrt_SNo_nonneg x * sqrt_SNo_nonneg y).
An exact proof term for the current goal is LsxsyS.
We will prove 0 ≤ sqrt_SNo_nonneg x * sqrt_SNo_nonneg y.
Apply mul_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
∎
Definition. We define modulus_CSNo to be λz ⇒ sqrt_SNo_nonneg (abs_sqr_CSNo z) of type set → set.
In Proofgold the corresponding term root is 181351... and object id is 30af8e...
Theorem. (SNo_modulus_CSNo)
∀z, CSNo z → SNo (modulus_CSNo z)
In Proofgold the corresponding term root is fac03c... and proposition id is 5c6052...
Proof:
Let z be given.
Assume Hz.
We will prove SNo (sqrt_SNo_nonneg (abs_sqr_CSNo z)).
Apply SNo_sqrt_SNo_nonneg to the current goal.
An exact proof term for the current goal is SNo_abs_sqr_CSNo z Hz.
An exact proof term for the current goal is abs_sqr_CSNo_nonneg z Hz.
∎
Theorem. (modulus_CSNo_nonneg)
∀z, CSNo z → 0 ≤ modulus_CSNo z
In Proofgold the corresponding term root is 9e4a15... and proposition id is 834a2a...
Proof:
Let z be given.
Assume Hz.
We will prove 0 ≤ sqrt_SNo_nonneg (abs_sqr_CSNo z).
Apply sqrt_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is SNo_abs_sqr_CSNo z Hz.
An exact proof term for the current goal is abs_sqr_CSNo_nonneg z Hz.
∎
Definition. We define sqrt_CSNo to be λz ⇒ if Im z < 0 ∨ Im z = 0 ∧ Re z < 0 then pa (sqrt_SNo_nonneg (eps_ 1 * (Re z + modulus_CSNo z))) (- sqrt_SNo_nonneg (eps_ 1 * (- Re z + modulus_CSNo z))) else pa (sqrt_SNo_nonneg (eps_ 1 * (Re z + modulus_CSNo z))) (sqrt_SNo_nonneg (eps_ 1 * (- Re z + modulus_CSNo z))) of type set → set.
In Proofgold the corresponding term root is d9166c... and object id is c77a46...
Theorem. (sqrt_CSNo_sqrt)
∀z, CSNo z → sqrt_CSNo z2 = z
In Proofgold the corresponding term root is 41ae0b... and proposition id is 025230...
Proof:
Let z be given.
Assume Hz.
Set x to be the term Re z.
Set y to be the term Im z.
Set gamma to be the term (sqrt_SNo_nonneg (eps_ 1 * (x + modulus_CSNo z))).
Set delta to be the term (sqrt_SNo_nonneg (eps_ 1 * (- x + modulus_CSNo z))).
We will prove (if y < 0 ∨ y = 0 ∧ x < 0 then pa gamma (- delta) else pa gamma delta)2 = z.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is CSNo_ReR z Hz.
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is CSNo_ImR z Hz.
We prove the intermediate claim Lmx: SNo (- x).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Lx.
We prove the intermediate claim Lmy: SNo (- y).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Ly.
We prove the intermediate claim LmS: SNo (modulus_CSNo z).
An exact proof term for the current goal is SNo_modulus_CSNo z Hz.
We prove the intermediate claim Lmnn: 0 ≤ modulus_CSNo z.
An exact proof term for the current goal is modulus_CSNo_nonneg z Hz.
We prove the intermediate claim Lx2S: SNo (x ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat x Lx 2 nat_2.
We prove the intermediate claim Ly2S: SNo (y ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat y Ly 2 nat_2.
We prove the intermediate claim Lx2nn: 0 ≤ x ^ 2.
rewrite the current goal using exp_SNo_nat_2 x Lx (from left to right).
An exact proof term for the current goal is SNo_sqr_nonneg x Lx.
We prove the intermediate claim Ly2nn: 0 ≤ y ^ 2.
rewrite the current goal using exp_SNo_nat_2 y Ly (from left to right).
An exact proof term for the current goal is SNo_sqr_nonneg y Ly.
We prove the intermediate claim Lx2mx2: x ^ 2 = (- x) ^ 2.
rewrite the current goal using exp_SNo_nat_2 x Lx (from left to right).
rewrite the current goal using exp_SNo_nat_2 (- x) Lmx (from left to right).
We will prove x * x = (- x) * (- x).
Use symmetry.
An exact proof term for the current goal is mul_SNo_minus_minus x x Lx Lx.
We prove the intermediate claim LazS: SNo (abs_sqr_CSNo z).
An exact proof term for the current goal is SNo_abs_sqr_CSNo z Hz.
We prove the intermediate claim Laznn: 0 ≤ abs_sqr_CSNo z.
An exact proof term for the current goal is abs_sqr_CSNo_nonneg z Hz.
We prove the intermediate claim Lsx2S: SNo (sqrt_SNo_nonneg (x ^ 2)).
An exact proof term for the current goal is SNo_sqrt_SNo_nonneg (x ^ 2) ?? ??.
We prove the intermediate claim Lsx2nn: 0 ≤ sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is sqrt_SNo_nonneg_nonneg (x ^ 2) ?? ??.
We prove the intermediate claim Lsy2S: SNo (sqrt_SNo_nonneg (y ^ 2)).
An exact proof term for the current goal is SNo_sqrt_SNo_nonneg (y ^ 2) ?? ??.
We prove the intermediate claim Lmgtx: x ≤ modulus_CSNo z.
We will prove x ≤ sqrt_SNo_nonneg (x ^ 2 + y ^ 2).
Apply SNoLe_tra x (sqrt_SNo_nonneg (x ^ 2)) (sqrt_SNo_nonneg (x ^ 2 + y ^ 2)) Lx ?? ?? to the current goal.
We will prove x ≤ sqrt_SNo_nonneg (x ^ 2).
Apply SNoLtLe_or x 0 Lx SNo_0 to the current goal.
Assume H1: x < 0.
Apply SNoLe_tra x 0 (sqrt_SNo_nonneg (x ^ 2)) Lx SNo_0 ?? to the current goal.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H1.
We will prove 0 ≤ sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is Lsx2nn.
Assume H1: 0 ≤ x.
rewrite the current goal using sqrt_SNo_nonneg_sqr_id x Lx H1 (from left to right).
Apply SNoLe_ref to the current goal.
We will prove sqrt_SNo_nonneg (x ^ 2) ≤ sqrt_SNo_nonneg (x ^ 2 + y ^ 2).
Apply sqrt_SNo_nonneg_mon to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We will prove x ^ 2 ≤ x ^ 2 + y ^ 2.
rewrite the current goal using add_SNo_0R (x ^ 2) ?? (from right to left) at position 1.
We will prove x ^ 2 + 0 ≤ x ^ 2 + y ^ 2.
Apply add_SNo_Le2 to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is SNo_0.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lmgtnx: - x ≤ modulus_CSNo z.
We will prove - x ≤ sqrt_SNo_nonneg (x ^ 2 + y ^ 2).
Apply SNoLe_tra (- x) (sqrt_SNo_nonneg (x ^ 2)) (sqrt_SNo_nonneg (x ^ 2 + y ^ 2)) Lmx ?? ?? to the current goal.
We will prove - x ≤ sqrt_SNo_nonneg (x ^ 2).
Apply SNoLtLe_or (- x) 0 Lmx SNo_0 to the current goal.
Assume H1: - x < 0.
Apply SNoLe_tra (- x) 0 (sqrt_SNo_nonneg (x ^ 2)) Lmx SNo_0 ?? to the current goal.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H1.
We will prove 0 ≤ sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is Lsx2nn.
Assume H1: 0 ≤ - x.
rewrite the current goal using Lx2mx2 (from left to right).
rewrite the current goal using sqrt_SNo_nonneg_sqr_id (- x) Lmx H1 (from left to right).
Apply SNoLe_ref to the current goal.
We will prove sqrt_SNo_nonneg (x ^ 2) ≤ sqrt_SNo_nonneg (x ^ 2 + y ^ 2).
Apply sqrt_SNo_nonneg_mon to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We will prove x ^ 2 ≤ x ^ 2 + y ^ 2.
rewrite the current goal using add_SNo_0R (x ^ 2) ?? (from right to left) at position 1.
We will prove x ^ 2 + 0 ≤ x ^ 2 + y ^ 2.
Apply add_SNo_Le2 to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is SNo_0.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim LaS: SNo (x + modulus_CSNo z).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim LmaS: SNo (- x + modulus_CSNo z).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim LmmS: SNo (- modulus_CSNo z).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim LammS: SNo (x + - modulus_CSNo z).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Le1S: SNo (eps_ 1).
An exact proof term for the current goal is SNo_eps_ 1 (nat_p_omega 1 nat_1).
We prove the intermediate claim Le1nn: 0 ≤ eps_ 1.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos 1 (nat_p_omega 1 nat_1).
We prove the intermediate claim Le12S: SNo (eps_ 1 ^ 2).
Apply SNo_exp_SNo_nat to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is nat_2.
We prove the intermediate claim Le12nn: 0 ≤ eps_ 1 ^ 2.
rewrite the current goal using exp_SNo_nat_2 (eps_ 1) ?? (from left to right).
Apply mul_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Le1aS: SNo (eps_ 1 * (x + modulus_CSNo z)).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lann: 0 ≤ x + modulus_CSNo z.
rewrite the current goal using add_SNo_com x (modulus_CSNo z) ?? ?? (from left to right).
We will prove 0 ≤ modulus_CSNo z + x.
rewrite the current goal using minus_SNo_invol x Lx (from right to left).
We will prove 0 ≤ modulus_CSNo z + - - x.
Apply add_SNo_minus_Le2b (modulus_CSNo z) (- x) 0 ?? Lmx SNo_0 to the current goal.
We will prove 0 + - x ≤ modulus_CSNo z.
rewrite the current goal using add_SNo_0L (- x) Lmx (from left to right).
We will prove - x ≤ modulus_CSNo z.
An exact proof term for the current goal is Lmgtnx.
We prove the intermediate claim Le1ann: 0 ≤ eps_ 1 * (x + modulus_CSNo z).
Apply mul_SNo_nonneg_nonneg (eps_ 1) (x + modulus_CSNo z) to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Le1maS: SNo (eps_ 1 * (- x + modulus_CSNo z)).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lmann: 0 ≤ - x + modulus_CSNo z.
rewrite the current goal using add_SNo_com (- x) (modulus_CSNo z) ?? ?? (from left to right).
We will prove 0 ≤ modulus_CSNo z + - x.
Apply add_SNo_minus_Le2b (modulus_CSNo z) x 0 ?? Lx SNo_0 to the current goal.
We will prove 0 + x ≤ modulus_CSNo z.
rewrite the current goal using add_SNo_0L x Lx (from left to right).
We will prove x ≤ modulus_CSNo z.
An exact proof term for the current goal is Lmgtx.
We prove the intermediate claim Le1mann: 0 ≤ eps_ 1 * (- x + modulus_CSNo z).
Apply mul_SNo_nonneg_nonneg (eps_ 1) (- x + modulus_CSNo z) to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim LmxmzxmzS: SNo ((- x + modulus_CSNo z) * (x + modulus_CSNo z)).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lmxmzxmznn: 0 ≤ (- x + modulus_CSNo z) * (x + modulus_CSNo z).
Apply mul_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim LgammaS: SNo gamma.
Apply SNo_sqrt_SNo_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lgammann: 0 ≤ gamma.
Apply sqrt_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim LdeltaS: SNo delta.
Apply SNo_sqrt_SNo_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Ldeltann: 0 ≤ delta.
Apply sqrt_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim LmdeltaS: SNo (- delta).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim LdeltagammaS: SNo (delta * gamma).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lpa1: CSNo (pa gamma (- delta)).
Apply CSNo_I to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lpa2: CSNo (pa gamma delta).
Apply CSNo_I to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lpa1s: CSNo (pa gamma (- delta)2).
Apply CSNo_exp_CSNo_nat to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is nat_2.
We prove the intermediate claim Lpa2s: CSNo (pa gamma delta2).
Apply CSNo_exp_CSNo_nat to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is nat_2.
We prove the intermediate claim Lgamma2eq: gamma * gamma = eps_ 1 * (x + modulus_CSNo z).
An exact proof term for the current goal is sqrt_SNo_nonneg_sqr (eps_ 1 * (x + modulus_CSNo z)) ?? ??.
We prove the intermediate claim Ldelta2eq: delta * delta = eps_ 1 * (- x + modulus_CSNo z).
An exact proof term for the current goal is sqrt_SNo_nonneg_sqr (eps_ 1 * (- x + modulus_CSNo z)) ?? ??.
We prove the intermediate claim Ldeltagamma: delta * gamma = eps_ 1 * sqrt_SNo_nonneg (y ^ 2).
Apply sqrt_SNo_nonneg_mul_SNo (eps_ 1 * (- x + modulus_CSNo z)) (eps_ 1 * (x + modulus_CSNo z)) ?? ?? ?? ?? (λu _ ⇒ u = eps_ 1 * sqrt_SNo_nonneg (y ^ 2)) to the current goal.
We will prove sqrt_SNo_nonneg ((eps_ 1 * (- x + modulus_CSNo z)) * (eps_ 1 * (x + modulus_CSNo z))) = eps_ 1 * sqrt_SNo_nonneg (y ^ 2).
rewrite the current goal using mul_SNo_com_4_inner_mid (eps_ 1) (- x + modulus_CSNo z) (eps_ 1) (x + modulus_CSNo z) ?? ?? ?? ?? (from left to right).
We will prove sqrt_SNo_nonneg ((eps_ 1 * eps_ 1) * ((- x + modulus_CSNo z) * (x + modulus_CSNo z))) = eps_ 1 * sqrt_SNo_nonneg (y ^ 2).
rewrite the current goal using exp_SNo_nat_2 (eps_ 1) ?? (from right to left).
Apply sqrt_SNo_nonneg_mul_SNo (eps_ 1 ^ 2) ((- x + modulus_CSNo z) * (x + modulus_CSNo z)) ?? ?? ?? ?? (λ_ v ⇒ v = eps_ 1 * sqrt_SNo_nonneg (y ^ 2)) to the current goal.
We will prove sqrt_SNo_nonneg (eps_ 1 ^ 2) * sqrt_SNo_nonneg ((- x + modulus_CSNo z) * (x + modulus_CSNo z)) = eps_ 1 * sqrt_SNo_nonneg (y ^ 2).
rewrite the current goal using sqrt_SNo_nonneg_sqr_id (eps_ 1) ?? ?? (from left to right).
We will prove (eps_ 1) * sqrt_SNo_nonneg ((- x + modulus_CSNo z) * (x + modulus_CSNo z)) = eps_ 1 * sqrt_SNo_nonneg (y ^ 2).
Use f_equal.
Use f_equal.
We will prove (- x + modulus_CSNo z) * (x + modulus_CSNo z) = y ^ 2.
rewrite the current goal using SNo_foil (- x) (modulus_CSNo z) x (modulus_CSNo z) ?? ?? ?? ?? (from left to right).
We will prove (- x) * x + (- x) * modulus_CSNo z + modulus_CSNo z * x + modulus_CSNo z * modulus_CSNo z = y ^ 2.
rewrite the current goal using mul_SNo_minus_distrL x (modulus_CSNo z) ?? ?? (from left to right).
rewrite the current goal using mul_SNo_com (modulus_CSNo z) x ?? ?? (from left to right).
rewrite the current goal using add_SNo_minus_L2 (x * modulus_CSNo z) (modulus_CSNo z * modulus_CSNo z) (SNo_mul_SNo x (modulus_CSNo z) ?? ??) (SNo_mul_SNo (modulus_CSNo z) (modulus_CSNo z) ?? ??) (from left to right).
We will prove (- x) * x + modulus_CSNo z * modulus_CSNo z = y ^ 2.
We will prove (- x) * x + sqrt_SNo_nonneg (abs_sqr_CSNo z) * sqrt_SNo_nonneg (abs_sqr_CSNo z) = y ^ 2.
rewrite the current goal using sqrt_SNo_nonneg_sqr (abs_sqr_CSNo z) ?? ?? (from left to right).
We will prove (- x) * x + x ^ 2 + y ^ 2 = y ^ 2.
Apply mul_SNo_minus_distrL x x ?? ?? (λ_ v ⇒ v + x ^ 2 + y ^ 2 = y ^ 2) to the current goal.
rewrite the current goal using exp_SNo_nat_2 x ?? (from right to left).
We will prove - x ^ 2 + x ^ 2 + y ^ 2 = y ^ 2.
An exact proof term for the current goal is add_SNo_minus_L2 (x ^ 2) (y ^ 2) ?? ??.
We prove the intermediate claim Lgamma2mdelta2: gamma * gamma + - (delta * delta) = x.
rewrite the current goal using Lgamma2eq (from left to right).
rewrite the current goal using Ldelta2eq (from left to right).
We will prove eps_ 1 * (x + modulus_CSNo z) + - eps_ 1 * (- x + modulus_CSNo z) = x.
rewrite the current goal using mul_SNo_minus_distrR (eps_ 1) (- x + modulus_CSNo z) ?? ?? (from right to left).
We will prove eps_ 1 * (x + modulus_CSNo z) + eps_ 1 * (- (- x + modulus_CSNo z)) = x.
rewrite the current goal using minus_add_SNo_distr (- x) (modulus_CSNo z) ?? ?? (from left to right).
rewrite the current goal using minus_SNo_invol x ?? (from left to right).
We will prove eps_ 1 * (x + modulus_CSNo z) + eps_ 1 * (x + - modulus_CSNo z) = x.
rewrite the current goal using mul_SNo_distrL (eps_ 1) (x + modulus_CSNo z) (x + - modulus_CSNo z) ?? ?? ?? (from right to left).
We will prove eps_ 1 * ((x + modulus_CSNo z) + (x + - modulus_CSNo z)) = x.
rewrite the current goal using add_SNo_com_4_inner_mid x (modulus_CSNo z) x (- modulus_CSNo z) ?? ?? ?? ?? (from left to right).
We will prove eps_ 1 * ((x + x) + (modulus_CSNo z + - modulus_CSNo z)) = x.
rewrite the current goal using add_SNo_minus_SNo_rinv (modulus_CSNo z) ?? (from left to right).
We will prove eps_ 1 * ((x + x) + 0) = x.
rewrite the current goal using add_SNo_0R (x + x) (SNo_add_SNo x x ?? ??) (from left to right).
We will prove eps_ 1 * (x + x) = x.
rewrite the current goal using mul_SNo_distrL (eps_ 1) x x ?? ?? ?? (from left to right).
We will prove eps_ 1 * x + eps_ 1 * x = x.
rewrite the current goal using mul_SNo_distrR (eps_ 1) (eps_ 1) x ?? ?? ?? (from right to left).
We will prove (eps_ 1 + eps_ 1) * x = x.
rewrite the current goal using eps_1_half_eq1 (from left to right).
An exact proof term for the current goal is mul_SNo_oneL x ??.
Apply SNoLt_trichotomy_or_impred y 0 Ly SNo_0 to the current goal.
Assume H1: y < 0.
We prove the intermediate claim Lcase1cond: y < 0 ∨ y = 0 ∧ x < 0.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
rewrite the current goal using If_i_1 (y < 0 ∨ y = 0 ∧ x < 0) (pa gamma (- delta)) (pa gamma delta) Lcase1cond (from left to right).
We will prove pa gamma (- delta)2 = z.
Apply CSNo_ReIm_split (pa gamma (- delta)2) z ?? Hz to the current goal.
rewrite the current goal using exp_CSNo_nat_2 (pa gamma (- delta)) ?? (from left to right).
We will prove Re (pa gamma (- delta) ⨯ pa gamma (- delta)) = x.
rewrite the current goal using mul_CSNo_CRe (pa gamma (- delta)) (pa gamma (- delta)) ?? ?? (from left to right).
rewrite the current goal using CSNo_Re2 gamma (- delta) ?? ?? (from left to right).
rewrite the current goal using CSNo_Im2 gamma (- delta) ?? ?? (from left to right).
We will prove gamma * gamma + - ((- delta) * (- delta)) = x.
rewrite the current goal using mul_SNo_minus_minus delta delta ?? ?? (from left to right).
We will prove gamma * gamma + - (delta * delta) = x.
An exact proof term for the current goal is Lgamma2mdelta2.
rewrite the current goal using exp_CSNo_nat_2 (pa gamma (- delta)) ?? (from left to right).
We will prove Im (pa gamma (- delta) ⨯ pa gamma (- delta)) = y.
rewrite the current goal using mul_CSNo_CIm (pa gamma (- delta)) (pa gamma (- delta)) ?? ?? (from left to right).
rewrite the current goal using CSNo_Re2 gamma (- delta) ?? ?? (from left to right).
rewrite the current goal using CSNo_Im2 gamma (- delta) ?? ?? (from left to right).
We will prove (- delta) * gamma + (- delta) * gamma = y.
rewrite the current goal using mul_SNo_minus_distrL delta gamma ?? ?? (from left to right).
We will prove - delta * gamma + - delta * gamma = y.
rewrite the current goal using minus_add_SNo_distr (delta * gamma) (delta * gamma) ?? ?? (from right to left).
We will prove - (delta * gamma + delta * gamma) = y.
rewrite the current goal using Ldeltagamma (from left to right).
We will prove - (eps_ 1 * sqrt_SNo_nonneg (y ^ 2) + eps_ 1 * sqrt_SNo_nonneg (y ^ 2)) = y.
rewrite the current goal using mul_SNo_distrR (eps_ 1) (eps_ 1) (sqrt_SNo_nonneg (y ^ 2)) ?? ?? ?? (from right to left).
rewrite the current goal using eps_1_half_eq1 (from left to right).
rewrite the current goal using mul_SNo_oneL (sqrt_SNo_nonneg (y ^ 2)) ?? (from left to right).
We will prove - sqrt_SNo_nonneg (y ^ 2) = y.
rewrite the current goal using exp_SNo_nat_2 y ?? (from left to right).
We will prove - sqrt_SNo_nonneg (y * y) = y.
rewrite the current goal using mul_SNo_minus_minus y y ?? ?? (from right to left).
We will prove - sqrt_SNo_nonneg ((- y) * (- y)) = y.
rewrite the current goal using exp_SNo_nat_2 (- y) ?? (from right to left).
We will prove - sqrt_SNo_nonneg ((- y) ^ 2) = y.
We prove the intermediate claim L1: 0 ≤ - y.
Apply SNoLtLe to the current goal.
We will prove 0 < - y.
Apply minus_SNo_Lt_contra2 y 0 ?? SNo_0 to the current goal.
We will prove y < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1.
rewrite the current goal using sqrt_SNo_nonneg_sqr_id (- y) ?? ?? (from left to right).
An exact proof term for the current goal is minus_SNo_invol y ??.
Assume H1: y = 0.
Apply SNoLtLe_or x 0 Lx SNo_0 to the current goal.
Assume H2: x < 0.
We prove the intermediate claim Lcase1cond: y < 0 ∨ y = 0 ∧ x < 0.
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.
rewrite the current goal using If_i_1 (y < 0 ∨ y = 0 ∧ x < 0) (pa gamma (- delta)) (pa gamma delta) Lcase1cond (from left to right).
We will prove pa gamma (- delta)2 = z.
Apply CSNo_ReIm_split (pa gamma (- delta)2) z ?? Hz to the current goal.
rewrite the current goal using exp_CSNo_nat_2 (pa gamma (- delta)) ?? (from left to right).
We will prove Re (pa gamma (- delta) ⨯ pa gamma (- delta)) = x.
rewrite the current goal using mul_CSNo_CRe (pa gamma (- delta)) (pa gamma (- delta)) ?? ?? (from left to right).
rewrite the current goal using CSNo_Re2 gamma (- delta) ?? ?? (from left to right).
rewrite the current goal using CSNo_Im2 gamma (- delta) ?? ?? (from left to right).
We will prove gamma * gamma + - ((- delta) * (- delta)) = x.
rewrite the current goal using mul_SNo_minus_minus delta delta ?? ?? (from left to right).
We will prove gamma * gamma + - (delta * delta) = x.
An exact proof term for the current goal is Lgamma2mdelta2.
rewrite the current goal using exp_CSNo_nat_2 (pa gamma (- delta)) ?? (from left to right).
We will prove Im (pa gamma (- delta) ⨯ pa gamma (- delta)) = y.
rewrite the current goal using mul_CSNo_CIm (pa gamma (- delta)) (pa gamma (- delta)) ?? ?? (from left to right).
rewrite the current goal using CSNo_Re2 gamma (- delta) ?? ?? (from left to right).
rewrite the current goal using CSNo_Im2 gamma (- delta) ?? ?? (from left to right).
We will prove (- delta) * gamma + (- delta) * gamma = y.
rewrite the current goal using mul_SNo_minus_distrL delta gamma ?? ?? (from left to right).
We will prove - delta * gamma + - delta * gamma = y.
rewrite the current goal using Ldeltagamma (from left to right).
We will prove - eps_ 1 * sqrt_SNo_nonneg (y ^ 2) + - eps_ 1 * sqrt_SNo_nonneg (y ^ 2) = y.
rewrite the current goal using exp_SNo_nat_2 y ?? (from left to right).
rewrite the current goal using H1 (from left to right).
We will prove - eps_ 1 * sqrt_SNo_nonneg (0 * 0) + - eps_ 1 * sqrt_SNo_nonneg (0 * 0) = 0.
rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).
rewrite the current goal using sqrt_SNo_nonneg_0 (from left to right).
We will prove - eps_ 1 * 0 + - eps_ 1 * 0 = 0.
rewrite the current goal using mul_SNo_zeroR (eps_ 1) ?? (from left to right).
We will prove - 0 + - 0 = 0.
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove 0 + 0 = 0.
An exact proof term for the current goal is add_SNo_0L 0 SNo_0.
Assume H2: 0 ≤ x.
We prove the intermediate claim Lcase2cond: ¬ (y < 0 ∨ y = 0 ∧ x < 0).
Assume H.
Apply H to the current goal.
Assume H3: y < 0.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
rewrite the current goal using H1 (from left to right) at position 2.
An exact proof term for the current goal is H3.
Assume H.
Apply H to the current goal.
Assume H3: y = 0.
Assume H4: x < 0.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
An exact proof term for the current goal is SNoLtLe_tra x 0 x ?? SNo_0 ?? H4 H2.
rewrite the current goal using If_i_0 (y < 0 ∨ y = 0 ∧ x < 0) (pa gamma (- delta)) (pa gamma delta) Lcase2cond (from left to right).
We will prove pa gamma delta2 = z.
Apply CSNo_ReIm_split (pa gamma delta2) z ?? Hz to the current goal.
rewrite the current goal using exp_CSNo_nat_2 (pa gamma delta) ?? (from left to right).
We will prove Re (pa gamma delta ⨯ pa gamma delta) = x.
rewrite the current goal using mul_CSNo_CRe (pa gamma delta) (pa gamma delta) ?? ?? (from left to right).
rewrite the current goal using CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using CSNo_Im2 gamma delta ?? ?? (from left to right).
We will prove gamma * gamma + - (delta * delta) = x.
An exact proof term for the current goal is Lgamma2mdelta2.
rewrite the current goal using exp_CSNo_nat_2 (pa gamma delta) ?? (from left to right).
We will prove Im (pa gamma delta ⨯ pa gamma delta) = y.
rewrite the current goal using mul_CSNo_CIm (pa gamma delta) (pa gamma delta) ?? ?? (from left to right).
rewrite the current goal using CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using CSNo_Im2 gamma delta ?? ?? (from left to right).
We will prove delta * gamma + delta * gamma = y.
rewrite the current goal using Ldeltagamma (from left to right).
We will prove eps_ 1 * sqrt_SNo_nonneg (y ^ 2) + eps_ 1 * sqrt_SNo_nonneg (y ^ 2) = y.
rewrite the current goal using exp_SNo_nat_2 y ?? (from left to right).
rewrite the current goal using H1 (from left to right).
We will prove eps_ 1 * sqrt_SNo_nonneg (0 * 0) + eps_ 1 * sqrt_SNo_nonneg (0 * 0) = 0.
rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).
rewrite the current goal using sqrt_SNo_nonneg_0 (from left to right).
We will prove eps_ 1 * 0 + eps_ 1 * 0 = 0.
rewrite the current goal using mul_SNo_zeroR (eps_ 1) ?? (from left to right).
We will prove 0 + 0 = 0.
An exact proof term for the current goal is add_SNo_0L 0 SNo_0.
Assume H1: 0 < y.
We prove the intermediate claim Lcase2cond: ¬ (y < 0 ∨ y = 0 ∧ x < 0).
Assume H.
Apply H to the current goal.
Assume H2: y < 0.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
An exact proof term for the current goal is SNoLt_tra y 0 y ?? SNo_0 ?? H2 H1.
Assume H.
Apply H to the current goal.
Assume H2: y = 0.
Assume H3: x < 0.
Apply SNoLt_irref y to the current goal.
rewrite the current goal using H2 (from left to right) at position 1.
An exact proof term for the current goal is H1.
rewrite the current goal using If_i_0 (y < 0 ∨ y = 0 ∧ x < 0) (pa gamma (- delta)) (pa gamma delta) Lcase2cond (from left to right).
We will prove pa gamma delta2 = z.
Apply CSNo_ReIm_split (pa gamma delta2) z ?? Hz to the current goal.
rewrite the current goal using exp_CSNo_nat_2 (pa gamma delta) ?? (from left to right).
We will prove Re (pa gamma delta ⨯ pa gamma delta) = x.
rewrite the current goal using mul_CSNo_CRe (pa gamma delta) (pa gamma delta) ?? ?? (from left to right).
rewrite the current goal using CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using CSNo_Im2 gamma delta ?? ?? (from left to right).
We will prove gamma * gamma + - (delta * delta) = x.
An exact proof term for the current goal is Lgamma2mdelta2.
rewrite the current goal using exp_CSNo_nat_2 (pa gamma delta) ?? (from left to right).
We will prove Im (pa gamma delta ⨯ pa gamma delta) = y.
rewrite the current goal using mul_CSNo_CIm (pa gamma delta) (pa gamma delta) ?? ?? (from left to right).
rewrite the current goal using CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using CSNo_Im2 gamma delta ?? ?? (from left to right).
We will prove delta * gamma + delta * gamma = y.
rewrite the current goal using Ldeltagamma (from left to right).
We will prove eps_ 1 * sqrt_SNo_nonneg (y ^ 2) + eps_ 1 * sqrt_SNo_nonneg (y ^ 2) = y.
rewrite the current goal using mul_SNo_distrR (eps_ 1) (eps_ 1) (sqrt_SNo_nonneg (y ^ 2)) ?? ?? ?? (from right to left).
rewrite the current goal using eps_1_half_eq1 (from left to right).
rewrite the current goal using mul_SNo_oneL (sqrt_SNo_nonneg (y ^ 2)) ?? (from left to right).
We will prove sqrt_SNo_nonneg (y ^ 2) = y.
Apply sqrt_SNo_nonneg_sqr_id y ?? to the current goal.
We will prove 0 ≤ y.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H1.
∎
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.
Let i ≝ Complex_i
Let Re : set → set ≝ CSNo_Re
Let Im : set → set ≝ CSNo_Im
Let pa : set → set → set ≝ SNo_pair
Definition. We define complex to be {pa (u 0) (u 1)|u ∈ real ⨯ real} of type set.
In Proofgold the corresponding term root is c599ee... and object id is f73979...
Theorem. (complex_I)
∀x y ∈ real, pa x y ∈ complex
In Proofgold the corresponding term root is 179d8d... and proposition id is 1f9d1b...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
We will prove pa x y ∈ complex.
rewrite the current goal using tuple_2_0_eq x y (from right to left).
rewrite the current goal using tuple_2_1_eq x y (from right to left) at position 2.
We will prove pa ((x,y) 0) ((x,y) 1) ∈ complex.
Apply ReplI (real ⨯ real) (λu ⇒ pa (u 0) (u 1)) to the current goal.
We will prove (x,y) ∈ real ⨯ real.
An exact proof term for the current goal is tuple_2_setprod real real x Hx y Hy.
∎
Theorem. (complex_E)
∀z ∈ complex, ∀p : prop, (∀x y ∈ real, z = pa x y → p) → p
In Proofgold the corresponding term root is d4f71b... and proposition id is aee8b5...
Proof:
Let z be given.
Assume Hz.
Let p be given.
Assume Hp.
Apply ReplE_impred (real ⨯ real) (λu ⇒ pa (u 0) (u 1)) z Hz to the current goal.
Let u be given.
Assume Hu: u ∈ real ⨯ real.
Assume Hzu: z = pa (u 0) (u 1).
An exact proof term for the current goal is Hp (u 0) (ap0_Sigma real (λ_ ⇒ real) u Hu) (u 1) (ap1_Sigma real (λ_ ⇒ real) u Hu) Hzu.
∎
Theorem. (complex_CSNo)
∀z ∈ complex, CSNo z
In Proofgold the corresponding term root is 582187... and proposition id is 4bb77f...
Proof:
Let z be given.
Assume Hz.
Apply complex_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Assume Hzxy: z = pa x y.
We will prove CSNo z.
rewrite the current goal using Hzxy (from left to right).
Apply CSNo_I to the current goal.
An exact proof term for the current goal is real_SNo x Hx.
An exact proof term for the current goal is real_SNo y Hy.
∎
Theorem. (real_complex)
real ⊆ complex
In Proofgold the corresponding term root is 2e80dd... and proposition id is 303d34...
Proof:
Let x be given.
Assume Hx: x ∈ real.
We will prove x ∈ complex.
rewrite the current goal using SNo_pair_0 x (from right to left).
We will prove pa x 0 ∈ complex.
Apply complex_I to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is real_0.
∎
Theorem. (complex_0)
0 ∈ complex
In Proofgold the corresponding term root is c4c56d... and proposition id is e71ee2...
Proof:
An exact proof term for the current goal is real_complex 0 real_0.
∎
Theorem. (complex_1)
1 ∈ complex
In Proofgold the corresponding term root is 5b4c72... and proposition id is 614efe...
Proof:
An exact proof term for the current goal is real_complex 1 real_1.
∎
Theorem. (complex_i)
i ∈ complex
In Proofgold the corresponding term root is f45bb2... and proposition id is 61712b...
Proof:
We will prove pa 0 1 ∈ complex.
Apply complex_I to the current goal.
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is real_1.
∎
Theorem. (complex_Re_eq)
∀x y ∈ real, Re (pa x y) = x
In Proofgold the corresponding term root is 7b2cad... and proposition id is 14b73d...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
An exact proof term for the current goal is CSNo_Re2 x y (real_SNo x Hx) (real_SNo y Hy).
∎
Theorem. (complex_Im_eq)
∀x y ∈ real, Im (pa x y) = y
In Proofgold the corresponding term root is db9a6a... and proposition id is 1f8050...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
An exact proof term for the current goal is CSNo_Im2 x y (real_SNo x Hx) (real_SNo y Hy).
∎
Theorem. (complex_Re_real)
∀z ∈ complex, Re z ∈ real
In Proofgold the corresponding term root is 9febfe... and proposition id is c0c90f...
Proof:
Let z be given.
Assume Hz.
Apply complex_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy Hzxy.
rewrite the current goal using Hzxy (from left to right).
We will prove Re (pa x y) ∈ real.
rewrite the current goal using complex_Re_eq x Hx y Hy (from left to right).
We will prove x ∈ real.
An exact proof term for the current goal is Hx.
∎
Theorem. (complex_Im_real)
∀z ∈ complex, Im z ∈ real
In Proofgold the corresponding term root is c46a91... and proposition id is 21df46...
Proof:
Let z be given.
Assume Hz.
Apply complex_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy Hzxy.
rewrite the current goal using Hzxy (from left to right).
We will prove Im (pa x y) ∈ real.
rewrite the current goal using complex_Im_eq x Hx y Hy (from left to right).
We will prove y ∈ real.
An exact proof term for the current goal is Hy.
∎
Theorem. (complex_ReIm_split)
∀z w ∈ complex, Re z = Re w → Im z = Im w → z = w
In Proofgold the corresponding term root is 1bd022... and proposition id is 98bc08...
Proof:
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
An exact proof term for the current goal is CSNo_ReIm_split z w (complex_CSNo z Hz) (complex_CSNo w Hw).
∎
Theorem. (complex_minus_CSNo)
∀z ∈ complex, - z ∈ complex
In Proofgold the corresponding term root is 520df6... and proposition id is c94747...
Proof:
Let z be given.
Assume Hz.
We will prove pa (minus_SNo (Re z)) (minus_SNo (Im z)) ∈ complex.
Apply complex_I to the current goal.
Apply real_minus_SNo to the current goal.
An exact proof term for the current goal is complex_Re_real z Hz.
Apply real_minus_SNo to the current goal.
An exact proof term for the current goal is complex_Im_real z Hz.
∎
Theorem. (complex_conj_CSNo)
∀z ∈ complex, conj_CSNo z ∈ complex
In Proofgold the corresponding term root is e2bf24... and proposition id is d48643...
Proof:
Let z be given.
Assume Hz.
We will prove pa (Re z) (minus_SNo (Im z)) ∈ complex.
Apply complex_I to the current goal.
An exact proof term for the current goal is complex_Re_real z Hz.
Apply real_minus_SNo to the current goal.
An exact proof term for the current goal is complex_Im_real z Hz.
∎
Theorem. (complex_add_CSNo)
∀z w ∈ complex, z + w ∈ complex
In Proofgold the corresponding term root is 5605eb... and proposition id is cd011e...
Proof:
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
We will prove pa (add_SNo (Re z) (Re w)) (add_SNo (Im z) (Im w)) ∈ complex.
Apply complex_I to the current goal.
Apply real_add_SNo to the current goal.
An exact proof term for the current goal is complex_Re_real z Hz.
An exact proof term for the current goal is complex_Re_real w Hw.
Apply real_add_SNo to the current goal.
An exact proof term for the current goal is complex_Im_real z Hz.
An exact proof term for the current goal is complex_Im_real w Hw.
∎
Theorem. (complex_mul_CSNo)
∀z w ∈ complex, z * w ∈ complex
In Proofgold the corresponding term root is 1caebd... and proposition id is 2d494f...
Proof:
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
We will prove pa (add_SNo (mul_SNo (Re z) (Re w)) (minus_SNo (mul_SNo (Im w) (Im z)))) (add_SNo (mul_SNo (Im w) (Re z)) (mul_SNo (Im z) (Re w))) ∈ complex.
We prove the intermediate claim Lz0: Re z ∈ real.
An exact proof term for the current goal is complex_Re_real z Hz.
We prove the intermediate claim Lz1: Im z ∈ real.
An exact proof term for the current goal is complex_Im_real z Hz.
We prove the intermediate claim Lw0: Re w ∈ real.
An exact proof term for the current goal is complex_Re_real w Hw.
We prove the intermediate claim Lw1: Im w ∈ real.
An exact proof term for the current goal is complex_Im_real w Hw.
Apply complex_I to the current goal.
Apply real_add_SNo to the current goal.
Apply real_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply real_minus_SNo to the current goal.
Apply real_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply real_add_SNo to the current goal.
Apply real_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply real_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
∎
Theorem. (real_Re_eq)
∀x ∈ real, Re x = x
In Proofgold the corresponding term root is c8dfe7... and proposition id is de9b16...
Proof:
Let x be given.
Assume Hx.
rewrite the current goal using SNo_pair_0 x (from right to left) at position 1.
An exact proof term for the current goal is complex_Re_eq x Hx 0 real_0.
∎
Theorem. (real_Im_eq)
∀x ∈ real, Im x = 0
In Proofgold the corresponding term root is b04b30... and proposition id is 0ec6b4...
Proof:
Let x be given.
Assume Hx.
rewrite the current goal using SNo_pair_0 x (from right to left).
An exact proof term for the current goal is complex_Im_eq x Hx 0 real_0.
∎
Theorem. (mul_i_real_eq)
∀x ∈ real, i * x = pa 0 x
In Proofgold the corresponding term root is c137fe... and proposition id is 59baae...
Proof:
Let x be given.
Assume Hx.
We will prove pa (add_SNo (mul_SNo (Re (pa 0 1)) (Re x)) (minus_SNo (mul_SNo (Im x) (Im (pa 0 1))))) (add_SNo (mul_SNo (Im x) (Re (pa 0 1))) (mul_SNo (Im (pa 0 1)) (Re x))) = pa 0 x.
rewrite the current goal using real_Re_eq x Hx (from left to right).
rewrite the current goal using real_Im_eq x Hx (from left to right).
rewrite the current goal using complex_Re_eq 0 real_0 1 real_1 (from left to right).
rewrite the current goal using complex_Im_eq 0 real_0 1 real_1 (from left to right).
We will prove pa (add_SNo (mul_SNo 0 x) (minus_SNo (mul_SNo 0 1))) (add_SNo (mul_SNo 0 0) (mul_SNo 1 x)) = pa 0 x.
rewrite the current goal using mul_SNo_zeroL x (real_SNo x Hx) (from left to right).
rewrite the current goal using mul_SNo_zeroL 1 SNo_1 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).
rewrite the current goal using mul_SNo_oneL x (real_SNo x Hx) (from left to right).
We will prove pa (add_SNo 0 0) (add_SNo 0 x) = pa 0 x.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from left to right).
rewrite the current goal using add_SNo_0L x (real_SNo x Hx) (from left to right).
Use reflexivity.
∎
Theorem. (real_Re_i_eq)
∀x ∈ real, Re (i * x) = 0
In Proofgold the corresponding term root is 93568a... and proposition id is b18615...
Proof:
Let x be given.
Assume Hx.
rewrite the current goal using mul_i_real_eq x Hx (from left to right).
We will prove Re (pa 0 x) = 0.
An exact proof term for the current goal is complex_Re_eq 0 real_0 x Hx.
∎
Theorem. (real_Im_i_eq)
∀x ∈ real, Im (i * x) = x
In Proofgold the corresponding term root is 0dabe6... and proposition id is b8efce...
Proof:
Let x be given.
Assume Hx.
rewrite the current goal using mul_i_real_eq x Hx (from left to right).
We will prove Im (pa 0 x) = x.
An exact proof term for the current goal is complex_Im_eq 0 real_0 x Hx.
∎
Theorem. (complex_eta)
∀z ∈ complex, z = Re z + i * Im z
In Proofgold the corresponding term root is 233acb... and proposition id is 9c8714...
Proof:
Let z be given.
Assume Hz.
Apply complex_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy Hzxy.
rewrite the current goal using Hzxy (from left to right).
rewrite the current goal using complex_Re_eq x Hx y Hy (from left to right).
rewrite the current goal using complex_Im_eq x Hx y Hy (from left to right).
We will prove pa x y = x + i * y.
We will prove pa x y = pa (add_SNo (Re x) (Re (i * y))) (add_SNo (Im x) (Im (i * y))).
rewrite the current goal using real_Re_eq x Hx (from left to right).
rewrite the current goal using real_Im_eq x Hx (from left to right).
rewrite the current goal using real_Re_i_eq y Hy (from left to right).
rewrite the current goal using real_Im_i_eq y Hy (from left to right).
We will prove pa x y = pa (add_SNo x 0) (add_SNo 0 y).
rewrite the current goal using add_SNo_0R x (real_SNo x Hx) (from left to right).
rewrite the current goal using add_SNo_0L y (real_SNo y Hy) (from left to right).
Use reflexivity.
∎
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.
Theorem. (complex_recip_CSNo)
∀z ∈ complex, recip_CSNo z ∈ complex
In Proofgold the corresponding term root is a91c24... and proposition id is 310f5f...
Proof:
Let z be given.
Assume Hz.
We prove the intermediate claim Lz: CSNo z.
An exact proof term for the current goal is complex_CSNo z Hz.
Apply complex_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Assume Hzxy: z = pa x y.
We will prove recip_CSNo z ∈ complex.
We will prove pa (Re z :/: (Re z ^ 2 + Im z ^ 2)) (- (Im z :/: (Re z ^ 2 + Im z ^ 2))) ∈ complex.
We prove the intermediate claim LRez: Re z ∈ real.
rewrite the current goal using Hzxy (from left to right).
rewrite the current goal using complex_Re_eq x Hx y Hy (from left to right).
An exact proof term for the current goal is Hx.
We prove the intermediate claim LImz: Im z ∈ real.
rewrite the current goal using Hzxy (from left to right).
rewrite the current goal using complex_Im_eq x Hx y Hy (from left to right).
An exact proof term for the current goal is Hy.
We prove the intermediate claim LRez2: Re z ^ 2 ∈ real.
rewrite the current goal using exp_SNo_nat_2 (Re z) (CSNo_ReR z Lz) (from left to right).
An exact proof term for the current goal is real_mul_SNo (Re z) ?? (Re z) ??.
We prove the intermediate claim LImz2: Im z ^ 2 ∈ real.
rewrite the current goal using exp_SNo_nat_2 (Im z) (CSNo_ImR z Lz) (from left to right).
An exact proof term for the current goal is real_mul_SNo (Im z) ?? (Im z) ??.
We prove the intermediate claim LRez2Imz2: Re z ^ 2 + Im z ^ 2 ∈ real.
Apply real_add_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply complex_I to the current goal.
We will prove Re z :/: (Re z ^ 2 + Im z ^ 2) ∈ real.
Apply real_div_SNo to the current goal.
An exact proof term for the current goal is LRez.
An exact proof term for the current goal is LRez2Imz2.
We will prove - (Im z :/: (Re z ^ 2 + Im z ^ 2)) ∈ real.
Apply real_minus_SNo to the current goal.
Apply real_div_SNo to the current goal.
An exact proof term for the current goal is LImz.
An exact proof term for the current goal is LRez2Imz2.
∎
Theorem. (complex_div_CSNo)
∀z w ∈ complex, div_CSNo z w ∈ complex
In Proofgold the corresponding term root is efba54... and proposition id is b82141...
Proof:
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
An exact proof term for the current goal is complex_mul_CSNo z Hz (recip_CSNo w) (complex_recip_CSNo w Hw).
∎
End of Section ComplexDiv
Theorem. (complex_real_set_eq)
real = {z ∈ complex|Re z = z}
In Proofgold the corresponding term root is 6d3ae0... and proposition id is 3414d9...
Proof:
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ real.
Apply SepI to the current goal.
An exact proof term for the current goal is real_complex x Hx.
An exact proof term for the current goal is real_Re_eq x Hx.
Let z be given.
Assume Hz: z ∈ {z ∈ complex|Re z = z}.
Apply SepE complex (λz ⇒ Re z = z) z Hz to the current goal.
Assume Hz1: z ∈ complex.
Assume Hz2: Re z = z.
We will prove z ∈ real.
rewrite the current goal using Hz2 (from right to left).
An exact proof term for the current goal is complex_Re_real z Hz1.
∎
End of Section Complex