Proof of Theorem 2xp3dxp2ge1d
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2xp3dxp2ge1d.1 | . . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (-1[,)+∞)) | 
| 2 |  | neg1rr 12381 | . . . . . . . . 9
⊢ -1 ∈
ℝ | 
| 3 |  | elicopnf 13485 | . . . . . . . . 9
⊢ (-1
∈ ℝ → (𝑋
∈ (-1[,)+∞) ↔ (𝑋 ∈ ℝ ∧ -1 ≤ 𝑋))) | 
| 4 | 2, 3 | ax-mp 5 | . . . . . . . 8
⊢ (𝑋 ∈ (-1[,)+∞) ↔
(𝑋 ∈ ℝ ∧ -1
≤ 𝑋)) | 
| 5 | 1, 4 | sylib 218 | . . . . . . 7
⊢ (𝜑 → (𝑋 ∈ ℝ ∧ -1 ≤ 𝑋)) | 
| 6 | 5 | simpld 494 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 7 |  | 2re 12340 | . . . . . . 7
⊢ 2 ∈
ℝ | 
| 8 |  | readdcl 11238 | . . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 2 ∈
ℝ) → (𝑋 + 2)
∈ ℝ) | 
| 9 | 7, 8 | mpan2 691 | . . . . . 6
⊢ (𝑋 ∈ ℝ → (𝑋 + 2) ∈
ℝ) | 
| 10 | 6, 9 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑋 + 2) ∈ ℝ) | 
| 11 |  | neg1cn 12380 | . . . . . . . . . 10
⊢ -1 ∈
ℂ | 
| 12 |  | 2cn 12341 | . . . . . . . . . 10
⊢ 2 ∈
ℂ | 
| 13 |  | addcom 11447 | . . . . . . . . . 10
⊢ ((-1
∈ ℂ ∧ 2 ∈ ℂ) → (-1 + 2) = (2 +
-1)) | 
| 14 | 11, 12, 13 | mp2an 692 | . . . . . . . . 9
⊢ (-1 + 2)
= (2 + -1) | 
| 15 |  | ax-1cn 11213 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 16 |  | negsub 11557 | . . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ 1 ∈ ℂ) → (2 + -1) = (2 −
1)) | 
| 17 | 12, 15, 16 | mp2an 692 | . . . . . . . . 9
⊢ (2 + -1)
= (2 − 1) | 
| 18 |  | 2m1e1 12392 | . . . . . . . . 9
⊢ (2
− 1) = 1 | 
| 19 | 14, 17, 18 | 3eqtri 2769 | . . . . . . . 8
⊢ (-1 + 2)
= 1 | 
| 20 | 5 | simprd 495 | . . . . . . . . 9
⊢ (𝜑 → -1 ≤ 𝑋) | 
| 21 |  | leadd1 11731 | . . . . . . . . . . 11
⊢ ((-1
∈ ℝ ∧ 𝑋
∈ ℝ ∧ 2 ∈ ℝ) → (-1 ≤ 𝑋 ↔ (-1 + 2) ≤ (𝑋 + 2))) | 
| 22 | 2, 7, 21 | mp3an13 1454 | . . . . . . . . . 10
⊢ (𝑋 ∈ ℝ → (-1 ≤
𝑋 ↔ (-1 + 2) ≤
(𝑋 + 2))) | 
| 23 | 6, 22 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (-1 ≤ 𝑋 ↔ (-1 + 2) ≤ (𝑋 + 2))) | 
| 24 | 20, 23 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → (-1 + 2) ≤ (𝑋 + 2)) | 
| 25 | 19, 24 | eqbrtrrid 5179 | . . . . . . 7
⊢ (𝜑 → 1 ≤ (𝑋 + 2)) | 
| 26 |  | 0lt1 11785 | . . . . . . 7
⊢ 0 <
1 | 
| 27 | 25, 26 | jctil 519 | . . . . . 6
⊢ (𝜑 → (0 < 1 ∧ 1 ≤
(𝑋 + 2))) | 
| 28 |  | 0re 11263 | . . . . . . . 8
⊢ 0 ∈
ℝ | 
| 29 |  | 1re 11261 | . . . . . . . 8
⊢ 1 ∈
ℝ | 
| 30 |  | ltletr 11353 | . . . . . . . 8
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑋 + 2) ∈ ℝ) → ((0 < 1
∧ 1 ≤ (𝑋 + 2))
→ 0 < (𝑋 +
2))) | 
| 31 | 28, 29, 30 | mp3an12 1453 | . . . . . . 7
⊢ ((𝑋 + 2) ∈ ℝ → ((0
< 1 ∧ 1 ≤ (𝑋 +
2)) → 0 < (𝑋 +
2))) | 
| 32 | 10, 31 | syl 17 | . . . . . 6
⊢ (𝜑 → ((0 < 1 ∧ 1 ≤
(𝑋 + 2)) → 0 <
(𝑋 + 2))) | 
| 33 | 27, 32 | mpd 15 | . . . . 5
⊢ (𝜑 → 0 < (𝑋 + 2)) | 
| 34 | 10, 33 | jca 511 | . . . 4
⊢ (𝜑 → ((𝑋 + 2) ∈ ℝ ∧ 0 < (𝑋 + 2))) | 
| 35 |  | elrp 13036 | . . . . 5
⊢ ((𝑋 + 2) ∈ ℝ+
↔ ((𝑋 + 2) ∈
ℝ ∧ 0 < (𝑋 +
2))) | 
| 36 | 35 | imbi2i 336 | . . . 4
⊢ ((𝜑 → (𝑋 + 2) ∈ ℝ+) ↔
(𝜑 → ((𝑋 + 2) ∈ ℝ ∧ 0 < (𝑋 + 2)))) | 
| 37 | 34, 36 | mpbir 231 | . . 3
⊢ (𝜑 → (𝑋 + 2) ∈
ℝ+) | 
| 38 |  | remulcl 11240 | . . . . . 6
⊢ ((2
∈ ℝ ∧ 𝑋
∈ ℝ) → (2 · 𝑋) ∈ ℝ) | 
| 39 | 7, 38 | mpan 690 | . . . . 5
⊢ (𝑋 ∈ ℝ → (2
· 𝑋) ∈
ℝ) | 
| 40 | 6, 39 | syl 17 | . . . 4
⊢ (𝜑 → (2 · 𝑋) ∈
ℝ) | 
| 41 |  | 3re 12346 | . . . . 5
⊢ 3 ∈
ℝ | 
| 42 |  | readdcl 11238 | . . . . 5
⊢ (((2
· 𝑋) ∈ ℝ
∧ 3 ∈ ℝ) → ((2 · 𝑋) + 3) ∈ ℝ) | 
| 43 | 41, 42 | mpan2 691 | . . . 4
⊢ ((2
· 𝑋) ∈ ℝ
→ ((2 · 𝑋) + 3)
∈ ℝ) | 
| 44 | 40, 43 | syl 17 | . . 3
⊢ (𝜑 → ((2 · 𝑋) + 3) ∈
ℝ) | 
| 45 | 7 | a1i 11 | . . . . 5
⊢ (𝜑 → 2 ∈
ℝ) | 
| 46 |  | 1red 11262 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) | 
| 47 | 40, 46 | readdcld 11290 | . . . . 5
⊢ (𝜑 → ((2 · 𝑋) + 1) ∈
ℝ) | 
| 48 |  | recn 11245 | . . . . . . . 8
⊢ (𝑋 ∈ ℝ → 𝑋 ∈
ℂ) | 
| 49 |  | addrid 11441 | . . . . . . . 8
⊢ (𝑋 ∈ ℂ → (𝑋 + 0) = 𝑋) | 
| 50 | 48, 49 | syl 17 | . . . . . . 7
⊢ (𝑋 ∈ ℝ → (𝑋 + 0) = 𝑋) | 
| 51 | 6, 50 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝑋 + 0) = 𝑋) | 
| 52 | 11, 15 | addcomi 11452 | . . . . . . . . . 10
⊢ (-1 + 1)
= (1 + -1) | 
| 53 | 15 | negidi 11578 | . . . . . . . . . 10
⊢ (1 + -1)
= 0 | 
| 54 | 52, 53 | eqtri 2765 | . . . . . . . . 9
⊢ (-1 + 1)
= 0 | 
| 55 |  | leadd1 11731 | . . . . . . . . . . . 12
⊢ ((-1
∈ ℝ ∧ 𝑋
∈ ℝ ∧ 1 ∈ ℝ) → (-1 ≤ 𝑋 ↔ (-1 + 1) ≤ (𝑋 + 1))) | 
| 56 | 2, 29, 55 | mp3an13 1454 | . . . . . . . . . . 11
⊢ (𝑋 ∈ ℝ → (-1 ≤
𝑋 ↔ (-1 + 1) ≤
(𝑋 + 1))) | 
| 57 | 6, 56 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (-1 ≤ 𝑋 ↔ (-1 + 1) ≤ (𝑋 + 1))) | 
| 58 | 20, 57 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (-1 + 1) ≤ (𝑋 + 1)) | 
| 59 | 54, 58 | eqbrtrrid 5179 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ (𝑋 + 1)) | 
| 60 |  | readdcl 11238 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑋 + 1)
∈ ℝ) | 
| 61 | 29, 60 | mpan2 691 | . . . . . . . . . . 11
⊢ (𝑋 ∈ ℝ → (𝑋 + 1) ∈
ℝ) | 
| 62 | 6, 61 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑋 + 1) ∈ ℝ) | 
| 63 | 62, 6 | jca 511 | . . . . . . . . 9
⊢ (𝜑 → ((𝑋 + 1) ∈ ℝ ∧ 𝑋 ∈ ℝ)) | 
| 64 |  | leadd2 11732 | . . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (𝑋 +
1) ∈ ℝ ∧ 𝑋
∈ ℝ) → (0 ≤ (𝑋 + 1) ↔ (𝑋 + 0) ≤ (𝑋 + (𝑋 + 1)))) | 
| 65 | 28, 64 | mp3an1 1450 | . . . . . . . . 9
⊢ (((𝑋 + 1) ∈ ℝ ∧ 𝑋 ∈ ℝ) → (0 ≤
(𝑋 + 1) ↔ (𝑋 + 0) ≤ (𝑋 + (𝑋 + 1)))) | 
| 66 | 63, 65 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (0 ≤ (𝑋 + 1) ↔ (𝑋 + 0) ≤ (𝑋 + (𝑋 + 1)))) | 
| 67 | 59, 66 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (𝑋 + 0) ≤ (𝑋 + (𝑋 + 1))) | 
| 68 | 6, 48 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 69 | 68 | 2timesd 12509 | . . . . . . . . 9
⊢ (𝜑 → (2 · 𝑋) = (𝑋 + 𝑋)) | 
| 70 | 69 | oveq1d 7446 | . . . . . . . 8
⊢ (𝜑 → ((2 · 𝑋) + 1) = ((𝑋 + 𝑋) + 1)) | 
| 71 |  | addass 11242 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑋 + 𝑋) + 1) = (𝑋 + (𝑋 + 1))) | 
| 72 | 15, 71 | mp3an3 1452 | . . . . . . . . . 10
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((𝑋 + 𝑋) + 1) = (𝑋 + (𝑋 + 1))) | 
| 73 | 72 | anidms 566 | . . . . . . . . 9
⊢ (𝑋 ∈ ℂ → ((𝑋 + 𝑋) + 1) = (𝑋 + (𝑋 + 1))) | 
| 74 | 68, 73 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ((𝑋 + 𝑋) + 1) = (𝑋 + (𝑋 + 1))) | 
| 75 | 70, 74 | eqtrd 2777 | . . . . . . 7
⊢ (𝜑 → ((2 · 𝑋) + 1) = (𝑋 + (𝑋 + 1))) | 
| 76 | 67, 75 | breqtrrd 5171 | . . . . . 6
⊢ (𝜑 → (𝑋 + 0) ≤ ((2 · 𝑋) + 1)) | 
| 77 | 51, 76 | eqbrtrrd 5167 | . . . . 5
⊢ (𝜑 → 𝑋 ≤ ((2 · 𝑋) + 1)) | 
| 78 | 45 | leidd 11829 | . . . . 5
⊢ (𝜑 → 2 ≤ 2) | 
| 79 | 6, 45, 47, 45, 77, 78 | le2addd 11882 | . . . 4
⊢ (𝜑 → (𝑋 + 2) ≤ (((2 · 𝑋) + 1) + 2)) | 
| 80 | 40 | recnd 11289 | . . . . . 6
⊢ (𝜑 → (2 · 𝑋) ∈
ℂ) | 
| 81 | 15 | a1i 11 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) | 
| 82 | 12 | a1i 11 | . . . . . 6
⊢ (𝜑 → 2 ∈
ℂ) | 
| 83 | 80, 81, 82 | addassd 11283 | . . . . 5
⊢ (𝜑 → (((2 · 𝑋) + 1) + 2) = ((2 · 𝑋) + (1 + 2))) | 
| 84 |  | 1p2e3 12409 | . . . . . 6
⊢ (1 + 2) =
3 | 
| 85 |  | oveq2 7439 | . . . . . 6
⊢ ((1 + 2)
= 3 → ((2 · 𝑋)
+ (1 + 2)) = ((2 · 𝑋) + 3)) | 
| 86 | 84, 85 | ax-mp 5 | . . . . 5
⊢ ((2
· 𝑋) + (1 + 2)) =
((2 · 𝑋) +
3) | 
| 87 | 83, 86 | eqtrdi 2793 | . . . 4
⊢ (𝜑 → (((2 · 𝑋) + 1) + 2) = ((2 · 𝑋) + 3)) | 
| 88 | 79, 87 | breqtrd 5169 | . . 3
⊢ (𝜑 → (𝑋 + 2) ≤ ((2 · 𝑋) + 3)) | 
| 89 | 37, 44, 88 | 3jca 1129 | . 2
⊢ (𝜑 → ((𝑋 + 2) ∈ ℝ+ ∧ ((2
· 𝑋) + 3) ∈
ℝ ∧ (𝑋 + 2) ≤
((2 · 𝑋) +
3))) | 
| 90 |  | divge1 13103 | . 2
⊢ (((𝑋 + 2) ∈ ℝ+
∧ ((2 · 𝑋) + 3)
∈ ℝ ∧ (𝑋 +
2) ≤ ((2 · 𝑋) +
3)) → 1 ≤ (((2 · 𝑋) + 3) / (𝑋 + 2))) | 
| 91 | 89, 90 | syl 17 | 1
⊢ (𝜑 → 1 ≤ (((2 · 𝑋) + 3) / (𝑋 + 2))) |