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