\chapter{Explicit Complex Numbers}
\section{explicit\_Complex}\label{fgihahmgjgdgjgehpfdepgngahmgfgih}Let $ C : {\iota}$ be given.
Let $ Re, Im : {{\iota}\unicdbdjdcd{\iota}}$ be given.
Let $ zero, one, i : {\iota}$ be given.
Let $ plus, mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
Let $R$ be ${\{z \in {C}|{{{Re}~{z}}={z}}\}}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfdepgngahmgfgih}
$\mname{explicit\_Complex}$ is the opaque object of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & bacb8536bbb356aa59ba321fb8eade607d1654d8a7e0b33887be9afbcfa5c504 \\
Pure Object Address: & TMa5hw3hNC7WqagUsMEGJJWin8GCkpqUbye \\
Theory Object Id: & b05866b1253726652d5f4c1d3535f4becde9eb97625c4d28ff50ec895ae17e92 \\
Theory Object Address: & TMRhnV2LR2j1o74NVG7hN916xvy2TnzLfWi
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdepgngahmgfgihpfje} ${{{{{{{\mname{explicit\_Field}}~{C}}~{zero}}~{one}}~{plus}}~{mult}}\unicdbdjdcd{{({\unicdcdaddd leq : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{{{{{\mname{explicit\_Reals}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}})}\unicdbdjdcd{{({\unicdcdadad z \in {C} .  {{{Im}~{z}} \in {R}}})}\unicdbdjdcd{{({{i} \in {C}})}\unicdbdjdcd{{({\unicdcdadad z \in {C} .  {{{Re}~{z}} \in {C}}})}\unicdbdjdcd{{({\unicdcdadad z \in {C} .  {{{Im}~{z}} \in {C}}})}\unicdbdjdcd{{({\unicdcdadad z \in {C} .  {{z}={{{Re}~{z}}+{{i}*{{Im}~{z}}}}}})}\unicdbdjdcd{{({\unicdcdadad z w \in {C} .  {{{{Re}~{z}}={{Re}~{w}}}\unicdbdjdcd{{{{Im}~{z}}={{Im}~{w}}}\unicdbdjdcd{{z}={w}}}}})}\unicdbdjdcd{{({{{{i}*{i}}+{one}}={zero}})}\unicdbdjdcd{\mname{explicit\_Complex}}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 268f09d277e2bc0bbdfd926099d5d0debc50c59632e87cb4880853219a5af391 \\
Pure Prop Address: & TMRxTtLhVXgTi52JwYrkhvhZ4W438K5Bc75 \\
Theory Prop Id: & 96b235cacae981b88c42f891a869e55791d51cd380dc6f034e33a36b2a934b7f \\
Theory Prop Address: & TMNg8okmnYHks6UoVuT2Cwi18J8zvS1fDhA
\end{tabular}
\end{center}

\end{theorem}
\section{RealsToComplex}\label{cffgbgmgdhefpgdepgngahmgfgih}Let $ R : {\iota}$ be given.
Let $ zero, one : {\iota}$ be given.
Let $ plus, mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
{\bf{Notation.}} We use $\prenc{-}$ as a prefix operator  corresponding to applying term ${{{{{{\mname{explicit\_Field\_minus}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}$.
Let $ leq : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ be given.
Let $ pa : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
Let $C : {\iota}$ be ${{{{{\mname{ReplSep2}}~{R}}~{({\uniddcgcg \_ .  {R}})}}~{({\uniddcgcg x y .  {\mname{True}}})}}~{pa}}$.
Let $Re : {{\iota}\unicdbdjdcd{\iota}}$ be ${\uniddcgcg z .  {{\mname{Eps\_i}}~{({\uniddcgcg x .  {{{x} \in {R}}\unicdcdcdhd{\unicdcdaddd y \in {R} .  {{z}={{{pa}~{x}}~{y}}}}}})}}}$.
Let $Im : {{\iota}\unicdbdjdcd{\iota}}$ be ${\uniddcgcg z .  {{\mname{Eps\_i}}~{({\uniddcgcg y .  {{{y} \in {R}}\unicdcdcdhd{{z}={{{pa}~{({{Re}~{z}})}}~{y}}}}})}}}$.
Let $Re' : {{\iota}\unicdbdjdcd{\iota}}$ be ${\uniddcgcg z .  {{{pa}~{({{Re}~{z}})}}~{zero}}}$.
Let $Im' : {{\iota}\unicdbdjdcd{\iota}}$ be ${\uniddcgcg z .  {{{pa}~{({{Im}~{z}})}}~{zero}}}$.
Let $R'$ be ${\{z \in {C}|{{{Re'}~{z}}={z}}\}}$.
Let $zero' : {\iota}$ be ${{{pa}~{zero}}~{zero}}$.
Let $one' : {\iota}$ be ${{{pa}~{one}}~{zero}}$.
Let $i' : {\iota}$ be ${{{pa}~{zero}}~{one}}$.
Let $plus' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be ${\uniddcgcg z w .  {{{pa}~{({{{Re}~{z}}+{{Re}~{w}}})}}~{({{{Im}~{z}}+{{Im}~{w}}})}}}$.
Let $mult' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be ${\uniddcgcg z w .  {{{pa}~{({{{{Re}~{z}}*{{Re}~{w}}}+{\prenc{{({{{Im}~{z}}*{{Im}~{w}}})}}}})}}~{({{{{Re}~{z}}*{{Im}~{w}}}+{{{Im}~{z}}*{{Re}~{w}}}})}}}$.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcffgbgmgdhefpgdepgngahmgfgih} ${{{{{{{{\mname{explicit\_Reals}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}\unicdbdjdcd{{({\unicdcdadad x1 y1 x2 y2 \in {R} .  {{{{{pa}~{x1}}~{y1}}={{{pa}~{x2}}~{y2}}}\unicdbdjdcd{{{x1}={x2}}\unicdcdcdhd{{y1}={y2}}}}})}\unicdbdjdcd{{{{{{{{{\mname{explicit\_Complex}}~{C}}~{Re'}}~{Im'}}~{zero'}}~{one'}}~{i'}}~{plus'}}~{mult'}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2ad9aca053f28eb85de9030b6d0c162b4a5b9d27321469a234f5fd4f7494f082 \\
Pure Prop Address: & TMZe3552GyhJu3DKLRhE4SjsgRt2gUXYYAj \\
Theory Prop Id: & 94ebebccd5b25112c23201728486a12ca244ef29cec6c0b6edb5800c93b915a1 \\
Theory Prop Address: & TMYxnxapnSFDiLDun4UJDavvHoYvtr8q8ig
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcffgbgmgdhefpgdepgngahmgfgihpffgihbgdgehpfdffhcgbh} ${{{{{{{{\mname{explicit\_Reals}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}\unicdbdjdcd{{({\unicdcdadad x1 y1 x2 y2 \in {R} .  {{{{{pa}~{x1}}~{y1}}={{{pa}~{x2}}~{y2}}}\unicdbdjdcd{{{x1}={x2}}\unicdcdcdhd{{y1}={y2}}}}})}\unicdbdjdcd{{({\unicdcdadad x \in {R} .  {{{{pa}~{x}}~{zero}}={x}}})}\unicdbdjdcd{{{{{{{{{{{{{{{\mname{explicit\_Complex}}~{C}}~{Re'}}~{Im'}}~{zero'}}~{one'}}~{i'}}~{plus'}}~{mult'}}\unicdcdcdhd{{R} \subseteq {C}}}\unicdcdcdhd{({\unicdcdadad x \in {R} .  {{{Re}~{x}}={x}}})}}\unicdcdcdhd{{zero'}={zero}}}\unicdcdcdhd{{one'}={one}}}\unicdcdcdhd{({\unicdcdadad x y \in {R} .  {{{{plus'}~{x}}~{y}}={{x}+{y}}}})}}\unicdcdcdhd{({\unicdcdadad x y \in {R} .  {{{{mult'}~{x}}~{y}}={{x}*{y}}}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 51e5a4d1ee792ab93743b09a8d55064358a260b77bd867b77ab2daff184f7a69 \\
Pure Prop Address: & TMTBqnvgpx9i3Hkd8KYMbTasfi1QQ5opvQp \\
Theory Prop Id: & 3374381402db954a24b8597cb95c93bc1377e068c7c8bb9687c3849cb7a77c53 \\
Theory Prop Address: & TMMpvJrvnSTg7ZDxz5rVpUpARY5uc36QjPi
\end{tabular}
\end{center}

\end{theorem}
