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	$⊢ φ \to X \in ℂ$
	xov1plusxeqvd.2	$⊢ φ \to X \neq - 1$
Assertion	xov1plusxeqvd	$⊢ φ \to (X \in ℝ^{+} \leftrightarrow \frac{X}{1 + X} \in (0, 1))$

Proof

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

Metamath Proof Explorer

Theorem xov1plusxeqvd

Proof