Theorem cndrng

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

	Ref	Expression
Assertion	cndrng	⊢ ℂfld ∈ DivRing

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
2	1	a1i	⊢ ( ⊤ → ℂ = ( Base ‘ ℂfld ) )
3		cnfldmul	⊢ · = ( .r ‘ ℂfld )
4	3	a1i	⊢ ( ⊤ → · = ( .r ‘ ℂfld ) )
5		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
6	5	a1i	⊢ ( ⊤ → 0 = ( 0g ‘ ℂfld ) )
7		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
8	7	a1i	⊢ ( ⊤ → 1 = ( 1r ‘ ℂfld ) )
9		cnring	⊢ ℂfld ∈ Ring
10	9	a1i	⊢ ( ⊤ → ℂfld ∈ Ring )
11		mulne0	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
12	11	3adant1	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
13		ax-1ne0	⊢ 1 ≠ 0
14	13	a1i	⊢ ( ⊤ → 1 ≠ 0 )
15		reccl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ ℂ )
16	15	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ ℂ )
17		recne0	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ≠ 0 )
18	17	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ≠ 0 )
19		recid2	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( ( 1 / 𝑥 ) · 𝑥 ) = 1 )
20	19	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( 1 / 𝑥 ) · 𝑥 ) = 1 )
21	2 4 6 8 10 12 14 16 18 20	isdrngd	⊢ ( ⊤ → ℂfld ∈ DivRing )
22	21	mptru	⊢ ℂfld ∈ DivRing