Metamath Proof Explorer

Theorem abssubne0

Description: If the absolute value of a complex number is less than a real, its difference from the real is nonzero. (Contributed by NM, 2-Nov-2007) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion abssubne0 
|- ( ( A e. CC /\ B e. RR /\ ( abs ` A ) < B ) -> ( B - A ) =/= 0 )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> B e. RR )
2 1 recnd 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> B e. CC )
3 simpll 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> A e. CC )
4 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
5 3 4 syl 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> ( abs ` A ) e. RR )
6 abscl 
 |-  ( B e. CC -> ( abs ` B ) e. RR )
7 2 6 syl 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> ( abs ` B ) e. RR )
8 simpr 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> ( abs ` A ) < B )
9 leabs 
 |-  ( B e. RR -> B <_ ( abs ` B ) )
10 1 9 syl 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> B <_ ( abs ` B ) )
11 5 1 7 8 10 ltletrd 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> ( abs ` A ) < ( abs ` B ) )
12 5 11 gtned 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> ( abs ` B ) =/= ( abs ` A ) )
13 fveq2 
 |-  ( B = A -> ( abs ` B ) = ( abs ` A ) )
14 13 necon3i 
 |-  ( ( abs ` B ) =/= ( abs ` A ) -> B =/= A )
15 12 14 syl 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> B =/= A )
16 2 3 15 subne0d 
 |-  ( ( ( A e. CC /\ B e. RR ) /\ ( abs ` A ) < B ) -> ( B - A ) =/= 0 )
17 16 3impa 
 |-  ( ( A e. CC /\ B e. RR /\ ( abs ` A ) < B ) -> ( B - A ) =/= 0 )