Step | Hyp | Ref
| Expression |
1 | | mulnqprlemru 7497 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ⊆
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) |
2 | | ltsonq 7321 |
. . . . . . . . 9
⊢
<Q Or Q |
3 | | mulclnq 7299 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
·Q 𝐵) ∈ Q) |
4 | | sonr 4280 |
. . . . . . . . 9
⊢ ((
<Q Or Q ∧ (𝐴 ·Q 𝐵) ∈ Q) →
¬ (𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵)) |
5 | 2, 3, 4 | sylancr 411 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵)) |
6 | | ltrelnq 7288 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
7 | 6 | brel 4641 |
. . . . . . . . . . 11
⊢ ((𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵) → ((𝐴 ·Q 𝐵) ∈ Q ∧
(𝐴
·Q 𝐵) ∈ Q)) |
8 | 7 | simpld 111 |
. . . . . . . . . 10
⊢ ((𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵) → (𝐴 ·Q 𝐵) ∈
Q) |
9 | | elex 2723 |
. . . . . . . . . 10
⊢ ((𝐴
·Q 𝐵) ∈ Q → (𝐴
·Q 𝐵) ∈ V) |
10 | 8, 9 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵) → (𝐴 ·Q 𝐵) ∈ V) |
11 | | breq2 3971 |
. . . . . . . . 9
⊢ (𝑢 = (𝐴 ·Q 𝐵) → ((𝐴 ·Q 𝐵) <Q
𝑢 ↔ (𝐴 ·Q 𝐵) <Q
(𝐴
·Q 𝐵))) |
12 | 10, 11 | elab3 2864 |
. . . . . . . 8
⊢ ((𝐴
·Q 𝐵) ∈ {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢} ↔ (𝐴
·Q 𝐵) <Q (𝐴
·Q 𝐵)) |
13 | 5, 12 | sylnibr 667 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
·Q 𝐵) ∈ {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}) |
14 | | ltnqex 7472 |
. . . . . . . . 9
⊢ {𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)} ∈ V |
15 | | gtnqex 7473 |
. . . . . . . . 9
⊢ {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢} ∈
V |
16 | 14, 15 | op2nd 6098 |
. . . . . . . 8
⊢
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) = {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢} |
17 | 16 | eleq2i 2224 |
. . . . . . 7
⊢ ((𝐴
·Q 𝐵) ∈ (2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) ↔ (𝐴
·Q 𝐵) ∈ {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}) |
18 | 13, 17 | sylnibr 667 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
·Q 𝐵) ∈ (2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) |
19 | 1, 18 | ssneldd 3131 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
·Q 𝐵) ∈ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
20 | 19 | adantr 274 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) → ¬
(𝐴
·Q 𝐵) ∈ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
21 | | nqprlu 7470 |
. . . . . . 7
⊢ (𝐴 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈
P) |
22 | | nqprlu 7470 |
. . . . . . 7
⊢ (𝐵 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉 ∈
P) |
23 | | mulclpr 7495 |
. . . . . . 7
⊢
((〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈ P
∧ 〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉 ∈ P)
→ (〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) ∈
P) |
24 | 21, 22, 23 | syl2an 287 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) ∈
P) |
25 | | prop 7398 |
. . . . . 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 2715 |
. . . . . . 7
⊢ 𝑟 ∈ V |
28 | | breq1 3970 |
. . . . . . 7
⊢ (𝑙 = 𝑟 → (𝑙 <Q (𝐴
·Q 𝐵) ↔ 𝑟 <Q (𝐴
·Q 𝐵))) |
29 | 14, 15 | op1st 6097 |
. . . . . . 7
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) = {𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)} |
30 | 27, 28, 29 | elab2 2860 |
. . . . . 6
⊢ (𝑟 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) ↔ 𝑟 <Q
(𝐴
·Q 𝐵)) |
31 | 30 | biimpi 119 |
. . . . 5
⊢ (𝑟 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) → 𝑟 <Q
(𝐴
·Q 𝐵)) |
32 | | prloc 7414 |
. . . . 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 287 |
. . . 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 1331 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) → 𝑟 ∈ (1st
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
35 | 34 | ex 114 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) → 𝑟 ∈ (1st
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)))) |
36 | 35 | ssrdv 3134 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) ⊆
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |