Proof of Theorem xov1plusxeqvd
Step | Hyp | Ref
| Expression |
1 | | simpr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 𝑋 ∈
ℝ+) |
2 | 1 | rpred 12156 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 𝑋 ∈
ℝ) |
3 | | 1rp 12116 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 1 ∈
ℝ+) |
5 | 4, 1 | rpaddcld 12171 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 +
𝑋) ∈
ℝ+) |
6 | 2, 5 | rerpdivcld 12187 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) ∈ ℝ) |
7 | 5 | rprecred 12167 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 / (1
+ 𝑋)) ∈
ℝ) |
8 | | 1red 10357 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 1 ∈
ℝ) |
9 | | 0red 10360 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 ∈
ℝ) |
10 | 8, 2 | readdcld 10386 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 +
𝑋) ∈
ℝ) |
11 | 8, 1 | ltaddrpd 12189 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 1 <
(1 + 𝑋)) |
12 | | recgt1i 11250 |
. . . . . . . 8
⊢ (((1 +
𝑋) ∈ ℝ ∧ 1
< (1 + 𝑋)) → (0
< (1 / (1 + 𝑋)) ∧ (1
/ (1 + 𝑋)) <
1)) |
13 | 10, 11, 12 | syl2anc 579 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (0 <
(1 / (1 + 𝑋)) ∧ (1 / (1
+ 𝑋)) <
1)) |
14 | 13 | simprd 491 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 / (1
+ 𝑋)) <
1) |
15 | | 1m0e1 11479 |
. . . . . 6
⊢ (1
− 0) = 1 |
16 | 14, 15 | syl6breqr 4915 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 / (1
+ 𝑋)) < (1 −
0)) |
17 | 7, 8, 9, 16 | ltsub13d 10958 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 <
(1 − (1 / (1 + 𝑋)))) |
18 | | 1cnd 10351 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) |
19 | | xov1plusxeqvd.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
20 | 18, 19 | addcld 10376 |
. . . . . . 7
⊢ (𝜑 → (1 + 𝑋) ∈ ℂ) |
21 | 18 | negcld 10700 |
. . . . . . . . 9
⊢ (𝜑 → -1 ∈
ℂ) |
22 | | xov1plusxeqvd.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≠ -1) |
23 | 18, 19, 21, 22 | addneintrd 10562 |
. . . . . . . 8
⊢ (𝜑 → (1 + 𝑋) ≠ (1 + -1)) |
24 | | 1pneg1e0 11477 |
. . . . . . . . 9
⊢ (1 + -1)
= 0 |
25 | 24 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (1 + -1) =
0) |
26 | 23, 25 | neeqtrd 3068 |
. . . . . . 7
⊢ (𝜑 → (1 + 𝑋) ≠ 0) |
27 | 20, 18, 20, 26 | divsubdird 11166 |
. . . . . 6
⊢ (𝜑 → (((1 + 𝑋) − 1) / (1 + 𝑋)) = (((1 + 𝑋) / (1 + 𝑋)) − (1 / (1 + 𝑋)))) |
28 | 18, 19 | pncan2d 10715 |
. . . . . . 7
⊢ (𝜑 → ((1 + 𝑋) − 1) = 𝑋) |
29 | 28 | oveq1d 6920 |
. . . . . 6
⊢ (𝜑 → (((1 + 𝑋) − 1) / (1 + 𝑋)) = (𝑋 / (1 + 𝑋))) |
30 | 20, 26 | dividd 11125 |
. . . . . . 7
⊢ (𝜑 → ((1 + 𝑋) / (1 + 𝑋)) = 1) |
31 | 30 | oveq1d 6920 |
. . . . . 6
⊢ (𝜑 → (((1 + 𝑋) / (1 + 𝑋)) − (1 / (1 + 𝑋))) = (1 − (1 / (1 + 𝑋)))) |
32 | 27, 29, 31 | 3eqtr3d 2869 |
. . . . 5
⊢ (𝜑 → (𝑋 / (1 + 𝑋)) = (1 − (1 / (1 + 𝑋)))) |
33 | 32 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) = (1 − (1 / (1 + 𝑋)))) |
34 | 17, 33 | breqtrrd 4901 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 <
(𝑋 / (1 + 𝑋))) |
35 | | 1m1e0 11423 |
. . . . . 6
⊢ (1
− 1) = 0 |
36 | 13 | simpld 490 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 <
(1 / (1 + 𝑋))) |
37 | 35, 36 | syl5eqbr 4908 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1
− 1) < (1 / (1 + 𝑋))) |
38 | 8, 8, 7, 37 | ltsub23d 10957 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1
− (1 / (1 + 𝑋))) <
1) |
39 | 33, 38 | eqbrtrd 4895 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) < 1) |
40 | | 0xr 10403 |
. . . 4
⊢ 0 ∈
ℝ* |
41 | | 1xr 10416 |
. . . 4
⊢ 1 ∈
ℝ* |
42 | | elioo2 12504 |
. . . 4
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑋 / (1 + 𝑋)) ∈ (0(,)1) ↔ ((𝑋 / (1 + 𝑋)) ∈ ℝ ∧ 0 < (𝑋 / (1 + 𝑋)) ∧ (𝑋 / (1 + 𝑋)) < 1))) |
43 | 40, 41, 42 | mp2an 683 |
. . 3
⊢ ((𝑋 / (1 + 𝑋)) ∈ (0(,)1) ↔ ((𝑋 / (1 + 𝑋)) ∈ ℝ ∧ 0 < (𝑋 / (1 + 𝑋)) ∧ (𝑋 / (1 + 𝑋)) < 1)) |
44 | 6, 34, 39, 43 | syl3anbrc 1447 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) |
45 | 28 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((1 + 𝑋) − 1) = 𝑋) |
46 | 20 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 𝑋) ∈
ℂ) |
47 | 26 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 𝑋) ≠ 0) |
48 | 46, 47 | recrecd 11124 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 / (1 +
𝑋))) = (1 + 𝑋)) |
49 | 20, 19, 20, 26 | divsubdird 11166 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 + 𝑋) − 𝑋) / (1 + 𝑋)) = (((1 + 𝑋) / (1 + 𝑋)) − (𝑋 / (1 + 𝑋)))) |
50 | 18, 19 | pncand 10714 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 + 𝑋) − 𝑋) = 1) |
51 | 50 | oveq1d 6920 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 + 𝑋) − 𝑋) / (1 + 𝑋)) = (1 / (1 + 𝑋))) |
52 | 30 | oveq1d 6920 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 + 𝑋) / (1 + 𝑋)) − (𝑋 / (1 + 𝑋))) = (1 − (𝑋 / (1 + 𝑋)))) |
53 | 49, 51, 52 | 3eqtr3d 2869 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / (1 + 𝑋)) = (1 − (𝑋 / (1 + 𝑋)))) |
54 | 53 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) = (1 − (𝑋 / (1 + 𝑋)))) |
55 | | 1red 10357 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 1 ∈
ℝ) |
56 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) |
57 | 56, 43 | sylib 210 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((𝑋 / (1 + 𝑋)) ∈ ℝ ∧ 0 < (𝑋 / (1 + 𝑋)) ∧ (𝑋 / (1 + 𝑋)) < 1)) |
58 | 57 | simp1d 1176 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) ∈ ℝ) |
59 | 55, 58 | resubcld 10782 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 − (𝑋 / (1 + 𝑋))) ∈ ℝ) |
60 | 54, 59 | eqeltrd 2906 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) ∈
ℝ) |
61 | | 0red 10360 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 ∈
ℝ) |
62 | 57 | simp3d 1178 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) < 1) |
63 | 62, 15 | syl6breqr 4915 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) < (1 − 0)) |
64 | 58, 55, 61, 63 | ltsub13d 10958 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < (1 −
(𝑋 / (1 + 𝑋)))) |
65 | 64, 54 | breqtrrd 4901 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < (1 / (1 +
𝑋))) |
66 | 60, 65 | elrpd 12153 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) ∈
ℝ+) |
67 | 66 | rprecred 12167 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 / (1 +
𝑋))) ∈
ℝ) |
68 | 48, 67 | eqeltrrd 2907 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 𝑋) ∈
ℝ) |
69 | 68, 55 | resubcld 10782 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((1 + 𝑋) − 1) ∈
ℝ) |
70 | 45, 69 | eqeltrrd 2907 |
. . 3
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 𝑋 ∈ ℝ) |
71 | | 1p0e1 11482 |
. . . . 5
⊢ (1 + 0) =
1 |
72 | 57 | simp2d 1177 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < (𝑋 / (1 + 𝑋))) |
73 | 35, 72 | syl5eqbr 4908 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 − 1) <
(𝑋 / (1 + 𝑋))) |
74 | 55, 55, 58, 73 | ltsub23d 10957 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 − (𝑋 / (1 + 𝑋))) < 1) |
75 | 54, 74 | eqbrtrd 4895 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) < 1) |
76 | 66 | reclt1d 12169 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((1 / (1 + 𝑋)) < 1 ↔ 1 < (1 / (1
/ (1 + 𝑋))))) |
77 | 75, 76 | mpbid 224 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 1 < (1 / (1 /
(1 + 𝑋)))) |
78 | 77, 48 | breqtrd 4899 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 1 < (1 + 𝑋)) |
79 | 71, 78 | syl5eqbr 4908 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 0) < (1 +
𝑋)) |
80 | 61, 70, 55 | ltadd2d 10512 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (0 < 𝑋 ↔ (1 + 0) < (1 + 𝑋))) |
81 | 79, 80 | mpbird 249 |
. . 3
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < 𝑋) |
82 | 70, 81 | elrpd 12153 |
. 2
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 𝑋 ∈
ℝ+) |
83 | 44, 82 | impbida 835 |
1
⊢ (𝜑 → (𝑋 ∈ ℝ+ ↔ (𝑋 / (1 + 𝑋)) ∈ (0(,)1))) |