Metamath Proof Explorer

Theorem knoppndvlem20

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 18-Aug-2021)

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

Proof

Step Hyp Ref Expression
1 knoppndvlem20.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
2 knoppndvlem20.n 
 |-  ( ph -> N e. NN )
3 knoppndvlem20.1 
 |-  ( ph -> 1 < ( N x. ( abs ` C ) ) )
4 1 2 3 knoppndvlem12 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) =/= 1 /\ 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
5 4 simprd 
 |-  ( ph -> 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) )
6 2re 
 |-  2 e. RR
7 6 a1i 
 |-  ( ph -> 2 e. RR )
8 2 nnred 
 |-  ( ph -> N e. RR )
9 7 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 1red 
 |-  ( ph -> 1 e. RR )
16 14 15 resubcld 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) e. RR )
17 0red 
 |-  ( ph -> 0 e. RR )
18 0lt1 
 |-  0 < 1
19 18 a1i 
 |-  ( ph -> 0 < 1 )
20 17 15 16 19 5 lttrd 
 |-  ( ph -> 0 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) )
21 16 20 elrpd 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) e. RR+ )
22 21 recgt1d 
 |-  ( ph -> ( 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) <-> ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) < 1 ) )
23 5 22 mpbid 
 |-  ( ph -> ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) < 1 )
24 21 rprecred 
 |-  ( ph -> ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. RR )
25 24 15 jca 
 |-  ( ph -> ( ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. RR /\ 1 e. RR ) )
26 difrp 
 |-  ( ( ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. RR /\ 1 e. RR ) -> ( ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) < 1 <-> ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR+ ) )
27 25 26 syl 
 |-  ( ph -> ( ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) < 1 <-> ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR+ ) )
28 23 27 mpbid 
 |-  ( ph -> ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR+ )