Step | Hyp | Ref
| Expression |
1 | | mulnqprlemru 6672 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ⊆
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) |
2 | | ltsonq 6496 |
. . . . . . . . 9
⊢
<Q Or Q |
3 | | mulclnq 6474 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
·Q 𝐵) ∈ Q) |
4 | | sonr 4054 |
. . . . . . . . 9
⊢ ((
<Q Or Q ∧ (𝐴 ·Q 𝐵) ∈ Q) →
¬ (𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵)) |
5 | 2, 3, 4 | sylancr 393 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵)) |
6 | | ltrelnq 6463 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
7 | 6 | brel 4392 |
. . . . . . . . . . 11
⊢ ((𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵) → ((𝐴 ·Q 𝐵) ∈ Q ∧
(𝐴
·Q 𝐵) ∈ Q)) |
8 | 7 | simpld 105 |
. . . . . . . . . 10
⊢ ((𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵) → (𝐴 ·Q 𝐵) ∈
Q) |
9 | | elex 2566 |
. . . . . . . . . 10
⊢ ((𝐴
·Q 𝐵) ∈ Q → (𝐴
·Q 𝐵) ∈ V) |
10 | 8, 9 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵) → (𝐴 ·Q 𝐵) ∈ V) |
11 | | breq2 3768 |
. . . . . . . . 9
⊢ (𝑢 = (𝐴 ·Q 𝐵) → ((𝐴 ·Q 𝐵) <Q
𝑢 ↔ (𝐴 ·Q 𝐵) <Q
(𝐴
·Q 𝐵))) |
12 | 10, 11 | elab3 2694 |
. . . . . . . 8
⊢ ((𝐴
·Q 𝐵) ∈ {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢} ↔ (𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵)) |
13 | 5, 12 | sylnibr 602 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
·Q 𝐵) ∈ {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}) |
14 | | ltnqex 6647 |
. . . . . . . . 9
⊢ {𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)} ∈ V |
15 | | gtnqex 6648 |
. . . . . . . . 9
⊢ {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢} ∈
V |
16 | 14, 15 | op2nd 5774 |
. . . . . . . 8
⊢
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) = {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢} |
17 | 16 | eleq2i 2104 |
. . . . . . 7
⊢ ((𝐴
·Q 𝐵) ∈ (2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) ↔ (𝐴
·Q 𝐵) ∈ {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}) |
18 | 13, 17 | sylnibr 602 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
·Q 𝐵) ∈ (2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) |
19 | 1, 18 | ssneldd 2948 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
·Q 𝐵) ∈ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
20 | 19 | adantr 261 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) → ¬
(𝐴
·Q 𝐵) ∈ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
21 | | nqprlu 6645 |
. . . . . . 7
⊢ (𝐴 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈
P) |
22 | | nqprlu 6645 |
. . . . . . 7
⊢ (𝐵 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉 ∈
P) |
23 | | mulclpr 6670 |
. . . . . . 7
⊢
((〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈ P
∧ 〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉 ∈ P)
→ (〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) ∈
P) |
24 | 21, 22, 23 | syl2an 273 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) ∈
P) |
25 | | prop 6573 |
. . . . . 6
⊢
((〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) ∈ P
→ 〈(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)), (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))〉 ∈
P) |
26 | 24, 25 | syl 14 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ 〈(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)), (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))〉 ∈
P) |
27 | | vex 2560 |
. . . . . . 7
⊢ 𝑟 ∈ V |
28 | | breq1 3767 |
. . . . . . 7
⊢ (𝑙 = 𝑟 → (𝑙 <Q (𝐴
·Q 𝐵) ↔ 𝑟 <Q (𝐴
·Q 𝐵))) |
29 | 14, 15 | op1st 5773 |
. . . . . . 7
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) = {𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)} |
30 | 27, 28, 29 | elab2 2690 |
. . . . . 6
⊢ (𝑟 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) ↔ 𝑟 <Q
(𝐴
·Q 𝐵)) |
31 | 30 | biimpi 113 |
. . . . 5
⊢ (𝑟 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) → 𝑟 <Q
(𝐴
·Q 𝐵)) |
32 | | prloc 6589 |
. . . . 5
⊢
((〈(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)), (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))〉 ∈
P ∧ 𝑟
<Q (𝐴 ·Q 𝐵)) → (𝑟 ∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ∨ (𝐴
·Q 𝐵) ∈ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)))) |
33 | 26, 31, 32 | syl2an 273 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) → (𝑟 ∈ (1st
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ∨ (𝐴
·Q 𝐵) ∈ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)))) |
34 | 20, 33 | ecased 1239 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) → 𝑟 ∈ (1st
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
35 | 34 | ex 108 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) → 𝑟 ∈ (1st
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)))) |
36 | 35 | ssrdv 2951 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) ⊆
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |