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

Theorem mulextsr1lem 6516
Description: Lemma for mulextsr1 6517. (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 6403 . . . . . . 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 6378 . . . . . . . 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 912 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑍 P)
6 simp3r 915 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑉 P)
7 mulclpr 6402 . . . . . . . 8 ((𝑍 P 𝑉 P) → (𝑍 ·P 𝑉) P)
85, 6, 7syl2anc 391 . . . . . . 7 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑍 ·P 𝑉) P)
9 simp1r 911 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑌 P)
10 mulclpr 6402 . . . . . . . 8 ((𝑌 P 𝑉 P) → (𝑌 ·P 𝑉) P)
119, 6, 10syl2anc 391 . . . . . . 7 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑌 ·P 𝑉) P)
124, 8, 11caovcld 5565 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) P)
13 simp1l 910 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑋 P)
14 simp3l 914 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑈 P)
15 mulclpr 6402 . . . . . . . 8 ((𝑋 P 𝑈 P) → (𝑋 ·P 𝑈) P)
1613, 14, 15syl2anc 391 . . . . . . 7 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑋 ·P 𝑈) P)
17 simp2r 913 . . . . . . . 8 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → 𝑊 P)
18 mulclpr 6402 . . . . . . . 8 ((𝑊 P 𝑈 P) → (𝑊 ·P 𝑈) P)
1917, 14, 18syl2anc 391 . . . . . . 7 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑊 ·P 𝑈) P)
204, 16, 19caovcld 5565 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) P)
212, 12, 20caovcomd 5568 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) +P ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈))) = (((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) +P ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉))))
22 addassprg 6404 . . . . . . 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 5597 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 ·P 𝑈) +P (𝑌 ·P 𝑉)) +P ((𝑍 ·P 𝑉) +P (𝑊 ·P 𝑈))) = (((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) +P ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈))))
25 distrprg 6413 . . . . . . . 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 6405 . . . . . . . 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 5588 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊) ·P 𝑈) = ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)))
3026, 5, 9, 6, 4, 28caovdir2d 5588 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌) ·P 𝑉) = ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)))
3129, 30oveq12d 5442 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 +P 𝑊) ·P 𝑈) +P ((𝑍 +P 𝑌) ·P 𝑉)) = (((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) +P ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉))))
3221, 24, 313eqtr4d 2055 . . . 4 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 ·P 𝑈) +P (𝑌 ·P 𝑉)) +P ((𝑍 ·P 𝑉) +P (𝑊 ·P 𝑈))) = (((𝑋 +P 𝑊) ·P 𝑈) +P ((𝑍 +P 𝑌) ·P 𝑉)))
33 mulclpr 6402 . . . . . . 7 ((𝑋 P 𝑉 P) → (𝑋 ·P 𝑉) P)
3413, 6, 33syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑋 ·P 𝑉) P)
35 mulclpr 6402 . . . . . . 7 ((𝑌 P 𝑈 P) → (𝑌 ·P 𝑈) P)
369, 14, 35syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑌 ·P 𝑈) P)
37 mulclpr 6402 . . . . . . 7 ((𝑍 P 𝑈 P) → (𝑍 ·P 𝑈) P)
385, 14, 37syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑍 ·P 𝑈) P)
39 mulclpr 6402 . . . . . . 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 5597 . . . . 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 5588 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌) ·P 𝑈) = ((𝑍 ·P 𝑈) +P (𝑌 ·P 𝑈)))
4326, 13, 17, 6, 4, 28caovdir2d 5588 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊) ·P 𝑉) = ((𝑋 ·P 𝑉) +P (𝑊 ·P 𝑉)))
4442, 43oveq12d 5442 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑍 +P 𝑌) ·P 𝑈) +P ((𝑋 +P 𝑊) ·P 𝑉)) = (((𝑍 ·P 𝑈) +P (𝑌 ·P 𝑈)) +P ((𝑋 ·P 𝑉) +P (𝑊 ·P 𝑉))))
4541, 44eqtr4d 2048 . . . 4 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 ·P 𝑉) +P (𝑌 ·P 𝑈)) +P ((𝑍 ·P 𝑈) +P (𝑊 ·P 𝑉))) = (((𝑍 +P 𝑌) ·P 𝑈) +P ((𝑋 +P 𝑊) ·P 𝑉)))
4632, 45breq12d 3740 . . 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 2087 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊) ·P 𝑈) P)
4830, 12eqeltrd 2087 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌) ·P 𝑉) P)
49 addclpr 6378 . . . . . . 7 ((𝑍 P 𝑌 P) → (𝑍 +P 𝑌) P)
505, 9, 49syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑍 +P 𝑌) P)
51 mulclpr 6402 . . . . . 6 (((𝑍 +P 𝑌) P 𝑈 P) → ((𝑍 +P 𝑌) ·P 𝑈) P)
5250, 14, 51syl2anc 391 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌) ·P 𝑈) P)
53 addclpr 6378 . . . . . . 7 ((𝑋 P 𝑊 P) → (𝑋 +P 𝑊) P)
5413, 17, 53syl2anc 391 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑋 +P 𝑊) P)
55 mulclpr 6402 . . . . . 6 (((𝑋 +P 𝑊) P 𝑉 P) → ((𝑋 +P 𝑊) ·P 𝑉) P)
5654, 6, 55syl2anc 391 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊) ·P 𝑉) P)
57 addextpr 6442 . . . . 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 1117 . . . 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 6405 . . . . . . . . 9 (((𝑋 +P 𝑊) P 𝑈 P) → ((𝑋 +P 𝑊) ·P 𝑈) = (𝑈 ·P (𝑋 +P 𝑊)))
60593adant2 905 . . . . . . . 8 (((𝑋 +P 𝑊) P (𝑍 +P 𝑌) P 𝑈 P) → ((𝑋 +P 𝑊) ·P 𝑈) = (𝑈 ·P (𝑋 +P 𝑊)))
61 mulcomprg 6405 . . . . . . . . 9 (((𝑍 +P 𝑌) P 𝑈 P) → ((𝑍 +P 𝑌) ·P 𝑈) = (𝑈 ·P (𝑍 +P 𝑌)))
62613adant1 904 . . . . . . . 8 (((𝑋 +P 𝑊) P (𝑍 +P 𝑌) P 𝑈 P) → ((𝑍 +P 𝑌) ·P 𝑈) = (𝑈 ·P (𝑍 +P 𝑌)))
6360, 62breq12d 3740 . . . . . . 7 (((𝑋 +P 𝑊) P (𝑍 +P 𝑌) P 𝑈 P) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) ↔ (𝑈 ·P (𝑋 +P 𝑊))<P (𝑈 ·P (𝑍 +P 𝑌))))
64 ltmprr 6463 . . . . . . 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 1116 . . . . 5 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) → (𝑋 +P 𝑊)<P (𝑍 +P 𝑌)))
67 mulcomprg 6405 . . . . . . . 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 6405 . . . . . . . 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 3740 . . . . . 6 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (((𝑍 +P 𝑌) ·P 𝑉)<P ((𝑋 +P 𝑊) ·P 𝑉) ↔ (𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊))))
72 ltmprr 6463 . . . . . . 7 (((𝑍 +P 𝑌) P (𝑋 +P 𝑊) P 𝑉 P) → ((𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊)) → (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)))
7350, 54, 6, 72syl3anc 1116 . . . . . 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 684 . . . 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 6403 . . . . 5 ((𝑍 P 𝑌 P) → (𝑍 +P 𝑌) = (𝑌 +P 𝑍))
795, 9, 78syl2anc 391 . . . 4 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑍 +P 𝑌) = (𝑌 +P 𝑍))
8079breq2d 3739 . . 3 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑋 +P 𝑊)<P (𝑍 +P 𝑌) ↔ (𝑋 +P 𝑊)<P (𝑌 +P 𝑍)))
81 addcomprg 6403 . . . . 5 ((𝑋 P 𝑊 P) → (𝑋 +P 𝑊) = (𝑊 +P 𝑋))
8213, 17, 81syl2anc 391 . . . 4 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → (𝑋 +P 𝑊) = (𝑊 +P 𝑋))
8382breq2d 3739 . . 3 (((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((𝑍 +P 𝑌)<P (𝑋 +P 𝑊) ↔ (𝑍 +P 𝑌)<P (𝑊 +P 𝑋)))
8480, 83orbi12d 691 . 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 613   w3a 867   = wceq 1223   wcel 1366   class class class wbr 3727  (class class class)co 5424  Pcnp 6137   +P cpp 6139   ·P cmp 6140  <P cltp 6141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-13 1377  ax-14 1378  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995  ax-coll 3835  ax-sep 3838  ax-nul 3846  ax-pow 3890  ax-pr 3907  ax-un 4108  ax-setind 4192  ax-iinf 4226
This theorem depends on definitions:  df-bi 110  df-dc 727  df-3or 868  df-3an 869  df-tru 1226  df-fal 1229  df-nf 1323  df-sb 1619  df-eu 1876  df-mo 1877  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-ne 2179  df-ral 2280  df-rex 2281  df-reu 2282  df-rab 2284  df-v 2528  df-sbc 2733  df-csb 2821  df-dif 2888  df-un 2890  df-in 2892  df-ss 2899  df-nul 3193  df-pw 3325  df-sn 3345  df-pr 3346  df-op 3348  df-uni 3544  df-int 3579  df-iun 3622  df-br 3728  df-opab 3782  df-mpt 3783  df-tr 3818  df-eprel 3989  df-id 3993  df-po 3996  df-iso 3997  df-iord 4041  df-on 4043  df-suc 4046  df-iom 4229  df-xp 4266  df-rel 4267  df-cnv 4268  df-co 4269  df-dm 4270  df-rn 4271  df-res 4272  df-ima 4273  df-iota 4782  df-fun 4819  df-fn 4820  df-f 4821  df-f1 4822  df-fo 4823  df-f1o 4824  df-fv 4825  df-ov 5427  df-oprab 5428  df-mpt2 5429  df-1st 5678  df-2nd 5679  df-recs 5830  df-irdg 5866  df-1o 5904  df-2o 5905  df-oadd 5908  df-omul 5909  df-er 6005  df-ec 6007  df-qs 6011  df-ni 6150  df-pli 6151  df-mi 6152  df-lti 6153  df-plpq 6189  df-mpq 6190  df-enq 6192  df-nqqs 6193  df-plqqs 6194  df-mqqs 6195  df-1nqqs 6196  df-rq 6197  df-ltnqqs 6198  df-enq0 6265  df-nq0 6266  df-0nq0 6267  df-plq0 6268  df-mq0 6269  df-inp 6306  df-i1p 6307  df-iplp 6308  df-imp 6309  df-iltp 6310
This theorem is referenced by:  mulextsr1  6517
  Copyright terms: Public domain W3C validator