Step | Hyp | Ref
| Expression |
1 | | rpge0 12725 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ 𝑥) |
2 | 1 | adantl 481 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 0 ≤ 𝑥) |
3 | | simplr 765 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐵 ∈ ℝ) |
4 | | rpre 12720 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
5 | 4 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ) |
6 | 3, 5 | addge01d 11546 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → (0 ≤ 𝑥 ↔ 𝐵 ≤ (𝐵 + 𝑥))) |
7 | 2, 6 | mpbid 231 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐵 ≤ (𝐵 + 𝑥)) |
8 | | simpll 763 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐴 ∈
ℝ*) |
9 | 3 | rexrd 11009 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐵 ∈
ℝ*) |
10 | 3, 5 | readdcld 10988 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → (𝐵 + 𝑥) ∈ ℝ) |
11 | 10 | rexrd 11009 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → (𝐵 + 𝑥) ∈
ℝ*) |
12 | | xrletr 12874 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐵 + 𝑥) ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ (𝐵 + 𝑥)) → 𝐴 ≤ (𝐵 + 𝑥))) |
13 | 8, 9, 11, 12 | syl3anc 1369 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ (𝐵 + 𝑥)) → 𝐴 ≤ (𝐵 + 𝑥))) |
14 | 7, 13 | mpan2d 690 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ 𝑥 ∈
ℝ+) → (𝐴 ≤ 𝐵 → 𝐴 ≤ (𝐵 + 𝑥))) |
15 | 14 | ralrimdva 3114 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴 ≤ 𝐵 → ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥))) |
16 | | rexr 11005 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
17 | 16 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ 𝐵 ∈
ℝ*) |
18 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ 𝐴 ∈
ℝ*) |
19 | | qbtwnxr 12916 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐴 ∈
ℝ* ∧ 𝐵
< 𝐴) → ∃𝑦 ∈ ℚ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴)) |
20 | 19 | 3expia 1119 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝐵 < 𝐴 → ∃𝑦 ∈ ℚ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) |
21 | 17, 18, 20 | syl2anc 583 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐵 < 𝐴 → ∃𝑦 ∈ ℚ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) |
22 | | simprrl 777 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝐵 < 𝑦) |
23 | | simplr 765 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝐵 ∈ ℝ) |
24 | | qre 12675 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℚ → 𝑦 ∈
ℝ) |
25 | 24 | ad2antrl 724 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝑦 ∈ ℝ) |
26 | | difrp 12750 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐵 < 𝑦 ↔ (𝑦 − 𝐵) ∈
ℝ+)) |
27 | 23, 25, 26 | syl2anc 583 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → (𝐵 < 𝑦 ↔ (𝑦 − 𝐵) ∈
ℝ+)) |
28 | 22, 27 | mpbid 231 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → (𝑦 − 𝐵) ∈
ℝ+) |
29 | | simprrr 778 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝑦 < 𝐴) |
30 | 25 | rexrd 11009 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝑦 ∈ ℝ*) |
31 | | simpll 763 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝐴 ∈
ℝ*) |
32 | | xrltnle 11026 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝑦 < 𝐴 ↔ ¬ 𝐴 ≤ 𝑦)) |
33 | 30, 31, 32 | syl2anc 583 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → (𝑦 < 𝐴 ↔ ¬ 𝐴 ≤ 𝑦)) |
34 | 29, 33 | mpbid 231 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → ¬ 𝐴 ≤ 𝑦) |
35 | 23 | recnd 10987 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝐵 ∈ ℂ) |
36 | 25 | recnd 10987 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → 𝑦 ∈ ℂ) |
37 | 35, 36 | pncan3d 11318 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → (𝐵 + (𝑦 − 𝐵)) = 𝑦) |
38 | 37 | breq2d 5090 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → (𝐴 ≤ (𝐵 + (𝑦 − 𝐵)) ↔ 𝐴 ≤ 𝑦)) |
39 | 34, 38 | mtbird 324 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → ¬ 𝐴 ≤ (𝐵 + (𝑦 − 𝐵))) |
40 | | oveq2 7276 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 − 𝐵) → (𝐵 + 𝑥) = (𝐵 + (𝑦 − 𝐵))) |
41 | 40 | breq2d 5090 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 − 𝐵) → (𝐴 ≤ (𝐵 + 𝑥) ↔ 𝐴 ≤ (𝐵 + (𝑦 − 𝐵)))) |
42 | 41 | notbid 317 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 − 𝐵) → (¬ 𝐴 ≤ (𝐵 + 𝑥) ↔ ¬ 𝐴 ≤ (𝐵 + (𝑦 − 𝐵)))) |
43 | 42 | rspcev 3560 |
. . . . . . . 8
⊢ (((𝑦 − 𝐵) ∈ ℝ+ ∧ ¬
𝐴 ≤ (𝐵 + (𝑦 − 𝐵))) → ∃𝑥 ∈ ℝ+ ¬ 𝐴 ≤ (𝐵 + 𝑥)) |
44 | 28, 39, 43 | syl2anc 583 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → ∃𝑥 ∈ ℝ+ ¬ 𝐴 ≤ (𝐵 + 𝑥)) |
45 | | rexnal 3167 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℝ+ ¬ 𝐴
≤ (𝐵 + 𝑥) ↔ ¬ ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥)) |
46 | 44, 45 | sylib 217 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
∧ (𝑦 ∈ ℚ
∧ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴))) → ¬ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + 𝑥)) |
47 | 46 | rexlimdvaa 3215 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (∃𝑦 ∈
ℚ (𝐵 < 𝑦 ∧ 𝑦 < 𝐴) → ¬ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + 𝑥))) |
48 | 21, 47 | syld 47 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐵 < 𝐴 → ¬ ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥))) |
49 | 48 | con2d 134 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (∀𝑥 ∈
ℝ+ 𝐴 ≤
(𝐵 + 𝑥) → ¬ 𝐵 < 𝐴)) |
50 | | xrlenlt 11024 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
51 | 16, 50 | sylan2 592 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
52 | 49, 51 | sylibrd 258 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (∀𝑥 ∈
ℝ+ 𝐴 ≤
(𝐵 + 𝑥) → 𝐴 ≤ 𝐵)) |
53 | 15, 52 | impbid 211 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥))) |