Theorem cndrng

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

	Ref	Expression
Assertion	cndrng	|- CCfld e. DivRing

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	|- CC = ( Base ` CCfld )
2	1	a1i	|- ( T. -> CC = ( Base ` CCfld ) )
3		cnfldmul	|- x. = ( .r ` CCfld )
4	3	a1i	|- ( T. -> x. = ( .r ` CCfld ) )
5		cnfld0	|- 0 = ( 0g ` CCfld )
6	5	a1i	|- ( T. -> 0 = ( 0g ` CCfld ) )
7		cnfld1	|- 1 = ( 1r ` CCfld )
8	7	a1i	|- ( T. -> 1 = ( 1r ` CCfld ) )
9		cnring	|- CCfld e. Ring
10	9	a1i	|- ( T. -> CCfld e. Ring )
11		mulne0	|- ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x x. y ) =/= 0 )
12	11	3adant1	|- ( ( T. /\ ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x x. y ) =/= 0 )
13		ax-1ne0	|- 1 =/= 0
14	13	a1i	|- ( T. -> 1 =/= 0 )
15		reccl	|- ( ( x e. CC /\ x =/= 0 ) -> ( 1 / x ) e. CC )
16	15	adantl	|- ( ( T. /\ ( x e. CC /\ x =/= 0 ) ) -> ( 1 / x ) e. CC )
17		recne0	|- ( ( x e. CC /\ x =/= 0 ) -> ( 1 / x ) =/= 0 )
18	17	adantl	|- ( ( T. /\ ( x e. CC /\ x =/= 0 ) ) -> ( 1 / x ) =/= 0 )
19		recid2	|- ( ( x e. CC /\ x =/= 0 ) -> ( ( 1 / x ) x. x ) = 1 )
20	19	adantl	|- ( ( T. /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( 1 / x ) x. x ) = 1 )
21	2 4 6 8 10 12 14 16 18 20	isdrngd	|- ( T. -> CCfld e. DivRing )
22	21	mptru	|- CCfld e. DivRing