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.
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 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.