>>160
＞虚数を定義して複素数を使って実数公理系の定理を証明していいんですか？

体の言語において、実数は複素数から解釈可能ではない
つまり、複素数体Cにおいて実数体Rのコピーを定義することさえできないので、実数の定理を証明することもできないはず