This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qsscn

Description: The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion qsscn 
|- QQ C_ CC

Proof

Step Hyp Ref Expression
1 qssre 
 |-  QQ C_ RR
2 ax-resscn 
 |-  RR C_ CC
3 1 2 sstri 
 |-  QQ C_ CC