Step | Hyp | Ref
| Expression |
1 | | ltrelnq 6349 |
. . . . 5
⊢
<Q ⊆ (Q ×
Q) |
2 | 1 | brel 4335 |
. . . 4
⊢ (A <Q B → (A
∈ Q ∧ B ∈ Q)) |
3 | 2 | simpld 105 |
. . 3
⊢ (A <Q B → A ∈ Q) |
4 | | ltexnqi 6392 |
. . 3
⊢ (A <Q B → ∃y ∈ Q (A +Q y) = B) |
5 | | nsmallnq 6396 |
. . . . . 6
⊢ (y ∈
Q → ∃z z
<Q y) |
6 | 1 | brel 4335 |
. . . . . . . . . . . . . . 15
⊢ (z <Q y → (z
∈ Q ∧ y ∈ Q)) |
7 | 6 | simpld 105 |
. . . . . . . . . . . . . 14
⊢ (z <Q y → z ∈ Q) |
8 | | ltaddnq 6390 |
. . . . . . . . . . . . . 14
⊢
((A ∈ Q ∧ z ∈ Q) → A <Q (A +Q z)) |
9 | 7, 8 | sylan2 270 |
. . . . . . . . . . . . 13
⊢
((A ∈ Q ∧ z
<Q y) →
A <Q (A +Q z)) |
10 | 9 | ancoms 255 |
. . . . . . . . . . . 12
⊢
((z <Q
y ∧
A ∈
Q) → A
<Q (A
+Q z)) |
11 | 10 | adantr 261 |
. . . . . . . . . . 11
⊢
(((z <Q
y ∧
A ∈
Q) ∧ (A +Q y) = B) →
A <Q (A +Q z)) |
12 | | ltanqi 6386 |
. . . . . . . . . . . . 13
⊢
((z <Q
y ∧
A ∈
Q) → (A
+Q z)
<Q (A
+Q y)) |
13 | 12 | adantr 261 |
. . . . . . . . . . . 12
⊢
(((z <Q
y ∧
A ∈
Q) ∧ (A +Q y) = B) →
(A +Q z) <Q (A +Q y)) |
14 | | breq2 3759 |
. . . . . . . . . . . . 13
⊢
((A +Q
y) = B
→ ((A +Q
z) <Q (A +Q y) ↔ (A
+Q z)
<Q B)) |
15 | 14 | adantl 262 |
. . . . . . . . . . . 12
⊢
(((z <Q
y ∧
A ∈
Q) ∧ (A +Q y) = B) →
((A +Q z) <Q (A +Q y) ↔ (A
+Q z)
<Q B)) |
16 | 13, 15 | mpbid 135 |
. . . . . . . . . . 11
⊢
(((z <Q
y ∧
A ∈
Q) ∧ (A +Q y) = B) →
(A +Q z) <Q B) |
17 | | addclnq 6359 |
. . . . . . . . . . . . . . 15
⊢
((A ∈ Q ∧ z ∈ Q) → (A +Q z) ∈
Q) |
18 | 7, 17 | sylan2 270 |
. . . . . . . . . . . . . 14
⊢
((A ∈ Q ∧ z
<Q y) →
(A +Q z) ∈
Q) |
19 | 18 | ancoms 255 |
. . . . . . . . . . . . 13
⊢
((z <Q
y ∧
A ∈
Q) → (A
+Q z) ∈ Q) |
20 | 19 | adantr 261 |
. . . . . . . . . . . 12
⊢
(((z <Q
y ∧
A ∈
Q) ∧ (A +Q y) = B) →
(A +Q z) ∈
Q) |
21 | | breq2 3759 |
. . . . . . . . . . . . . 14
⊢ (x = (A
+Q z) →
(A <Q x ↔ A
<Q (A
+Q z))) |
22 | | breq1 3758 |
. . . . . . . . . . . . . 14
⊢ (x = (A
+Q z) →
(x <Q B ↔ (A
+Q z)
<Q B)) |
23 | 21, 22 | anbi12d 442 |
. . . . . . . . . . . . 13
⊢ (x = (A
+Q z) →
((A <Q x ∧ x <Q B) ↔ (A
<Q (A
+Q z) ∧ (A
+Q z)
<Q B))) |
24 | 23 | adantl 262 |
. . . . . . . . . . . 12
⊢
((((z <Q
y ∧
A ∈
Q) ∧ (A +Q y) = B) ∧ x = (A +Q z)) → ((A
<Q x ∧ x
<Q B) ↔
(A <Q (A +Q z) ∧ (A +Q z) <Q B))) |
25 | 20, 24 | rspcedv 2654 |
. . . . . . . . . . 11
⊢
(((z <Q
y ∧
A ∈
Q) ∧ (A +Q y) = B) →
((A <Q
(A +Q z) ∧ (A +Q z) <Q B) → ∃x ∈ Q (A <Q x ∧ x <Q B))) |
26 | 11, 16, 25 | mp2and 409 |
. . . . . . . . . 10
⊢
(((z <Q
y ∧
A ∈
Q) ∧ (A +Q y) = B) →
∃x ∈ Q (A <Q x ∧ x <Q B)) |
27 | 26 | 3impa 1098 |
. . . . . . . . 9
⊢
((z <Q
y ∧
A ∈
Q ∧ (A +Q y) = B) →
∃x ∈ Q (A <Q x ∧ x <Q B)) |
28 | 27 | 3coml 1110 |
. . . . . . . 8
⊢
((A ∈ Q ∧ (A
+Q y) = B ∧ z <Q y) → ∃x ∈ Q (A <Q x ∧ x <Q B)) |
29 | 28 | 3expia 1105 |
. . . . . . 7
⊢
((A ∈ Q ∧ (A
+Q y) = B) → (z
<Q y →
∃x ∈ Q (A <Q x ∧ x <Q B))) |
30 | 29 | exlimdv 1697 |
. . . . . 6
⊢
((A ∈ Q ∧ (A
+Q y) = B) → (∃z z <Q y → ∃x ∈ Q (A <Q x ∧ x <Q B))) |
31 | 5, 30 | syl5 28 |
. . . . 5
⊢
((A ∈ Q ∧ (A
+Q y) = B) → (y
∈ Q → ∃x ∈ Q (A <Q x ∧ x <Q B))) |
32 | 31 | impancom 247 |
. . . 4
⊢
((A ∈ Q ∧ y ∈ Q) → ((A +Q y) = B →
∃x ∈ Q (A <Q x ∧ x <Q B))) |
33 | 32 | rexlimdva 2427 |
. . 3
⊢ (A ∈
Q → (∃y ∈
Q (A
+Q y) = B → ∃x ∈ Q (A <Q x ∧ x <Q B))) |
34 | 3, 4, 33 | sylc 56 |
. 2
⊢ (A <Q B → ∃x ∈ Q (A <Q x ∧ x <Q B)) |
35 | | ltsonq 6382 |
. . . 4
⊢
<Q Or Q |
36 | 35, 1 | sotri 4663 |
. . 3
⊢
((A <Q
x ∧
x <Q B) → A
<Q B) |
37 | 36 | rexlimivw 2423 |
. 2
⊢ (∃x ∈ Q (A <Q x ∧ x <Q B) → A
<Q B) |
38 | 34, 37 | impbii 117 |
1
⊢ (A <Q B ↔ ∃x ∈ Q (A <Q x ∧ x <Q B)) |