cndrng

Description: The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
2	1	a1i	$⊢ ⊤ \to ℂ = {Base}_{ℂ_{fld}}$
3		mpocnfldmul	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) = \cdot_{ℂ_{fld}}$
4	3	a1i	$⊢ ⊤ \to (u \in ℂ, v \in ℂ ⟼ u v) = \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		ovmpot	$⊢ (x \in ℂ \land y \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) y = x y$
12	11	ad2ant2r	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x (u \in ℂ, v \in ℂ ⟼ u v) y = x y$
13		mulne0	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x y \neq 0$
14	12 13	eqnetrd	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x (u \in ℂ, v \in ℂ ⟼ u v) y \neq 0$
15	14	3adant1	$⊢ (⊤ \land (x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x (u \in ℂ, v \in ℂ ⟼ u v) y \neq 0$
16		ax-1ne0	$⊢ 1 \neq 0$
17	16	a1i	$⊢ ⊤ \to 1 \neq 0$
18		reccl	$⊢ (x \in ℂ \land x \neq 0) \to \frac{1}{x} \in ℂ$
19	18	adantl	$⊢ (⊤ \land (x \in ℂ \land x \neq 0)) \to \frac{1}{x} \in ℂ$
20		simpl	$⊢ (x \in ℂ \land x \neq 0) \to x \in ℂ$
21		ovmpot	$⊢ (\frac{1}{x} \in ℂ \land x \in ℂ) \to (\frac{1}{x}) (u \in ℂ, v \in ℂ ⟼ u v) x = (\frac{1}{x}) x$
22	18 20 21	syl2anc	$⊢ (x \in ℂ \land x \neq 0) \to (\frac{1}{x}) (u \in ℂ, v \in ℂ ⟼ u v) x = (\frac{1}{x}) x$
23		recid2	$⊢ (x \in ℂ \land x \neq 0) \to (\frac{1}{x}) x = 1$
24	22 23	eqtrd	$⊢ (x \in ℂ \land x \neq 0) \to (\frac{1}{x}) (u \in ℂ, v \in ℂ ⟼ u v) x = 1$
25	24	adantl	$⊢ (⊤ \land (x \in ℂ \land x \neq 0)) \to (\frac{1}{x}) (u \in ℂ, v \in ℂ ⟼ u v) x = 1$
26	2 4 6 8 10 15 17 19 25	isdrngd	$⊢ ⊤ \to ℂ_{fld} \in DivRing$
27	26	mptru	$⊢ ℂ_{fld} \in DivRing$

Metamath Proof Explorer

Theorem cndrng

Proof