Metamath Proof Explorer

Theorem knoppndvlem12

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem12.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
2 knoppndvlem12.n 
 |-  ( ph -> N e. NN )
3 knoppndvlem12.1 
 |-  ( ph -> 1 < ( N x. ( abs ` C ) ) )
4 1red 
 |-  ( ph -> 1 e. RR )
5 2re 
 |-  2 e. RR
6 5 a1i 
 |-  ( ph -> 2 e. RR )
7 nnre 
 |-  ( N e. NN -> N e. RR )
8 2 7 syl 
 |-  ( ph -> N e. RR )
9 6 8 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
10 1 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
11 10 simpld 
 |-  ( ph -> C e. RR )
12 11 recnd 
 |-  ( ph -> C e. CC )
13 12 abscld 
 |-  ( ph -> ( abs ` C ) e. RR )
14 9 13 remulcld 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) e. RR )
15 1lt2 
 |-  1 < 2
16 15 a1i 
 |-  ( ph -> 1 < 2 )
17 2t1e2 
 |-  ( 2 x. 1 ) = 2
18 17 eqcomi 
 |-  2 = ( 2 x. 1 )
19 18 a1i 
 |-  ( ph -> 2 = ( 2 x. 1 ) )
20 8 13 remulcld 
 |-  ( ph -> ( N x. ( abs ` C ) ) e. RR )
21 2rp 
 |-  2 e. RR+
22 21 a1i 
 |-  ( ph -> 2 e. RR+ )
23 4 20 22 3 ltmul2dd 
 |-  ( ph -> ( 2 x. 1 ) < ( 2 x. ( N x. ( abs ` C ) ) ) )
24 19 23 eqbrtrd 
 |-  ( ph -> 2 < ( 2 x. ( N x. ( abs ` C ) ) ) )
25 6 recnd 
 |-  ( ph -> 2 e. CC )
26 8 recnd 
 |-  ( ph -> N e. CC )
27 13 recnd 
 |-  ( ph -> ( abs ` C ) e. CC )
28 25 26 27 mulassd 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) = ( 2 x. ( N x. ( abs ` C ) ) ) )
29 28 eqcomd 
 |-  ( ph -> ( 2 x. ( N x. ( abs ` C ) ) ) = ( ( 2 x. N ) x. ( abs ` C ) ) )
30 24 29 breqtrd 
 |-  ( ph -> 2 < ( ( 2 x. N ) x. ( abs ` C ) ) )
31 4 6 14 16 30 lttrd 
 |-  ( ph -> 1 < ( ( 2 x. N ) x. ( abs ` C ) ) )
32 4 31 jca 
 |-  ( ph -> ( 1 e. RR /\ 1 < ( ( 2 x. N ) x. ( abs ` C ) ) ) )
33 ltne 
 |-  ( ( 1 e. RR /\ 1 < ( ( 2 x. N ) x. ( abs ` C ) ) ) -> ( ( 2 x. N ) x. ( abs ` C ) ) =/= 1 )
34 32 33 syl 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) =/= 1 )
35 1p1e2 
 |-  ( 1 + 1 ) = 2
36 35 a1i 
 |-  ( ph -> ( 1 + 1 ) = 2 )
37 36 30 eqbrtrd 
 |-  ( ph -> ( 1 + 1 ) < ( ( 2 x. N ) x. ( abs ` C ) ) )
38 4 4 14 ltaddsubd 
 |-  ( ph -> ( ( 1 + 1 ) < ( ( 2 x. N ) x. ( abs ` C ) ) <-> 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
39 37 38 mpbid 
 |-  ( ph -> 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) )
40 34 39 jca 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) =/= 1 /\ 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )