Proof of Theorem xov1plusxeqvd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 𝑋 ∈
ℝ+) | 
| 2 | 1 | rpred 13078 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 𝑋 ∈
ℝ) | 
| 3 |  | 1rp 13039 | . . . . . 6
⊢ 1 ∈
ℝ+ | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 1 ∈
ℝ+) | 
| 5 | 4, 1 | rpaddcld 13093 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 +
𝑋) ∈
ℝ+) | 
| 6 | 2, 5 | rerpdivcld 13109 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) ∈ ℝ) | 
| 7 | 5 | rprecred 13089 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 / (1
+ 𝑋)) ∈
ℝ) | 
| 8 |  | 1red 11263 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 1 ∈
ℝ) | 
| 9 |  | 0red 11265 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 ∈
ℝ) | 
| 10 | 8, 2 | readdcld 11291 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 +
𝑋) ∈
ℝ) | 
| 11 | 8, 1 | ltaddrpd 13111 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 1 <
(1 + 𝑋)) | 
| 12 |  | recgt1i 12166 | . . . . . . . 8
⊢ (((1 +
𝑋) ∈ ℝ ∧ 1
< (1 + 𝑋)) → (0
< (1 / (1 + 𝑋)) ∧ (1
/ (1 + 𝑋)) <
1)) | 
| 13 | 10, 11, 12 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (0 <
(1 / (1 + 𝑋)) ∧ (1 / (1
+ 𝑋)) <
1)) | 
| 14 | 13 | simprd 495 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 / (1
+ 𝑋)) <
1) | 
| 15 |  | 1m0e1 12388 | . . . . . 6
⊢ (1
− 0) = 1 | 
| 16 | 14, 15 | breqtrrdi 5184 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1 / (1
+ 𝑋)) < (1 −
0)) | 
| 17 | 7, 8, 9, 16 | ltsub13d 11870 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 <
(1 − (1 / (1 + 𝑋)))) | 
| 18 |  | 1cnd 11257 | . . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) | 
| 19 |  | xov1plusxeqvd.1 | . . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 20 | 18, 19 | addcld 11281 | . . . . . . 7
⊢ (𝜑 → (1 + 𝑋) ∈ ℂ) | 
| 21 | 18 | negcld 11608 | . . . . . . . . 9
⊢ (𝜑 → -1 ∈
ℂ) | 
| 22 |  | xov1plusxeqvd.2 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ≠ -1) | 
| 23 | 18, 19, 21, 22 | addneintrd 11469 | . . . . . . . 8
⊢ (𝜑 → (1 + 𝑋) ≠ (1 + -1)) | 
| 24 |  | 1pneg1e0 12386 | . . . . . . . . 9
⊢ (1 + -1)
= 0 | 
| 25 | 24 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (1 + -1) =
0) | 
| 26 | 23, 25 | neeqtrd 3009 | . . . . . . 7
⊢ (𝜑 → (1 + 𝑋) ≠ 0) | 
| 27 | 20, 18, 20, 26 | divsubdird 12083 | . . . . . 6
⊢ (𝜑 → (((1 + 𝑋) − 1) / (1 + 𝑋)) = (((1 + 𝑋) / (1 + 𝑋)) − (1 / (1 + 𝑋)))) | 
| 28 | 18, 19 | pncan2d 11623 | . . . . . . 7
⊢ (𝜑 → ((1 + 𝑋) − 1) = 𝑋) | 
| 29 | 28 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → (((1 + 𝑋) − 1) / (1 + 𝑋)) = (𝑋 / (1 + 𝑋))) | 
| 30 | 20, 26 | dividd 12042 | . . . . . . 7
⊢ (𝜑 → ((1 + 𝑋) / (1 + 𝑋)) = 1) | 
| 31 | 30 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → (((1 + 𝑋) / (1 + 𝑋)) − (1 / (1 + 𝑋))) = (1 − (1 / (1 + 𝑋)))) | 
| 32 | 27, 29, 31 | 3eqtr3d 2784 | . . . . 5
⊢ (𝜑 → (𝑋 / (1 + 𝑋)) = (1 − (1 / (1 + 𝑋)))) | 
| 33 | 32 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) = (1 − (1 / (1 + 𝑋)))) | 
| 34 | 17, 33 | breqtrrd 5170 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 <
(𝑋 / (1 + 𝑋))) | 
| 35 |  | 1m1e0 12339 | . . . . . 6
⊢ (1
− 1) = 0 | 
| 36 | 13 | simpld 494 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → 0 <
(1 / (1 + 𝑋))) | 
| 37 | 35, 36 | eqbrtrid 5177 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1
− 1) < (1 / (1 + 𝑋))) | 
| 38 | 8, 8, 7, 37 | ltsub23d 11869 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (1
− (1 / (1 + 𝑋))) <
1) | 
| 39 | 33, 38 | eqbrtrd 5164 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) < 1) | 
| 40 |  | 0xr 11309 | . . . 4
⊢ 0 ∈
ℝ* | 
| 41 |  | 1xr 11321 | . . . 4
⊢ 1 ∈
ℝ* | 
| 42 |  | elioo2 13429 | . . . 4
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑋 / (1 + 𝑋)) ∈ (0(,)1) ↔ ((𝑋 / (1 + 𝑋)) ∈ ℝ ∧ 0 < (𝑋 / (1 + 𝑋)) ∧ (𝑋 / (1 + 𝑋)) < 1))) | 
| 43 | 40, 41, 42 | mp2an 692 | . . 3
⊢ ((𝑋 / (1 + 𝑋)) ∈ (0(,)1) ↔ ((𝑋 / (1 + 𝑋)) ∈ ℝ ∧ 0 < (𝑋 / (1 + 𝑋)) ∧ (𝑋 / (1 + 𝑋)) < 1)) | 
| 44 | 6, 34, 39, 43 | syl3anbrc 1343 | . 2
⊢ ((𝜑 ∧ 𝑋 ∈ ℝ+) → (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) | 
| 45 | 28 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((1 + 𝑋) − 1) = 𝑋) | 
| 46 | 20 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 𝑋) ∈
ℂ) | 
| 47 | 26 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 𝑋) ≠ 0) | 
| 48 | 46, 47 | recrecd 12041 | . . . . . 6
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 / (1 +
𝑋))) = (1 + 𝑋)) | 
| 49 | 20, 19, 20, 26 | divsubdird 12083 | . . . . . . . . . . 11
⊢ (𝜑 → (((1 + 𝑋) − 𝑋) / (1 + 𝑋)) = (((1 + 𝑋) / (1 + 𝑋)) − (𝑋 / (1 + 𝑋)))) | 
| 50 | 18, 19 | pncand 11622 | . . . . . . . . . . . 12
⊢ (𝜑 → ((1 + 𝑋) − 𝑋) = 1) | 
| 51 | 50 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (((1 + 𝑋) − 𝑋) / (1 + 𝑋)) = (1 / (1 + 𝑋))) | 
| 52 | 30 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (((1 + 𝑋) / (1 + 𝑋)) − (𝑋 / (1 + 𝑋))) = (1 − (𝑋 / (1 + 𝑋)))) | 
| 53 | 49, 51, 52 | 3eqtr3d 2784 | . . . . . . . . . 10
⊢ (𝜑 → (1 / (1 + 𝑋)) = (1 − (𝑋 / (1 + 𝑋)))) | 
| 54 | 53 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) = (1 − (𝑋 / (1 + 𝑋)))) | 
| 55 |  | 1red 11263 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 1 ∈
ℝ) | 
| 56 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) | 
| 57 | 56, 43 | sylib 218 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((𝑋 / (1 + 𝑋)) ∈ ℝ ∧ 0 < (𝑋 / (1 + 𝑋)) ∧ (𝑋 / (1 + 𝑋)) < 1)) | 
| 58 | 57 | simp1d 1142 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) ∈ ℝ) | 
| 59 | 55, 58 | resubcld 11692 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 − (𝑋 / (1 + 𝑋))) ∈ ℝ) | 
| 60 | 54, 59 | eqeltrd 2840 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) ∈
ℝ) | 
| 61 |  | 0red 11265 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 ∈
ℝ) | 
| 62 | 57 | simp3d 1144 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) < 1) | 
| 63 | 62, 15 | breqtrrdi 5184 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (𝑋 / (1 + 𝑋)) < (1 − 0)) | 
| 64 | 58, 55, 61, 63 | ltsub13d 11870 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < (1 −
(𝑋 / (1 + 𝑋)))) | 
| 65 | 64, 54 | breqtrrd 5170 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < (1 / (1 +
𝑋))) | 
| 66 | 60, 65 | elrpd 13075 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) ∈
ℝ+) | 
| 67 | 66 | rprecred 13089 | . . . . . 6
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 / (1 +
𝑋))) ∈
ℝ) | 
| 68 | 48, 67 | eqeltrrd 2841 | . . . . 5
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 𝑋) ∈
ℝ) | 
| 69 | 68, 55 | resubcld 11692 | . . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((1 + 𝑋) − 1) ∈
ℝ) | 
| 70 | 45, 69 | eqeltrrd 2841 | . . 3
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 𝑋 ∈ ℝ) | 
| 71 |  | 1p0e1 12391 | . . . . 5
⊢ (1 + 0) =
1 | 
| 72 | 57 | simp2d 1143 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < (𝑋 / (1 + 𝑋))) | 
| 73 | 35, 72 | eqbrtrid 5177 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 − 1) <
(𝑋 / (1 + 𝑋))) | 
| 74 | 55, 55, 58, 73 | ltsub23d 11869 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 − (𝑋 / (1 + 𝑋))) < 1) | 
| 75 | 54, 74 | eqbrtrd 5164 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 / (1 + 𝑋)) < 1) | 
| 76 | 66 | reclt1d 13091 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → ((1 / (1 + 𝑋)) < 1 ↔ 1 < (1 / (1
/ (1 + 𝑋))))) | 
| 77 | 75, 76 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 1 < (1 / (1 /
(1 + 𝑋)))) | 
| 78 | 77, 48 | breqtrd 5168 | . . . . 5
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 1 < (1 + 𝑋)) | 
| 79 | 71, 78 | eqbrtrid 5177 | . . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (1 + 0) < (1 +
𝑋)) | 
| 80 | 61, 70, 55 | ltadd2d 11418 | . . . 4
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → (0 < 𝑋 ↔ (1 + 0) < (1 + 𝑋))) | 
| 81 | 79, 80 | mpbird 257 | . . 3
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 0 < 𝑋) | 
| 82 | 70, 81 | elrpd 13075 | . 2
⊢ ((𝜑 ∧ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)) → 𝑋 ∈
ℝ+) | 
| 83 | 44, 82 | impbida 800 | 1
⊢ (𝜑 → (𝑋 ∈ ℝ+ ↔ (𝑋 / (1 + 𝑋)) ∈ (0(,)1))) |