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

Theorem mulextsr1lem 6706
 Description: Lemma for mulextsr1 6707. (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 f g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addcomprg 6554 . . . . . . 7 ((f P g P) → (f +P g) = (g +P f))
21adantl 262 . . . . . 6 ((((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) (f P g P)) → (f +P g) = (g +P f))
3 addclpr 6520 . . . . . . . 8 ((f P g P) → (f +P g) P)
43adantl 262 . . . . . . 7 ((((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) (f P g P)) → (f +P g) P)
5 simp2l 929 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑍 P)
6 simp3r 932 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑉 P)
7 mulclpr 6553 . . . . . . . 8 ((𝑍 P 𝑉 P) → (𝑍 ·P 𝑉) P)
85, 6, 7syl2anc 391 . . . . . . 7 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑍 ·P 𝑉) P)
9 simp1r 928 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑌 P)
10 mulclpr 6553 . . . . . . . 8 ((𝑌 P 𝑉 P) → (𝑌 ·P 𝑉) P)
119, 6, 10syl2anc 391 . . . . . . 7 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑌 ·P 𝑉) P)
124, 8, 11caovcld 5596 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) P)
13 simp1l 927 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑋 P)
14 simp3l 931 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑈 P)
15 mulclpr 6553 . . . . . . . 8 ((𝑋 P 𝑈 P) → (𝑋 ·P 𝑈) P)
1613, 14, 15syl2anc 391 . . . . . . 7 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑋 ·P 𝑈) P)
17 simp2r 930 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑊 P)
18 mulclpr 6553 . . . . . . . 8 ((𝑊 P 𝑈 P) → (𝑊 ·P 𝑈) P)
1917, 14, 18syl2anc 391 . . . . . . 7 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑊 ·P 𝑈) P)
204, 16, 19caovcld 5596 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) P)
212, 12, 20caovcomd 5599 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) +P ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈))) = (((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) +P ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉))))
22 addassprg 6555 . . . . . . 7 ((f P g P P) → ((f +P g) +P ) = (f +P (g +P )))
2322adantl 262 . . . . . 6 ((((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) (f P g P P)) → ((f +P g) +P ) = (f +P (g +P )))
2416, 11, 8, 2, 23, 19, 4caov411d 5628 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 ·P 𝑈) +P (𝑌 ·P 𝑉)) +P ((𝑍 ·P 𝑉) +P (𝑊 ·P 𝑈))) = (((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) +P ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈))))
25 distrprg 6564 . . . . . . . 8 ((f P g P P) → (f ·P (g +P )) = ((f ·P g) +P (f ·P )))
2625adantl 262 . . . . . . 7 ((((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) (f P g P P)) → (f ·P (g +P )) = ((f ·P g) +P (f ·P )))
27 mulcomprg 6556 . . . . . . . 8 ((f P g P) → (f ·P g) = (g ·P f))
2827adantl 262 . . . . . . 7 ((((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) (f P g P)) → (f ·P g) = (g ·P f))
2926, 13, 17, 14, 4, 28caovdir2d 5619 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊) ·P 𝑈) = ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)))
3026, 5, 9, 6, 4, 28caovdir2d 5619 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌) ·P 𝑉) = ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)))
3129, 30oveq12d 5473 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 +P 𝑊) ·P 𝑈) +P ((𝑍 +P 𝑌) ·P 𝑉)) = (((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) +P ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉))))
3221, 24, 313eqtr4d 2079 . . . 4 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 ·P 𝑈) +P (𝑌 ·P 𝑉)) +P ((𝑍 ·P 𝑉) +P (𝑊 ·P 𝑈))) = (((𝑋 +P 𝑊) ·P 𝑈) +P ((𝑍 +P 𝑌) ·P 𝑉)))
33 mulclpr 6553 . . . . . . 7 ((𝑋 P 𝑉 P) → (𝑋 ·P 𝑉) P)
3413, 6, 33syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑋 ·P 𝑉) P)
35 mulclpr 6553 . . . . . . 7 ((𝑌 P 𝑈 P) → (𝑌 ·P 𝑈) P)
369, 14, 35syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑌 ·P 𝑈) P)
37 mulclpr 6553 . . . . . . 7 ((𝑍 P 𝑈 P) → (𝑍 ·P 𝑈) P)
385, 14, 37syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑍 ·P 𝑈) P)
39 mulclpr 6553 . . . . . . 7 ((𝑊 P 𝑉 P) → (𝑊 ·P 𝑉) P)
4017, 6, 39syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑊 ·P 𝑉) P)
4134, 36, 38, 2, 23, 40, 4caov411d 5628 . . . . 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 5619 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌) ·P 𝑈) = ((𝑍 ·P 𝑈) +P (𝑌 ·P 𝑈)))
4326, 13, 17, 6, 4, 28caovdir2d 5619 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊) ·P 𝑉) = ((𝑋 ·P 𝑉) +P (𝑊 ·P 𝑉)))
4442, 43oveq12d 5473 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑍 +P 𝑌) ·P 𝑈) +P ((𝑋 +P 𝑊) ·P 𝑉)) = (((𝑍 ·P 𝑈) +P (𝑌 ·P 𝑈)) +P ((𝑋 ·P 𝑉) +P (𝑊 ·P 𝑉))))
4541, 44eqtr4d 2072 . . . 4 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 ·P 𝑉) +P (𝑌 ·P 𝑈)) +P ((𝑍 ·P 𝑈) +P (𝑊 ·P 𝑉))) = (((𝑍 +P 𝑌) ·P 𝑈) +P ((𝑋 +P 𝑊) ·P 𝑉)))
4632, 45breq12d 3768 . . 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 2111 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊) ·P 𝑈) P)
4830, 12eqeltrd 2111 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌) ·P 𝑉) P)
49 addclpr 6520 . . . . . . 7 ((𝑍 P 𝑌 P) → (𝑍 +P 𝑌) P)
505, 9, 49syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑍 +P 𝑌) P)
51 mulclpr 6553 . . . . . 6 (((𝑍 +P 𝑌) P 𝑈 P) → ((𝑍 +P 𝑌) ·P 𝑈) P)
5250, 14, 51syl2anc 391 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌) ·P 𝑈) P)
53 addclpr 6520 . . . . . . 7 ((𝑋 P 𝑊 P) → (𝑋 +P 𝑊) P)
5413, 17, 53syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑋 +P 𝑊) P)
55 mulclpr 6553 . . . . . 6 (((𝑋 +P 𝑊) P 𝑉 P) → ((𝑋 +P 𝑊) ·P 𝑉) P)
5654, 6, 55syl2anc 391 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊) ·P 𝑉) P)
57 addextpr 6593 . . . . 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 1135 . . . 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 6556 . . . . . . . . 9 (((𝑋 +P 𝑊) P 𝑈 P) → ((𝑋 +P 𝑊) ·P 𝑈) = (𝑈 ·P (𝑋 +P 𝑊)))
60593adant2 922 . . . . . . . 8 (((𝑋 +P 𝑊) P (𝑍 +P 𝑌) P 𝑈 P) → ((𝑋 +P 𝑊) ·P 𝑈) = (𝑈 ·P (𝑋 +P 𝑊)))
61 mulcomprg 6556 . . . . . . . . 9 (((𝑍 +P 𝑌) P 𝑈 P) → ((𝑍 +P 𝑌) ·P 𝑈) = (𝑈 ·P (𝑍 +P 𝑌)))
62613adant1 921 . . . . . . . 8 (((𝑋 +P 𝑊) P (𝑍 +P 𝑌) P 𝑈 P) → ((𝑍 +P 𝑌) ·P 𝑈) = (𝑈 ·P (𝑍 +P 𝑌)))
6360, 62breq12d 3768 . . . . . . 7 (((𝑋 +P 𝑊) P (𝑍 +P 𝑌) P 𝑈 P) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) ↔ (𝑈 ·P (𝑋 +P 𝑊))<P (𝑈 ·P (𝑍 +P 𝑌))))
64 ltmprr 6614 . . . . . . 7 (((𝑋 +P 𝑊) P (𝑍 +P 𝑌) P 𝑈 P) → ((𝑈 ·P (𝑋 +P 𝑊))<P (𝑈 ·P (𝑍 +P 𝑌)) → (𝑋 +P 𝑊)<P (𝑍 +P 𝑌)))
6563, 64sylbid 139 . . . . . 6 (((𝑋 +P 𝑊) P (𝑍 +P 𝑌) P 𝑈 P) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) → (𝑋 +P 𝑊)<P (𝑍 +P 𝑌)))
6654, 50, 14, 65syl3anc 1134 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) → (𝑋 +P 𝑊)<P (𝑍 +P 𝑌)))
67 mulcomprg 6556 . . . . . . . 8 (((𝑍 +P 𝑌) P 𝑉 P) → ((𝑍 +P 𝑌) ·P 𝑉) = (𝑉 ·P (𝑍 +P 𝑌)))
6850, 6, 67syl2anc 391 . . . . . . 7 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌) ·P 𝑉) = (𝑉 ·P (𝑍 +P 𝑌)))
69 mulcomprg 6556 . . . . . . . 8 (((𝑋 +P 𝑊) P 𝑉 P) → ((𝑋 +P 𝑊) ·P 𝑉) = (𝑉 ·P (𝑋 +P 𝑊)))
7054, 6, 69syl2anc 391 . . . . . . 7 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊) ·P 𝑉) = (𝑉 ·P (𝑋 +P 𝑊)))
7168, 70breq12d 3768 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑍 +P 𝑌) ·P 𝑉)<P ((𝑋 +P 𝑊) ·P 𝑉) ↔ (𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊))))
72 ltmprr 6614 . . . . . . 7 (((𝑍 +P 𝑌) P (𝑋 +P 𝑊) P 𝑉 P) → ((𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊)) → (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)))
7350, 54, 6, 72syl3anc 1134 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊)) → (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)))
7471, 73sylbid 139 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑍 +P 𝑌) ·P 𝑉)<P ((𝑋 +P 𝑊) ·P 𝑉) → (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)))
7566, 74orim12d 699 . . . 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 40 . . 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 139 . 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 6554 . . . . 5 ((𝑍 P 𝑌 P) → (𝑍 +P 𝑌) = (𝑌 +P 𝑍))
795, 9, 78syl2anc 391 . . . 4 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑍 +P 𝑌) = (𝑌 +P 𝑍))
8079breq2d 3767 . . 3 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊)<P (𝑍 +P 𝑌) ↔ (𝑋 +P 𝑊)<P (𝑌 +P 𝑍)))
81 addcomprg 6554 . . . . 5 ((𝑋 P 𝑊 P) → (𝑋 +P 𝑊) = (𝑊 +P 𝑋))
8213, 17, 81syl2anc 391 . . . 4 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑋 +P 𝑊) = (𝑊 +P 𝑋))
8382breq2d 3767 . . 3 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌)<P (𝑋 +P 𝑊) ↔ (𝑍 +P 𝑌)<P (𝑊 +P 𝑋)))
8480, 83orbi12d 706 . 2 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 +P 𝑊)<P (𝑍 +P 𝑌) (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)) ↔ ((𝑋 +P 𝑊)<P (𝑌 +P 𝑍) (𝑍 +P 𝑌)<P (𝑊 +P 𝑋))))
8577, 84sylibd 138 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 97   ∨ wo 628   ∧ w3a 884   = wceq 1242   ∈ wcel 1390   class class class wbr 3755  (class class class)co 5455  Pcnp 6275   +P cpp 6277   ·P cmp 6278
 Copyright terms: Public domain W3C validator