Step | Hyp | Ref
| Expression |
1 | | ltexnqq 7328 |
. . . . . 6
⊢ ((𝑞 ∈ Q ∧
𝑟 ∈ Q)
→ (𝑞
<Q 𝑟 ↔ ∃𝑝 ∈ Q (𝑞 +Q 𝑝) = 𝑟)) |
2 | 1 | biimpa 294 |
. . . . 5
⊢ (((𝑞 ∈ Q ∧
𝑟 ∈ Q)
∧ 𝑞
<Q 𝑟) → ∃𝑝 ∈ Q (𝑞 +Q 𝑝) = 𝑟) |
3 | 2 | 3adant1 1000 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q) ∧ 𝑞 <Q 𝑟) → ∃𝑝 ∈ Q (𝑞 +Q
𝑝) = 𝑟) |
4 | | halfnqq 7330 |
. . . . . 6
⊢ (𝑝 ∈ Q →
∃ℎ ∈
Q (ℎ
+Q ℎ) = 𝑝) |
5 | 4 | ad2antrl 482 |
. . . . 5
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) → ∃ℎ ∈ Q (ℎ +Q ℎ) = 𝑝) |
6 | | prop 7395 |
. . . . . . . . . 10
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
7 | | prarloc 7423 |
. . . . . . . . . 10
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ ℎ ∈ Q) →
∃𝑑 ∈
(1st ‘𝐴)∃𝑢 ∈ (2nd ‘𝐴)𝑢 <Q (𝑑 +Q
ℎ)) |
8 | 6, 7 | sylan 281 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
ℎ ∈ Q)
→ ∃𝑑 ∈
(1st ‘𝐴)∃𝑢 ∈ (2nd ‘𝐴)𝑢 <Q (𝑑 +Q
ℎ)) |
9 | 8 | adantlr 469 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ ℎ ∈
Q) → ∃𝑑 ∈ (1st ‘𝐴)∃𝑢 ∈ (2nd ‘𝐴)𝑢 <Q (𝑑 +Q
ℎ)) |
10 | 9 | 3ad2antl1 1144 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q) ∧ 𝑞 <Q 𝑟) ∧ ℎ ∈ Q) → ∃𝑑 ∈ (1st
‘𝐴)∃𝑢 ∈ (2nd
‘𝐴)𝑢 <Q (𝑑 +Q
ℎ)) |
11 | 10 | ad2ant2r 501 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) → ∃𝑑 ∈ (1st ‘𝐴)∃𝑢 ∈ (2nd ‘𝐴)𝑢 <Q (𝑑 +Q
ℎ)) |
12 | | prop 7395 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
13 | | prarloc 7423 |
. . . . . . . . . . . . . 14
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ ℎ ∈ Q) →
∃𝑒 ∈
(1st ‘𝐵)∃𝑡 ∈ (2nd ‘𝐵)𝑡 <Q (𝑒 +Q
ℎ)) |
14 | 12, 13 | sylan 281 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ P ∧
ℎ ∈ Q)
→ ∃𝑒 ∈
(1st ‘𝐵)∃𝑡 ∈ (2nd ‘𝐵)𝑡 <Q (𝑒 +Q
ℎ)) |
15 | 14 | adantll 468 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ ℎ ∈
Q) → ∃𝑒 ∈ (1st ‘𝐵)∃𝑡 ∈ (2nd ‘𝐵)𝑡 <Q (𝑒 +Q
ℎ)) |
16 | 15 | 3ad2antl1 1144 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q) ∧ 𝑞 <Q 𝑟) ∧ ℎ ∈ Q) → ∃𝑒 ∈ (1st
‘𝐵)∃𝑡 ∈ (2nd
‘𝐵)𝑡 <Q (𝑒 +Q
ℎ)) |
17 | 16 | ad2ant2r 501 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) → ∃𝑒 ∈ (1st ‘𝐵)∃𝑡 ∈ (2nd ‘𝐵)𝑡 <Q (𝑒 +Q
ℎ)) |
18 | 17 | adantr 274 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) → ∃𝑒 ∈ (1st
‘𝐵)∃𝑡 ∈ (2nd
‘𝐵)𝑡 <Q (𝑒 +Q
ℎ)) |
19 | | simpll1 1021 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
20 | 19 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
21 | 20 | simpld 111 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → 𝐴 ∈ P) |
22 | 20 | simprd 113 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → 𝐵 ∈ P) |
23 | | simpll3 1023 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) → 𝑞 <Q 𝑟) |
24 | 23 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → 𝑞 <Q 𝑟) |
25 | | simplrl 525 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) → ℎ ∈
Q) |
26 | 25 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → ℎ ∈ Q) |
27 | | simplrr 526 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) → (𝑞 +Q 𝑝) = 𝑟) |
28 | | oveq2 5832 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ +Q
ℎ) = 𝑝 → (𝑞 +Q (ℎ +Q
ℎ)) = (𝑞 +Q 𝑝)) |
29 | 28 | eqeq1d 2166 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ +Q
ℎ) = 𝑝 → ((𝑞 +Q (ℎ +Q
ℎ)) = 𝑟 ↔ (𝑞 +Q 𝑝) = 𝑟)) |
30 | 29 | ad2antll 483 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) → ((𝑞 +Q (ℎ +Q
ℎ)) = 𝑟 ↔ (𝑞 +Q 𝑝) = 𝑟)) |
31 | 27, 30 | mpbird 166 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) → (𝑞 +Q (ℎ +Q
ℎ)) = 𝑟) |
32 | 31 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → (𝑞 +Q (ℎ +Q
ℎ)) = 𝑟) |
33 | | simprll 527 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) → 𝑑 ∈ (1st
‘𝐴)) |
34 | 33 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → 𝑑 ∈ (1st ‘𝐴)) |
35 | | simprlr 528 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) → 𝑢 ∈ (2nd
‘𝐴)) |
36 | 35 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → 𝑢 ∈ (2nd ‘𝐴)) |
37 | | simplrr 526 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → 𝑢 <Q (𝑑 +Q
ℎ)) |
38 | | simprll 527 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → 𝑒 ∈ (1st ‘𝐵)) |
39 | | simprlr 528 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → 𝑡 ∈ (2nd ‘𝐵)) |
40 | | simprr 522 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → 𝑡 <Q (𝑒 +Q
ℎ)) |
41 | 21, 22, 24, 26, 32, 34, 36, 37, 38, 39, 40 | addlocprlem 7455 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ ((𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) ∧ 𝑡 <Q
(𝑒
+Q ℎ))) → (𝑞 ∈ (1st ‘(𝐴 +P
𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵)))) |
42 | 41 | expr 373 |
. . . . . . . . . 10
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) ∧ (𝑒 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵))) → (𝑡 <Q
(𝑒
+Q ℎ) → (𝑞 ∈ (1st ‘(𝐴 +P
𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵))))) |
43 | 42 | rexlimdvva 2582 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) → (∃𝑒 ∈ (1st
‘𝐵)∃𝑡 ∈ (2nd
‘𝐵)𝑡 <Q (𝑒 +Q
ℎ) → (𝑞 ∈ (1st
‘(𝐴
+P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵))))) |
44 | 18, 43 | mpd 13 |
. . . . . . . 8
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴)) ∧ 𝑢 <Q (𝑑 +Q
ℎ))) → (𝑞 ∈ (1st
‘(𝐴
+P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵)))) |
45 | 44 | expr 373 |
. . . . . . 7
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) ∧ (𝑑 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) → (𝑢 <Q (𝑑 +Q
ℎ) → (𝑞 ∈ (1st
‘(𝐴
+P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵))))) |
46 | 45 | rexlimdvva 2582 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) → (∃𝑑 ∈ (1st ‘𝐴)∃𝑢 ∈ (2nd ‘𝐴)𝑢 <Q (𝑑 +Q
ℎ) → (𝑞 ∈ (1st
‘(𝐴
+P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵))))) |
47 | 11, 46 | mpd 13 |
. . . . 5
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑞 ∈ Q ∧ 𝑟 ∈ Q) ∧
𝑞
<Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) ∧ (ℎ ∈ Q ∧ (ℎ +Q
ℎ) = 𝑝)) → (𝑞 ∈ (1st ‘(𝐴 +P
𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵)))) |
48 | 5, 47 | rexlimddv 2579 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈ Q ∧ (𝑞 +Q
𝑝) = 𝑟)) → (𝑞 ∈ (1st ‘(𝐴 +P
𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵)))) |
49 | 3, 48 | rexlimddv 2579 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q) ∧ 𝑞 <Q 𝑟) → (𝑞 ∈ (1st ‘(𝐴 +P
𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵)))) |
50 | 49 | 3expia 1187 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑞 ∈
Q ∧ 𝑟
∈ Q)) → (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 +P
𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵))))) |
51 | 50 | ralrimivva 2539 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ∀𝑞 ∈
Q ∀𝑟
∈ Q (𝑞
<Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 +P
𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P
𝐵))))) |