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) ?? ?? ??).
∎