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 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
xov1plusxeqvd.2 ⊢ ( 𝜑 → 𝑋 ≠ - 1 )
Assertion xov1plusxeqvd ( 𝜑 → ( 𝑋 ∈ ℝ+ ↔ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) )

Proof

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