Metamath Proof Explorer

Theorem absabv

Description: The regular absolute value function on the complex numbers is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Assertion absabv 
|- abs e. ( AbsVal ` CCfld )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( T. -> ( AbsVal ` CCfld ) = ( AbsVal ` CCfld ) )
2 cnfldbas 
 |-  CC = ( Base ` CCfld )
3 2 a1i 
 |-  ( T. -> CC = ( Base ` CCfld ) )
4 cnfldadd 
 |-  + = ( +g ` CCfld )
5 4 a1i 
 |-  ( T. -> + = ( +g ` CCfld ) )
6 cnfldmul 
 |-  x. = ( .r ` CCfld )
7 6 a1i 
 |-  ( T. -> x. = ( .r ` CCfld ) )
8 cnfld0 
 |-  0 = ( 0g ` CCfld )
9 8 a1i 
 |-  ( T. -> 0 = ( 0g ` CCfld ) )
10 cnring 
 |-  CCfld e. Ring
11 10 a1i 
 |-  ( T. -> CCfld e. Ring )
12 absf 
 |-  abs : CC --> RR
13 12 a1i 
 |-  ( T. -> abs : CC --> RR )
14 abs0 
 |-  ( abs ` 0 ) = 0
15 14 a1i 
 |-  ( T. -> ( abs ` 0 ) = 0 )
16 absgt0 
 |-  ( x e. CC -> ( x =/= 0 <-> 0 < ( abs ` x ) ) )
17 16 biimpa 
 |-  ( ( x e. CC /\ x =/= 0 ) -> 0 < ( abs ` x ) )
18 17 3adant1 
 |-  ( ( T. /\ x e. CC /\ x =/= 0 ) -> 0 < ( abs ` x ) )
19 absmul 
 |-  ( ( x e. CC /\ y e. CC ) -> ( abs ` ( x x. y ) ) = ( ( abs ` x ) x. ( abs ` y ) ) )
20 19 ad2ant2r 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( abs ` ( x x. y ) ) = ( ( abs ` x ) x. ( abs ` y ) ) )
21 20 3adant1 
 |-  ( ( T. /\ ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( abs ` ( x x. y ) ) = ( ( abs ` x ) x. ( abs ` y ) ) )
22 abstri 
 |-  ( ( x e. CC /\ y e. CC ) -> ( abs ` ( x + y ) ) <_ ( ( abs ` x ) + ( abs ` y ) ) )
23 22 ad2ant2r 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( abs ` ( x + y ) ) <_ ( ( abs ` x ) + ( abs ` y ) ) )
24 23 3adant1 
 |-  ( ( T. /\ ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( abs ` ( x + y ) ) <_ ( ( abs ` x ) + ( abs ` y ) ) )
25 1 3 5 7 9 11 13 15 18 21 24 isabvd 
 |-  ( T. -> abs e. ( AbsVal ` CCfld ) )
26 25 mptru 
 |-  abs e. ( AbsVal ` CCfld )