Metamath Proof Explorer


Theorem imcncf

Description: Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Assertion imcncf : cn

Proof

Step Hyp Ref Expression
1 imf :
2 imcn2 x y + z + w w x < z w x < y
3 2 rgen2 x y + z + w w x < z w x < y
4 ssid
5 ax-resscn
6 elcncf2 : cn : x y + z + w w x < z w x < y
7 4 5 6 mp2an : cn : x y + z + w w x < z w x < y
8 1 3 7 mpbir2an : cn