| Step | Hyp | Ref
| Expression |
| 1 | | ssdif0 4366 |
. . . 4
⊢ (𝑅 ⊆ ℝ ↔ (𝑅 ∖ ℝ) =
∅) |
| 2 | | simpr 484 |
. . . . . 6
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑅 ⊆ ℝ) → 𝑅 ⊆ ℝ) |
| 3 | | simplr 769 |
. . . . . 6
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑅 ⊆ ℝ) → ℝ ⊆
𝑅) |
| 4 | 2, 3 | eqssd 4001 |
. . . . 5
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑅 ⊆ ℝ) → 𝑅 = ℝ) |
| 5 | 4 | orcd 874 |
. . . 4
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑅 ⊆ ℝ) → (𝑅 = ℝ ∨ 𝑅 = ℂ)) |
| 6 | 1, 5 | sylan2br 595 |
. . 3
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑅 ∖ ℝ) = ∅) → (𝑅 = ℝ ∨ 𝑅 = ℂ)) |
| 7 | | n0 4353 |
. . . 4
⊢ ((𝑅 ∖ ℝ) ≠ ∅
↔ ∃𝑥 𝑥 ∈ (𝑅 ∖ ℝ)) |
| 8 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → 𝑅 ∈
(SubRing‘ℂfld)) |
| 9 | | cnfldbas 21368 |
. . . . . . . . . . 11
⊢ ℂ =
(Base‘ℂfld) |
| 10 | 9 | subrgss 20572 |
. . . . . . . . . 10
⊢ (𝑅 ∈
(SubRing‘ℂfld) → 𝑅 ⊆ ℂ) |
| 11 | 8, 10 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → 𝑅 ⊆ ℂ) |
| 12 | | replim 15155 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → 𝑦 = ((ℜ‘𝑦) + (i ·
(ℑ‘𝑦)))) |
| 13 | 12 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → 𝑦 = ((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) |
| 14 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → 𝑅 ∈
(SubRing‘ℂfld)) |
| 15 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → ℝ ⊆
𝑅) |
| 16 | | recl 15149 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ →
(ℜ‘𝑦) ∈
ℝ) |
| 17 | 16 | ad2antll 729 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → (ℜ‘𝑦) ∈
ℝ) |
| 18 | 15, 17 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → (ℜ‘𝑦) ∈ 𝑅) |
| 19 | | ax-icn 11214 |
. . . . . . . . . . . . . . . . . . 19
⊢ i ∈
ℂ |
| 20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → i ∈
ℂ) |
| 21 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝑅 ∖ ℝ) → 𝑥 ∈ 𝑅) |
| 22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → 𝑥 ∈ 𝑅) |
| 23 | 11, 22 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → 𝑥 ∈ ℂ) |
| 24 | | imcl 15150 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ →
(ℑ‘𝑥) ∈
ℝ) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) →
(ℑ‘𝑥) ∈
ℝ) |
| 26 | 25 | recnd 11289 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) →
(ℑ‘𝑥) ∈
ℂ) |
| 27 | | eldifn 4132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑅 ∖ ℝ) → ¬ 𝑥 ∈
ℝ) |
| 28 | 27 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → ¬ 𝑥 ∈
ℝ) |
| 29 | | reim0b 15158 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → (𝑥 ∈ ℝ ↔
(ℑ‘𝑥) =
0)) |
| 30 | 29 | necon3bbid 2978 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ → (¬
𝑥 ∈ ℝ ↔
(ℑ‘𝑥) ≠
0)) |
| 31 | 23, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (¬ 𝑥 ∈ ℝ ↔
(ℑ‘𝑥) ≠
0)) |
| 32 | 28, 31 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) →
(ℑ‘𝑥) ≠
0) |
| 33 | 20, 26, 32 | divcan4d 12049 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → ((i ·
(ℑ‘𝑥)) /
(ℑ‘𝑥)) =
i) |
| 34 | | mulcl 11239 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((i
∈ ℂ ∧ (ℑ‘𝑥) ∈ ℂ) → (i ·
(ℑ‘𝑥)) ∈
ℂ) |
| 35 | 19, 26, 34 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (i ·
(ℑ‘𝑥)) ∈
ℂ) |
| 36 | 35, 26, 32 | divrecd 12046 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → ((i ·
(ℑ‘𝑥)) /
(ℑ‘𝑥)) = ((i
· (ℑ‘𝑥))
· (1 / (ℑ‘𝑥)))) |
| 37 | 33, 36 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → i = ((i ·
(ℑ‘𝑥)) ·
(1 / (ℑ‘𝑥)))) |
| 38 | 23 | recld 15233 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) →
(ℜ‘𝑥) ∈
ℝ) |
| 39 | 38 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) →
(ℜ‘𝑥) ∈
ℂ) |
| 40 | 23, 39 | negsubd 11626 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (𝑥 + -(ℜ‘𝑥)) = (𝑥 − (ℜ‘𝑥))) |
| 41 | | replim 15155 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → 𝑥 = ((ℜ‘𝑥) + (i ·
(ℑ‘𝑥)))) |
| 42 | 23, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → 𝑥 = ((ℜ‘𝑥) + (i · (ℑ‘𝑥)))) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (𝑥 − (ℜ‘𝑥)) = (((ℜ‘𝑥) + (i ·
(ℑ‘𝑥))) −
(ℜ‘𝑥))) |
| 44 | 39, 35 | pncan2d 11622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) →
(((ℜ‘𝑥) + (i
· (ℑ‘𝑥))) − (ℜ‘𝑥)) = (i · (ℑ‘𝑥))) |
| 45 | 40, 43, 44 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (𝑥 + -(ℜ‘𝑥)) = (i ·
(ℑ‘𝑥))) |
| 46 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → ℝ ⊆
𝑅) |
| 47 | 38 | renegcld 11690 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) →
-(ℜ‘𝑥) ∈
ℝ) |
| 48 | 46, 47 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) →
-(ℜ‘𝑥) ∈
𝑅) |
| 49 | | cnfldadd 21370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ + =
(+g‘ℂfld) |
| 50 | 49 | subrgacl 20583 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈
(SubRing‘ℂfld) ∧ 𝑥 ∈ 𝑅 ∧ -(ℜ‘𝑥) ∈ 𝑅) → (𝑥 + -(ℜ‘𝑥)) ∈ 𝑅) |
| 51 | 8, 22, 48, 50 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (𝑥 + -(ℜ‘𝑥)) ∈ 𝑅) |
| 52 | 45, 51 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (i ·
(ℑ‘𝑥)) ∈
𝑅) |
| 53 | 25, 32 | rereccld 12094 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (1 /
(ℑ‘𝑥)) ∈
ℝ) |
| 54 | 46, 53 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (1 /
(ℑ‘𝑥)) ∈
𝑅) |
| 55 | | cnfldmul 21372 |
. . . . . . . . . . . . . . . . . 18
⊢ ·
= (.r‘ℂfld) |
| 56 | 55 | subrgmcl 20584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈
(SubRing‘ℂfld) ∧ (i · (ℑ‘𝑥)) ∈ 𝑅 ∧ (1 / (ℑ‘𝑥)) ∈ 𝑅) → ((i · (ℑ‘𝑥)) · (1 /
(ℑ‘𝑥))) ∈
𝑅) |
| 57 | 8, 52, 54, 56 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → ((i ·
(ℑ‘𝑥)) ·
(1 / (ℑ‘𝑥)))
∈ 𝑅) |
| 58 | 37, 57 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → i ∈ 𝑅) |
| 59 | 58 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → i ∈ 𝑅) |
| 60 | | imcl 15150 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℂ →
(ℑ‘𝑦) ∈
ℝ) |
| 61 | 60 | ad2antll 729 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → (ℑ‘𝑦) ∈
ℝ) |
| 62 | 15, 61 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → (ℑ‘𝑦) ∈ 𝑅) |
| 63 | 55 | subrgmcl 20584 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈
(SubRing‘ℂfld) ∧ i ∈ 𝑅 ∧ (ℑ‘𝑦) ∈ 𝑅) → (i · (ℑ‘𝑦)) ∈ 𝑅) |
| 64 | 14, 59, 62, 63 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → (i ·
(ℑ‘𝑦)) ∈
𝑅) |
| 65 | 49 | subrgacl 20583 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈
(SubRing‘ℂfld) ∧ (ℜ‘𝑦) ∈ 𝑅 ∧ (i · (ℑ‘𝑦)) ∈ 𝑅) → ((ℜ‘𝑦) + (i · (ℑ‘𝑦))) ∈ 𝑅) |
| 66 | 14, 18, 64, 65 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → ((ℜ‘𝑦) + (i ·
(ℑ‘𝑦))) ∈
𝑅) |
| 67 | 13, 66 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑥 ∈ (𝑅 ∖ ℝ) ∧ 𝑦 ∈ ℂ)) → 𝑦 ∈ 𝑅) |
| 68 | 67 | expr 456 |
. . . . . . . . . 10
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (𝑦 ∈ ℂ → 𝑦 ∈ 𝑅)) |
| 69 | 68 | ssrdv 3989 |
. . . . . . . . 9
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → ℂ ⊆
𝑅) |
| 70 | 11, 69 | eqssd 4001 |
. . . . . . . 8
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → 𝑅 = ℂ) |
| 71 | 70 | olcd 875 |
. . . . . . 7
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ 𝑥 ∈ (𝑅 ∖ ℝ)) → (𝑅 = ℝ ∨ 𝑅 = ℂ)) |
| 72 | 71 | ex 412 |
. . . . . 6
⊢ ((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → (𝑥 ∈ (𝑅 ∖ ℝ) → (𝑅 = ℝ ∨ 𝑅 = ℂ))) |
| 73 | 72 | exlimdv 1933 |
. . . . 5
⊢ ((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → (∃𝑥 𝑥 ∈ (𝑅 ∖ ℝ) → (𝑅 = ℝ ∨ 𝑅 = ℂ))) |
| 74 | 73 | imp 406 |
. . . 4
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ ∃𝑥 𝑥 ∈ (𝑅 ∖ ℝ)) → (𝑅 = ℝ ∨ 𝑅 = ℂ)) |
| 75 | 7, 74 | sylan2b 594 |
. . 3
⊢ (((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) ∧ (𝑅 ∖ ℝ) ≠ ∅) →
(𝑅 = ℝ ∨ 𝑅 = ℂ)) |
| 76 | 6, 75 | pm2.61dane 3029 |
. 2
⊢ ((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → (𝑅 = ℝ ∨ 𝑅 = ℂ)) |
| 77 | | elprg 4648 |
. . 3
⊢ (𝑅 ∈
(SubRing‘ℂfld) → (𝑅 ∈ {ℝ, ℂ} ↔ (𝑅 = ℝ ∨ 𝑅 = ℂ))) |
| 78 | 77 | adantr 480 |
. 2
⊢ ((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → (𝑅 ∈ {ℝ, ℂ} ↔ (𝑅 = ℝ ∨ 𝑅 = ℂ))) |
| 79 | 76, 78 | mpbird 257 |
1
⊢ ((𝑅 ∈
(SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ}) |