Proof of Theorem xrlexaddrp
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xrlexaddrp.1 | . . . . 5
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 2 |  | pnfge 13173 | . . . . 5
⊢ (𝐴 ∈ ℝ*
→ 𝐴 ≤
+∞) | 
| 3 | 1, 2 | syl 17 | . . . 4
⊢ (𝜑 → 𝐴 ≤ +∞) | 
| 4 | 3 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐵 = +∞) → 𝐴 ≤ +∞) | 
| 5 |  | id 22 | . . . . 5
⊢ (𝐵 = +∞ → 𝐵 = +∞) | 
| 6 | 5 | eqcomd 2742 | . . . 4
⊢ (𝐵 = +∞ → +∞ =
𝐵) | 
| 7 | 6 | adantl 481 | . . 3
⊢ ((𝜑 ∧ 𝐵 = +∞) → +∞ = 𝐵) | 
| 8 | 4, 7 | breqtrd 5168 | . 2
⊢ ((𝜑 ∧ 𝐵 = +∞) → 𝐴 ≤ 𝐵) | 
| 9 |  | simpl 482 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → 𝜑) | 
| 10 |  | neqne 2947 | . . . 4
⊢ (¬
𝐵 = +∞ → 𝐵 ≠ +∞) | 
| 11 | 10 | adantl 481 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → 𝐵 ≠ +∞) | 
| 12 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 = -∞) → 𝐴 = -∞) | 
| 13 |  | xrlexaddrp.2 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 14 |  | mnfle 13178 | . . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ -∞ ≤ 𝐵) | 
| 15 | 13, 14 | syl 17 | . . . . . . 7
⊢ (𝜑 → -∞ ≤ 𝐵) | 
| 16 | 15 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 = -∞) → -∞ ≤ 𝐵) | 
| 17 | 12, 16 | eqbrtrd 5164 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = -∞) → 𝐴 ≤ 𝐵) | 
| 18 | 17 | adantlr 715 | . . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 = -∞) → 𝐴 ≤ 𝐵) | 
| 19 |  | simpl 482 | . . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐴 = -∞) → (𝜑 ∧ 𝐵 ≠ +∞)) | 
| 20 |  | neqne 2947 | . . . . . 6
⊢ (¬
𝐴 = -∞ → 𝐴 ≠ -∞) | 
| 21 | 20 | adantl 481 | . . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ≠ -∞) | 
| 22 |  | simpll 766 | . . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) → 𝜑) | 
| 23 | 13 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → 𝐵 ∈
ℝ*) | 
| 24 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → 𝐵 ≠ +∞) | 
| 25 | 23, 24 | jca 511 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → (𝐵 ∈ ℝ* ∧ 𝐵 ≠
+∞)) | 
| 26 |  | xrnepnf 13161 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
↔ (𝐵 ∈ ℝ
∨ 𝐵 =
-∞)) | 
| 27 | 25, 26 | sylib 218 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → (𝐵 ∈ ℝ ∨ 𝐵 = -∞)) | 
| 28 | 27 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐵 ∈ ℝ) → (𝐵 ∈ ℝ ∨ 𝐵 = -∞)) | 
| 29 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐵 ∈ ℝ) → ¬
𝐵 ∈
ℝ) | 
| 30 |  | pm2.53 851 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∨ 𝐵 = -∞) → (¬ 𝐵 ∈ ℝ → 𝐵 = -∞)) | 
| 31 | 28, 29, 30 | sylc 65 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐵 ∈ ℝ) → 𝐵 = -∞) | 
| 32 | 31 | adantlr 715 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) ∧ ¬ 𝐵 ∈ ℝ) → 𝐵 = -∞) | 
| 33 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝜑) | 
| 34 |  | 1rp 13039 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ | 
| 35 | 34 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℝ+) | 
| 36 |  | 1re 11262 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ | 
| 37 | 36 | elexi 3502 | . . . . . . . . . . . . . 14
⊢ 1 ∈
V | 
| 38 |  | eleq1 2828 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → (𝑥 ∈ ℝ+ ↔ 1 ∈
ℝ+)) | 
| 39 | 38 | anbi2d 630 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ∈ ℝ+) ↔ (𝜑 ∧ 1 ∈
ℝ+))) | 
| 40 |  | oveq2 7440 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → (𝐵 +𝑒 𝑥) = (𝐵 +𝑒 1)) | 
| 41 | 40 | breq2d 5154 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 1 → (𝐴 ≤ (𝐵 +𝑒 𝑥) ↔ 𝐴 ≤ (𝐵 +𝑒 1))) | 
| 42 | 39, 41 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 +𝑒 𝑥)) ↔ ((𝜑 ∧ 1 ∈ ℝ+) →
𝐴 ≤ (𝐵 +𝑒
1)))) | 
| 43 |  | xrlexaddrp.3 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 +𝑒 𝑥)) | 
| 44 | 37, 42, 43 | vtocl 3557 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 1 ∈
ℝ+) → 𝐴 ≤ (𝐵 +𝑒 1)) | 
| 45 | 33, 35, 44 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ (𝐵 +𝑒 1)) | 
| 46 | 45 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → 𝐴 ≤ (𝐵 +𝑒 1)) | 
| 47 |  | oveq1 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 = -∞ → (𝐵 +𝑒 1) =
(-∞ +𝑒 1)) | 
| 48 |  | 1xr 11321 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ* | 
| 49 |  | ltpnf 13163 | . . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
ℝ → 1 < +∞) | 
| 50 | 36, 49 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 <
+∞ | 
| 51 | 36, 50 | ltneii 11375 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ≠
+∞ | 
| 52 |  | xaddmnf2 13272 | . . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ* ∧ 1 ≠ +∞) → (-∞
+𝑒 1) = -∞) | 
| 53 | 48, 51, 52 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢ (-∞
+𝑒 1) = -∞ | 
| 54 | 53 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 = -∞ → (-∞
+𝑒 1) = -∞) | 
| 55 | 47, 54 | eqtr2d 2777 | . . . . . . . . . . . . . . 15
⊢ (𝐵 = -∞ → -∞ =
(𝐵 +𝑒
1)) | 
| 56 | 55 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → -∞ = (𝐵 +𝑒
1)) | 
| 57 | 56 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → (𝐵 +𝑒 1) =
-∞) | 
| 58 | 1 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 ≠ -∞) → 𝐴 ∈
ℝ*) | 
| 59 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 ≠ -∞) → 𝐴 ≠ -∞) | 
| 60 |  | nemnftgtmnft 45360 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
→ -∞ < 𝐴) | 
| 61 | 58, 59, 60 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ≠ -∞) → -∞ < 𝐴) | 
| 62 | 61 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → -∞ < 𝐴) | 
| 63 | 57, 62 | eqbrtrd 5164 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → (𝐵 +𝑒 1) < 𝐴) | 
| 64 | 13 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → 𝐵 ∈
ℝ*) | 
| 65 | 48 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → 1 ∈
ℝ*) | 
| 66 | 64, 65 | xaddcld 13344 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → (𝐵 +𝑒 1) ∈
ℝ*) | 
| 67 | 1 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → 𝐴 ∈
ℝ*) | 
| 68 |  | xrltnle 11329 | . . . . . . . . . . . . 13
⊢ (((𝐵 +𝑒 1) ∈
ℝ* ∧ 𝐴
∈ ℝ*) → ((𝐵 +𝑒 1) < 𝐴 ↔ ¬ 𝐴 ≤ (𝐵 +𝑒 1))) | 
| 69 | 66, 67, 68 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → ((𝐵 +𝑒 1) < 𝐴 ↔ ¬ 𝐴 ≤ (𝐵 +𝑒 1))) | 
| 70 | 63, 69 | mpbid 232 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → ¬ 𝐴 ≤ (𝐵 +𝑒 1)) | 
| 71 | 46, 70 | pm2.65da 816 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ -∞) → ¬ 𝐵 = -∞) | 
| 72 | 71 | neqned 2946 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ -∞) → 𝐵 ≠ -∞) | 
| 73 | 72 | ad4ant13 751 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) ∧ ¬ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞) | 
| 74 | 73 | neneqd 2944 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) ∧ ¬ 𝐵 ∈ ℝ) → ¬
𝐵 =
-∞) | 
| 75 | 32, 74 | condan 817 | . . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) → 𝐵 ∈ ℝ) | 
| 76 | 43 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 +𝑒 𝑥)) | 
| 77 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ+)
→ 𝐵 ∈
ℝ) | 
| 78 |  | rpre 13044 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) | 
| 79 | 78 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ+)
→ 𝑥 ∈
ℝ) | 
| 80 |  | rexadd 13275 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐵 +𝑒 𝑥) = (𝐵 + 𝑥)) | 
| 81 | 77, 79, 80 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ+)
→ (𝐵
+𝑒 𝑥) =
(𝐵 + 𝑥)) | 
| 82 | 81 | adantll 714 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → (𝐵 +𝑒 𝑥) = (𝐵 + 𝑥)) | 
| 83 | 76, 82 | breqtrd 5168 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 + 𝑥)) | 
| 84 | 83 | ralrimiva 3145 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥)) | 
| 85 | 1 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → 𝐴 ∈
ℝ*) | 
| 86 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ) | 
| 87 |  | xralrple 13248 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥))) | 
| 88 | 85, 86, 87 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + 𝑥))) | 
| 89 | 84, 88 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ 𝐵) | 
| 90 | 22, 75, 89 | syl2anc 584 | . . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) → 𝐴 ≤ 𝐵) | 
| 91 | 19, 21, 90 | syl2anc 584 | . . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ≤ 𝐵) | 
| 92 | 18, 91 | pm2.61dan 812 | . . 3
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → 𝐴 ≤ 𝐵) | 
| 93 | 9, 11, 92 | syl2anc 584 | . 2
⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → 𝐴 ≤ 𝐵) | 
| 94 | 8, 93 | pm2.61dan 812 | 1
⊢ (𝜑 → 𝐴 ≤ 𝐵) |