Let x0 of type ι be given.
Apply complex_CSNo with
x0.
The subproof is completed by applying H0.
Apply complex_E with
x0,
recip_CSNo x0 ∈ complex leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply H4 with
λ x3 x4 . CSNo_Re x4 ∈ real.
Apply complex_Re_eq with
x1,
x2,
λ x3 x4 . x4 ∈ real leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
Apply H4 with
λ x3 x4 . CSNo_Im x4 ∈ real.
Apply complex_Im_eq with
x1,
x2,
λ x3 x4 . x4 ∈ real leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H3.
Apply exp_SNo_nat_2 with
CSNo_Re x0,
λ x3 x4 . x4 ∈ real leaving 2 subgoals.
Apply CSNo_ReR with
x0.
The subproof is completed by applying L1.
Apply real_mul_SNo with
CSNo_Re x0,
CSNo_Re x0 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L5.
Apply exp_SNo_nat_2 with
CSNo_Im x0,
λ x3 x4 . x4 ∈ real leaving 2 subgoals.
Apply CSNo_ImR with
x0.
The subproof is completed by applying L1.
Apply real_mul_SNo with
CSNo_Im x0,
CSNo_Im x0 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L6.
Apply real_add_SNo with
exp_SNo_nat (CSNo_Re x0) 2,
exp_SNo_nat (CSNo_Im x0) 2 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L8.