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 ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) → 𝑅 ∈ { ℝ , ℂ } )

Proof

Step Hyp Ref Expression
1 ssdif0 ⊢ ( 𝑅 ⊆ ℝ ↔ ( 𝑅 ∖ ℝ ) = ∅ )
2 simpr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑅 ⊆ ℝ ) → 𝑅 ⊆ ℝ )
3 simplr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑅 ⊆ ℝ ) → ℝ ⊆ 𝑅 )
4 2 3 eqssd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑅 ⊆ ℝ ) → 𝑅 = ℝ )
5 4 orcd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑅 ⊆ ℝ ) → ( 𝑅 = ℝ ∨ 𝑅 = ℂ ) )
6 1 5 sylan2br ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑅 ∖ ℝ ) = ∅ ) → ( 𝑅 = ℝ ∨ 𝑅 = ℂ ) )
7 n0 ⊢ ( ( 𝑅 ∖ ℝ ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑅 ∖ ℝ ) )
8 simpll ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → 𝑅 ∈ ( SubRing ‘ ℂfld ) )
9 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
10 9 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ ℂfld ) → 𝑅 ⊆ ℂ )
11 8 10 syl ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → 𝑅 ⊆ ℂ )
12 replim ⊢ ( 𝑦 ∈ ℂ → 𝑦 = ( ( ℜ ‘ 𝑦 ) + ( i · ( ℑ ‘ 𝑦 ) ) ) )
13 12 ad2antll ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → 𝑦 = ( ( ℜ ‘ 𝑦 ) + ( i · ( ℑ ‘ 𝑦 ) ) ) )
14 simpll ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → 𝑅 ∈ ( SubRing ‘ ℂfld ) )
15 simplr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → ℝ ⊆ 𝑅 )
16 recl ⊢ ( 𝑦 ∈ ℂ → ( ℜ ‘ 𝑦 ) ∈ ℝ )
17 16 ad2antll ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → ( ℜ ‘ 𝑦 ) ∈ ℝ )
18 15 17 sseldd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → ( ℜ ‘ 𝑦 ) ∈ 𝑅 )
19 ax-icn ⊢ i ∈ ℂ
20 19 a1i ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → i ∈ ℂ )
21 eldifi ⊢ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) → 𝑥 ∈ 𝑅 )
22 21 adantl ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → 𝑥 ∈ 𝑅 )
23 11 22 sseldd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → 𝑥 ∈ ℂ )
24 imcl ⊢ ( 𝑥 ∈ ℂ → ( ℑ ‘ 𝑥 ) ∈ ℝ )
25 23 24 syl ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( ℑ ‘ 𝑥 ) ∈ ℝ )
26 25 recnd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( ℑ ‘ 𝑥 ) ∈ ℂ )
27 eldifn ⊢ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) → ¬ 𝑥 ∈ ℝ )
28 27 adantl ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ¬ 𝑥 ∈ ℝ )
29 reim0b ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) = 0 ) )
30 29 necon3bbid ⊢ ( 𝑥 ∈ ℂ → ( ¬ 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) ≠ 0 ) )
31 23 30 syl ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( ¬ 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) ≠ 0 ) )
32 28 31 mpbid ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( ℑ ‘ 𝑥 ) ≠ 0 )
33 20 26 32 divcan4d ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( ( i · ( ℑ ‘ 𝑥 ) ) / ( ℑ ‘ 𝑥 ) ) = i )
34 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝑥 ) ) ∈ ℂ )
35 19 26 34 sylancr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( i · ( ℑ ‘ 𝑥 ) ) ∈ ℂ )
36 35 26 32 divrecd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( ( i · ( ℑ ‘ 𝑥 ) ) / ( ℑ ‘ 𝑥 ) ) = ( ( i · ( ℑ ‘ 𝑥 ) ) · ( 1 / ( ℑ ‘ 𝑥 ) ) ) )
37 33 36 eqtr3d ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → i = ( ( i · ( ℑ ‘ 𝑥 ) ) · ( 1 / ( ℑ ‘ 𝑥 ) ) ) )
38 23 recld ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( ℜ ‘ 𝑥 ) ∈ ℝ )
39 38 recnd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( ℜ ‘ 𝑥 ) ∈ ℂ )
40 23 39 negsubd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( 𝑥 + - ( ℜ ‘ 𝑥 ) ) = ( 𝑥 − ( ℜ ‘ 𝑥 ) ) )
41 replim ⊢ ( 𝑥 ∈ ℂ → 𝑥 = ( ( ℜ ‘ 𝑥 ) + ( i · ( ℑ ‘ 𝑥 ) ) ) )
42 23 41 syl ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → 𝑥 = ( ( ℜ ‘ 𝑥 ) + ( i · ( ℑ ‘ 𝑥 ) ) ) )
43 42 oveq1d ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( 𝑥 − ( ℜ ‘ 𝑥 ) ) = ( ( ( ℜ ‘ 𝑥 ) + ( i · ( ℑ ‘ 𝑥 ) ) ) − ( ℜ ‘ 𝑥 ) ) )
44 39 35 pncan2d ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( ( ( ℜ ‘ 𝑥 ) + ( i · ( ℑ ‘ 𝑥 ) ) ) − ( ℜ ‘ 𝑥 ) ) = ( i · ( ℑ ‘ 𝑥 ) ) )
45 40 43 44 3eqtrd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( 𝑥 + - ( ℜ ‘ 𝑥 ) ) = ( i · ( ℑ ‘ 𝑥 ) ) )
46 simplr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ℝ ⊆ 𝑅 )
47 38 renegcld ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → - ( ℜ ‘ 𝑥 ) ∈ ℝ )
48 46 47 sseldd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → - ( ℜ ‘ 𝑥 ) ∈ 𝑅 )
49 cnfldadd ⊢ + = ( +g ‘ ℂfld )
50 49 subrgacl ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑥 ∈ 𝑅 ∧ - ( ℜ ‘ 𝑥 ) ∈ 𝑅 ) → ( 𝑥 + - ( ℜ ‘ 𝑥 ) ) ∈ 𝑅 )
51 8 22 48 50 syl3anc ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( 𝑥 + - ( ℜ ‘ 𝑥 ) ) ∈ 𝑅 )
52 45 51 eqeltrrd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( i · ( ℑ ‘ 𝑥 ) ) ∈ 𝑅 )
53 25 32 rereccld ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( 1 / ( ℑ ‘ 𝑥 ) ) ∈ ℝ )
54 46 53 sseldd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( 1 / ( ℑ ‘ 𝑥 ) ) ∈ 𝑅 )
55 cnfldmul ⊢ · = ( .r ‘ ℂfld )
56 55 subrgmcl ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( i · ( ℑ ‘ 𝑥 ) ) ∈ 𝑅 ∧ ( 1 / ( ℑ ‘ 𝑥 ) ) ∈ 𝑅 ) → ( ( i · ( ℑ ‘ 𝑥 ) ) · ( 1 / ( ℑ ‘ 𝑥 ) ) ) ∈ 𝑅 )
57 8 52 54 56 syl3anc ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( ( i · ( ℑ ‘ 𝑥 ) ) · ( 1 / ( ℑ ‘ 𝑥 ) ) ) ∈ 𝑅 )
58 37 57 eqeltrd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → i ∈ 𝑅 )
59 58 adantrr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → i ∈ 𝑅 )
60 imcl ⊢ ( 𝑦 ∈ ℂ → ( ℑ ‘ 𝑦 ) ∈ ℝ )
61 60 ad2antll ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → ( ℑ ‘ 𝑦 ) ∈ ℝ )
62 15 61 sseldd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → ( ℑ ‘ 𝑦 ) ∈ 𝑅 )
63 55 subrgmcl ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ i ∈ 𝑅 ∧ ( ℑ ‘ 𝑦 ) ∈ 𝑅 ) → ( i · ( ℑ ‘ 𝑦 ) ) ∈ 𝑅 )
64 14 59 62 63 syl3anc ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → ( i · ( ℑ ‘ 𝑦 ) ) ∈ 𝑅 )
65 49 subrgacl ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℜ ‘ 𝑦 ) ∈ 𝑅 ∧ ( i · ( ℑ ‘ 𝑦 ) ) ∈ 𝑅 ) → ( ( ℜ ‘ 𝑦 ) + ( i · ( ℑ ‘ 𝑦 ) ) ) ∈ 𝑅 )
66 14 18 64 65 syl3anc ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → ( ( ℜ ‘ 𝑦 ) + ( i · ( ℑ ‘ 𝑦 ) ) ) ∈ 𝑅 )
67 13 66 eqeltrd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) ∧ 𝑦 ∈ ℂ ) ) → 𝑦 ∈ 𝑅 )
68 67 expr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( 𝑦 ∈ ℂ → 𝑦 ∈ 𝑅 ) )
69 68 ssrdv ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ℂ ⊆ 𝑅 )
70 11 69 eqssd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → 𝑅 = ℂ )
71 70 olcd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( 𝑅 = ℝ ∨ 𝑅 = ℂ ) )
72 71 ex ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) → ( 𝑥 ∈ ( 𝑅 ∖ ℝ ) → ( 𝑅 = ℝ ∨ 𝑅 = ℂ ) ) )
73 72 exlimdv ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) → ( ∃ 𝑥 𝑥 ∈ ( 𝑅 ∖ ℝ ) → ( 𝑅 = ℝ ∨ 𝑅 = ℂ ) ) )
74 73 imp ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ∃ 𝑥 𝑥 ∈ ( 𝑅 ∖ ℝ ) ) → ( 𝑅 = ℝ ∨ 𝑅 = ℂ ) )
75 7 74 sylan2b ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) ∧ ( 𝑅 ∖ ℝ ) ≠ ∅ ) → ( 𝑅 = ℝ ∨ 𝑅 = ℂ ) )
76 6 75 pm2.61dane ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) → ( 𝑅 = ℝ ∨ 𝑅 = ℂ ) )
77 elprg ⊢ ( 𝑅 ∈ ( SubRing ‘ ℂfld ) → ( 𝑅 ∈ { ℝ , ℂ } ↔ ( 𝑅 = ℝ ∨ 𝑅 = ℂ ) ) )
78 77 adantr ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) → ( 𝑅 ∈ { ℝ , ℂ } ↔ ( 𝑅 = ℝ ∨ 𝑅 = ℂ ) ) )
79 76 78 mpbird ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ℝ ⊆ 𝑅 ) → 𝑅 ∈ { ℝ , ℂ } )