Proof of Theorem xrltnsym
Step | Hyp | Ref
| Expression |
1 | | elxr 9683 |
. 2
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
2 | | elxr 9683 |
. 2
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
3 | | ltnsym 7963 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
4 | | rexr 7923 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
5 | | pnfnlt 9694 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ*
→ ¬ +∞ < 𝐴) |
6 | 4, 5 | syl 14 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ¬
+∞ < 𝐴) |
7 | 6 | adantr 274 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → ¬
+∞ < 𝐴) |
8 | | breq1 3968 |
. . . . . . 7
⊢ (𝐵 = +∞ → (𝐵 < 𝐴 ↔ +∞ < 𝐴)) |
9 | 8 | adantl 275 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 < 𝐴 ↔ +∞ < 𝐴)) |
10 | 7, 9 | mtbird 663 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → ¬ 𝐵 < 𝐴) |
11 | 10 | a1d 22 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
12 | | nltmnf 9695 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ*
→ ¬ 𝐴 <
-∞) |
13 | 4, 12 | syl 14 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ¬
𝐴 <
-∞) |
14 | 13 | adantr 274 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞) |
15 | | breq2 3969 |
. . . . . . 7
⊢ (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 𝐴 < -∞)) |
16 | 15 | adantl 275 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞)) |
17 | 14, 16 | mtbird 663 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵) |
18 | 17 | pm2.21d 609 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
19 | 3, 11, 18 | 3jaodan 1288 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
20 | | pnfnlt 9694 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
→ ¬ +∞ < 𝐵) |
21 | 20 | adantl 275 |
. . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ ¬ +∞ < 𝐵) |
22 | | breq1 3968 |
. . . . . . 7
⊢ (𝐴 = +∞ → (𝐴 < 𝐵 ↔ +∞ < 𝐵)) |
23 | 22 | adantr 274 |
. . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔ +∞ < 𝐵)) |
24 | 21, 23 | mtbird 663 |
. . . . 5
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ ¬ 𝐴 < 𝐵) |
25 | 24 | pm2.21d 609 |
. . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
26 | 2, 25 | sylan2br 286 |
. . 3
⊢ ((𝐴 = +∞ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
27 | | rexr 7923 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
28 | | nltmnf 9695 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ ¬ 𝐵 <
-∞) |
29 | 27, 28 | syl 14 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → ¬
𝐵 <
-∞) |
30 | 29 | adantl 275 |
. . . . . 6
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → ¬
𝐵 <
-∞) |
31 | | breq2 3969 |
. . . . . . 7
⊢ (𝐴 = -∞ → (𝐵 < 𝐴 ↔ 𝐵 < -∞)) |
32 | 31 | adantr 274 |
. . . . . 6
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 < 𝐴 ↔ 𝐵 < -∞)) |
33 | 30, 32 | mtbird 663 |
. . . . 5
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → ¬
𝐵 < 𝐴) |
34 | 33 | a1d 22 |
. . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
35 | | mnfxr 7934 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
36 | | pnfnlt 9694 |
. . . . . . . 8
⊢ (-∞
∈ ℝ* → ¬ +∞ <
-∞) |
37 | 35, 36 | ax-mp 5 |
. . . . . . 7
⊢ ¬
+∞ < -∞ |
38 | | breq12 3970 |
. . . . . . 7
⊢ ((𝐵 = +∞ ∧ 𝐴 = -∞) → (𝐵 < 𝐴 ↔ +∞ <
-∞)) |
39 | 37, 38 | mtbiri 665 |
. . . . . 6
⊢ ((𝐵 = +∞ ∧ 𝐴 = -∞) → ¬ 𝐵 < 𝐴) |
40 | 39 | ancoms 266 |
. . . . 5
⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → ¬ 𝐵 < 𝐴) |
41 | 40 | a1d 22 |
. . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
42 | | xrltnr 9686 |
. . . . . . 7
⊢ (-∞
∈ ℝ* → ¬ -∞ <
-∞) |
43 | 35, 42 | ax-mp 5 |
. . . . . 6
⊢ ¬
-∞ < -∞ |
44 | | breq12 3970 |
. . . . . 6
⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ -∞ <
-∞)) |
45 | 43, 44 | mtbiri 665 |
. . . . 5
⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵) |
46 | 45 | pm2.21d 609 |
. . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
47 | 34, 41, 46 | 3jaodan 1288 |
. . 3
⊢ ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
48 | 19, 26, 47 | 3jaoian 1287 |
. 2
⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
49 | 1, 2, 48 | syl2anb 289 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |