Step | Hyp | Ref
| Expression |
1 | | prop 7424 |
. . . . . . . 8
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
2 | | prmuloc 7515 |
. . . . . . . 8
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑞 <Q
𝑟) → ∃𝑑 ∈ Q
∃𝑢 ∈
Q (𝑑 ∈
(1st ‘𝐴)
∧ 𝑢 ∈
(2nd ‘𝐴)
∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟))) |
3 | 1, 2 | sylan 281 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑞
<Q 𝑟) → ∃𝑑 ∈ Q ∃𝑢 ∈ Q (𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟))) |
4 | | r2ex 2490 |
. . . . . . 7
⊢
(∃𝑑 ∈
Q ∃𝑢
∈ Q (𝑑
∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴) ∧ (𝑢 ·Q 𝑞) <Q
(𝑑
·Q 𝑟)) ↔ ∃𝑑∃𝑢((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) |
5 | 3, 4 | sylib 121 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑞
<Q 𝑟) → ∃𝑑∃𝑢((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) |
6 | 5 | adantlr 474 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ 𝑞
<Q 𝑟) → ∃𝑑∃𝑢((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) |
7 | 6 | adantlr 474 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q)) ∧ 𝑞 <Q 𝑟) → ∃𝑑∃𝑢((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) |
8 | | simprr3 1042 |
. . . . . . . 8
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) → (𝑢 ·Q 𝑞) <Q
(𝑑
·Q 𝑟)) |
9 | | simprl 526 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) → (𝑑 ∈ Q ∧ 𝑢 ∈
Q)) |
10 | | mulclnq 7325 |
. . . . . . . . 9
⊢ ((𝑑 ∈ Q ∧
𝑢 ∈ Q)
→ (𝑑
·Q 𝑢) ∈ Q) |
11 | 9, 10 | syl 14 |
. . . . . . . 8
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) → (𝑑 ·Q 𝑢) ∈
Q) |
12 | | appdivnq 7512 |
. . . . . . . 8
⊢ (((𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟) ∧ (𝑑 ·Q 𝑢) ∈ Q) →
∃𝑒 ∈
Q ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟))) |
13 | 8, 11, 12 | syl2anc 409 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) → ∃𝑒 ∈ Q ((𝑢 ·Q 𝑞) <Q
(𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟))) |
14 | | simprrr 535 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)) |
15 | 11 | adantr 274 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑑 ·Q 𝑢) ∈
Q) |
16 | | appdivnq 7512 |
. . . . . . . . 9
⊢ (((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑑 ·Q 𝑟) ∧ (𝑑 ·Q 𝑢) ∈ Q) →
∃𝑡 ∈
Q ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟))) |
17 | 14, 15, 16 | syl2anc 409 |
. . . . . . . 8
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → ∃𝑡 ∈ Q ((𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑡
·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟))) |
18 | | simplll 528 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
19 | 18 | ad2antrr 485 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
20 | | simprl 526 |
. . . . . . . . . 10
⊢ ((𝑒 ∈ Q ∧
((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟))) → (𝑢 ·Q 𝑞) <Q
(𝑒
·Q (𝑑 ·Q 𝑢))) |
21 | 20 | ad2antlr 486 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑢 ·Q 𝑞) <Q
(𝑒
·Q (𝑑 ·Q 𝑢))) |
22 | | simprrl 534 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑡
·Q (𝑑 ·Q 𝑢))) |
23 | | simprrr 535 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)) |
24 | | simpllr 529 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) → (𝑞 ∈ Q ∧ 𝑟 ∈
Q)) |
25 | 24 | ad2antrr 485 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑞 ∈ Q ∧ 𝑟 ∈
Q)) |
26 | 9 | ad2antrr 485 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑑 ∈ Q ∧ 𝑢 ∈
Q)) |
27 | | 3simpa 989 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)) → (𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) |
28 | 27 | ad2antll 488 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) → (𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) |
29 | 28 | ad2antrr 485 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) |
30 | | simplrl 530 |
. . . . . . . . . 10
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → 𝑒 ∈ Q) |
31 | | simprl 526 |
. . . . . . . . . 10
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → 𝑡 ∈ Q) |
32 | 30, 31 | jca 304 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑒 ∈ Q ∧ 𝑡 ∈
Q)) |
33 | 19, 21, 22, 23, 25, 26, 29, 32 | mullocprlem 7519 |
. . . . . . . 8
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) ∧ (𝑡 ∈ Q ∧ ((𝑒
·Q (𝑑 ·Q 𝑢))
<Q (𝑡 ·Q (𝑑
·Q 𝑢)) ∧ (𝑡 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑞 ∈ (1st ‘(𝐴
·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴
·P 𝐵)))) |
34 | 17, 33 | rexlimddv 2592 |
. . . . . . 7
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) ∧ (𝑒 ∈ Q ∧ ((𝑢
·Q 𝑞) <Q (𝑒
·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑
·Q 𝑢)) <Q (𝑑
·Q 𝑟)))) → (𝑞 ∈ (1st ‘(𝐴
·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴
·P 𝐵)))) |
35 | 13, 34 | rexlimddv 2592 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q)) ∧
𝑞
<Q 𝑟) ∧ ((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟)))) → (𝑞 ∈ (1st ‘(𝐴
·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴
·P 𝐵)))) |
36 | 35 | ex 114 |
. . . . 5
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q)) ∧ 𝑞 <Q 𝑟) → (((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟))) → (𝑞 ∈ (1st ‘(𝐴
·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴
·P 𝐵))))) |
37 | 36 | exlimdvv 1890 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q)) ∧ 𝑞 <Q 𝑟) → (∃𝑑∃𝑢((𝑑 ∈ Q ∧ 𝑢 ∈ Q) ∧
(𝑑 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (2nd
‘𝐴) ∧ (𝑢
·Q 𝑞) <Q (𝑑
·Q 𝑟))) → (𝑞 ∈ (1st ‘(𝐴
·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴
·P 𝐵))))) |
38 | 7, 37 | mpd 13 |
. . 3
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q)) ∧ 𝑞 <Q 𝑟) → (𝑞 ∈ (1st ‘(𝐴
·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴
·P 𝐵)))) |
39 | 38 | ex 114 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q)) → (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴
·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴
·P 𝐵))))) |
40 | 39 | ralrimivva 2552 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ∀𝑞 ∈
Q ∀𝑟
∈ Q (𝑞
<Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴
·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴
·P 𝐵))))) |