Step | Hyp | Ref
| Expression |
1 | | ltrelnq 6555 |
. . . . 5
⊢
<Q ⊆ (Q ×
Q) |
2 | 1 | brel 4410 |
. . . 4
⊢ (𝐴 <Q
𝐵 → (𝐴 ∈ Q ∧ 𝐵 ∈
Q)) |
3 | 2 | simpld 110 |
. . 3
⊢ (𝐴 <Q
𝐵 → 𝐴 ∈ Q) |
4 | | ltexnqi 6599 |
. . 3
⊢ (𝐴 <Q
𝐵 → ∃𝑦 ∈ Q (𝐴 +Q
𝑦) = 𝐵) |
5 | | nsmallnq 6603 |
. . . . . 6
⊢ (𝑦 ∈ Q →
∃𝑧 𝑧 <Q 𝑦) |
6 | 1 | brel 4410 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 <Q
𝑦 → (𝑧 ∈ Q ∧
𝑦 ∈
Q)) |
7 | 6 | simpld 110 |
. . . . . . . . . . . . . 14
⊢ (𝑧 <Q
𝑦 → 𝑧 ∈ Q) |
8 | | ltaddnq 6597 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Q ∧
𝑧 ∈ Q)
→ 𝐴
<Q (𝐴 +Q 𝑧)) |
9 | 7, 8 | sylan2 280 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Q ∧
𝑧
<Q 𝑦) → 𝐴 <Q (𝐴 +Q
𝑧)) |
10 | 9 | ancoms 264 |
. . . . . . . . . . . 12
⊢ ((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) → 𝐴 <Q
(𝐴
+Q 𝑧)) |
11 | 10 | adantr 270 |
. . . . . . . . . . 11
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → 𝐴 <Q (𝐴 +Q
𝑧)) |
12 | | ltanqi 6592 |
. . . . . . . . . . . . 13
⊢ ((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) → (𝐴 +Q
𝑧)
<Q (𝐴 +Q 𝑦)) |
13 | 12 | adantr 270 |
. . . . . . . . . . . 12
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → (𝐴 +Q 𝑧) <Q
(𝐴
+Q 𝑦)) |
14 | | breq2 3789 |
. . . . . . . . . . . . 13
⊢ ((𝐴 +Q
𝑦) = 𝐵 → ((𝐴 +Q 𝑧) <Q
(𝐴
+Q 𝑦) ↔ (𝐴 +Q 𝑧) <Q
𝐵)) |
15 | 14 | adantl 271 |
. . . . . . . . . . . 12
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → ((𝐴 +Q 𝑧) <Q
(𝐴
+Q 𝑦) ↔ (𝐴 +Q 𝑧) <Q
𝐵)) |
16 | 13, 15 | mpbid 145 |
. . . . . . . . . . 11
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → (𝐴 +Q 𝑧) <Q
𝐵) |
17 | | addclnq 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Q ∧
𝑧 ∈ Q)
→ (𝐴
+Q 𝑧) ∈ Q) |
18 | 7, 17 | sylan2 280 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Q ∧
𝑧
<Q 𝑦) → (𝐴 +Q 𝑧) ∈
Q) |
19 | 18 | ancoms 264 |
. . . . . . . . . . . . 13
⊢ ((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) → (𝐴 +Q
𝑧) ∈
Q) |
20 | 19 | adantr 270 |
. . . . . . . . . . . 12
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → (𝐴 +Q 𝑧) ∈
Q) |
21 | | breq2 3789 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐴 +Q 𝑧) → (𝐴 <Q 𝑥 ↔ 𝐴 <Q (𝐴 +Q
𝑧))) |
22 | | breq1 3788 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐴 +Q 𝑧) → (𝑥 <Q 𝐵 ↔ (𝐴 +Q 𝑧) <Q
𝐵)) |
23 | 21, 22 | anbi12d 456 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐴 +Q 𝑧) → ((𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵) ↔ (𝐴 <Q (𝐴 +Q
𝑧) ∧ (𝐴 +Q 𝑧) <Q
𝐵))) |
24 | 23 | adantl 271 |
. . . . . . . . . . . 12
⊢ ((((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) ∧ 𝑥 = (𝐴 +Q 𝑧)) → ((𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵) ↔ (𝐴 <Q (𝐴 +Q
𝑧) ∧ (𝐴 +Q 𝑧) <Q
𝐵))) |
25 | 20, 24 | rspcedv 2705 |
. . . . . . . . . . 11
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → ((𝐴 <Q (𝐴 +Q
𝑧) ∧ (𝐴 +Q 𝑧) <Q
𝐵) → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵))) |
26 | 11, 16, 25 | mp2and 423 |
. . . . . . . . . 10
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → ∃𝑥 ∈ Q (𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵)) |
27 | 26 | 3impa 1133 |
. . . . . . . . 9
⊢ ((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q ∧ (𝐴 +Q
𝑦) = 𝐵) → ∃𝑥 ∈ Q (𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵)) |
28 | 27 | 3coml 1145 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
(𝐴
+Q 𝑦) = 𝐵 ∧ 𝑧 <Q 𝑦) → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵)) |
29 | 28 | 3expia 1140 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
(𝐴
+Q 𝑦) = 𝐵) → (𝑧 <Q 𝑦 → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵))) |
30 | 29 | exlimdv 1740 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
(𝐴
+Q 𝑦) = 𝐵) → (∃𝑧 𝑧 <Q 𝑦 → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵))) |
31 | 5, 30 | syl5 32 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
(𝐴
+Q 𝑦) = 𝐵) → (𝑦 ∈ Q → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵))) |
32 | 31 | impancom 256 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝑦 ∈ Q)
→ ((𝐴
+Q 𝑦) = 𝐵 → ∃𝑥 ∈ Q (𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵))) |
33 | 32 | rexlimdva 2477 |
. . 3
⊢ (𝐴 ∈ Q →
(∃𝑦 ∈
Q (𝐴
+Q 𝑦) = 𝐵 → ∃𝑥 ∈ Q (𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵))) |
34 | 3, 4, 33 | sylc 61 |
. 2
⊢ (𝐴 <Q
𝐵 → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵)) |
35 | | ltsonq 6588 |
. . . 4
⊢
<Q Or Q |
36 | 35, 1 | sotri 4740 |
. . 3
⊢ ((𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵) → 𝐴 <Q 𝐵) |
37 | 36 | rexlimivw 2473 |
. 2
⊢
(∃𝑥 ∈
Q (𝐴
<Q 𝑥 ∧ 𝑥 <Q 𝐵) → 𝐴 <Q 𝐵) |
38 | 34, 37 | impbii 124 |
1
⊢ (𝐴 <Q
𝐵 ↔ ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵)) |