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

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.

∎