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 \in SubRing (ℂ_{fld}) \land ℝ \subseteq R) \to R \in \{ℝ, ℂ\}$

Proof

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

Metamath Proof Explorer

Theorem cnsubrg

Proof