Step | Hyp | Ref
| Expression |
1 | | addcomprg 7540 |
. . . . . . 7
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
2 | 1 | adantl 275 |
. . . . . 6
⊢ ((((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P)) → (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
3 | | addclpr 7499 |
. . . . . . . 8
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓
+P 𝑔) ∈ P) |
4 | 3 | adantl 275 |
. . . . . . 7
⊢ ((((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P)) → (𝑓
+P 𝑔) ∈ P) |
5 | | simp2l 1018 |
. . . . . . . 8
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
𝑍 ∈
P) |
6 | | simp3r 1021 |
. . . . . . . 8
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
𝑉 ∈
P) |
7 | | mulclpr 7534 |
. . . . . . . 8
⊢ ((𝑍 ∈ P ∧
𝑉 ∈ P)
→ (𝑍
·P 𝑉) ∈ P) |
8 | 5, 6, 7 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑍
·P 𝑉) ∈ P) |
9 | | simp1r 1017 |
. . . . . . . 8
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
𝑌 ∈
P) |
10 | | mulclpr 7534 |
. . . . . . . 8
⊢ ((𝑌 ∈ P ∧
𝑉 ∈ P)
→ (𝑌
·P 𝑉) ∈ P) |
11 | 9, 6, 10 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑌
·P 𝑉) ∈ P) |
12 | 4, 8, 11 | caovcld 6006 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑍
·P 𝑉) +P (𝑌
·P 𝑉)) ∈ P) |
13 | | simp1l 1016 |
. . . . . . . 8
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
𝑋 ∈
P) |
14 | | simp3l 1020 |
. . . . . . . 8
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
𝑈 ∈
P) |
15 | | mulclpr 7534 |
. . . . . . . 8
⊢ ((𝑋 ∈ P ∧
𝑈 ∈ P)
→ (𝑋
·P 𝑈) ∈ P) |
16 | 13, 14, 15 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑋
·P 𝑈) ∈ P) |
17 | | simp2r 1019 |
. . . . . . . 8
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
𝑊 ∈
P) |
18 | | mulclpr 7534 |
. . . . . . . 8
⊢ ((𝑊 ∈ P ∧
𝑈 ∈ P)
→ (𝑊
·P 𝑈) ∈ P) |
19 | 17, 14, 18 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑊
·P 𝑈) ∈ P) |
20 | 4, 16, 19 | caovcld 6006 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑋
·P 𝑈) +P (𝑊
·P 𝑈)) ∈ P) |
21 | 2, 12, 20 | caovcomd 6009 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑍
·P 𝑉) +P (𝑌
·P 𝑉)) +P ((𝑋
·P 𝑈) +P (𝑊
·P 𝑈))) = (((𝑋 ·P 𝑈) +P
(𝑊
·P 𝑈)) +P ((𝑍
·P 𝑉) +P (𝑌
·P 𝑉)))) |
22 | | addassprg 7541 |
. . . . . . 7
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P
∧ ℎ ∈
P) → ((𝑓
+P 𝑔) +P ℎ) = (𝑓 +P (𝑔 +P
ℎ))) |
23 | 22 | adantl 275 |
. . . . . 6
⊢ ((((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P ∧ ℎ
∈ P)) → ((𝑓 +P 𝑔) +P
ℎ) = (𝑓 +P (𝑔 +P
ℎ))) |
24 | 16, 11, 8, 2, 23, 19, 4 | caov411d 6038 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑋
·P 𝑈) +P (𝑌
·P 𝑉)) +P ((𝑍
·P 𝑉) +P (𝑊
·P 𝑈))) = (((𝑍 ·P 𝑉) +P
(𝑌
·P 𝑉)) +P ((𝑋
·P 𝑈) +P (𝑊
·P 𝑈)))) |
25 | | distrprg 7550 |
. . . . . . . 8
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P
∧ ℎ ∈
P) → (𝑓
·P (𝑔 +P ℎ)) = ((𝑓 ·P 𝑔) +P
(𝑓
·P ℎ))) |
26 | 25 | adantl 275 |
. . . . . . 7
⊢ ((((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P ∧ ℎ
∈ P)) → (𝑓 ·P (𝑔 +P
ℎ)) = ((𝑓 ·P 𝑔) +P
(𝑓
·P ℎ))) |
27 | | mulcomprg 7542 |
. . . . . . . 8
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓
·P 𝑔) = (𝑔 ·P 𝑓)) |
28 | 27 | adantl 275 |
. . . . . . 7
⊢ ((((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P)) → (𝑓
·P 𝑔) = (𝑔 ·P 𝑓)) |
29 | 26, 13, 17, 14, 4, 28 | caovdir2d 6029 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑋
+P 𝑊) ·P 𝑈) = ((𝑋 ·P 𝑈) +P
(𝑊
·P 𝑈))) |
30 | 26, 5, 9, 6, 4, 28 | caovdir2d 6029 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑍
+P 𝑌) ·P 𝑉) = ((𝑍 ·P 𝑉) +P
(𝑌
·P 𝑉))) |
31 | 29, 30 | oveq12d 5871 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑋
+P 𝑊) ·P 𝑈) +P
((𝑍
+P 𝑌) ·P 𝑉)) = (((𝑋 ·P 𝑈) +P
(𝑊
·P 𝑈)) +P ((𝑍
·P 𝑉) +P (𝑌
·P 𝑉)))) |
32 | 21, 24, 31 | 3eqtr4d 2213 |
. . . 4
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑋
·P 𝑈) +P (𝑌
·P 𝑉)) +P ((𝑍
·P 𝑉) +P (𝑊
·P 𝑈))) = (((𝑋 +P 𝑊)
·P 𝑈) +P ((𝑍 +P
𝑌)
·P 𝑉))) |
33 | | mulclpr 7534 |
. . . . . . 7
⊢ ((𝑋 ∈ P ∧
𝑉 ∈ P)
→ (𝑋
·P 𝑉) ∈ P) |
34 | 13, 6, 33 | syl2anc 409 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑋
·P 𝑉) ∈ P) |
35 | | mulclpr 7534 |
. . . . . . 7
⊢ ((𝑌 ∈ P ∧
𝑈 ∈ P)
→ (𝑌
·P 𝑈) ∈ P) |
36 | 9, 14, 35 | syl2anc 409 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑌
·P 𝑈) ∈ P) |
37 | | mulclpr 7534 |
. . . . . . 7
⊢ ((𝑍 ∈ P ∧
𝑈 ∈ P)
→ (𝑍
·P 𝑈) ∈ P) |
38 | 5, 14, 37 | syl2anc 409 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑍
·P 𝑈) ∈ P) |
39 | | mulclpr 7534 |
. . . . . . 7
⊢ ((𝑊 ∈ P ∧
𝑉 ∈ P)
→ (𝑊
·P 𝑉) ∈ P) |
40 | 17, 6, 39 | syl2anc 409 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑊
·P 𝑉) ∈ P) |
41 | 34, 36, 38, 2, 23, 40, 4 | caov411d 6038 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑋
·P 𝑉) +P (𝑌
·P 𝑈)) +P ((𝑍
·P 𝑈) +P (𝑊
·P 𝑉))) = (((𝑍 ·P 𝑈) +P
(𝑌
·P 𝑈)) +P ((𝑋
·P 𝑉) +P (𝑊
·P 𝑉)))) |
42 | 26, 5, 9, 14, 4, 28 | caovdir2d 6029 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑍
+P 𝑌) ·P 𝑈) = ((𝑍 ·P 𝑈) +P
(𝑌
·P 𝑈))) |
43 | 26, 13, 17, 6, 4, 28 | caovdir2d 6029 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑋
+P 𝑊) ·P 𝑉) = ((𝑋 ·P 𝑉) +P
(𝑊
·P 𝑉))) |
44 | 42, 43 | oveq12d 5871 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑍
+P 𝑌) ·P 𝑈) +P
((𝑋
+P 𝑊) ·P 𝑉)) = (((𝑍 ·P 𝑈) +P
(𝑌
·P 𝑈)) +P ((𝑋
·P 𝑉) +P (𝑊
·P 𝑉)))) |
45 | 41, 44 | eqtr4d 2206 |
. . . 4
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑋
·P 𝑉) +P (𝑌
·P 𝑈)) +P ((𝑍
·P 𝑈) +P (𝑊
·P 𝑉))) = (((𝑍 +P 𝑌)
·P 𝑈) +P ((𝑋 +P
𝑊)
·P 𝑉))) |
46 | 32, 45 | breq12d 4002 |
. . 3
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((((𝑋
·P 𝑈) +P (𝑌
·P 𝑉)) +P ((𝑍
·P 𝑉) +P (𝑊
·P 𝑈)))<P (((𝑋
·P 𝑉) +P (𝑌
·P 𝑈)) +P ((𝑍
·P 𝑈) +P (𝑊
·P 𝑉))) ↔ (((𝑋 +P 𝑊)
·P 𝑈) +P ((𝑍 +P
𝑌)
·P 𝑉))<P (((𝑍 +P
𝑌)
·P 𝑈) +P ((𝑋 +P
𝑊)
·P 𝑉)))) |
47 | 29, 20 | eqeltrd 2247 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑋
+P 𝑊) ·P 𝑈) ∈
P) |
48 | 30, 12 | eqeltrd 2247 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑍
+P 𝑌) ·P 𝑉) ∈
P) |
49 | | addclpr 7499 |
. . . . . . 7
⊢ ((𝑍 ∈ P ∧
𝑌 ∈ P)
→ (𝑍
+P 𝑌) ∈ P) |
50 | 5, 9, 49 | syl2anc 409 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑍
+P 𝑌) ∈ P) |
51 | | mulclpr 7534 |
. . . . . 6
⊢ (((𝑍 +P
𝑌) ∈ P
∧ 𝑈 ∈
P) → ((𝑍
+P 𝑌) ·P 𝑈) ∈
P) |
52 | 50, 14, 51 | syl2anc 409 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑍
+P 𝑌) ·P 𝑈) ∈
P) |
53 | | addclpr 7499 |
. . . . . . 7
⊢ ((𝑋 ∈ P ∧
𝑊 ∈ P)
→ (𝑋
+P 𝑊) ∈ P) |
54 | 13, 17, 53 | syl2anc 409 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑋
+P 𝑊) ∈ P) |
55 | | mulclpr 7534 |
. . . . . 6
⊢ (((𝑋 +P
𝑊) ∈ P
∧ 𝑉 ∈
P) → ((𝑋
+P 𝑊) ·P 𝑉) ∈
P) |
56 | 54, 6, 55 | syl2anc 409 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑋
+P 𝑊) ·P 𝑉) ∈
P) |
57 | | addextpr 7583 |
. . . . 5
⊢
(((((𝑋
+P 𝑊) ·P 𝑈) ∈ P ∧
((𝑍
+P 𝑌) ·P 𝑉) ∈ P) ∧
(((𝑍
+P 𝑌) ·P 𝑈) ∈ P ∧
((𝑋
+P 𝑊) ·P 𝑉) ∈ P))
→ ((((𝑋
+P 𝑊) ·P 𝑈) +P
((𝑍
+P 𝑌) ·P 𝑉))<P
(((𝑍
+P 𝑌) ·P 𝑈) +P
((𝑋
+P 𝑊) ·P 𝑉)) → (((𝑋 +P 𝑊)
·P 𝑈)<P ((𝑍 +P
𝑌)
·P 𝑈) ∨ ((𝑍 +P 𝑌)
·P 𝑉)<P ((𝑋 +P
𝑊)
·P 𝑉)))) |
58 | 47, 48, 52, 56, 57 | syl22anc 1234 |
. . . 4
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((((𝑋
+P 𝑊) ·P 𝑈) +P
((𝑍
+P 𝑌) ·P 𝑉))<P
(((𝑍
+P 𝑌) ·P 𝑈) +P
((𝑋
+P 𝑊) ·P 𝑉)) → (((𝑋 +P 𝑊)
·P 𝑈)<P ((𝑍 +P
𝑌)
·P 𝑈) ∨ ((𝑍 +P 𝑌)
·P 𝑉)<P ((𝑋 +P
𝑊)
·P 𝑉)))) |
59 | | mulcomprg 7542 |
. . . . . . . . 9
⊢ (((𝑋 +P
𝑊) ∈ P
∧ 𝑈 ∈
P) → ((𝑋
+P 𝑊) ·P 𝑈) = (𝑈 ·P (𝑋 +P
𝑊))) |
60 | 59 | 3adant2 1011 |
. . . . . . . 8
⊢ (((𝑋 +P
𝑊) ∈ P
∧ (𝑍
+P 𝑌) ∈ P ∧ 𝑈 ∈ P) →
((𝑋
+P 𝑊) ·P 𝑈) = (𝑈 ·P (𝑋 +P
𝑊))) |
61 | | mulcomprg 7542 |
. . . . . . . . 9
⊢ (((𝑍 +P
𝑌) ∈ P
∧ 𝑈 ∈
P) → ((𝑍
+P 𝑌) ·P 𝑈) = (𝑈 ·P (𝑍 +P
𝑌))) |
62 | 61 | 3adant1 1010 |
. . . . . . . 8
⊢ (((𝑋 +P
𝑊) ∈ P
∧ (𝑍
+P 𝑌) ∈ P ∧ 𝑈 ∈ P) →
((𝑍
+P 𝑌) ·P 𝑈) = (𝑈 ·P (𝑍 +P
𝑌))) |
63 | 60, 62 | breq12d 4002 |
. . . . . . 7
⊢ (((𝑋 +P
𝑊) ∈ P
∧ (𝑍
+P 𝑌) ∈ P ∧ 𝑈 ∈ P) →
(((𝑋
+P 𝑊) ·P 𝑈)<P
((𝑍
+P 𝑌) ·P 𝑈) ↔ (𝑈 ·P (𝑋 +P
𝑊))<P (𝑈
·P (𝑍 +P 𝑌)))) |
64 | | ltmprr 7604 |
. . . . . . 7
⊢ (((𝑋 +P
𝑊) ∈ P
∧ (𝑍
+P 𝑌) ∈ P ∧ 𝑈 ∈ P) →
((𝑈
·P (𝑋 +P 𝑊))<P
(𝑈
·P (𝑍 +P 𝑌)) → (𝑋 +P 𝑊)<P
(𝑍
+P 𝑌))) |
65 | 63, 64 | sylbid 149 |
. . . . . 6
⊢ (((𝑋 +P
𝑊) ∈ P
∧ (𝑍
+P 𝑌) ∈ P ∧ 𝑈 ∈ P) →
(((𝑋
+P 𝑊) ·P 𝑈)<P
((𝑍
+P 𝑌) ·P 𝑈) → (𝑋 +P 𝑊)<P
(𝑍
+P 𝑌))) |
66 | 54, 50, 14, 65 | syl3anc 1233 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑋
+P 𝑊) ·P 𝑈)<P
((𝑍
+P 𝑌) ·P 𝑈) → (𝑋 +P 𝑊)<P
(𝑍
+P 𝑌))) |
67 | | mulcomprg 7542 |
. . . . . . . 8
⊢ (((𝑍 +P
𝑌) ∈ P
∧ 𝑉 ∈
P) → ((𝑍
+P 𝑌) ·P 𝑉) = (𝑉 ·P (𝑍 +P
𝑌))) |
68 | 50, 6, 67 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑍
+P 𝑌) ·P 𝑉) = (𝑉 ·P (𝑍 +P
𝑌))) |
69 | | mulcomprg 7542 |
. . . . . . . 8
⊢ (((𝑋 +P
𝑊) ∈ P
∧ 𝑉 ∈
P) → ((𝑋
+P 𝑊) ·P 𝑉) = (𝑉 ·P (𝑋 +P
𝑊))) |
70 | 54, 6, 69 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑋
+P 𝑊) ·P 𝑉) = (𝑉 ·P (𝑋 +P
𝑊))) |
71 | 68, 70 | breq12d 4002 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑍
+P 𝑌) ·P 𝑉)<P
((𝑋
+P 𝑊) ·P 𝑉) ↔ (𝑉 ·P (𝑍 +P
𝑌))<P (𝑉
·P (𝑋 +P 𝑊)))) |
72 | | ltmprr 7604 |
. . . . . . 7
⊢ (((𝑍 +P
𝑌) ∈ P
∧ (𝑋
+P 𝑊) ∈ P ∧ 𝑉 ∈ P) →
((𝑉
·P (𝑍 +P 𝑌))<P
(𝑉
·P (𝑋 +P 𝑊)) → (𝑍 +P 𝑌)<P
(𝑋
+P 𝑊))) |
73 | 50, 54, 6, 72 | syl3anc 1233 |
. . . . . 6
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑉
·P (𝑍 +P 𝑌))<P
(𝑉
·P (𝑋 +P 𝑊)) → (𝑍 +P 𝑌)<P
(𝑋
+P 𝑊))) |
74 | 71, 73 | sylbid 149 |
. . . . 5
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑍
+P 𝑌) ·P 𝑉)<P
((𝑋
+P 𝑊) ·P 𝑉) → (𝑍 +P 𝑌)<P
(𝑋
+P 𝑊))) |
75 | 66, 74 | orim12d 781 |
. . . 4
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((((𝑋
+P 𝑊) ·P 𝑈)<P
((𝑍
+P 𝑌) ·P 𝑈) ∨ ((𝑍 +P 𝑌)
·P 𝑉)<P ((𝑋 +P
𝑊)
·P 𝑉)) → ((𝑋 +P 𝑊)<P
(𝑍
+P 𝑌) ∨ (𝑍 +P 𝑌)<P
(𝑋
+P 𝑊)))) |
76 | 58, 75 | syld 45 |
. . 3
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((((𝑋
+P 𝑊) ·P 𝑈) +P
((𝑍
+P 𝑌) ·P 𝑉))<P
(((𝑍
+P 𝑌) ·P 𝑈) +P
((𝑋
+P 𝑊) ·P 𝑉)) → ((𝑋 +P 𝑊)<P
(𝑍
+P 𝑌) ∨ (𝑍 +P 𝑌)<P
(𝑋
+P 𝑊)))) |
77 | 46, 76 | sylbid 149 |
. 2
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((((𝑋
·P 𝑈) +P (𝑌
·P 𝑉)) +P ((𝑍
·P 𝑉) +P (𝑊
·P 𝑈)))<P (((𝑋
·P 𝑉) +P (𝑌
·P 𝑈)) +P ((𝑍
·P 𝑈) +P (𝑊
·P 𝑉))) → ((𝑋 +P 𝑊)<P
(𝑍
+P 𝑌) ∨ (𝑍 +P 𝑌)<P
(𝑋
+P 𝑊)))) |
78 | | addcomprg 7540 |
. . . . 5
⊢ ((𝑍 ∈ P ∧
𝑌 ∈ P)
→ (𝑍
+P 𝑌) = (𝑌 +P 𝑍)) |
79 | 5, 9, 78 | syl2anc 409 |
. . . 4
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑍
+P 𝑌) = (𝑌 +P 𝑍)) |
80 | 79 | breq2d 4001 |
. . 3
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑋
+P 𝑊)<P (𝑍 +P
𝑌) ↔ (𝑋 +P
𝑊)<P (𝑌 +P
𝑍))) |
81 | | addcomprg 7540 |
. . . . 5
⊢ ((𝑋 ∈ P ∧
𝑊 ∈ P)
→ (𝑋
+P 𝑊) = (𝑊 +P 𝑋)) |
82 | 13, 17, 81 | syl2anc 409 |
. . . 4
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(𝑋
+P 𝑊) = (𝑊 +P 𝑋)) |
83 | 82 | breq2d 4001 |
. . 3
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((𝑍
+P 𝑌)<P (𝑋 +P
𝑊) ↔ (𝑍 +P
𝑌)<P (𝑊 +P
𝑋))) |
84 | 80, 83 | orbi12d 788 |
. 2
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
(((𝑋
+P 𝑊)<P (𝑍 +P
𝑌) ∨ (𝑍 +P 𝑌)<P
(𝑋
+P 𝑊)) ↔ ((𝑋 +P 𝑊)<P
(𝑌
+P 𝑍) ∨ (𝑍 +P 𝑌)<P
(𝑊
+P 𝑋)))) |
85 | 77, 84 | sylibd 148 |
1
⊢ (((𝑋 ∈ P ∧
𝑌 ∈ P)
∧ (𝑍 ∈
P ∧ 𝑊
∈ P) ∧ (𝑈 ∈ P ∧ 𝑉 ∈ P)) →
((((𝑋
·P 𝑈) +P (𝑌
·P 𝑉)) +P ((𝑍
·P 𝑉) +P (𝑊
·P 𝑈)))<P (((𝑋
·P 𝑉) +P (𝑌
·P 𝑈)) +P ((𝑍
·P 𝑈) +P (𝑊
·P 𝑉))) → ((𝑋 +P 𝑊)<P
(𝑌
+P 𝑍) ∨ (𝑍 +P 𝑌)<P
(𝑊
+P 𝑋)))) |