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 simpr ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) )
57 56 43 sylib ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ℝ ∧ 0 < ( 𝑋 / ( 1 + 𝑋 ) ) ∧ ( 𝑋 / ( 1 + 𝑋 ) ) < 1 ) )
58 57 simp1d ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ℝ )
59 55 58 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 1 − ( 𝑋 / ( 1 + 𝑋 ) ) ) ∈ ℝ )
60 54 59 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 1 / ( 1 + 𝑋 ) ) ∈ ℝ )
61 0red ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → 0 ∈ ℝ )
62 57 simp3d ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 𝑋 / ( 1 + 𝑋 ) ) < 1 )
63 62 17 breqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 𝑋 / ( 1 + 𝑋 ) ) < ( 1 − 0 ) )
64 58 55 61 63 ltsub13d ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → 0 < ( 1 − ( 𝑋 / ( 1 + 𝑋 ) ) ) )
65 64 54 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → 0 < ( 1 / ( 1 + 𝑋 ) ) )
66 60 65 elrpd ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 1 / ( 1 + 𝑋 ) ) ∈ ℝ+ )
67 66 rprecred ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 1 / ( 1 / ( 1 + 𝑋 ) ) ) ∈ ℝ )
68 48 67 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 1 + 𝑋 ) ∈ ℝ )
69 68 55 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( ( 1 + 𝑋 ) − 1 ) ∈ ℝ )
70 45 69 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → 𝑋 ∈ ℝ )
71 1p0e1 ⊢ ( 1 + 0 ) = 1
72 57 simp2d ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → 0 < ( 𝑋 / ( 1 + 𝑋 ) ) )
73 35 72 eqbrtrid ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 1 − 1 ) < ( 𝑋 / ( 1 + 𝑋 ) ) )
74 55 55 58 73 ltsub23d ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 1 − ( 𝑋 / ( 1 + 𝑋 ) ) ) < 1 )
75 54 74 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 1 / ( 1 + 𝑋 ) ) < 1 )
76 66 reclt1d ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( ( 1 / ( 1 + 𝑋 ) ) < 1 ↔ 1 < ( 1 / ( 1 / ( 1 + 𝑋 ) ) ) ) )
77 75 76 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → 1 < ( 1 / ( 1 / ( 1 + 𝑋 ) ) ) )
78 77 48 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → 1 < ( 1 + 𝑋 ) )
79 71 78 eqbrtrid ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 1 + 0 ) < ( 1 + 𝑋 ) )
80 61 70 55 ltadd2d ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → ( 0 < 𝑋 ↔ ( 1 + 0 ) < ( 1 + 𝑋 ) ) )
81 79 80 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → 0 < 𝑋 )
82 70 81 elrpd ⊢ ( ( 𝜑 ∧ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) → 𝑋 ∈ ℝ+ )
83 44 82 impbida ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ↔ ( 𝑋 / ( 1 + 𝑋 ) ) ∈ ( 0 (,) 1 ) ) )