Step | Hyp | Ref
| Expression |
1 | | prml 7397 |
. . . . . . 7
⊢
(〈𝐿, 𝑈〉 ∈ P
→ ∃𝑥 ∈
Q 𝑥 ∈
𝐿) |
2 | | df-rex 2441 |
. . . . . . 7
⊢
(∃𝑥 ∈
Q 𝑥 ∈
𝐿 ↔ ∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿)) |
3 | 1, 2 | sylib 121 |
. . . . . 6
⊢
(〈𝐿, 𝑈〉 ∈ P
→ ∃𝑥(𝑥 ∈ Q ∧
𝑥 ∈ 𝐿)) |
4 | 3 | adantr 274 |
. . . . 5
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑃 ∈
Q) → ∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿)) |
5 | | prmu 7398 |
. . . . . . 7
⊢
(〈𝐿, 𝑈〉 ∈ P
→ ∃𝑦 ∈
Q 𝑦 ∈
𝑈) |
6 | | df-rex 2441 |
. . . . . . 7
⊢
(∃𝑦 ∈
Q 𝑦 ∈
𝑈 ↔ ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈)) |
7 | 5, 6 | sylib 121 |
. . . . . 6
⊢
(〈𝐿, 𝑈〉 ∈ P
→ ∃𝑦(𝑦 ∈ Q ∧
𝑦 ∈ 𝑈)) |
8 | 7 | adantr 274 |
. . . . 5
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑃 ∈
Q) → ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈)) |
9 | | subhalfnqq 7334 |
. . . . . . . . 9
⊢ (𝑃 ∈ Q →
∃𝑞 ∈
Q (𝑞
+Q 𝑞) <Q 𝑃) |
10 | 9 | adantl 275 |
. . . . . . . 8
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑃 ∈
Q) → ∃𝑞 ∈ Q (𝑞 +Q 𝑞) <Q
𝑃) |
11 | | df-rex 2441 |
. . . . . . . 8
⊢
(∃𝑞 ∈
Q (𝑞
+Q 𝑞) <Q 𝑃 ↔ ∃𝑞(𝑞 ∈ Q ∧ (𝑞 +Q
𝑞)
<Q 𝑃)) |
12 | 10, 11 | sylib 121 |
. . . . . . 7
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑃 ∈
Q) → ∃𝑞(𝑞 ∈ Q ∧ (𝑞 +Q
𝑞)
<Q 𝑃)) |
13 | 12 | ancli 321 |
. . . . . 6
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑃 ∈
Q) → ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
∃𝑞(𝑞 ∈ Q ∧ (𝑞 +Q
𝑞)
<Q 𝑃))) |
14 | | 19.42v 1886 |
. . . . . 6
⊢
(∃𝑞((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃)) ↔ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
∃𝑞(𝑞 ∈ Q ∧ (𝑞 +Q
𝑞)
<Q 𝑃))) |
15 | 13, 14 | sylibr 133 |
. . . . 5
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑃 ∈
Q) → ∃𝑞((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) |
16 | | eeeanv 1913 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑞((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ↔ (∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ∃𝑞((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃)))) |
17 | 4, 8, 15, 16 | syl3anbrc 1166 |
. . . 4
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑃 ∈
Q) → ∃𝑥∃𝑦∃𝑞((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃)))) |
18 | | prarloclemarch2 7339 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Q ∧
𝑥 ∈ Q
∧ 𝑞 ∈
Q) → ∃𝑛 ∈ N (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞)))) |
19 | | df-rex 2441 |
. . . . . . . . . . . . . 14
⊢
(∃𝑛 ∈
N (1o <N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))) ↔ ∃𝑛(𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) |
20 | 18, 19 | sylib 121 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ Q ∧
𝑥 ∈ Q
∧ 𝑞 ∈
Q) → ∃𝑛(𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) |
21 | 20 | 3com12 1189 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑞 ∈
Q) → ∃𝑛(𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) |
22 | 21 | 3adant1r 1213 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ 𝑦 ∈ Q ∧ 𝑞 ∈ Q) →
∃𝑛(𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) |
23 | 22 | 3adant2r 1215 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ 𝑞 ∈ Q) → ∃𝑛(𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) |
24 | 23 | 3adant3r 1217 |
. . . . . . . . 9
⊢ (((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ (𝑞 ∈ Q ∧ (𝑞 +Q
𝑞)
<Q 𝑃)) → ∃𝑛(𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) |
25 | 24 | 3adant3l 1216 |
. . . . . . . 8
⊢ (((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) → ∃𝑛(𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) |
26 | 25 | ancli 321 |
. . . . . . 7
⊢ (((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) → (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ ∃𝑛(𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞)))))) |
27 | | 19.42v 1886 |
. . . . . . 7
⊢
(∃𝑛(((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) ↔ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ ∃𝑛(𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞)))))) |
28 | 26, 27 | sylibr 133 |
. . . . . 6
⊢ (((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) → ∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞)))))) |
29 | 28 | 2eximi 1581 |
. . . . 5
⊢
(∃𝑦∃𝑞((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) → ∃𝑦∃𝑞∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞)))))) |
30 | 29 | eximi 1580 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑞((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) → ∃𝑥∃𝑦∃𝑞∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞)))))) |
31 | | simpl1l 1033 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → 𝑥 ∈ Q) |
32 | | simp3rl 1055 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) → 𝑞 ∈ Q) |
33 | 32 | adantr 274 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → 𝑞 ∈ Q) |
34 | | simp3rr 1056 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) → (𝑞 +Q 𝑞) <Q
𝑃) |
35 | 34 | adantr 274 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → (𝑞 +Q 𝑞) <Q
𝑃) |
36 | 31, 33, 35 | 3jca 1162 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → (𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃)) |
37 | | simp3ll 1053 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) → 〈𝐿, 𝑈〉 ∈
P) |
38 | 37 | adantr 274 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → 〈𝐿, 𝑈〉 ∈
P) |
39 | | simpl1r 1034 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → 𝑥 ∈ 𝐿) |
40 | | simprl 521 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → 𝑛 ∈ N) |
41 | | simprrl 529 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → 1o
<N 𝑛) |
42 | | simprrr 530 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))) |
43 | | simpl2r 1036 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → 𝑦 ∈ 𝑈) |
44 | | prcunqu 7405 |
. . . . . . . . . . . . 13
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑦 ∈ 𝑈) → (𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞)) → (𝑥 +Q ([〈𝑛, 1o〉]
~Q ·Q 𝑞)) ∈ 𝑈)) |
45 | 38, 43, 44 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → (𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞)) → (𝑥 +Q ([〈𝑛, 1o〉]
~Q ·Q 𝑞)) ∈ 𝑈)) |
46 | 42, 45 | mpd 13 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → (𝑥 +Q ([〈𝑛, 1o〉]
~Q ·Q 𝑞)) ∈ 𝑈) |
47 | | prarloclem 7421 |
. . . . . . . . . . 11
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝑥 ∈ 𝐿) ∧ (𝑛 ∈ N ∧ 𝑞 ∈ Q ∧
1o <N 𝑛) ∧ (𝑥 +Q ([〈𝑛, 1o〉]
~Q ·Q 𝑞)) ∈ 𝑈) → ∃𝑚 ∈ ω ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)) |
48 | 38, 39, 40, 33, 41, 46, 47 | syl231anc 1240 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → ∃𝑚 ∈ ω ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)) |
49 | | df-rex 2441 |
. . . . . . . . . 10
⊢
(∃𝑚 ∈
ω ((𝑥
+Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈) ↔ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) |
50 | 48, 49 | sylib 121 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) |
51 | 36, 50 | jca 304 |
. . . . . . . 8
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))) |
52 | | 19.42v 1886 |
. . . . . . . 8
⊢
(∃𝑚((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) ↔ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))) |
53 | 51, 52 | sylibr 133 |
. . . . . . 7
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → ∃𝑚((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))) |
54 | | simprrl 529 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) → (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿) |
55 | | eleq1 2220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) → (𝑎 ∈ 𝐿 ↔ (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿)) |
56 | 55 | anbi1d 461 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) → ((𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈) ↔ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) |
57 | 56 | anbi2d 460 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)) ↔ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))) |
58 | 57 | anbi2d 460 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) → (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) ↔ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))))) |
59 | 58 | ceqsexgv 2841 |
. . . . . . . . . . . . 13
⊢ ((𝑥 +Q0
([〈𝑚,
1o〉] ~Q0
·Q0 𝑞)) ∈ 𝐿 → (∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))) ↔ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))))) |
60 | 59 | biimprcd 159 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) → ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 → ∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))))) |
61 | 54, 60 | mpd 13 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) → ∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))))) |
62 | | simprrr 530 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) → (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈) |
63 | | eleq1 2220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) → (𝑏 ∈ 𝑈 ↔ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)) |
64 | 63 | anbi2d 460 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) → ((𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈) ↔ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) |
65 | 64 | anbi2d 460 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)) ↔ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))) |
66 | 65 | anbi2d 460 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) → (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))) ↔ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))))) |
67 | 66 | anbi2d 460 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) → ((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) ↔ (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))))) |
68 | 67 | exbidv 1805 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) → (∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) ↔ ∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))))) |
69 | 68 | ceqsexgv 2841 |
. . . . . . . . . . . 12
⊢ ((𝑥 +Q
([〈(𝑚 +o
2o), 1o〉] ~Q
·Q 𝑞)) ∈ 𝑈 → (∃𝑏(𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) ↔ ∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))))) |
70 | 69 | biimprcd 159 |
. . . . . . . . . . 11
⊢
(∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈)))) → ((𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈 → ∃𝑏(𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))))) |
71 | 61, 62, 70 | sylc 62 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) → ∃𝑏(𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))))) |
72 | | 19.42v 1886 |
. . . . . . . . . . 11
⊢
(∃𝑎(𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) ↔ (𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))))) |
73 | 72 | exbii 1585 |
. . . . . . . . . 10
⊢
(∃𝑏∃𝑎(𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) ↔ ∃𝑏(𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))))) |
74 | 71, 73 | sylibr 133 |
. . . . . . . . 9
⊢ (((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) → ∃𝑏∃𝑎(𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))))) |
75 | | simprrl 529 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))) → 𝑎 ∈ 𝐿) |
76 | 75 | adantl 275 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑎 ∈ 𝐿) |
77 | | simprrr 530 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))) → 𝑏 ∈ 𝑈) |
78 | 77 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑏 ∈ 𝑈) |
79 | | simpl 108 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)))) |
80 | | simprl2 1028 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑞 ∈ Q) |
81 | | simprl3 1029 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑞 +Q 𝑞) <Q
𝑃) |
82 | 80, 81 | jca 304 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑞 ∈ Q ∧ (𝑞 +Q
𝑞)
<Q 𝑃)) |
83 | | simprl1 1027 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑥 ∈ Q) |
84 | | simprrl 529 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑚 ∈ ω) |
85 | 83, 84 | jca 304 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑥 ∈ Q ∧ 𝑚 ∈
ω)) |
86 | | prarloclemcalc 7422 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑞 ∈ Q ∧ (𝑞 +Q
𝑞)
<Q 𝑃) ∧ (𝑥 ∈ Q ∧ 𝑚 ∈ ω))) → 𝑏 <Q
(𝑎
+Q 𝑃)) |
87 | 79, 82, 85, 86 | syl12anc 1218 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑏 <Q (𝑎 +Q
𝑃)) |
88 | 78, 87 | jca 304 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃))) |
89 | 76, 88 | jca 304 |
. . . . . . . . . . . 12
⊢ (((𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
90 | 89 | ancom1s 559 |
. . . . . . . . . . 11
⊢ (((𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ 𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
91 | 90 | anasss 397 |
. . . . . . . . . 10
⊢ ((𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) → (𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
92 | 91 | 2eximi 1581 |
. . . . . . . . 9
⊢
(∃𝑏∃𝑎(𝑏 = (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧
(𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
93 | 74, 92 | syl 14 |
. . . . . . . 8
⊢ (((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
94 | 93 | exlimiv 1578 |
. . . . . . 7
⊢
(∃𝑚((𝑥 ∈ Q ∧
𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([〈𝑚, 1o〉]
~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([〈(𝑚 +o 2o),
1o〉] ~Q
·Q 𝑞)) ∈ 𝑈))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
95 | 53, 94 | syl 14 |
. . . . . 6
⊢ ((((𝑥 ∈ Q ∧
𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
96 | 95 | exlimivv 1876 |
. . . . 5
⊢
(∃𝑞∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
97 | 96 | exlimivv 1876 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑞∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝑃 ∈ Q) ∧
(𝑞 ∈ Q
∧ (𝑞
+Q 𝑞) <Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1o
<N 𝑛 ∧ 𝑦 <Q (𝑥 +Q
([〈𝑛,
1o〉] ~Q
·Q 𝑞))))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
98 | 17, 30, 97 | 3syl 17 |
. . 3
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑃 ∈
Q) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
99 | | excom 1644 |
. . 3
⊢
(∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃))) ↔ ∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
100 | 98, 99 | sylib 121 |
. 2
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑃 ∈
Q) → ∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
101 | | 19.42v 1886 |
. . . . 5
⊢
(∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃))) ↔ (𝑎 ∈ 𝐿 ∧ ∃𝑏(𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
102 | | df-rex 2441 |
. . . . . 6
⊢
(∃𝑏 ∈
𝑈 𝑏 <Q (𝑎 +Q
𝑃) ↔ ∃𝑏(𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃))) |
103 | 102 | anbi2i 453 |
. . . . 5
⊢ ((𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <Q (𝑎 +Q
𝑃)) ↔ (𝑎 ∈ 𝐿 ∧ ∃𝑏(𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃)))) |
104 | 101, 103 | bitr4i 186 |
. . . 4
⊢
(∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃))) ↔ (𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <Q (𝑎 +Q
𝑃))) |
105 | 104 | exbii 1585 |
. . 3
⊢
(∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃))) ↔ ∃𝑎(𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <Q (𝑎 +Q
𝑃))) |
106 | | df-rex 2441 |
. . 3
⊢
(∃𝑎 ∈
𝐿 ∃𝑏 ∈ 𝑈 𝑏 <Q (𝑎 +Q
𝑃) ↔ ∃𝑎(𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <Q (𝑎 +Q
𝑃))) |
107 | 105, 106 | bitr4i 186 |
. 2
⊢
(∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <Q (𝑎 +Q
𝑃))) ↔ ∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <Q (𝑎 +Q
𝑃)) |
108 | 100, 107 | sylib 121 |
1
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝑃 ∈
Q) → ∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <Q (𝑎 +Q
𝑃)) |