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 ℚ ⊆ ℂ

Proof

Step Hyp Ref Expression
1 qssre ℚ ⊆ ℝ
2 ax-resscn ℝ ⊆ ℂ
3 1 2 sstri ℚ ⊆ ℂ