Step | Hyp | Ref
| Expression |
1 | | prop 7397 |
. . . 4
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
2 | | prml 7399 |
. . . 4
⊢
(〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P →
∃𝑝 ∈
Q 𝑝 ∈
(1st ‘𝐵)) |
3 | 1, 2 | syl 14 |
. . 3
⊢ (𝐵 ∈ P →
∃𝑝 ∈
Q 𝑝 ∈
(1st ‘𝐵)) |
4 | 3 | adantl 275 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ∃𝑝 ∈
Q 𝑝 ∈
(1st ‘𝐵)) |
5 | | prop 7397 |
. . . . 5
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
6 | | prarloc 7425 |
. . . . 5
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑝 ∈ Q) →
∃𝑟 ∈
(1st ‘𝐴)∃𝑞 ∈ (2nd ‘𝐴)𝑞 <Q (𝑟 +Q
𝑝)) |
7 | 5, 6 | sylan 281 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝑝 ∈ Q)
→ ∃𝑟 ∈
(1st ‘𝐴)∃𝑞 ∈ (2nd ‘𝐴)𝑞 <Q (𝑟 +Q
𝑝)) |
8 | 7 | ad2ant2r 501 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑝 ∈
Q ∧ 𝑝
∈ (1st ‘𝐵))) → ∃𝑟 ∈ (1st ‘𝐴)∃𝑞 ∈ (2nd ‘𝐴)𝑞 <Q (𝑟 +Q
𝑝)) |
9 | | elprnqu 7404 |
. . . . . . . . . . 11
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑞 ∈ (2nd
‘𝐴)) → 𝑞 ∈
Q) |
10 | 5, 9 | sylan 281 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
𝑞 ∈ (2nd
‘𝐴)) → 𝑞 ∈
Q) |
11 | 10 | adantlr 469 |
. . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ 𝑞 ∈
(2nd ‘𝐴))
→ 𝑞 ∈
Q) |
12 | 11 | ad2ant2rl 503 |
. . . . . . . 8
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑝 ∈
Q ∧ 𝑝
∈ (1st ‘𝐵))) ∧ (𝑟 ∈ (1st ‘𝐴) ∧ 𝑞 ∈ (2nd ‘𝐴))) → 𝑞 ∈ Q) |
13 | 12 | adantr 274 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑝 ∈ Q ∧ 𝑝 ∈ (1st
‘𝐵))) ∧ (𝑟 ∈ (1st
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐴))) ∧ 𝑞 <Q
(𝑟
+Q 𝑝)) → 𝑞 ∈ Q) |
14 | | simplrr 526 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑝 ∈ Q ∧ 𝑝 ∈ (1st
‘𝐵))) ∧ (𝑟 ∈ (1st
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐴))) ∧ 𝑞 <Q
(𝑟
+Q 𝑝)) → 𝑞 ∈ (2nd ‘𝐴)) |
15 | | simprl 521 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ Q ∧
𝑝 ∈ (1st
‘𝐵)) ∧ (𝑟 ∈ (1st
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐴))) → 𝑟 ∈ (1st
‘𝐴)) |
16 | | simplr 520 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ Q ∧
𝑝 ∈ (1st
‘𝐵)) ∧ (𝑟 ∈ (1st
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐴))) → 𝑝 ∈ (1st
‘𝐵)) |
17 | 15, 16 | jca 304 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ Q ∧
𝑝 ∈ (1st
‘𝐵)) ∧ (𝑟 ∈ (1st
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐴))) → (𝑟 ∈ (1st
‘𝐴) ∧ 𝑝 ∈ (1st
‘𝐵))) |
18 | | df-iplp 7390 |
. . . . . . . . . . . . 13
⊢
+P = (𝑥 ∈ P, 𝑦 ∈ P ↦ 〈{𝑓 ∈ Q ∣
∃𝑔 ∈
Q ∃ℎ
∈ Q (𝑔
∈ (1st ‘𝑥) ∧ ℎ ∈ (1st ‘𝑦) ∧ 𝑓 = (𝑔 +Q ℎ))}, {𝑓 ∈ Q ∣ ∃𝑔 ∈ Q
∃ℎ ∈
Q (𝑔 ∈
(2nd ‘𝑥)
∧ ℎ ∈
(2nd ‘𝑦)
∧ 𝑓 = (𝑔 +Q
ℎ))}〉) |
19 | | addclnq 7297 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
20 | 18, 19 | genpprecll 7436 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑟 ∈
(1st ‘𝐴)
∧ 𝑝 ∈
(1st ‘𝐵))
→ (𝑟
+Q 𝑝) ∈ (1st ‘(𝐴 +P
𝐵)))) |
21 | 17, 20 | syl5 32 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (((𝑝 ∈
Q ∧ 𝑝
∈ (1st ‘𝐵)) ∧ (𝑟 ∈ (1st ‘𝐴) ∧ 𝑞 ∈ (2nd ‘𝐴))) → (𝑟 +Q 𝑝) ∈ (1st
‘(𝐴
+P 𝐵)))) |
22 | 21 | imdistani 442 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ ((𝑝 ∈
Q ∧ 𝑝
∈ (1st ‘𝐵)) ∧ (𝑟 ∈ (1st ‘𝐴) ∧ 𝑞 ∈ (2nd ‘𝐴)))) → ((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧
(𝑟
+Q 𝑝) ∈ (1st ‘(𝐴 +P
𝐵)))) |
23 | | addclpr 7459 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴
+P 𝐵) ∈ P) |
24 | | prop 7397 |
. . . . . . . . . . . 12
⊢ ((𝐴 +P
𝐵) ∈ P
→ 〈(1st ‘(𝐴 +P 𝐵)), (2nd
‘(𝐴
+P 𝐵))〉 ∈
P) |
25 | | prcdnql 7406 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘(𝐴 +P 𝐵)), (2nd
‘(𝐴
+P 𝐵))〉 ∈ P ∧ (𝑟 +Q
𝑝) ∈ (1st
‘(𝐴
+P 𝐵))) → (𝑞 <Q (𝑟 +Q
𝑝) → 𝑞 ∈ (1st
‘(𝐴
+P 𝐵)))) |
26 | 24, 25 | sylan 281 |
. . . . . . . . . . 11
⊢ (((𝐴 +P
𝐵) ∈ P
∧ (𝑟
+Q 𝑝) ∈ (1st ‘(𝐴 +P
𝐵))) → (𝑞 <Q
(𝑟
+Q 𝑝) → 𝑞 ∈ (1st ‘(𝐴 +P
𝐵)))) |
27 | 23, 26 | sylan 281 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑟
+Q 𝑝) ∈ (1st ‘(𝐴 +P
𝐵))) → (𝑞 <Q
(𝑟
+Q 𝑝) → 𝑞 ∈ (1st ‘(𝐴 +P
𝐵)))) |
28 | 22, 27 | syl 14 |
. . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ ((𝑝 ∈
Q ∧ 𝑝
∈ (1st ‘𝐵)) ∧ (𝑟 ∈ (1st ‘𝐴) ∧ 𝑞 ∈ (2nd ‘𝐴)))) → (𝑞 <Q (𝑟 +Q
𝑝) → 𝑞 ∈ (1st
‘(𝐴
+P 𝐵)))) |
29 | 28 | anassrs 398 |
. . . . . . . 8
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑝 ∈
Q ∧ 𝑝
∈ (1st ‘𝐵))) ∧ (𝑟 ∈ (1st ‘𝐴) ∧ 𝑞 ∈ (2nd ‘𝐴))) → (𝑞 <Q (𝑟 +Q
𝑝) → 𝑞 ∈ (1st
‘(𝐴
+P 𝐵)))) |
30 | 29 | imp 123 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑝 ∈ Q ∧ 𝑝 ∈ (1st
‘𝐵))) ∧ (𝑟 ∈ (1st
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐴))) ∧ 𝑞 <Q
(𝑟
+Q 𝑝)) → 𝑞 ∈ (1st ‘(𝐴 +P
𝐵))) |
31 | | rspe 2506 |
. . . . . . 7
⊢ ((𝑞 ∈ Q ∧
(𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘(𝐴
+P 𝐵)))) → ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝐴) ∧ 𝑞 ∈ (1st ‘(𝐴 +P
𝐵)))) |
32 | 13, 14, 30, 31 | syl12anc 1218 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑝 ∈ Q ∧ 𝑝 ∈ (1st
‘𝐵))) ∧ (𝑟 ∈ (1st
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐴))) ∧ 𝑞 <Q
(𝑟
+Q 𝑝)) → ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝐴) ∧ 𝑞 ∈ (1st ‘(𝐴 +P
𝐵)))) |
33 | | ltdfpr 7428 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
(𝐴
+P 𝐵) ∈ P) → (𝐴<P
(𝐴
+P 𝐵) ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝐴) ∧ 𝑞 ∈ (1st ‘(𝐴 +P
𝐵))))) |
34 | 23, 33 | syldan 280 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴<P (𝐴 +P
𝐵) ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘(𝐴
+P 𝐵))))) |
35 | 34 | ad3antrrr 484 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑝 ∈ Q ∧ 𝑝 ∈ (1st
‘𝐵))) ∧ (𝑟 ∈ (1st
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐴))) ∧ 𝑞 <Q
(𝑟
+Q 𝑝)) → (𝐴<P (𝐴 +P
𝐵) ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘(𝐴
+P 𝐵))))) |
36 | 32, 35 | mpbird 166 |
. . . . 5
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P) ∧ (𝑝 ∈ Q ∧ 𝑝 ∈ (1st
‘𝐵))) ∧ (𝑟 ∈ (1st
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐴))) ∧ 𝑞 <Q
(𝑟
+Q 𝑝)) → 𝐴<P (𝐴 +P
𝐵)) |
37 | 36 | ex 114 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑝 ∈
Q ∧ 𝑝
∈ (1st ‘𝐵))) ∧ (𝑟 ∈ (1st ‘𝐴) ∧ 𝑞 ∈ (2nd ‘𝐴))) → (𝑞 <Q (𝑟 +Q
𝑝) → 𝐴<P (𝐴 +P
𝐵))) |
38 | 37 | rexlimdvva 2582 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑝 ∈
Q ∧ 𝑝
∈ (1st ‘𝐵))) → (∃𝑟 ∈ (1st ‘𝐴)∃𝑞 ∈ (2nd ‘𝐴)𝑞 <Q (𝑟 +Q
𝑝) → 𝐴<P (𝐴 +P
𝐵))) |
39 | 8, 38 | mpd 13 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑝 ∈
Q ∧ 𝑝
∈ (1st ‘𝐵))) → 𝐴<P (𝐴 +P
𝐵)) |
40 | 4, 39 | rexlimddv 2579 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ 𝐴<P (𝐴 +P
𝐵)) |