Metamath Proof Explorer

Theorem cnsubrg

Description: There are no subrings of the complex numbers strictly between RR and CC . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion cnsubrg 
|- ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) -> R e. { RR , CC } )

Proof

Step Hyp Ref Expression
1 ssdif0 
 |-  ( R C_ RR <-> ( R \ RR ) = (/) )
2 simpr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ R C_ RR ) -> R C_ RR )
3 simplr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ R C_ RR ) -> RR C_ R )
4 2 3 eqssd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ R C_ RR ) -> R = RR )
5 4 orcd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ R C_ RR ) -> ( R = RR \/ R = CC ) )
6 1 5 sylan2br 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( R \ RR ) = (/) ) -> ( R = RR \/ R = CC ) )
7 n0 
 |-  ( ( R \ RR ) =/= (/) <-> E. x x e. ( R \ RR ) )
8 simpll 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> R e. ( SubRing ` CCfld ) )
9 cnfldbas 
 |-  CC = ( Base ` CCfld )
10 9 subrgss 
 |-  ( R e. ( SubRing ` CCfld ) -> R C_ CC )
11 8 10 syl 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> R C_ CC )
12 replim 
 |-  ( y e. CC -> y = ( ( Re ` y ) + ( _i x. ( Im ` y ) ) ) )
13 12 ad2antll 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> y = ( ( Re ` y ) + ( _i x. ( Im ` y ) ) ) )
14 simpll 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> R e. ( SubRing ` CCfld ) )
15 simplr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> RR C_ R )
16 recl 
 |-  ( y e. CC -> ( Re ` y ) e. RR )
17 16 ad2antll 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> ( Re ` y ) e. RR )
18 15 17 sseldd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> ( Re ` y ) e. R )
19 ax-icn 
 |-  _i e. CC
20 19 a1i 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> _i e. CC )
21 eldifi 
 |-  ( x e. ( R \ RR ) -> x e. R )
22 21 adantl 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> x e. R )
23 11 22 sseldd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> x e. CC )
24 imcl 
 |-  ( x e. CC -> ( Im ` x ) e. RR )
25 23 24 syl 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( Im ` x ) e. RR )
26 25 recnd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( Im ` x ) e. CC )
27 eldifn 
 |-  ( x e. ( R \ RR ) -> -. x e. RR )
28 27 adantl 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> -. x e. RR )
29 reim0b 
 |-  ( x e. CC -> ( x e. RR <-> ( Im ` x ) = 0 ) )
30 29 necon3bbid 
 |-  ( x e. CC -> ( -. x e. RR <-> ( Im ` x ) =/= 0 ) )
