Proof of Theorem xrlexaddrp
Step | Hyp | Ref
| Expression |
1 | | xrlexaddrp.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
2 | | pnfge 12866 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ 𝐴 ≤
+∞) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ≤ +∞) |
4 | 3 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = +∞) → 𝐴 ≤ +∞) |
5 | | id 22 |
. . . . 5
⊢ (𝐵 = +∞ → 𝐵 = +∞) |
6 | 5 | eqcomd 2744 |
. . . 4
⊢ (𝐵 = +∞ → +∞ =
𝐵) |
7 | 6 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = +∞) → +∞ = 𝐵) |
8 | 4, 7 | breqtrd 5100 |
. 2
⊢ ((𝜑 ∧ 𝐵 = +∞) → 𝐴 ≤ 𝐵) |
9 | | simpl 483 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → 𝜑) |
10 | | neqne 2951 |
. . . 4
⊢ (¬
𝐵 = +∞ → 𝐵 ≠ +∞) |
11 | 10 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → 𝐵 ≠ +∞) |
12 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 = -∞) → 𝐴 = -∞) |
13 | | xrlexaddrp.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
14 | | mnfle 12870 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ -∞ ≤ 𝐵) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → -∞ ≤ 𝐵) |
16 | 15 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 = -∞) → -∞ ≤ 𝐵) |
17 | 12, 16 | eqbrtrd 5096 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = -∞) → 𝐴 ≤ 𝐵) |
18 | 17 | adantlr 712 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 = -∞) → 𝐴 ≤ 𝐵) |
19 | | simpl 483 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐴 = -∞) → (𝜑 ∧ 𝐵 ≠ +∞)) |
20 | | neqne 2951 |
. . . . . 6
⊢ (¬
𝐴 = -∞ → 𝐴 ≠ -∞) |
21 | 20 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ≠ -∞) |
22 | | simpll 764 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) → 𝜑) |
23 | 13 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → 𝐵 ∈
ℝ*) |
24 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → 𝐵 ≠ +∞) |
25 | 23, 24 | jca 512 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → (𝐵 ∈ ℝ* ∧ 𝐵 ≠
+∞)) |
26 | | xrnepnf 12854 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
↔ (𝐵 ∈ ℝ
∨ 𝐵 =
-∞)) |
27 | 25, 26 | sylib 217 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → (𝐵 ∈ ℝ ∨ 𝐵 = -∞)) |
28 | 27 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐵 ∈ ℝ) → (𝐵 ∈ ℝ ∨ 𝐵 = -∞)) |
29 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐵 ∈ ℝ) → ¬
𝐵 ∈
ℝ) |
30 | | pm2.53 848 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∨ 𝐵 = -∞) → (¬ 𝐵 ∈ ℝ → 𝐵 = -∞)) |
31 | 28, 29, 30 | sylc 65 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐵 ∈ ℝ) → 𝐵 = -∞) |
32 | 31 | adantlr 712 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) ∧ ¬ 𝐵 ∈ ℝ) → 𝐵 = -∞) |
33 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝜑) |
34 | | 1rp 12734 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ |
35 | 34 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℝ+) |
36 | | 1re 10975 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
37 | 36 | elexi 3451 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
V |
38 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → (𝑥 ∈ ℝ+ ↔ 1 ∈
ℝ+)) |
39 | 38 | anbi2d 629 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ∈ ℝ+) ↔ (𝜑 ∧ 1 ∈
ℝ+))) |
40 | | oveq2 7283 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → (𝐵 +𝑒 𝑥) = (𝐵 +𝑒 1)) |
41 | 40 | breq2d 5086 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 1 → (𝐴 ≤ (𝐵 +𝑒 𝑥) ↔ 𝐴 ≤ (𝐵 +𝑒 1))) |
42 | 39, 41 | imbi12d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 +𝑒 𝑥)) ↔ ((𝜑 ∧ 1 ∈ ℝ+) →
𝐴 ≤ (𝐵 +𝑒
1)))) |
43 | | xrlexaddrp.3 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 +𝑒 𝑥)) |
44 | 37, 42, 43 | vtocl 3498 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 1 ∈
ℝ+) → 𝐴 ≤ (𝐵 +𝑒 1)) |
45 | 33, 35, 44 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ (𝐵 +𝑒 1)) |
46 | 45 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → 𝐴 ≤ (𝐵 +𝑒 1)) |
47 | | oveq1 7282 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 = -∞ → (𝐵 +𝑒 1) =
(-∞ +𝑒 1)) |
48 | | 1xr 11034 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ* |
49 | | ltpnf 12856 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
ℝ → 1 < +∞) |
50 | 36, 49 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 <
+∞ |
51 | 36, 50 | ltneii 11088 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ≠
+∞ |
52 | | xaddmnf2 12963 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ* ∧ 1 ≠ +∞) → (-∞
+𝑒 1) = -∞) |
53 | 48, 51, 52 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢ (-∞
+𝑒 1) = -∞ |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 = -∞ → (-∞
+𝑒 1) = -∞) |
55 | 47, 54 | eqtr2d 2779 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = -∞ → -∞ =
(𝐵 +𝑒
1)) |
56 | 55 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → -∞ = (𝐵 +𝑒
1)) |
57 | 56 | eqcomd 2744 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → (𝐵 +𝑒 1) =
-∞) |
58 | 1 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 ≠ -∞) → 𝐴 ∈
ℝ*) |
59 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 ≠ -∞) → 𝐴 ≠ -∞) |
60 | | nemnftgtmnft 42883 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
→ -∞ < 𝐴) |
61 | 58, 59, 60 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ≠ -∞) → -∞ < 𝐴) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → -∞ < 𝐴) |
63 | 57, 62 | eqbrtrd 5096 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → (𝐵 +𝑒 1) < 𝐴) |
64 | 13 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → 𝐵 ∈
ℝ*) |
65 | 48 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → 1 ∈
ℝ*) |
66 | 64, 65 | xaddcld 13035 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → (𝐵 +𝑒 1) ∈
ℝ*) |
67 | 1 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → 𝐴 ∈
ℝ*) |
68 | | xrltnle 11042 |
. . . . . . . . . . . . 13
⊢ (((𝐵 +𝑒 1) ∈
ℝ* ∧ 𝐴
∈ ℝ*) → ((𝐵 +𝑒 1) < 𝐴 ↔ ¬ 𝐴 ≤ (𝐵 +𝑒 1))) |
69 | 66, 67, 68 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → ((𝐵 +𝑒 1) < 𝐴 ↔ ¬ 𝐴 ≤ (𝐵 +𝑒 1))) |
70 | 63, 69 | mpbid 231 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ -∞) ∧ 𝐵 = -∞) → ¬ 𝐴 ≤ (𝐵 +𝑒 1)) |
71 | 46, 70 | pm2.65da 814 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ -∞) → ¬ 𝐵 = -∞) |
72 | 71 | neqned 2950 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ -∞) → 𝐵 ≠ -∞) |
73 | 72 | ad4ant13 748 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) ∧ ¬ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞) |
74 | 73 | neneqd 2948 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) ∧ ¬ 𝐵 ∈ ℝ) → ¬
𝐵 =
-∞) |
75 | 32, 74 | condan 815 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) → 𝐵 ∈ ℝ) |
76 | 43 | adantlr 712 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 +𝑒 𝑥)) |
77 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
78 | | rpre 12738 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
79 | 78 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ+)
→ 𝑥 ∈
ℝ) |
80 | | rexadd 12966 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐵 +𝑒 𝑥) = (𝐵 + 𝑥)) |
81 | 77, 79, 80 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ+)
→ (𝐵
+𝑒 𝑥) =
(𝐵 + 𝑥)) |
82 | 81 | adantll 711 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → (𝐵 +𝑒 𝑥) = (𝐵 + 𝑥)) |
83 | 76, 82 | breqtrd 5100 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 + 𝑥)) |
84 | 83 | ralrimiva 3103 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥)) |
85 | 1 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → 𝐴 ∈
ℝ*) |
86 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ) |
87 | | xralrple 12939 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+
𝐴 ≤ (𝐵 + 𝑥))) |
88 | 85, 86, 87 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + 𝑥))) |
89 | 84, 88 | mpbird 256 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ 𝐵) |
90 | 22, 75, 89 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐴 ≠ -∞) → 𝐴 ≤ 𝐵) |
91 | 19, 21, 90 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ≤ 𝐵) |
92 | 18, 91 | pm2.61dan 810 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → 𝐴 ≤ 𝐵) |
93 | 9, 11, 92 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → 𝐴 ≤ 𝐵) |
94 | 8, 93 | pm2.61dan 810 |
1
⊢ (𝜑 → 𝐴 ≤ 𝐵) |