Metamath Proof Explorer

Theorem xov1plusxeqvd

Description: A complex number X is positive real iff X / ( 1 + X ) is in ( 0 (,) 1 ) . Deduction form. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses xov1plusxeqvd.1 
|- ( ph -> X e. CC )
xov1plusxeqvd.2 
|- ( ph -> X =/= -u 1 )
Assertion xov1plusxeqvd 
|- ( ph -> ( X e. RR+ <-> ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) )

Proof

Step Hyp Ref Expression
1 xov1plusxeqvd.1 
 |-  ( ph -> X e. CC )
2 xov1plusxeqvd.2 
 |-  ( ph -> X =/= -u 1 )
3 simpr 
 |-  ( ( ph /\ X e. RR+ ) -> X e. RR+ )
4 3 rpred 
 |-  ( ( ph /\ X e. RR+ ) -> X e. RR )
5 1rp 
 |-  1 e. RR+
6 5 a1i 
 |-  ( ( ph /\ X e. RR+ ) -> 1 e. RR+ )
7 6 3 rpaddcld 
 |-  ( ( ph /\ X e. RR+ ) -> ( 1 + X ) e. RR+ )
8 4 7 rerpdivcld 
 |-  ( ( ph /\ X e. RR+ ) -> ( X / ( 1 + X ) ) e. RR )
9 7 rprecred 
 |-  ( ( ph /\ X e. RR+ ) -> ( 1 / ( 1 + X ) ) e. RR )
10 1red 
 |-  ( ( ph /\ X e. RR+ ) -> 1 e. RR )
11 0red 
 |-  ( ( ph /\ X e. RR+ ) -> 0 e. RR )
12 10 4 readdcld 
 |-  ( ( ph /\ X e. RR+ ) -> ( 1 + X ) e. RR )
13 10 3 ltaddrpd 
 |-  ( ( ph /\ X e. RR+ ) -> 1 < ( 1 + X ) )
14 recgt1i 
 |-  ( ( ( 1 + X ) e. RR /\ 1 < ( 1 + X ) ) -> ( 0 < ( 1 / ( 1 + X ) ) /\ ( 1 / ( 1 + X ) ) < 1 ) )
15 12 13 14 syl2anc 
 |-  ( ( ph /\ X e. RR+ ) -> ( 0 < ( 1 / ( 1 + X ) ) /\ ( 1 / ( 1 + X ) ) < 1 ) )
16 15 simprd 
 |-  ( ( ph /\ X e. RR+ ) -> ( 1 / ( 1 + X ) ) < 1 )
17 1m0e1 
 |-  ( 1 - 0 ) = 1
18 16 17 breqtrrdi 
 |-  ( ( ph /\ X e. RR+ ) -> ( 1 / ( 1 + X ) ) < ( 1 - 0 ) )
19 9 10 11 18 ltsub13d 
 |-  ( ( ph /\ X e. RR+ ) -> 0 < ( 1 - ( 1 / ( 1 + X ) ) ) )
20 1cnd 
 |-  ( ph -> 1 e. CC )
21 20 1 addcld 
 |-  ( ph -> ( 1 + X ) e. CC )
22 20 negcld 
 |-  ( ph -> -u 1 e. CC )
23 20 1 22 2 addneintrd 
 |-  ( ph -> ( 1 + X ) =/= ( 1 + -u 1 ) )
24 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
25 24 a1i 
 |-  ( ph -> ( 1 + -u 1 ) = 0 )
26 23 25 neeqtrd 
 |-  ( ph -> ( 1 + X ) =/= 0 )
27 21 20 21 26 divsubdird 
 |-  ( ph -> ( ( ( 1 + X ) - 1 ) / ( 1 + X ) ) = ( ( ( 1 + X ) / ( 1 + X ) ) - ( 1 / ( 1 + X ) ) ) )
28 20 1 pncan2d 
 |-  ( ph -> ( ( 1 + X ) - 1 ) = X )
29 28 oveq1d 
 |-  ( ph -> ( ( ( 1 + X ) - 1 ) / ( 1 + X ) ) = ( X / ( 1 + X ) ) )
30 21 26 dividd 
 |-  ( ph -> ( ( 1 + X ) / ( 1 + X ) ) = 1 )
31 30 oveq1d 
 |-  ( ph -> ( ( ( 1 + X ) / ( 1 + X ) ) - ( 1 / ( 1 + X ) ) ) = ( 1 - ( 1 / ( 1 + X ) ) ) )
32 27 29 31 3eqtr3d 
 |-  ( ph -> ( X / ( 1 + X ) ) = ( 1 - ( 1 / ( 1 + X ) ) ) )
33 32 adantr 
 |-  ( ( ph /\ X e. RR+ ) -> ( X / ( 1 + X ) ) = ( 1 - ( 1 / ( 1 + X ) ) ) )
34 19 33 breqtrrd 
 |-  ( ( ph /\ X e. RR+ ) -> 0 < ( X / ( 1 + X ) ) )
35 1m1e0 
 |-  ( 1 - 1 ) = 0
36 15 simpld 
 |-  ( ( ph /\ X e. RR+ ) -> 0 < ( 1 / ( 1 + X ) ) )