31 23 30 syl 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( -. x e. RR <-> ( Im ` x ) =/= 0 ) )
32 28 31 mpbid 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( Im ` x ) =/= 0 )
33 20 26 32 divcan4d 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( ( _i x. ( Im ` x ) ) / ( Im ` x ) ) = _i )
34 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` x ) e. CC ) -> ( _i x. ( Im ` x ) ) e. CC )
35 19 26 34 sylancr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( _i x. ( Im ` x ) ) e. CC )
36 35 26 32 divrecd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( ( _i x. ( Im ` x ) ) / ( Im ` x ) ) = ( ( _i x. ( Im ` x ) ) x. ( 1 / ( Im ` x ) ) ) )
37 33 36 eqtr3d 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> _i = ( ( _i x. ( Im ` x ) ) x. ( 1 / ( Im ` x ) ) ) )
38 23 recld 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( Re ` x ) e. RR )
39 38 recnd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( Re ` x ) e. CC )
40 23 39 negsubd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( x + -u ( Re ` x ) ) = ( x - ( Re ` x ) ) )
41 replim 
 |-  ( x e. CC -> x = ( ( Re ` x ) + ( _i x. ( Im ` x ) ) ) )
42 23 41 syl 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> x = ( ( Re ` x ) + ( _i x. ( Im ` x ) ) ) )
43 42 oveq1d 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( x - ( Re ` x ) ) = ( ( ( Re ` x ) + ( _i x. ( Im ` x ) ) ) - ( Re ` x ) ) )
44 39 35 pncan2d 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( ( ( Re ` x ) + ( _i x. ( Im ` x ) ) ) - ( Re ` x ) ) = ( _i x. ( Im ` x ) ) )
45 40 43 44 3eqtrd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( x + -u ( Re ` x ) ) = ( _i x. ( Im ` x ) ) )
46 simplr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> RR C_ R )
47 38 renegcld 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> -u ( Re ` x ) e. RR )
48 46 47 sseldd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> -u ( Re ` x ) e. R )
49 cnfldadd 
 |-  + = ( +g ` CCfld )
50 49 subrgacl 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. R /\ -u ( Re ` x ) e. R ) -> ( x + -u ( Re ` x ) ) e. R )
51 8 22 48 50 syl3anc 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( x + -u ( Re ` x ) ) e. R )
52 45 51 eqeltrrd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( _i x. ( Im ` x ) ) e. R )
53 25 32 rereccld 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( 1 / ( Im ` x ) ) e. RR )
54 46 53 sseldd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( 1 / ( Im ` x ) ) e. R )
55 cnfldmul 
 |-  x. = ( .r ` CCfld )
56 55 subrgmcl 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ ( _i x. ( Im ` x ) ) e. R /\ ( 1 / ( Im ` x ) ) e. R ) -> ( ( _i x. ( Im ` x ) ) x. ( 1 / ( Im ` x ) ) ) e. R )
57 8 52 54 56 syl3anc 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( ( _i x. ( Im ` x ) ) x. ( 1 / ( Im ` x ) ) ) e. R )
58 37 57 eqeltrd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> _i e. R )
59 58 adantrr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> _i e. R )
60 imcl 
 |-  ( y e. CC -> ( Im ` y ) e. RR )
61 60 ad2antll 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> ( Im ` y ) e. RR )
62 15 61 sseldd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> ( Im ` y ) e. R )
63 55 subrgmcl 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ _i e. R /\ ( Im ` y ) e. R ) -> ( _i x. ( Im ` y ) ) e. R )
64 14 59 62 63 syl3anc 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> ( _i x. ( Im ` y ) ) e. R )
65 49 subrgacl 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ ( Re ` y ) e. R /\ ( _i x. ( Im ` y ) ) e. R ) -> ( ( Re ` y ) + ( _i x. ( Im ` y ) ) ) e. R )
66 14 18 64 65 syl3anc 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> ( ( Re ` y ) + ( _i x. ( Im ` y ) ) ) e. R )
67 13 66 eqeltrd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( x e. ( R \ RR ) /\ y e. CC ) ) -> y e. R )
68 67 expr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( y e. CC -> y e. R ) )
69 68 ssrdv 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> CC C_ R )
70 11 69 eqssd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> R = CC )
71 70 olcd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ x e. ( R \ RR ) ) -> ( R = RR \/ R = CC ) )
72 71 ex 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) -> ( x e. ( R \ RR ) -> ( R = RR \/ R = CC ) ) )
73 72 exlimdv 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) -> ( E. x x e. ( R \ RR ) -> ( R = RR \/ R = CC ) ) )
74 73 imp 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ E. x x e. ( R \ RR ) ) -> ( R = RR \/ R = CC ) )
75 7 74 sylan2b 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) /\ ( R \ RR ) =/= (/) ) -> ( R = RR \/ R = CC ) )
76 6 75 pm2.61dane 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) -> ( R = RR \/ R = CC ) )
77 elprg 
 |-  ( R e. ( SubRing ` CCfld ) -> ( R e. { RR , CC } <-> ( R = RR \/ R = CC ) ) )
78 77 adantr 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) -> ( R e. { RR , CC } <-> ( R = RR \/ R = CC ) ) )
79 76 78 mpbird 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ RR C_ R ) -> R e. { RR , CC } )