| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rpge0 13048 | . . . . . 6
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ 𝑥) | 
| 2 | 1 | adantl 481 | . . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 0 ≤ 𝑥) | 
| 3 |  | simplr 769 | . . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐵 ∈ ℝ) | 
| 4 |  | rpre 13043 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) | 
| 5 | 4 | adantl 481 | . . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ) | 
| 6 | 3, 5 | addge01d 11851 | . . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → (0 ≤ 𝑥 ↔ 𝐵 ≤ (𝐵 + 𝑥))) | 
| 7 | 2, 6 | mpbid 232 | . . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐵 ≤ (𝐵 + 𝑥)) | 
| 8 |  | simpll 767 | . . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐴 ∈
ℝ*) | 
| 9 | 3 | rexrd 11311 | . . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐵 ∈
ℝ*) | 
| 10 | 3, 5 | readdcld 11290 | . . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → (𝐵 + 𝑥) ∈ ℝ) | 
| 11 | 10 | rexrd 11311 | . . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → (𝐵 + 𝑥) ∈
ℝ*) | 
| 12 |  | xrletr 13200 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐵 + 𝑥) ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ (𝐵 + 𝑥)) → 𝐴 ≤ (𝐵 + 𝑥))) | 
| 13 | 8, 9, 11, 12 | syl3anc 1373 | . . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ (𝐵 + 𝑥)) → 𝐴 ≤ (𝐵 + 𝑥))) | 
| 14 | 7, 13 | mpan2d 694 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → (𝐴 ≤ 𝐵 → 𝐴 ≤ (𝐵 + 𝑥))) | 
| 15 | 14 | ralrimdva 3154 | . 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴 ≤ 𝐵 → ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥))) | 
| 16 |  | rexr 11307 | . . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) | 
| 17 | 16 | adantl 481 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ 𝐵 ∈
ℝ*) | 
| 18 |  | simpl 482 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ 𝐴 ∈
ℝ*) | 
| 19 |  | qbtwnxr 13242 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐴 ∈
ℝ* ∧ 𝐵
< 𝐴) → ∃𝑦 ∈ ℚ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴)) | 
| 20 | 19 | 3expia 1122 | . . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝐵 < 𝐴 → ∃𝑦 ∈ ℚ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) | 
| 21 | 17, 18, 20 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐵 < 𝐴 → ∃𝑦 ∈ ℚ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) | 
| 22 |  | simprrl 781 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝐵 < 𝑦) | 
| 23 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝐵 ∈ ℝ) | 
| 24 |  | qre 12995 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ℚ → 𝑦 ∈
ℝ) | 
| 25 | 24 | ad2antrl 728 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝑦 ∈ ℝ) | 
| 26 |  | difrp 13073 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐵 < 𝑦 ↔ (𝑦 − 𝐵) ∈
ℝ+)) | 
| 27 | 23, 25, 26 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → (𝐵 < 𝑦 ↔ (𝑦 − 𝐵) ∈
ℝ+)) | 
| 28 | 22, 27 | mpbid 232 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → (𝑦 − 𝐵) ∈
ℝ+) | 
| 29 |  | simprrr 782 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝑦 < 𝐴) | 
| 30 | 25 | rexrd 11311 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝑦 ∈ ℝ*) | 
| 31 |  | simpll 767 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝐴 ∈
ℝ*) | 
| 32 |  | xrltnle 11328 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝑦 < 𝐴 ↔ ¬ 𝐴 ≤ 𝑦)) | 
| 33 | 30, 31, 32 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → (𝑦 < 𝐴 ↔ ¬ 𝐴 ≤ 𝑦)) | 
| 34 | 29, 33 | mpbid 232 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → ¬ 𝐴 ≤ 𝑦) | 
| 35 | 23 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝐵 ∈ ℂ) | 
| 36 | 25 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝑦 ∈ ℂ) | 
| 37 | 35, 36 | pncan3d 11623 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → (𝐵 + (𝑦 − 𝐵)) = 𝑦) | 
| 38 | 37 | breq2d 5155 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → (𝐴 ≤ (𝐵 + (𝑦 − 𝐵)) ↔ 𝐴 ≤ 𝑦)) | 
| 39 | 34, 38 | mtbird 325 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → ¬ 𝐴 ≤ (𝐵 + (𝑦 − 𝐵))) | 
| 40 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑦 − 𝐵) → (𝐵 + 𝑥) = (𝐵 + (𝑦 − 𝐵))) | 
| 41 | 40 | breq2d 5155 | . . . . . . . . . 10
⊢ (𝑥 = (𝑦 − 𝐵) → (𝐴 ≤ (𝐵 + 𝑥) ↔ 𝐴 ≤ (𝐵 + (𝑦 − 𝐵)))) | 
| 42 | 41 | notbid 318 | . . . . . . . . 9
⊢ (𝑥 = (𝑦 − 𝐵) → (¬ 𝐴 ≤ (𝐵 + 𝑥) ↔ ¬ 𝐴 ≤ (𝐵 + (𝑦 − 𝐵)))) | 
| 43 | 42 | rspcev 3622 | . . . . . . . 8
⊢ (((𝑦 − 𝐵) ∈ ℝ+ ∧ ¬
𝐴 ≤ (𝐵 + (𝑦 − 𝐵))) → ∃𝑥 ∈ ℝ+ ¬ 𝐴 ≤ (𝐵 + 𝑥)) | 
| 44 | 28, 39, 43 | syl2anc 584 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → ∃𝑥 ∈ ℝ+ ¬ 𝐴 ≤ (𝐵 + 𝑥)) | 
| 45 |  | rexnal 3100 | . . . . . . 7
⊢
(∃𝑥 ∈
ℝ+ ¬ 𝐴
≤ (𝐵 + 𝑥) ↔ ¬ ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥)) | 
| 46 | 44, 45 | sylib 218 | . . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → ¬ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + 𝑥)) | 
| 47 | 46 | rexlimdvaa 3156 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (∃𝑦 ∈
ℚ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴) → ¬ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + 𝑥))) | 
| 48 | 21, 47 | syld 47 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐵 < 𝐴 → ¬ ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥))) | 
| 49 | 48 | con2d 134 | . . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (∀𝑥 ∈
ℝ+ 𝐴 ≤
(𝐵 + 𝑥) → ¬ 𝐵 < 𝐴)) | 
| 50 |  | xrlenlt 11326 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | 
| 51 | 16, 50 | sylan2 593 | . . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | 
| 52 | 49, 51 | sylibrd 259 | . 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (∀𝑥 ∈
ℝ+ 𝐴 ≤
(𝐵 + 𝑥) → 𝐴 ≤ 𝐵)) | 
| 53 | 15, 52 | impbid 212 | 1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥))) |