Proof of Theorem xov1plusxeqvd
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 𝑋 ∈
ℝ+) |
2 | 1 | rpred 11748 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 𝑋 ∈
ℝ) |
3 | | 1rp 11712 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 1 ∈
ℝ+) |
5 | 4, 1 | rpaddcld 11763 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 +
𝑋) ∈
ℝ+) |
6 | 2, 5 | rerpdivcld 11779 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) ∈ ℝ) |
7 | 5 | rprecred 11759 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 / (1
+ 𝑋)) ∈
ℝ) |
8 | | 1red 9934 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 1 ∈
ℝ) |
9 | | 0red 9920 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 ∈
ℝ) |
10 | 8, 2 | readdcld 9948 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 +
𝑋) ∈
ℝ) |
11 | 8, 1 | ltaddrpd 11781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 1 <
(1 + 𝑋)) |
12 | | recgt1i 10799 |
. . . . . . . 8
⊢ (((1 +
𝑋) ∈ ℝ ∧ 1
< (1 + 𝑋)) → (0
< (1 / (1 + 𝑋)) ∧ (1
/ (1 + 𝑋)) <
1)) |
13 | 10, 11, 12 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (0 <
(1 / (1 + 𝑋)) ∧ (1 / (1
+ 𝑋)) <
1)) |
14 | 13 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 / (1
+ 𝑋)) <
1) |
15 | | 1m0e1 11008 |
. . . . . 6
⊢ (1
− 0) = 1 |
16 | 14, 15 | syl6breqr 4625 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 / (1
+ 𝑋)) < (1 −
0)) |
17 | 7, 8, 9, 16 | ltsub13d 10512 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 <
(1 − (1 / (1 + 𝑋)))) |
18 | | 1cnd 9935 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) |
19 | | xov1plusxeqvd.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
20 | 18, 19 | addcld 9938 |
. . . . . . 7
⊢ (𝜑 → (1 + 𝑋) ∈ ℂ) |
21 | 18 | negcld 10258 |
. . . . . . . . 9
⊢ (𝜑 → -1 ∈
ℂ) |
22 | | xov1plusxeqvd.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≠ -1) |
23 | 18, 19, 21, 22 | addneintrd 10122 |
. . . . . . . 8
⊢ (𝜑 → (1 + 𝑋) ≠ (1 + -1)) |
24 | | 1pneg1e0 11006 |
. . . . . . . . 9
⊢ (1 + -1)
= 0 |
25 | 24 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (1 + -1) =
0) |
26 | 23, 25 | neeqtrd 2851 |
. . . . . . 7
⊢ (𝜑 → (1 + 𝑋) ≠ 0) |
27 | 20, 18, 20, 26 | divsubdird 10719 |
. . . . . 6
⊢ (𝜑 → (((1 + 𝑋) − 1) / (1 + 𝑋)) = (((1 + 𝑋) / (1 + 𝑋)) − (1 / (1 + 𝑋)))) |
28 | 18, 19 | pncan2d 10273 |
. . . . . . 7
⊢ (𝜑 → ((1 + 𝑋) − 1) = 𝑋) |
29 | 28 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → (((1 + 𝑋) − 1) / (1 + 𝑋)) = (𝑋 / (1 + 𝑋))) |
30 | 20, 26 | dividd 10678 |
. . . . . . 7
⊢ (𝜑 → ((1 + 𝑋) / (1 + 𝑋)) = 1) |
31 | 30 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → (((1 + 𝑋) / (1 + 𝑋)) − (1 / (1 + 𝑋))) = (1 − (1 / (1 + 𝑋)))) |
32 | 27, 29, 31 | 3eqtr3d 2652 |
. . . . 5
⊢ (𝜑 → (𝑋 / (1 + 𝑋)) = (1 − (1 / (1 + 𝑋)))) |
33 | 32 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) = (1 − (1 / (1 + 𝑋)))) |
34 | 17, 33 | breqtrrd 4611 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 <
(𝑋 / (1 + 𝑋))) |
35 | | 1m1e0 10966 |
. . . . . 6
⊢ (1
− 1) = 0 |
36 | 13 | simpld 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 <
(1 / (1 + 𝑋))) |
37 | 35, 36 | syl5eqbr 4618 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1
− 1) < (1 / (1 + 𝑋))) |
38 | 8, 8, 7, 37 | ltsub23d 10511 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1
− (1 / (1 + 𝑋))) <
1) |
39 | 33, 38 | eqbrtrd 4605 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) < 1) |
40 | | 0xr 9965 |
. . . 4
⊢ 0 ∈
ℝ* |
41 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
42 | 41 | rexri 9976 |
. . . 4
⊢ 1 ∈
ℝ* |
43 | | elioo2 12087 |
. . . 4
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑋 / (1 + 𝑋)) ∈ (0(,)1) ↔ ((𝑋 / (1 + 𝑋)) ∈ ℝ ∧ 0 < (𝑋 / (1 + 𝑋)) ∧ (𝑋 / (1 + 𝑋)) < 1))) |
44 | 40, 42, 43 | mp2an 704 |
. . 3
⊢ ((𝑋 / (1 + 𝑋)) ∈ (0(,)1) ↔ ((𝑋 / (1 + 𝑋)) ∈ ℝ ∧ 0 < (𝑋 / (1 + 𝑋)) ∧ (𝑋 / (1 + 𝑋)) < 1)) |
45 | 6, 34, 39, 44 | syl3anbrc 1239 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) |
46 | 28 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((1 + 𝑋) − 1) = 𝑋) |
47 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 𝑋) ∈
ℂ) |
48 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 𝑋) ≠ 0) |
49 | 47, 48 | recrecd 10677 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 / (1 +
𝑋))) = (1 + 𝑋)) |
50 | 20, 19, 20, 26 | divsubdird 10719 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 + 𝑋) − 𝑋) / (1 + 𝑋)) = (((1 + 𝑋) / (1 + 𝑋)) − (𝑋 / (1 + 𝑋)))) |
51 | 18, 19 | pncand 10272 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 + 𝑋) − 𝑋) = 1) |
52 | 51 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 + 𝑋) − 𝑋) / (1 + 𝑋)) = (1 / (1 + 𝑋))) |
53 | 30 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 + 𝑋) / (1 + 𝑋)) − (𝑋 / (1 + 𝑋))) = (1 − (𝑋 / (1 + 𝑋)))) |
54 | 50, 52, 53 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / (1 + 𝑋)) = (1 − (𝑋 / (1 + 𝑋)))) |
55 | 54 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) = (1 − (𝑋 / (1 + 𝑋)))) |
56 | | 1red 9934 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 1 ∈
ℝ) |
57 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) |
58 | 57, 44 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((𝑋 / (1 + 𝑋)) ∈ ℝ ∧ 0 < (𝑋 / (1 + 𝑋)) ∧ (𝑋 / (1 + 𝑋)) < 1)) |
59 | 58 | simp1d 1066 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) ∈ ℝ) |
60 | 56, 59 | resubcld 10337 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 − (𝑋 / (1 + 𝑋))) ∈ ℝ) |
61 | 55, 60 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) ∈
ℝ) |
62 | | 0red 9920 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 ∈
ℝ) |
63 | 58 | simp3d 1068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) < 1) |
64 | 63, 15 | syl6breqr 4625 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) < (1 − 0)) |
65 | 59, 56, 62, 64 | ltsub13d 10512 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < (1 −
(𝑋 / (1 + 𝑋)))) |
66 | 65, 55 | breqtrrd 4611 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < (1 / (1 +
𝑋))) |
67 | 61, 66 | elrpd 11745 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) ∈
ℝ+) |
68 | 67 | rprecred 11759 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 / (1 +
𝑋))) ∈
ℝ) |
69 | 49, 68 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 𝑋) ∈
ℝ) |
70 | 69, 56 | resubcld 10337 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((1 + 𝑋) − 1) ∈
ℝ) |
71 | 46, 70 | eqeltrrd 2689 |
. . 3
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 𝑋 ∈ ℝ) |
72 | | 1p0e1 11010 |
. . . . 5
⊢ (1 + 0) =
1 |
73 | 58 | simp2d 1067 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < (𝑋 / (1 + 𝑋))) |
74 | 35, 73 | syl5eqbr 4618 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 − 1) <
(𝑋 / (1 + 𝑋))) |
75 | 56, 56, 59, 74 | ltsub23d 10511 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 − (𝑋 / (1 + 𝑋))) < 1) |
76 | 55, 75 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) < 1) |
77 | 67 | reclt1d 11761 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((1 / (1 + 𝑋)) < 1 ↔ 1 < (1 / (1
/ (1 + 𝑋))))) |
78 | 76, 77 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 1 < (1 / (1 /
(1 + 𝑋)))) |
79 | 78, 49 | breqtrd 4609 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 1 < (1 + 𝑋)) |
80 | 72, 79 | syl5eqbr 4618 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 0) < (1 +
𝑋)) |
81 | 62, 71, 56 | ltadd2d 10072 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (0 < 𝑋 ↔ (1 + 0) < (1 + 𝑋))) |
82 | 80, 81 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < 𝑋) |
83 | 71, 82 | elrpd 11745 |
. 2
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 𝑋 ∈
ℝ+) |
84 | 45, 83 | impbida 873 |
1
⊢ (𝜑 → (𝑋 ∈ ℝ+ ↔ (𝑋 / (1 + 𝑋)) ∈ (0(,)1))) |