Step 
Hyp 
Ref 
Expression 
1 

cnring 
 CCfld e. Ring 
2 

ringmnd 
 ( CCfld e. Ring > CCfld e. Mnd ) 
3 
1 2

axmp 
 CCfld e. Mnd 
4 

0z 
 0 e. ZZ 
5 

zsscn 
 ZZ C_ CC 
6 

dfzring 
 ZZring = ( CCfld `s ZZ ) 
7 

cnfldbas 
 CC = ( Base ` CCfld ) 
8 

cnfld0 
 0 = ( 0g ` CCfld ) 
9 

cnfldnm 
 abs = ( norm ` CCfld ) 
10 
6 7 8 9

ressnm 
 ( ( CCfld e. Mnd /\ 0 e. ZZ /\ ZZ C_ CC ) > ( abs ` ZZ ) = ( norm ` ZZring ) ) 
11 
10

eqcomd 
 ( ( CCfld e. Mnd /\ 0 e. ZZ /\ ZZ C_ CC ) > ( norm ` ZZring ) = ( abs ` ZZ ) ) 
12 
3 4 5 11

mp3an 
 ( norm ` ZZring ) = ( abs ` ZZ ) 