Step | Hyp | Ref
| Expression |
1 | | prop 7437 |
. . . . . . 7
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
2 | | prnminu 7451 |
. . . . . . 7
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑣 ∈ (2nd
‘𝐵)) →
∃𝑟 ∈
(2nd ‘𝐵)𝑟 <Q 𝑣) |
3 | 1, 2 | sylan 281 |
. . . . . 6
⊢ ((𝐵 ∈ P ∧
𝑣 ∈ (2nd
‘𝐵)) →
∃𝑟 ∈
(2nd ‘𝐵)𝑟 <Q 𝑣) |
4 | 3 | 3ad2antl2 1155 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ 𝑣
∈ (2nd ‘𝐵)) → ∃𝑟 ∈ (2nd ‘𝐵)𝑟 <Q 𝑣) |
5 | 4 | adantlr 474 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) → ∃𝑟 ∈ (2nd
‘𝐵)𝑟 <Q 𝑣) |
6 | | simprr 527 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) → 𝑟 <Q 𝑣) |
7 | | ltexnqi 7371 |
. . . . . 6
⊢ (𝑟 <Q
𝑣 → ∃𝑤 ∈ Q (𝑟 +Q
𝑤) = 𝑣) |
8 | 6, 7 | syl 14 |
. . . . 5
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) → ∃𝑤 ∈ Q (𝑟 +Q
𝑤) = 𝑣) |
9 | | simprl 526 |
. . . . . . 7
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) → 𝑤 ∈ Q) |
10 | | halfnqq 7372 |
. . . . . . 7
⊢ (𝑤 ∈ Q →
∃𝑡 ∈
Q (𝑡
+Q 𝑡) = 𝑤) |
11 | 9, 10 | syl 14 |
. . . . . 6
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) → ∃𝑡 ∈ Q (𝑡 +Q 𝑡) = 𝑤) |
12 | | prop 7437 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
13 | | prarloc2 7466 |
. . . . . . . . . . . . . 14
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑡 ∈ Q) →
∃𝑢 ∈
(1st ‘𝐴)(𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) |
14 | 12, 13 | sylan 281 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝑡 ∈ Q)
→ ∃𝑢 ∈
(1st ‘𝐴)(𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) |
15 | 14 | adantrr 476 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
(𝑡 ∈ Q
∧ (𝑡
+Q 𝑡) = 𝑤)) → ∃𝑢 ∈ (1st ‘𝐴)(𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) |
16 | 15 | 3ad2antl1 1154 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑡
∈ Q ∧ (𝑡 +Q 𝑡) = 𝑤)) → ∃𝑢 ∈ (1st ‘𝐴)(𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) |
17 | 16 | adantlr 474 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) → ∃𝑢 ∈ (1st ‘𝐴)(𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) |
18 | 17 | adantlr 474 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) → ∃𝑢 ∈ (1st ‘𝐴)(𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) |
19 | 18 | adantlr 474 |
. . . . . . . 8
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) → ∃𝑢 ∈ (1st ‘𝐴)(𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) |
20 | 19 | adantlr 474 |
. . . . . . 7
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) → ∃𝑢 ∈ (1st ‘𝐴)(𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) |
21 | | simplll 528 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) → (𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈
P)) |
22 | 21 | ad3antrrr 489 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P)) |
23 | 22 | simp1d 1004 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝐴 ∈
P) |
24 | 22 | simp2d 1005 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝐵 ∈
P) |
25 | | addclpr 7499 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴
+P 𝐵) ∈ P) |
26 | 23, 24, 25 | syl2anc 409 |
. . . . . . . . . . 11
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝐴 +P
𝐵) ∈
P) |
27 | | prop 7437 |
. . . . . . . . . . 11
⊢ ((𝐴 +P
𝐵) ∈ P
→ 〈(1st ‘(𝐴 +P 𝐵)), (2nd
‘(𝐴
+P 𝐵))〉 ∈
P) |
28 | 26, 27 | syl 14 |
. . . . . . . . . 10
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) →
〈(1st ‘(𝐴 +P 𝐵)), (2nd
‘(𝐴
+P 𝐵))〉 ∈
P) |
29 | 23, 12 | syl 14 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
30 | | simprl 526 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑢 ∈ (1st
‘𝐴)) |
31 | | elprnql 7443 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑢 ∈ (1st
‘𝐴)) → 𝑢 ∈
Q) |
32 | 29, 30, 31 | syl2anc 409 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑢 ∈
Q) |
33 | | simplrl 530 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑡 ∈
Q) |
34 | | addclnq 7337 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ Q ∧
𝑡 ∈ Q)
→ (𝑢
+Q 𝑡) ∈ Q) |
35 | 32, 33, 34 | syl2anc 409 |
. . . . . . . . . . 11
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝑢 +Q
𝑡) ∈
Q) |
36 | 24, 1 | syl 14 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
37 | | simprl 526 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) → 𝑟 ∈ (2nd ‘𝐵)) |
38 | 37 | ad3antrrr 489 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑟 ∈ (2nd
‘𝐵)) |
39 | | elprnqu 7444 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑟 ∈ (2nd
‘𝐵)) → 𝑟 ∈
Q) |
40 | 36, 38, 39 | syl2anc 409 |
. . . . . . . . . . 11
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑟 ∈
Q) |
41 | | addclnq 7337 |
. . . . . . . . . . 11
⊢ (((𝑢 +Q
𝑡) ∈ Q
∧ 𝑟 ∈
Q) → ((𝑢
+Q 𝑡) +Q 𝑟) ∈
Q) |
42 | 35, 40, 41 | syl2anc 409 |
. . . . . . . . . 10
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ Q) |
43 | | prdisj 7454 |
. . . . . . . . . 10
⊢
((〈(1st ‘(𝐴 +P 𝐵)), (2nd
‘(𝐴
+P 𝐵))〉 ∈ P ∧
((𝑢
+Q 𝑡) +Q 𝑟) ∈ Q) →
¬ (((𝑢
+Q 𝑡) +Q 𝑟) ∈ (1st
‘(𝐴
+P 𝐵)) ∧ ((𝑢 +Q 𝑡) +Q
𝑟) ∈ (2nd
‘(𝐴
+P 𝐵)))) |
44 | 28, 42, 43 | syl2anc 409 |
. . . . . . . . 9
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ¬
(((𝑢
+Q 𝑡) +Q 𝑟) ∈ (1st
‘(𝐴
+P 𝐵)) ∧ ((𝑢 +Q 𝑡) +Q
𝑟) ∈ (2nd
‘(𝐴
+P 𝐵)))) |
45 | | addassnqg 7344 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Q ∧
𝑡 ∈ Q
∧ 𝑟 ∈
Q) → ((𝑢
+Q 𝑡) +Q 𝑟) = (𝑢 +Q (𝑡 +Q
𝑟))) |
46 | 32, 33, 40, 45 | syl3anc 1233 |
. . . . . . . . . . . . . 14
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ((𝑢 +Q
𝑡)
+Q 𝑟) = (𝑢 +Q (𝑡 +Q
𝑟))) |
47 | | addcomnqg 7343 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ Q ∧
𝑟 ∈ Q)
→ (𝑡
+Q 𝑟) = (𝑟 +Q 𝑡)) |
48 | 47 | oveq2d 5869 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ Q ∧
𝑟 ∈ Q)
→ (𝑢
+Q (𝑡 +Q 𝑟)) = (𝑢 +Q (𝑟 +Q
𝑡))) |
49 | 33, 40, 48 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝑢 +Q
(𝑡
+Q 𝑟)) = (𝑢 +Q (𝑟 +Q
𝑡))) |
50 | 46, 49 | eqtrd 2203 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ((𝑢 +Q
𝑡)
+Q 𝑟) = (𝑢 +Q (𝑟 +Q
𝑡))) |
51 | 50 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → ((𝑢 +Q
𝑡)
+Q 𝑟) = (𝑢 +Q (𝑟 +Q
𝑡))) |
52 | | simplrl 530 |
. . . . . . . . . . . . 13
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → 𝑢 ∈ (1st
‘𝐴)) |
53 | | simpr 109 |
. . . . . . . . . . . . 13
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) |
54 | 23 | adantr 274 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → 𝐴 ∈
P) |
55 | 22 | simp3d 1006 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝐶 ∈
P) |
56 | 55 | adantr 274 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → 𝐶 ∈
P) |
57 | | df-iplp 7430 |
. . . . . . . . . . . . . . 15
⊢
+P = (𝑞 ∈ P, 𝑠 ∈ P ↦ 〈{𝑓 ∈ Q ∣
∃𝑔 ∈
Q ∃ℎ
∈ Q (𝑔
∈ (1st ‘𝑞) ∧ ℎ ∈ (1st ‘𝑠) ∧ 𝑓 = (𝑔 +Q ℎ))}, {𝑓 ∈ Q ∣ ∃𝑔 ∈ Q
∃ℎ ∈
Q (𝑔 ∈
(2nd ‘𝑞)
∧ ℎ ∈
(2nd ‘𝑠)
∧ 𝑓 = (𝑔 +Q
ℎ))}〉) |
58 | | addclnq 7337 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
59 | 57, 58 | genpprecll 7476 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ ((𝑢 ∈
(1st ‘𝐴)
∧ (𝑟
+Q 𝑡) ∈ (1st ‘𝐶)) → (𝑢 +Q (𝑟 +Q
𝑡)) ∈ (1st
‘(𝐴
+P 𝐶)))) |
60 | 54, 56, 59 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → ((𝑢 ∈ (1st
‘𝐴) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → (𝑢 +Q
(𝑟
+Q 𝑡)) ∈ (1st ‘(𝐴 +P
𝐶)))) |
61 | 52, 53, 60 | mp2and 431 |
. . . . . . . . . . . 12
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → (𝑢 +Q
(𝑟
+Q 𝑡)) ∈ (1st ‘(𝐴 +P
𝐶))) |
62 | 51, 61 | eqeltrd 2247 |
. . . . . . . . . . 11
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (1st ‘(𝐴 +P
𝐶))) |
63 | | fveq2 5496 |
. . . . . . . . . . . . 13
⊢ ((𝐴 +P
𝐵) = (𝐴 +P 𝐶) → (1st
‘(𝐴
+P 𝐵)) = (1st ‘(𝐴 +P
𝐶))) |
64 | 63 | eleq2d 2240 |
. . . . . . . . . . . 12
⊢ ((𝐴 +P
𝐵) = (𝐴 +P 𝐶) → (((𝑢 +Q 𝑡) +Q
𝑟) ∈ (1st
‘(𝐴
+P 𝐵)) ↔ ((𝑢 +Q 𝑡) +Q
𝑟) ∈ (1st
‘(𝐴
+P 𝐶)))) |
65 | 64 | ad7antlr 498 |
. . . . . . . . . . 11
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → (((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (1st ‘(𝐴 +P
𝐵)) ↔ ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (1st ‘(𝐴 +P
𝐶)))) |
66 | 62, 65 | mpbird 166 |
. . . . . . . . . 10
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (1st ‘(𝐴 +P
𝐵))) |
67 | 57, 58 | genppreclu 7477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (((𝑢
+Q 𝑡) ∈ (2nd ‘𝐴) ∧ 𝑟 ∈ (2nd ‘𝐵)) → ((𝑢 +Q 𝑡) +Q
𝑟) ∈ (2nd
‘(𝐴
+P 𝐵)))) |
68 | 67 | ancomsd 267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑟 ∈
(2nd ‘𝐵)
∧ (𝑢
+Q 𝑡) ∈ (2nd ‘𝐴)) → ((𝑢 +Q 𝑡) +Q
𝑟) ∈ (2nd
‘(𝐴
+P 𝐵)))) |
69 | 68 | 3adant3 1012 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑟
∈ (2nd ‘𝐵) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (2nd ‘(𝐴 +P
𝐵)))) |
70 | 69 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) → ((𝑟 ∈ (2nd ‘𝐵) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (2nd ‘(𝐴 +P
𝐵)))) |
71 | 70 | imp 123 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (2nd ‘(𝐴 +P
𝐵))) |
72 | 71 | adantrlr 482 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ ((𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (2nd ‘(𝐴 +P
𝐵))) |
73 | 72 | anassrs 398 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (2nd ‘(𝐴 +P
𝐵))) |
74 | 73 | ad2ant2rl 508 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (2nd ‘(𝐴 +P
𝐵))) |
75 | 74 | adantlr 474 |
. . . . . . . . . . 11
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (2nd ‘(𝐴 +P
𝐵))) |
76 | 75 | adantr 274 |
. . . . . . . . . 10
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (2nd ‘(𝐴 +P
𝐵))) |
77 | 66, 76 | jca 304 |
. . . . . . . . 9
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶)) → (((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (1st ‘(𝐴 +P
𝐵)) ∧ ((𝑢 +Q
𝑡)
+Q 𝑟) ∈ (2nd ‘(𝐴 +P
𝐵)))) |
78 | 44, 77 | mtand 660 |
. . . . . . . 8
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ¬
(𝑟
+Q 𝑡) ∈ (1st ‘𝐶)) |
79 | | prop 7437 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ P →
〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈
P) |
80 | 55, 79 | syl 14 |
. . . . . . . . . 10
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) →
〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈
P) |
81 | | ltaddnq 7369 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Q ∧
𝑡 ∈ Q)
→ 𝑡
<Q (𝑡 +Q 𝑡)) |
82 | 33, 33, 81 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑡 <Q
(𝑡
+Q 𝑡)) |
83 | | simplrr 531 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝑡 +Q
𝑡) = 𝑤) |
84 | 82, 83 | breqtrd 4015 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑡 <Q
𝑤) |
85 | | ltanqi 7364 |
. . . . . . . . . . . 12
⊢ ((𝑡 <Q
𝑤 ∧ 𝑟 ∈ Q) → (𝑟 +Q
𝑡)
<Q (𝑟 +Q 𝑤)) |
86 | 84, 40, 85 | syl2anc 409 |
. . . . . . . . . . 11
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝑟 +Q
𝑡)
<Q (𝑟 +Q 𝑤)) |
87 | | simprr 527 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) → (𝑟 +Q 𝑤) = 𝑣) |
88 | 87 | ad2antrr 485 |
. . . . . . . . . . 11
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝑟 +Q
𝑤) = 𝑣) |
89 | 86, 88 | breqtrd 4015 |
. . . . . . . . . 10
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝑟 +Q
𝑡)
<Q 𝑣) |
90 | | prloc 7453 |
. . . . . . . . . 10
⊢
((〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈ P ∧ (𝑟 +Q
𝑡)
<Q 𝑣) → ((𝑟 +Q 𝑡) ∈ (1st
‘𝐶) ∨ 𝑣 ∈ (2nd
‘𝐶))) |
91 | 80, 89, 90 | syl2anc 409 |
. . . . . . . . 9
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ((𝑟 +Q
𝑡) ∈ (1st
‘𝐶) ∨ 𝑣 ∈ (2nd
‘𝐶))) |
92 | 91 | orcomd 724 |
. . . . . . . 8
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝑣 ∈ (2nd
‘𝐶) ∨ (𝑟 +Q
𝑡) ∈ (1st
‘𝐶))) |
93 | 78, 92 | ecased 1344 |
. . . . . . 7
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑣 ∈ (2nd
‘𝐶)) |
94 | 20, 93 | rexlimddv 2592 |
. . . . . 6
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) ∧ (𝑡 ∈ Q ∧ (𝑡 +Q
𝑡) = 𝑤)) → 𝑣 ∈ (2nd ‘𝐶)) |
95 | 11, 94 | rexlimddv 2592 |
. . . . 5
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) ∧ (𝑤 ∈ Q ∧ (𝑟 +Q
𝑤) = 𝑣)) → 𝑣 ∈ (2nd ‘𝐶)) |
96 | 8, 95 | rexlimddv 2592 |
. . . 4
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) ∧ (𝑟 ∈ (2nd ‘𝐵) ∧ 𝑟 <Q 𝑣)) → 𝑣 ∈ (2nd ‘𝐶)) |
97 | 5, 96 | rexlimddv 2592 |
. . 3
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (2nd ‘𝐵)) → 𝑣 ∈ (2nd ‘𝐶)) |
98 | 97 | ex 114 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) → (𝑣 ∈ (2nd ‘𝐵) → 𝑣 ∈ (2nd ‘𝐶))) |
99 | 98 | ssrdv 3153 |
1
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) → (2nd
‘𝐵) ⊆
(2nd ‘𝐶)) |