Step | Hyp | Ref
| Expression |
1 | | ltrelnq 7285 |
. . . . 5
⊢
<Q ⊆ (Q ×
Q) |
2 | 1 | brel 4638 |
. . . 4
⊢ (𝐴 <Q
𝐵 → (𝐴 ∈ Q ∧ 𝐵 ∈
Q)) |
3 | 2 | simpld 111 |
. . 3
⊢ (𝐴 <Q
𝐵 → 𝐴 ∈ Q) |
4 | | ltexnqi 7329 |
. . 3
⊢ (𝐴 <Q
𝐵 → ∃𝑦 ∈ Q (𝐴 +Q
𝑦) = 𝐵) |
5 | | nsmallnq 7333 |
. . . . . 6
⊢ (𝑦 ∈ Q →
∃𝑧 𝑧 <Q 𝑦) |
6 | 1 | brel 4638 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 <Q
𝑦 → (𝑧 ∈ Q ∧
𝑦 ∈
Q)) |
7 | 6 | simpld 111 |
. . . . . . . . . . . . . 14
⊢ (𝑧 <Q
𝑦 → 𝑧 ∈ Q) |
8 | | ltaddnq 7327 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Q ∧
𝑧 ∈ Q)
→ 𝐴
<Q (𝐴 +Q 𝑧)) |
9 | 7, 8 | sylan2 284 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Q ∧
𝑧
<Q 𝑦) → 𝐴 <Q (𝐴 +Q
𝑧)) |
10 | 9 | ancoms 266 |
. . . . . . . . . . . 12
⊢ ((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) → 𝐴 <Q
(𝐴
+Q 𝑧)) |
11 | 10 | adantr 274 |
. . . . . . . . . . 11
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → 𝐴 <Q (𝐴 +Q
𝑧)) |
12 | | ltanqi 7322 |
. . . . . . . . . . . . 13
⊢ ((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) → (𝐴 +Q
𝑧)
<Q (𝐴 +Q 𝑦)) |
13 | 12 | adantr 274 |
. . . . . . . . . . . 12
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → (𝐴 +Q 𝑧) <Q
(𝐴
+Q 𝑦)) |
14 | | breq2 3969 |
. . . . . . . . . . . . 13
⊢ ((𝐴 +Q
𝑦) = 𝐵 → ((𝐴 +Q 𝑧) <Q
(𝐴
+Q 𝑦) ↔ (𝐴 +Q 𝑧) <Q
𝐵)) |
15 | 14 | adantl 275 |
. . . . . . . . . . . 12
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → ((𝐴 +Q 𝑧) <Q
(𝐴
+Q 𝑦) ↔ (𝐴 +Q 𝑧) <Q
𝐵)) |
16 | 13, 15 | mpbid 146 |
. . . . . . . . . . 11
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → (𝐴 +Q 𝑧) <Q
𝐵) |
17 | | addclnq 7295 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Q ∧
𝑧 ∈ Q)
→ (𝐴
+Q 𝑧) ∈ Q) |
18 | 7, 17 | sylan2 284 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Q ∧
𝑧
<Q 𝑦) → (𝐴 +Q 𝑧) ∈
Q) |
19 | 18 | ancoms 266 |
. . . . . . . . . . . . 13
⊢ ((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) → (𝐴 +Q
𝑧) ∈
Q) |
20 | 19 | adantr 274 |
. . . . . . . . . . . 12
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → (𝐴 +Q 𝑧) ∈
Q) |
21 | | breq2 3969 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐴 +Q 𝑧) → (𝐴 <Q 𝑥 ↔ 𝐴 <Q (𝐴 +Q
𝑧))) |
22 | | breq1 3968 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐴 +Q 𝑧) → (𝑥 <Q 𝐵 ↔ (𝐴 +Q 𝑧) <Q
𝐵)) |
23 | 21, 22 | anbi12d 465 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐴 +Q 𝑧) → ((𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵) ↔ (𝐴 <Q (𝐴 +Q
𝑧) ∧ (𝐴 +Q 𝑧) <Q
𝐵))) |
24 | 23 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) ∧ 𝑥 = (𝐴 +Q 𝑧)) → ((𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵) ↔ (𝐴 <Q (𝐴 +Q
𝑧) ∧ (𝐴 +Q 𝑧) <Q
𝐵))) |
25 | 20, 24 | rspcedv 2820 |
. . . . . . . . . . 11
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → ((𝐴 <Q (𝐴 +Q
𝑧) ∧ (𝐴 +Q 𝑧) <Q
𝐵) → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵))) |
26 | 11, 16, 25 | mp2and 430 |
. . . . . . . . . 10
⊢ (((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q) ∧ (𝐴 +Q
𝑦) = 𝐵) → ∃𝑥 ∈ Q (𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵)) |
27 | 26 | 3impa 1177 |
. . . . . . . . 9
⊢ ((𝑧 <Q
𝑦 ∧ 𝐴 ∈ Q ∧ (𝐴 +Q
𝑦) = 𝐵) → ∃𝑥 ∈ Q (𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵)) |
28 | 27 | 3coml 1192 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
(𝐴
+Q 𝑦) = 𝐵 ∧ 𝑧 <Q 𝑦) → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵)) |
29 | 28 | 3expia 1187 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
(𝐴
+Q 𝑦) = 𝐵) → (𝑧 <Q 𝑦 → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵))) |
30 | 29 | exlimdv 1799 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
(𝐴
+Q 𝑦) = 𝐵) → (∃𝑧 𝑧 <Q 𝑦 → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵))) |
31 | 5, 30 | syl5 32 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
(𝐴
+Q 𝑦) = 𝐵) → (𝑦 ∈ Q → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵))) |
32 | 31 | impancom 258 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝑦 ∈ Q)
→ ((𝐴
+Q 𝑦) = 𝐵 → ∃𝑥 ∈ Q (𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵))) |
33 | 32 | rexlimdva 2574 |
. . 3
⊢ (𝐴 ∈ Q →
(∃𝑦 ∈
Q (𝐴
+Q 𝑦) = 𝐵 → ∃𝑥 ∈ Q (𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵))) |
34 | 3, 4, 33 | sylc 62 |
. 2
⊢ (𝐴 <Q
𝐵 → ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵)) |
35 | | ltsonq 7318 |
. . . 4
⊢
<Q Or Q |
36 | 35, 1 | sotri 4981 |
. . 3
⊢ ((𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵) → 𝐴 <Q 𝐵) |
37 | 36 | rexlimivw 2570 |
. 2
⊢
(∃𝑥 ∈
Q (𝐴
<Q 𝑥 ∧ 𝑥 <Q 𝐵) → 𝐴 <Q 𝐵) |
38 | 34, 37 | impbii 125 |
1
⊢ (𝐴 <Q
𝐵 ↔ ∃𝑥 ∈ Q (𝐴 <Q
𝑥 ∧ 𝑥 <Q 𝐵)) |