37 35 36 eqbrtrid 
 |-  ( ( ph /\ X e. RR+ ) -> ( 1 - 1 ) < ( 1 / ( 1 + X ) ) )
38 10 10 9 37 ltsub23d 
 |-  ( ( ph /\ X e. RR+ ) -> ( 1 - ( 1 / ( 1 + X ) ) ) < 1 )
39 33 38 eqbrtrd 
 |-  ( ( ph /\ X e. RR+ ) -> ( X / ( 1 + X ) ) < 1 )
40 0xr 
 |-  0 e. RR*
41 1xr 
 |-  1 e. RR*
42 elioo2 
 |-  ( ( 0 e. RR* /\ 1 e. RR* ) -> ( ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) <-> ( ( X / ( 1 + X ) ) e. RR /\ 0 < ( X / ( 1 + X ) ) /\ ( X / ( 1 + X ) ) < 1 ) ) )
43 40 41 42 mp2an 
 |-  ( ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) <-> ( ( X / ( 1 + X ) ) e. RR /\ 0 < ( X / ( 1 + X ) ) /\ ( X / ( 1 + X ) ) < 1 ) )
44 8 34 39 43 syl3anbrc 
 |-  ( ( ph /\ X e. RR+ ) -> ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) )
45 28 adantr 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( ( 1 + X ) - 1 ) = X )
46 21 adantr 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 + X ) e. CC )
47 26 adantr 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 + X ) =/= 0 )
48 46 47 recrecd 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 / ( 1 / ( 1 + X ) ) ) = ( 1 + X ) )
49 21 1 21 26 divsubdird 
 |-  ( ph -> ( ( ( 1 + X ) - X ) / ( 1 + X ) ) = ( ( ( 1 + X ) / ( 1 + X ) ) - ( X / ( 1 + X ) ) ) )
50 20 1 pncand 
 |-  ( ph -> ( ( 1 + X ) - X ) = 1 )
51 50 oveq1d 
 |-  ( ph -> ( ( ( 1 + X ) - X ) / ( 1 + X ) ) = ( 1 / ( 1 + X ) ) )
52 30 oveq1d 
 |-  ( ph -> ( ( ( 1 + X ) / ( 1 + X ) ) - ( X / ( 1 + X ) ) ) = ( 1 - ( X / ( 1 + X ) ) ) )
53 49 51 52 3eqtr3d 
 |-  ( ph -> ( 1 / ( 1 + X ) ) = ( 1 - ( X / ( 1 + X ) ) ) )
54 53 adantr 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 / ( 1 + X ) ) = ( 1 - ( X / ( 1 + X ) ) ) )
55 1red 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> 1 e. RR )
56 43 bilani 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( ( X / ( 1 + X ) ) e. RR /\ 0 < ( X / ( 1 + X ) ) /\ ( X / ( 1 + X ) ) < 1 ) )
57 56 simp1d 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( X / ( 1 + X ) ) e. RR )
58 55 57 resubcld 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 - ( X / ( 1 + X ) ) ) e. RR )
59 54 58 eqeltrd 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 / ( 1 + X ) ) e. RR )
60 0red 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> 0 e. RR )
61 56 simp3d 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( X / ( 1 + X ) ) < 1 )
62 61 17 breqtrrdi 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( X / ( 1 + X ) ) < ( 1 - 0 ) )
63 57 55 60 62 ltsub13d 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> 0 < ( 1 - ( X / ( 1 + X ) ) ) )
64 63 54 breqtrrd 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> 0 < ( 1 / ( 1 + X ) ) )
65 59 64 elrpd 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 / ( 1 + X ) ) e. RR+ )
66 65 rprecred 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 / ( 1 / ( 1 + X ) ) ) e. RR )
67 48 66 eqeltrrd 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 + X ) e. RR )
68 67 55 resubcld 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( ( 1 + X ) - 1 ) e. RR )
69 45 68 eqeltrrd 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> X e. RR )
70 1p0e1 
 |-  ( 1 + 0 ) = 1
71 56 simp2d 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> 0 < ( X / ( 1 + X ) ) )
72 35 71 eqbrtrid 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 - 1 ) < ( X / ( 1 + X ) ) )
73 55 55 57 72 ltsub23d 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 - ( X / ( 1 + X ) ) ) < 1 )
74 54 73 eqbrtrd 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 / ( 1 + X ) ) < 1 )
75 65 reclt1d 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( ( 1 / ( 1 + X ) ) < 1 <-> 1 < ( 1 / ( 1 / ( 1 + X ) ) ) ) )
76 74 75 mpbid 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> 1 < ( 1 / ( 1 / ( 1 + X ) ) ) )
77 76 48 breqtrd 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> 1 < ( 1 + X ) )
78 70 77 eqbrtrid 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 1 + 0 ) < ( 1 + X ) )
79 60 69 55 ltadd2d 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> ( 0 < X <-> ( 1 + 0 ) < ( 1 + X ) ) )
80 78 79 mpbird 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> 0 < X )
81 69 80 elrpd 
 |-  ( ( ph /\ ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) -> X e. RR+ )
82 44 81 impbida 
 |-  ( ph -> ( X e. RR+ <-> ( X / ( 1 + X ) ) e. ( 0 (,) 1 ) ) )