cndrng

Description: The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014)

		Ref	Expression
	Assertion	cndrng	$⊢ ℂ_{fld} \in DivRing$

Step	Hyp	Ref	Expression
1		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
2	1	a1i	$⊢ ⊤ \to ℂ = {Base}_{ℂ_{fld}}$
3		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
4	3	a1i	$⊢ ⊤ \to \times = \cdot_{ℂ_{fld}}$
5		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
6	5	a1i	$⊢ ⊤ \to 0 = 0_{ℂ_{fld}}$
7		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
8	7	a1i	$⊢ ⊤ \to 1 = 1_{ℂ_{fld}}$
9		cnring	$⊢ ℂ_{fld} \in Ring$
10	9	a1i	$⊢ ⊤ \to ℂ_{fld} \in Ring$
11		mulne0	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x y \neq 0$
12	11	3adant1	$⊢ (⊤ \land (x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x y \neq 0$
13		ax-1ne0	$⊢ 1 \neq 0$
14	13	a1i	$⊢ ⊤ \to 1 \neq 0$
15		reccl	$⊢ (x \in ℂ \land x \neq 0) \to \frac{1}{x} \in ℂ$
16	15	adantl	$⊢ (⊤ \land (x \in ℂ \land x \neq 0)) \to \frac{1}{x} \in ℂ$
17		recne0	$⊢ (x \in ℂ \land x \neq 0) \to \frac{1}{x} \neq 0$
18	17	adantl	$⊢ (⊤ \land (x \in ℂ \land x \neq 0)) \to \frac{1}{x} \neq 0$
19		recid2	$⊢ (x \in ℂ \land x \neq 0) \to (\frac{1}{x}) x = 1$
20	19	adantl	$⊢ (⊤ \land (x \in ℂ \land x \neq 0)) \to (\frac{1}{x}) x = 1$
21	2 4 6 8 10 12 14 16 18 20	isdrngd	$⊢ ⊤ \to ℂ_{fld} \in DivRing$
22	21	mptru	$⊢ ℂ_{fld} \in DivRing$

Metamath Proof Explorer