Proof of Theorem xqltnle
Step | Hyp | Ref
| Expression |
1 | | qltnle 10313 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
2 | 1 | adantll 476 |
. . 3
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 ∈ ℚ) →
(𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
3 | | simplr 528 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → 𝐴 ∈
ℚ) |
4 | | qre 9690 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
5 | 3, 4 | syl 14 |
. . . . . 6
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → 𝐴 ∈
ℝ) |
6 | 5 | ltpnfd 9847 |
. . . . 5
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → 𝐴 < +∞) |
7 | | simpr 110 |
. . . . 5
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → 𝐵 = +∞) |
8 | 6, 7 | breqtrrd 4057 |
. . . 4
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → 𝐴 < 𝐵) |
9 | 5 | renepnfd 8070 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → 𝐴 ≠ +∞) |
10 | 9 | neneqd 2385 |
. . . . . 6
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → ¬
𝐴 =
+∞) |
11 | 5 | rexrd 8069 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → 𝐴 ∈
ℝ*) |
12 | | xgepnf 9882 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (+∞ ≤ 𝐴
↔ 𝐴 =
+∞)) |
13 | 11, 12 | syl 14 |
. . . . . 6
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) →
(+∞ ≤ 𝐴 ↔
𝐴 =
+∞)) |
14 | 10, 13 | mtbird 674 |
. . . . 5
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → ¬
+∞ ≤ 𝐴) |
15 | 7, 14 | eqnbrtrd 4047 |
. . . 4
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → ¬
𝐵 ≤ 𝐴) |
16 | 8, 15 | 2thd 175 |
. . 3
⊢
(((((𝐴 ∈
ℚ ∨ 𝐴 = +∞)
∧ (𝐵 ∈ ℚ
∨ 𝐵 = +∞)) ∧
𝐴 ∈ ℚ) ∧
𝐵 = +∞) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
17 | | simplr 528 |
. . 3
⊢ ((((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) ∧ 𝐴 ∈ ℚ) → (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) |
18 | 2, 16, 17 | mpjaodan 799 |
. 2
⊢ ((((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) ∧ 𝐴 ∈ ℚ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
19 | | simpr 110 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
20 | | qre 9690 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℝ) |
21 | 20 | rexrd 8069 |
. . . . . . . 8
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℝ*) |
22 | | pnfxr 8072 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
23 | | eleq1 2256 |
. . . . . . . . 9
⊢ (𝐵 = +∞ → (𝐵 ∈ ℝ*
↔ +∞ ∈ ℝ*)) |
24 | 22, 23 | mpbiri 168 |
. . . . . . . 8
⊢ (𝐵 = +∞ → 𝐵 ∈
ℝ*) |
25 | 21, 24 | jaoi 717 |
. . . . . . 7
⊢ ((𝐵 ∈ ℚ ∨ 𝐵 = +∞) → 𝐵 ∈
ℝ*) |
26 | 25 | adantl 277 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) → 𝐵 ∈
ℝ*) |
27 | | pnfnlt 9853 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ ¬ +∞ < 𝐵) |
28 | 26, 27 | syl 14 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) → ¬
+∞ < 𝐵) |
29 | 28 | adantr 276 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) ∧ 𝐴 = +∞) → ¬
+∞ < 𝐵) |
30 | 19, 29 | eqnbrtrd 4047 |
. . 3
⊢ ((((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) ∧ 𝐴 = +∞) → ¬ 𝐴 < 𝐵) |
31 | | pnfge 9855 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) |
32 | 26, 31 | syl 14 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) → 𝐵 ≤ +∞) |
33 | 32 | adantr 276 |
. . . . 5
⊢ ((((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) ∧ 𝐴 = +∞) → 𝐵 ≤ +∞) |
34 | 33, 19 | breqtrrd 4057 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) ∧ 𝐴 = +∞) → 𝐵 ≤ 𝐴) |
35 | 34 | notnotd 631 |
. . 3
⊢ ((((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) ∧ 𝐴 = +∞) → ¬ ¬
𝐵 ≤ 𝐴) |
36 | 30, 35 | 2falsed 703 |
. 2
⊢ ((((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) ∧ 𝐴 = +∞) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
37 | | simpl 109 |
. 2
⊢ (((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) → (𝐴 ∈ ℚ ∨ 𝐴 = +∞)) |
38 | 18, 36, 37 | mpjaodan 799 |
1
⊢ (((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |