Metamath Proof Explorer

Theorem knoppndvlem13

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 1-Jul-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppndvlem13.c 
|- ( ph -> C e. ( -u 1 (,) 1 ) )
knoppndvlem13.n 
|- ( ph -> N e. NN )
knoppndvlem13.1 
|- ( ph -> 1 < ( N x. ( abs ` C ) ) )
Assertion knoppndvlem13 
|- ( ph -> C =/= 0 )

Proof

Step Hyp Ref Expression
1 knoppndvlem13.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
2 knoppndvlem13.n 
 |-  ( ph -> N e. NN )
3 knoppndvlem13.1 
 |-  ( ph -> 1 < ( N x. ( abs ` C ) ) )
4 3 adantr 
 |-  ( ( ph /\ C = 0 ) -> 1 < ( N x. ( abs ` C ) ) )
5 0lt1 
 |-  0 < 1
6 0re 
 |-  0 e. RR
7 1re 
 |-  1 e. RR
8 6 7 ltnsymi 
 |-  ( 0 < 1 -> -. 1 < 0 )
9 5 8 ax-mp 
 |-  -. 1 < 0
10 9 a1i 
 |-  ( ( ph /\ C = 0 ) -> -. 1 < 0 )
11 id 
 |-  ( C = 0 -> C = 0 )
12 11 abs00bd 
 |-  ( C = 0 -> ( abs ` C ) = 0 )
13 12 oveq2d 
 |-  ( C = 0 -> ( N x. ( abs ` C ) ) = ( N x. 0 ) )
14 13 adantl 
 |-  ( ( ph /\ C = 0 ) -> ( N x. ( abs ` C ) ) = ( N x. 0 ) )
15 nncn 
 |-  ( N e. NN -> N e. CC )
16 2 15 syl 
 |-  ( ph -> N e. CC )
17 16 adantr 
 |-  ( ( ph /\ C = 0 ) -> N e. CC )
18 17 mul01d 
 |-  ( ( ph /\ C = 0 ) -> ( N x. 0 ) = 0 )
19 14 18 eqtrd 
 |-  ( ( ph /\ C = 0 ) -> ( N x. ( abs ` C ) ) = 0 )
20 19 eqcomd 
 |-  ( ( ph /\ C = 0 ) -> 0 = ( N x. ( abs ` C ) ) )
21 20 breq2d 
 |-  ( ( ph /\ C = 0 ) -> ( 1 < 0 <-> 1 < ( N x. ( abs ` C ) ) ) )
22 10 21 mtbid 
 |-  ( ( ph /\ C = 0 ) -> -. 1 < ( N x. ( abs ` C ) ) )
23 4 22 pm2.65da 
 |-  ( ph -> -. C = 0 )
24 23 neqned 
 |-  ( ph -> C =/= 0 )