Step | Hyp | Ref
| Expression |
1 | | ltexnqq 6391 |
. . . . . 6
⊢ ((𝑞 ∈ Q ∧ 𝑟
∈ Q) → (𝑞 <Q 𝑟 ↔ ∃𝑝 ∈
Q (𝑞
+Q 𝑝)
= 𝑟)) |
2 | 1 | biimpa 280 |
. . . . 5
⊢ (((𝑞 ∈ Q ∧ 𝑟
∈ Q) ∧ 𝑞
<Q 𝑟) → ∃𝑝 ∈
Q (𝑞
+Q 𝑝)
= 𝑟) |
3 | 2 | 3adant1 921 |
. . . 4
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) → ∃𝑝 ∈
Q (𝑞
+Q 𝑝)
= 𝑟) |
4 | | halfnqq 6393 |
. . . . . 6
⊢ (𝑝 ∈ Q → ∃ℎ
∈ Q (ℎ +Q ℎ) = 𝑝) |
5 | 4 | ad2antrl 459 |
. . . . 5
⊢
((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) → ∃ℎ
∈ Q (ℎ +Q ℎ) = 𝑝) |
6 | | prop 6458 |
. . . . . . . . . 10
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
7 | | prarloc 6486 |
. . . . . . . . . 10
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ ℎ
∈ Q) → ∃𝑑 ∈
(1st ‘A)∃u ∈ (2nd ‘A)u
<Q (𝑑 +Q ℎ)) |
8 | 6, 7 | sylan 267 |
. . . . . . . . 9
⊢
((A ∈ P ∧ ℎ
∈ Q) → ∃𝑑 ∈
(1st ‘A)∃u ∈ (2nd ‘A)u
<Q (𝑑 +Q ℎ)) |
9 | 8 | adantlr 446 |
. . . . . . . 8
⊢
(((A ∈ P ∧ B ∈ P) ∧ ℎ
∈ Q) → ∃𝑑 ∈
(1st ‘A)∃u ∈ (2nd ‘A)u
<Q (𝑑 +Q ℎ)) |
10 | 9 | 3ad2antl1 1065 |
. . . . . . 7
⊢
((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ ℎ
∈ Q) → ∃𝑑 ∈
(1st ‘A)∃u ∈ (2nd ‘A)u
<Q (𝑑 +Q ℎ)) |
11 | 10 | ad2ant2r 478 |
. . . . . 6
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) → ∃𝑑 ∈
(1st ‘A)∃u ∈ (2nd ‘A)u
<Q (𝑑 +Q ℎ)) |
12 | | prop 6458 |
. . . . . . . . . . . . . 14
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
13 | | prarloc 6486 |
. . . . . . . . . . . . . 14
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ ℎ
∈ Q) → ∃𝑒 ∈
(1st ‘B)∃𝑡 ∈
(2nd ‘B)𝑡 <Q (𝑒 +Q ℎ)) |
14 | 12, 13 | sylan 267 |
. . . . . . . . . . . . 13
⊢
((B ∈ P ∧ ℎ
∈ Q) → ∃𝑒 ∈
(1st ‘B)∃𝑡 ∈
(2nd ‘B)𝑡 <Q (𝑒 +Q ℎ)) |
15 | 14 | adantll 445 |
. . . . . . . . . . . 12
⊢
(((A ∈ P ∧ B ∈ P) ∧ ℎ
∈ Q) → ∃𝑒 ∈
(1st ‘B)∃𝑡 ∈
(2nd ‘B)𝑡 <Q (𝑒 +Q ℎ)) |
16 | 15 | 3ad2antl1 1065 |
. . . . . . . . . . 11
⊢
((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ ℎ
∈ Q) → ∃𝑒 ∈
(1st ‘B)∃𝑡 ∈
(2nd ‘B)𝑡 <Q (𝑒 +Q ℎ)) |
17 | 16 | ad2ant2r 478 |
. . . . . . . . . 10
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) → ∃𝑒 ∈
(1st ‘B)∃𝑡 ∈
(2nd ‘B)𝑡 <Q (𝑒 +Q ℎ)) |
18 | 17 | adantr 261 |
. . . . . . . . 9
⊢
((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) → ∃𝑒 ∈
(1st ‘B)∃𝑡 ∈
(2nd ‘B)𝑡 <Q (𝑒 +Q ℎ)) |
19 | | simpll1 942 |
. . . . . . . . . . . . . 14
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) → (A ∈
P ∧ B ∈
P)) |
20 | 19 | ad2antrr 457 |
. . . . . . . . . . . . 13
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → (A ∈
P ∧ B ∈
P)) |
21 | 20 | simpld 105 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → A ∈
P) |
22 | 20 | simprd 107 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → B ∈
P) |
23 | | simpll3 944 |
. . . . . . . . . . . . 13
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) → 𝑞 <Q 𝑟) |
24 | 23 | ad2antrr 457 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → 𝑞 <Q 𝑟) |
25 | | simplrl 487 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) → ℎ ∈
Q) |
26 | 25 | adantr 261 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → ℎ ∈
Q) |
27 | | simplrr 488 |
. . . . . . . . . . . . . 14
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) → (𝑞 +Q 𝑝) = 𝑟) |
28 | | oveq2 5463 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ +Q ℎ) = 𝑝 → (𝑞 +Q (ℎ +Q ℎ)) = (𝑞 +Q 𝑝)) |
29 | 28 | eqeq1d 2045 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ +Q ℎ) = 𝑝 → ((𝑞 +Q (ℎ +Q ℎ)) = 𝑟 ↔ (𝑞 +Q 𝑝) = 𝑟)) |
30 | 29 | ad2antll 460 |
. . . . . . . . . . . . . 14
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) → ((𝑞 +Q (ℎ +Q ℎ)) = 𝑟 ↔ (𝑞 +Q 𝑝) = 𝑟)) |
31 | 27, 30 | mpbird 156 |
. . . . . . . . . . . . 13
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) → (𝑞 +Q (ℎ +Q ℎ)) = 𝑟) |
32 | 31 | ad2antrr 457 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → (𝑞 +Q (ℎ +Q ℎ)) = 𝑟) |
33 | | simprll 489 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) → 𝑑 ∈
(1st ‘A)) |
34 | 33 | adantr 261 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → 𝑑 ∈
(1st ‘A)) |
35 | | simprlr 490 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) → u ∈
(2nd ‘A)) |
36 | 35 | adantr 261 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → u ∈
(2nd ‘A)) |
37 | | simplrr 488 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → u <Q (𝑑 +Q ℎ)) |
38 | | simprll 489 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → 𝑒 ∈
(1st ‘B)) |
39 | | simprlr 490 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → 𝑡 ∈
(2nd ‘B)) |
40 | | simprr 484 |
. . . . . . . . . . . 12
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → 𝑡 <Q (𝑒 +Q ℎ)) |
41 | 21, 22, 24, 26, 32, 34, 36, 37, 38, 39, 40 | addlocprlem 6518 |
. . . . . . . . . . 11
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ ((𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B)) ∧ 𝑡 <Q
(𝑒 +Q
ℎ))) → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B)))) |
42 | 41 | expr 357 |
. . . . . . . . . 10
⊢
(((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) ∧ (𝑒 ∈ (1st ‘B) ∧ 𝑡 ∈ (2nd ‘B))) → (𝑡 <Q (𝑒 +Q ℎ) → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B))))) |
43 | 42 | rexlimdvva 2434 |
. . . . . . . . 9
⊢
((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) → (∃𝑒 ∈
(1st ‘B)∃𝑡 ∈
(2nd ‘B)𝑡 <Q (𝑒 +Q ℎ) → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B))))) |
44 | 18, 43 | mpd 13 |
. . . . . . . 8
⊢
((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ ((𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A)) ∧ u
<Q (𝑑 +Q ℎ))) → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B)))) |
45 | 44 | expr 357 |
. . . . . . 7
⊢
((((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) ∧ (𝑑 ∈ (1st ‘A) ∧ u ∈
(2nd ‘A))) →
(u <Q (𝑑 +Q ℎ) → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B))))) |
46 | 45 | rexlimdvva 2434 |
. . . . . 6
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) → (∃𝑑 ∈
(1st ‘A)∃u ∈ (2nd ‘A)u
<Q (𝑑 +Q ℎ) → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B))))) |
47 | 11, 46 | mpd 13 |
. . . . 5
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) ∧ (ℎ ∈
Q ∧ (ℎ +Q ℎ) = 𝑝)) → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B)))) |
48 | 5, 47 | rexlimddv 2431 |
. . . 4
⊢
((((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) ∧ (𝑝 ∈
Q ∧ (𝑞 +Q 𝑝) = 𝑟)) → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B)))) |
49 | 3, 48 | rexlimddv 2431 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q) ∧ 𝑞 <Q 𝑟) → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B)))) |
50 | 49 | 3expia 1105 |
. 2
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝑞 ∈
Q ∧ 𝑟 ∈
Q)) → (𝑞
<Q 𝑟 → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B))))) |
51 | 50 | ralrimivva 2395 |
1
⊢
((A ∈ P ∧ B ∈ P) → ∀𝑞 ∈
Q ∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈
(1st ‘(A
+P B)) ∨ 𝑟
∈ (2nd ‘(A +P B))))) |