ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulextsr1lem GIF version

Theorem mulextsr1lem 7782
Description: Lemma for mulextsr1 7783. (Contributed by Jim Kingdon, 17-Feb-2020.)
Assertion
Ref Expression
mulextsr1lem (((𝑋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 𝑋))))

Proof of Theorem mulextsr1lem
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addcomprg 7580 . . . . . . 7 ((𝑓P𝑔P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
21adantl 277 . . . . . 6 ((((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) ∧ (𝑓P𝑔P)) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
3 addclpr 7539 . . . . . . . 8 ((𝑓P𝑔P) → (𝑓 +P 𝑔) ∈ P)
43adantl 277 . . . . . . 7 ((((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) ∧ (𝑓P𝑔P)) → (𝑓 +P 𝑔) ∈ P)
5 simp2l 1023 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑍P)
6 simp3r 1026 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑉P)
7 mulclpr 7574 . . . . . . . 8 ((𝑍P𝑉P) → (𝑍 ·P 𝑉) ∈ P)
85, 6, 7syl2anc 411 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑍 ·P 𝑉) ∈ P)
9 simp1r 1022 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑌P)
10 mulclpr 7574 . . . . . . . 8 ((𝑌P𝑉P) → (𝑌 ·P 𝑉) ∈ P)
119, 6, 10syl2anc 411 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑌 ·P 𝑉) ∈ P)
124, 8, 11caovcld 6031 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) ∈ P)
13 simp1l 1021 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑋P)
14 simp3l 1025 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑈P)
15 mulclpr 7574 . . . . . . . 8 ((𝑋P𝑈P) → (𝑋 ·P 𝑈) ∈ P)
1613, 14, 15syl2anc 411 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑋 ·P 𝑈) ∈ P)
17 simp2r 1024 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑊P)
18 mulclpr 7574 . . . . . . . 8 ((𝑊P𝑈P) → (𝑊 ·P 𝑈) ∈ P)
1917, 14, 18syl2anc 411 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑊 ·P 𝑈) ∈ P)
204, 16, 19caovcld 6031 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) ∈ P)
212, 12, 20caovcomd 6034 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) +P ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈))) = (((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) +P ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉))))
22 addassprg 7581 . . . . . . 7 ((𝑓P𝑔PP) → ((𝑓 +P 𝑔) +P ) = (𝑓 +P (𝑔 +P )))
2322adantl 277 . . . . . 6 ((((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) ∧ (𝑓P𝑔PP)) → ((𝑓 +P 𝑔) +P ) = (𝑓 +P (𝑔 +P )))
2416, 11, 8, 2, 23, 19, 4caov411d 6063 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 ·P 𝑈) +P (𝑌 ·P 𝑉)) +P ((𝑍 ·P 𝑉) +P (𝑊 ·P 𝑈))) = (((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) +P ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈))))
25 distrprg 7590 . . . . . . . 8 ((𝑓P𝑔PP) → (𝑓 ·P (𝑔 +P )) = ((𝑓 ·P 𝑔) +P (𝑓 ·P )))
2625adantl 277 . . . . . . 7 ((((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) ∧ (𝑓P𝑔PP)) → (𝑓 ·P (𝑔 +P )) = ((𝑓 ·P 𝑔) +P (𝑓 ·P )))
27 mulcomprg 7582 . . . . . . . 8 ((𝑓P𝑔P) → (𝑓 ·P 𝑔) = (𝑔 ·P 𝑓))
2827adantl 277 . . . . . . 7 ((((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) ∧ (𝑓P𝑔P)) → (𝑓 ·P 𝑔) = (𝑔 ·P 𝑓))
2926, 13, 17, 14, 4, 28caovdir2d 6054 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊) ·P 𝑈) = ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)))
3026, 5, 9, 6, 4, 28caovdir2d 6054 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌) ·P 𝑉) = ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)))
3129, 30oveq12d 5896 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 +P 𝑊) ·P 𝑈) +P ((𝑍 +P 𝑌) ·P 𝑉)) = (((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) +P ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉))))
3221, 24, 313eqtr4d 2220 . . . 4 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 ·P 𝑈) +P (𝑌 ·P 𝑉)) +P ((𝑍 ·P 𝑉) +P (𝑊 ·P 𝑈))) = (((𝑋 +P 𝑊) ·P 𝑈) +P ((𝑍 +P 𝑌) ·P 𝑉)))
33 mulclpr 7574 . . . . . . 7 ((𝑋P𝑉P) → (𝑋 ·P 𝑉) ∈ P)
3413, 6, 33syl2anc 411 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑋 ·P 𝑉) ∈ P)
35 mulclpr 7574 . . . . . . 7 ((𝑌P𝑈P) → (𝑌 ·P 𝑈) ∈ P)
369, 14, 35syl2anc 411 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑌 ·P 𝑈) ∈ P)
37 mulclpr 7574 . . . . . . 7 ((𝑍P𝑈P) → (𝑍 ·P 𝑈) ∈ P)
385, 14, 37syl2anc 411 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑍 ·P 𝑈) ∈ P)
39 mulclpr 7574 . . . . . . 7 ((𝑊P𝑉P) → (𝑊 ·P 𝑉) ∈ P)
4017, 6, 39syl2anc 411 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑊 ·P 𝑉) ∈ P)
4134, 36, 38, 2, 23, 40, 4caov411d 6063 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 ·P 𝑉) +P (𝑌 ·P 𝑈)) +P ((𝑍 ·P 𝑈) +P (𝑊 ·P 𝑉))) = (((𝑍 ·P 𝑈) +P (𝑌 ·P 𝑈)) +P ((𝑋 ·P 𝑉) +P (𝑊 ·P 𝑉))))
4226, 5, 9, 14, 4, 28caovdir2d 6054 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌) ·P 𝑈) = ((𝑍 ·P 𝑈) +P (𝑌 ·P 𝑈)))
4326, 13, 17, 6, 4, 28caovdir2d 6054 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊) ·P 𝑉) = ((𝑋 ·P 𝑉) +P (𝑊 ·P 𝑉)))
4442, 43oveq12d 5896 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑍 +P 𝑌) ·P 𝑈) +P ((𝑋 +P 𝑊) ·P 𝑉)) = (((𝑍 ·P 𝑈) +P (𝑌 ·P 𝑈)) +P ((𝑋 ·P 𝑉) +P (𝑊 ·P 𝑉))))
4541, 44eqtr4d 2213 . . . 4 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 ·P 𝑉) +P (𝑌 ·P 𝑈)) +P ((𝑍 ·P 𝑈) +P (𝑊 ·P 𝑉))) = (((𝑍 +P 𝑌) ·P 𝑈) +P ((𝑋 +P 𝑊) ·P 𝑉)))
4632, 45breq12d 4018 . . 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 𝑉))))
4729, 20eqeltrd 2254 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊) ·P 𝑈) ∈ P)
4830, 12eqeltrd 2254 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌) ·P 𝑉) ∈ P)
49 addclpr 7539 . . . . . . 7 ((𝑍P𝑌P) → (𝑍 +P 𝑌) ∈ P)
505, 9, 49syl2anc 411 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑍 +P 𝑌) ∈ P)
51 mulclpr 7574 . . . . . 6 (((𝑍 +P 𝑌) ∈ P𝑈P) → ((𝑍 +P 𝑌) ·P 𝑈) ∈ P)
5250, 14, 51syl2anc 411 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌) ·P 𝑈) ∈ P)
53 addclpr 7539 . . . . . . 7 ((𝑋P𝑊P) → (𝑋 +P 𝑊) ∈ P)
5413, 17, 53syl2anc 411 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑋 +P 𝑊) ∈ P)
55 mulclpr 7574 . . . . . 6 (((𝑋 +P 𝑊) ∈ P𝑉P) → ((𝑋 +P 𝑊) ·P 𝑉) ∈ P)
5654, 6, 55syl2anc 411 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊) ·P 𝑉) ∈ P)
57 addextpr 7623 . . . . 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 𝑉))))
5847, 48, 52, 56, 57syl22anc 1239 . . . 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 7582 . . . . . . . . 9 (((𝑋 +P 𝑊) ∈ P𝑈P) → ((𝑋 +P 𝑊) ·P 𝑈) = (𝑈 ·P (𝑋 +P 𝑊)))
60593adant2 1016 . . . . . . . 8 (((𝑋 +P 𝑊) ∈ P ∧ (𝑍 +P 𝑌) ∈ P𝑈P) → ((𝑋 +P 𝑊) ·P 𝑈) = (𝑈 ·P (𝑋 +P 𝑊)))
61 mulcomprg 7582 . . . . . . . . 9 (((𝑍 +P 𝑌) ∈ P𝑈P) → ((𝑍 +P 𝑌) ·P 𝑈) = (𝑈 ·P (𝑍 +P 𝑌)))
62613adant1 1015 . . . . . . . 8 (((𝑋 +P 𝑊) ∈ P ∧ (𝑍 +P 𝑌) ∈ P𝑈P) → ((𝑍 +P 𝑌) ·P 𝑈) = (𝑈 ·P (𝑍 +P 𝑌)))
6360, 62breq12d 4018 . . . . . . 7 (((𝑋 +P 𝑊) ∈ P ∧ (𝑍 +P 𝑌) ∈ P𝑈P) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) ↔ (𝑈 ·P (𝑋 +P 𝑊))<P (𝑈 ·P (𝑍 +P 𝑌))))
64 ltmprr 7644 . . . . . . 7 (((𝑋 +P 𝑊) ∈ P ∧ (𝑍 +P 𝑌) ∈ P𝑈P) → ((𝑈 ·P (𝑋 +P 𝑊))<P (𝑈 ·P (𝑍 +P 𝑌)) → (𝑋 +P 𝑊)<P (𝑍 +P 𝑌)))
6563, 64sylbid 150 . . . . . 6 (((𝑋 +P 𝑊) ∈ P ∧ (𝑍 +P 𝑌) ∈ P𝑈P) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) → (𝑋 +P 𝑊)<P (𝑍 +P 𝑌)))
6654, 50, 14, 65syl3anc 1238 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) → (𝑋 +P 𝑊)<P (𝑍 +P 𝑌)))
67 mulcomprg 7582 . . . . . . . 8 (((𝑍 +P 𝑌) ∈ P𝑉P) → ((𝑍 +P 𝑌) ·P 𝑉) = (𝑉 ·P (𝑍 +P 𝑌)))
6850, 6, 67syl2anc 411 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌) ·P 𝑉) = (𝑉 ·P (𝑍 +P 𝑌)))
69 mulcomprg 7582 . . . . . . . 8 (((𝑋 +P 𝑊) ∈ P𝑉P) → ((𝑋 +P 𝑊) ·P 𝑉) = (𝑉 ·P (𝑋 +P 𝑊)))
7054, 6, 69syl2anc 411 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊) ·P 𝑉) = (𝑉 ·P (𝑋 +P 𝑊)))
7168, 70breq12d 4018 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑍 +P 𝑌) ·P 𝑉)<P ((𝑋 +P 𝑊) ·P 𝑉) ↔ (𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊))))
72 ltmprr 7644 . . . . . . 7 (((𝑍 +P 𝑌) ∈ P ∧ (𝑋 +P 𝑊) ∈ P𝑉P) → ((𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊)) → (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)))
7350, 54, 6, 72syl3anc 1238 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊)) → (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)))
7471, 73sylbid 150 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑍 +P 𝑌) ·P 𝑉)<P ((𝑋 +P 𝑊) ·P 𝑉) → (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)))
7566, 74orim12d 786 . . . 4 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) ∨ ((𝑍 +P 𝑌) ·P 𝑉)<P ((𝑋 +P 𝑊) ·P 𝑉)) → ((𝑋 +P 𝑊)<P (𝑍 +P 𝑌) ∨ (𝑍 +P 𝑌)<P (𝑋 +P 𝑊))))
7658, 75syld 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 𝑊))))
7746, 76sylbid 150 . 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 7580 . . . . 5 ((𝑍P𝑌P) → (𝑍 +P 𝑌) = (𝑌 +P 𝑍))
795, 9, 78syl2anc 411 . . . 4 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑍 +P 𝑌) = (𝑌 +P 𝑍))
8079breq2d 4017 . . 3 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊)<P (𝑍 +P 𝑌) ↔ (𝑋 +P 𝑊)<P (𝑌 +P 𝑍)))
81 addcomprg 7580 . . . . 5 ((𝑋P𝑊P) → (𝑋 +P 𝑊) = (𝑊 +P 𝑋))
8213, 17, 81syl2anc 411 . . . 4 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑋 +P 𝑊) = (𝑊 +P 𝑋))
8382breq2d 4017 . . 3 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌)<P (𝑋 +P 𝑊) ↔ (𝑍 +P 𝑌)<P (𝑊 +P 𝑋)))
8480, 83orbi12d 793 . 2 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 +P 𝑊)<P (𝑍 +P 𝑌) ∨ (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)) ↔ ((𝑋 +P 𝑊)<P (𝑌 +P 𝑍) ∨ (𝑍 +P 𝑌)<P (𝑊 +P 𝑋))))
8577, 84sylibd 149 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 𝑋))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wo 708  w3a 978   = wceq 1353  wcel 2148   class class class wbr 4005  (class class class)co 5878  Pcnp 7293   +P cpp 7295   ·P cmp 7296  <P cltp 7297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-eprel 4291  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5881  df-oprab 5882  df-mpo 5883  df-1st 6144  df-2nd 6145  df-recs 6309  df-irdg 6374  df-1o 6420  df-2o 6421  df-oadd 6424  df-omul 6425  df-er 6538  df-ec 6540  df-qs 6544  df-ni 7306  df-pli 7307  df-mi 7308  df-lti 7309  df-plpq 7346  df-mpq 7347  df-enq 7349  df-nqqs 7350  df-plqqs 7351  df-mqqs 7352  df-1nqqs 7353  df-rq 7354  df-ltnqqs 7355  df-enq0 7426  df-nq0 7427  df-0nq0 7428  df-plq0 7429  df-mq0 7430  df-inp 7468  df-i1p 7469  df-iplp 7470  df-imp 7471  df-iltp 7472
This theorem is referenced by:  mulextsr1  7783
  Copyright terms: Public domain W3C validator