Metamath Proof Explorer

Theorem nthruc

Description: The sequence NN , ZZ , QQ , RR , and CC forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to ZZ but not NN , one-half belongs to QQ but not ZZ , the square root of 2 belongs to RR but not QQ , and finally that the imaginary number _i belongs to CC but not RR . See nthruz for a further refinement. (Contributed by NM, 12-Jan-2002)

Ref Expression
Assertion nthruc 
|- ( ( NN C. ZZ /\ ZZ C. QQ ) /\ ( QQ C. RR /\ RR C. CC ) )

Proof

Step Hyp Ref Expression
1 nnssz 
 |-  NN C_ ZZ
2 0z 
 |-  0 e. ZZ
3 0nnn 
 |-  -. 0 e. NN
4 2 3 pm3.2i 
 |-  ( 0 e. ZZ /\ -. 0 e. NN )
5 ssnelpss 
 |-  ( NN C_ ZZ -> ( ( 0 e. ZZ /\ -. 0 e. NN ) -> NN C. ZZ ) )
6 1 4 5 mp2 
 |-  NN C. ZZ
7 zssq 
 |-  ZZ C_ QQ
8 1z 
 |-  1 e. ZZ
9 2nn 
 |-  2 e. NN
10 znq 
 |-  ( ( 1 e. ZZ /\ 2 e. NN ) -> ( 1 / 2 ) e. QQ )
11 8 9 10 mp2an 
 |-  ( 1 / 2 ) e. QQ
12 halfnz 
 |-  -. ( 1 / 2 ) e. ZZ
13 11 12 pm3.2i 
 |-  ( ( 1 / 2 ) e. QQ /\ -. ( 1 / 2 ) e. ZZ )
14 ssnelpss 
 |-  ( ZZ C_ QQ -> ( ( ( 1 / 2 ) e. QQ /\ -. ( 1 / 2 ) e. ZZ ) -> ZZ C. QQ ) )
15 7 13 14 mp2 
 |-  ZZ C. QQ
16 6 15 pm3.2i 
 |-  ( NN C. ZZ /\ ZZ C. QQ )
17 qssre 
 |-  QQ C_ RR
18 sqrt2re 
 |-  ( sqrt ` 2 ) e. RR
19 sqrt2irr 
 |-  ( sqrt ` 2 ) e/ QQ
20 19 neli 
 |-  -. ( sqrt ` 2 ) e. QQ
21 18 20 pm3.2i 
 |-  ( ( sqrt ` 2 ) e. RR /\ -. ( sqrt ` 2 ) e. QQ )
22 ssnelpss 
 |-  ( QQ C_ RR -> ( ( ( sqrt ` 2 ) e. RR /\ -. ( sqrt ` 2 ) e. QQ ) -> QQ C. RR ) )
23 17 21 22 mp2 
 |-  QQ C. RR
24 ax-resscn 
 |-  RR C_ CC
25 ax-icn 
 |-  _i e. CC
26 inelr 
 |-  -. _i e. RR
27 25 26 pm3.2i 
 |-  ( _i e. CC /\ -. _i e. RR )
28 ssnelpss 
 |-  ( RR C_ CC -> ( ( _i e. CC /\ -. _i e. RR ) -> RR C. CC ) )
29 24 27 28 mp2 
 |-  RR C. CC
30 23 29 pm3.2i 
 |-  ( QQ C. RR /\ RR C. CC )
31 16 30 pm3.2i 
 |-  ( ( NN C. ZZ /\ ZZ C. QQ ) /\ ( QQ C. RR /\ RR C. CC ) )