Description: The rational numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | qsubdrg | |- ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | qcn | |- ( x e. QQ -> x e. CC ) |
|
| 2 | qaddcl | |- ( ( x e. QQ /\ y e. QQ ) -> ( x + y ) e. QQ ) |
|
| 3 | qnegcl | |- ( x e. QQ -> -u x e. QQ ) |
|
| 4 | zssq | |- ZZ C_ QQ |
|
| 5 | 1z | |- 1 e. ZZ |
|
| 6 | 4 5 | sselii | |- 1 e. QQ |
| 7 | qmulcl | |- ( ( x e. QQ /\ y e. QQ ) -> ( x x. y ) e. QQ ) |
|
| 8 | qreccl | |- ( ( x e. QQ /\ x =/= 0 ) -> ( 1 / x ) e. QQ ) |
|
| 9 | 1 2 3 6 7 8 | cnsubdrglem | |- ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) |