Step | Hyp | Ref
| Expression |
1 | | halfnqq 7330 |
. . . . . 6
⊢ (𝐴 ∈ Q →
∃𝑦 ∈
Q (𝑦
+Q 𝑦) = 𝐴) |
2 | | df-rex 2441 |
. . . . . . 7
⊢
(∃𝑦 ∈
Q (𝑦
+Q 𝑦) = 𝐴 ↔ ∃𝑦(𝑦 ∈ Q ∧ (𝑦 +Q
𝑦) = 𝐴)) |
3 | | halfnqq 7330 |
. . . . . . . . . 10
⊢ (𝑦 ∈ Q →
∃𝑥 ∈
Q (𝑥
+Q 𝑥) = 𝑦) |
4 | 3 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) → ∃𝑥 ∈ Q (𝑥 +Q 𝑥) = 𝑦) |
5 | 4 | ancli 321 |
. . . . . . . 8
⊢ ((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) → ((𝑦 ∈ Q ∧ (𝑦 +Q
𝑦) = 𝐴) ∧ ∃𝑥 ∈ Q (𝑥 +Q 𝑥) = 𝑦)) |
6 | 5 | eximi 1580 |
. . . . . . 7
⊢
(∃𝑦(𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) → ∃𝑦((𝑦 ∈ Q ∧ (𝑦 +Q
𝑦) = 𝐴) ∧ ∃𝑥 ∈ Q (𝑥 +Q 𝑥) = 𝑦)) |
7 | 2, 6 | sylbi 120 |
. . . . . 6
⊢
(∃𝑦 ∈
Q (𝑦
+Q 𝑦) = 𝐴 → ∃𝑦((𝑦 ∈ Q ∧ (𝑦 +Q
𝑦) = 𝐴) ∧ ∃𝑥 ∈ Q (𝑥 +Q 𝑥) = 𝑦)) |
8 | 1, 7 | syl 14 |
. . . . 5
⊢ (𝐴 ∈ Q →
∃𝑦((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ ∃𝑥 ∈ Q (𝑥 +Q 𝑥) = 𝑦)) |
9 | | df-rex 2441 |
. . . . . . 7
⊢
(∃𝑥 ∈
Q (𝑥
+Q 𝑥) = 𝑦 ↔ ∃𝑥(𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) |
10 | 9 | anbi2i 453 |
. . . . . 6
⊢ (((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ ∃𝑥 ∈ Q (𝑥 +Q 𝑥) = 𝑦) ↔ ((𝑦 ∈ Q ∧ (𝑦 +Q
𝑦) = 𝐴) ∧ ∃𝑥(𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦))) |
11 | 10 | exbii 1585 |
. . . . 5
⊢
(∃𝑦((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ ∃𝑥 ∈ Q (𝑥 +Q 𝑥) = 𝑦) ↔ ∃𝑦((𝑦 ∈ Q ∧ (𝑦 +Q
𝑦) = 𝐴) ∧ ∃𝑥(𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦))) |
12 | 8, 11 | sylib 121 |
. . . 4
⊢ (𝐴 ∈ Q →
∃𝑦((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ ∃𝑥(𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦))) |
13 | | exdistr 1889 |
. . . 4
⊢
(∃𝑦∃𝑥((𝑦 ∈ Q ∧ (𝑦 +Q
𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) ↔ ∃𝑦((𝑦 ∈ Q ∧ (𝑦 +Q
𝑦) = 𝐴) ∧ ∃𝑥(𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦))) |
14 | 12, 13 | sylibr 133 |
. . 3
⊢ (𝐴 ∈ Q →
∃𝑦∃𝑥((𝑦 ∈ Q ∧ (𝑦 +Q
𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦))) |
15 | | simprl 521 |
. . . . . 6
⊢ (((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) → 𝑥 ∈ Q) |
16 | | simpll 519 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) → 𝑦 ∈ Q) |
17 | | ltaddnq 7327 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Q ∧
𝑦 ∈ Q)
→ 𝑦
<Q (𝑦 +Q 𝑦)) |
18 | 16, 16, 17 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) → 𝑦 <Q (𝑦 +Q
𝑦)) |
19 | | breq2 3969 |
. . . . . . . . 9
⊢ ((𝑦 +Q
𝑦) = 𝐴 → (𝑦 <Q (𝑦 +Q
𝑦) ↔ 𝑦 <Q
𝐴)) |
20 | 19 | ad2antlr 481 |
. . . . . . . 8
⊢ (((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) → (𝑦 <Q (𝑦 +Q
𝑦) ↔ 𝑦 <Q
𝐴)) |
21 | 18, 20 | mpbid 146 |
. . . . . . 7
⊢ (((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) → 𝑦 <Q 𝐴) |
22 | | breq1 3968 |
. . . . . . . 8
⊢ ((𝑥 +Q
𝑥) = 𝑦 → ((𝑥 +Q 𝑥) <Q
𝐴 ↔ 𝑦 <Q 𝐴)) |
23 | 22 | ad2antll 483 |
. . . . . . 7
⊢ (((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) → ((𝑥 +Q 𝑥) <Q
𝐴 ↔ 𝑦 <Q 𝐴)) |
24 | 21, 23 | mpbird 166 |
. . . . . 6
⊢ (((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) → (𝑥 +Q 𝑥) <Q
𝐴) |
25 | 15, 24 | jca 304 |
. . . . 5
⊢ (((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) → (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝐴)) |
26 | 25 | eximi 1580 |
. . . 4
⊢
(∃𝑥((𝑦 ∈ Q ∧
(𝑦
+Q 𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) → ∃𝑥(𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝐴)) |
27 | 26 | exlimiv 1578 |
. . 3
⊢
(∃𝑦∃𝑥((𝑦 ∈ Q ∧ (𝑦 +Q
𝑦) = 𝐴) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑦)) → ∃𝑥(𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝐴)) |
28 | 14, 27 | syl 14 |
. 2
⊢ (𝐴 ∈ Q →
∃𝑥(𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝐴)) |
29 | | df-rex 2441 |
. 2
⊢
(∃𝑥 ∈
Q (𝑥
+Q 𝑥) <Q 𝐴 ↔ ∃𝑥(𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝐴)) |
30 | 28, 29 | sylibr 133 |
1
⊢ (𝐴 ∈ Q →
∃𝑥 ∈
Q (𝑥
+Q 𝑥) <Q 𝐴) |