Step | Hyp | Ref
| Expression |
1 | | addnqprlemfl 7571 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) ⊆
(1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))) |
2 | | addnqprlemrl 7569 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ⊆
(1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩)) |
3 | 1, 2 | eqssd 3184 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) = (1st
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))) |
4 | | addnqprlemfu 7572 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) ⊆
(2nd ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))) |
5 | | addnqprlemru 7570 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ⊆
(2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩)) |
6 | 4, 5 | eqssd 3184 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) = (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))) |
7 | | addclnq 7387 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
+Q 𝐵) ∈ Q) |
8 | | nqprlu 7559 |
. . . 4
⊢ ((𝐴 +Q
𝐵) ∈ Q
→ ⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩ ∈
P) |
9 | 7, 8 | syl 14 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩ ∈
P) |
10 | | nqprlu 7559 |
. . . 4
⊢ (𝐴 ∈ Q →
⟨{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ∈
P) |
11 | | nqprlu 7559 |
. . . 4
⊢ (𝐵 ∈ Q →
⟨{𝑙 ∣ 𝑙 <Q
𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩ ∈
P) |
12 | | addclpr 7549 |
. . . 4
⊢
((⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ∈ P
∧ ⟨{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩ ∈ P)
→ (⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩) ∈
P) |
13 | 10, 11, 12 | syl2an 289 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩) ∈
P) |
14 | | preqlu 7484 |
. . 3
⊢
((⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩ ∈
P ∧ (⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩) ∈ P)
→ (⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩) ↔ ((1st
‘⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) = (1st
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ∧ (2nd
‘⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) = (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))))) |
15 | 9, 13, 14 | syl2anc 411 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩) ↔ ((1st
‘⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) = (1st
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ∧ (2nd
‘⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) = (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))))) |
16 | 3, 6, 15 | mpbir2and 945 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) |