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

Theorem mulextsr1lem 7694
 Description: Lemma for mulextsr1 7695. (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 7492 . . . . . . 7 ((𝑓P𝑔P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
21adantl 275 . . . . . 6 ((((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) ∧ (𝑓P𝑔P)) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
3 addclpr 7451 . . . . . . . 8 ((𝑓P𝑔P) → (𝑓 +P 𝑔) ∈ P)
43adantl 275 . . . . . . 7 ((((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) ∧ (𝑓P𝑔P)) → (𝑓 +P 𝑔) ∈ P)
5 simp2l 1008 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑍P)
6 simp3r 1011 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑉P)
7 mulclpr 7486 . . . . . . . 8 ((𝑍P𝑉P) → (𝑍 ·P 𝑉) ∈ P)
85, 6, 7syl2anc 409 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑍 ·P 𝑉) ∈ P)
9 simp1r 1007 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑌P)
10 mulclpr 7486 . . . . . . . 8 ((𝑌P𝑉P) → (𝑌 ·P 𝑉) ∈ P)
119, 6, 10syl2anc 409 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑌 ·P 𝑉) ∈ P)
124, 8, 11caovcld 5971 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) ∈ P)
13 simp1l 1006 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑋P)
14 simp3l 1010 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑈P)
15 mulclpr 7486 . . . . . . . 8 ((𝑋P𝑈P) → (𝑋 ·P 𝑈) ∈ P)
1613, 14, 15syl2anc 409 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑋 ·P 𝑈) ∈ P)
17 simp2r 1009 . . . . . . . 8 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → 𝑊P)
18 mulclpr 7486 . . . . . . . 8 ((𝑊P𝑈P) → (𝑊 ·P 𝑈) ∈ P)
1917, 14, 18syl2anc 409 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑊 ·P 𝑈) ∈ P)
204, 16, 19caovcld 5971 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) ∈ P)
212, 12, 20caovcomd 5974 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) +P ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈))) = (((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) +P ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉))))
22 addassprg 7493 . . . . . . 7 ((𝑓P𝑔PP) → ((𝑓 +P 𝑔) +P ) = (𝑓 +P (𝑔 +P )))
2322adantl 275 . . . . . 6 ((((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) ∧ (𝑓P𝑔PP)) → ((𝑓 +P 𝑔) +P ) = (𝑓 +P (𝑔 +P )))
2416, 11, 8, 2, 23, 19, 4caov411d 6003 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 ·P 𝑈) +P (𝑌 ·P 𝑉)) +P ((𝑍 ·P 𝑉) +P (𝑊 ·P 𝑈))) = (((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)) +P ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈))))
25 distrprg 7502 . . . . . . . 8 ((𝑓P𝑔PP) → (𝑓 ·P (𝑔 +P )) = ((𝑓 ·P 𝑔) +P (𝑓 ·P )))
2625adantl 275 . . . . . . 7 ((((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) ∧ (𝑓P𝑔PP)) → (𝑓 ·P (𝑔 +P )) = ((𝑓 ·P 𝑔) +P (𝑓 ·P )))
27 mulcomprg 7494 . . . . . . . 8 ((𝑓P𝑔P) → (𝑓 ·P 𝑔) = (𝑔 ·P 𝑓))
2827adantl 275 . . . . . . 7 ((((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) ∧ (𝑓P𝑔P)) → (𝑓 ·P 𝑔) = (𝑔 ·P 𝑓))
2926, 13, 17, 14, 4, 28caovdir2d 5994 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊) ·P 𝑈) = ((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)))
3026, 5, 9, 6, 4, 28caovdir2d 5994 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌) ·P 𝑉) = ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉)))
3129, 30oveq12d 5839 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 +P 𝑊) ·P 𝑈) +P ((𝑍 +P 𝑌) ·P 𝑉)) = (((𝑋 ·P 𝑈) +P (𝑊 ·P 𝑈)) +P ((𝑍 ·P 𝑉) +P (𝑌 ·P 𝑉))))
3221, 24, 313eqtr4d 2200 . . . 4 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 ·P 𝑈) +P (𝑌 ·P 𝑉)) +P ((𝑍 ·P 𝑉) +P (𝑊 ·P 𝑈))) = (((𝑋 +P 𝑊) ·P 𝑈) +P ((𝑍 +P 𝑌) ·P 𝑉)))
33 mulclpr 7486 . . . . . . 7 ((𝑋P𝑉P) → (𝑋 ·P 𝑉) ∈ P)
3413, 6, 33syl2anc 409 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑋 ·P 𝑉) ∈ P)
35 mulclpr 7486 . . . . . . 7 ((𝑌P𝑈P) → (𝑌 ·P 𝑈) ∈ P)
369, 14, 35syl2anc 409 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑌 ·P 𝑈) ∈ P)
37 mulclpr 7486 . . . . . . 7 ((𝑍P𝑈P) → (𝑍 ·P 𝑈) ∈ P)
385, 14, 37syl2anc 409 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑍 ·P 𝑈) ∈ P)
39 mulclpr 7486 . . . . . . 7 ((𝑊P𝑉P) → (𝑊 ·P 𝑉) ∈ P)
4017, 6, 39syl2anc 409 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑊 ·P 𝑉) ∈ P)
4134, 36, 38, 2, 23, 40, 4caov411d 6003 . . . . 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 5994 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌) ·P 𝑈) = ((𝑍 ·P 𝑈) +P (𝑌 ·P 𝑈)))
4326, 13, 17, 6, 4, 28caovdir2d 5994 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊) ·P 𝑉) = ((𝑋 ·P 𝑉) +P (𝑊 ·P 𝑉)))
4442, 43oveq12d 5839 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑍 +P 𝑌) ·P 𝑈) +P ((𝑋 +P 𝑊) ·P 𝑉)) = (((𝑍 ·P 𝑈) +P (𝑌 ·P 𝑈)) +P ((𝑋 ·P 𝑉) +P (𝑊 ·P 𝑉))))
4541, 44eqtr4d 2193 . . . 4 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 ·P 𝑉) +P (𝑌 ·P 𝑈)) +P ((𝑍 ·P 𝑈) +P (𝑊 ·P 𝑉))) = (((𝑍 +P 𝑌) ·P 𝑈) +P ((𝑋 +P 𝑊) ·P 𝑉)))
4632, 45breq12d 3978 . . 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 2234 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊) ·P 𝑈) ∈ P)
4830, 12eqeltrd 2234 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌) ·P 𝑉) ∈ P)
49 addclpr 7451 . . . . . . 7 ((𝑍P𝑌P) → (𝑍 +P 𝑌) ∈ P)
505, 9, 49syl2anc 409 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑍 +P 𝑌) ∈ P)
51 mulclpr 7486 . . . . . 6 (((𝑍 +P 𝑌) ∈ P𝑈P) → ((𝑍 +P 𝑌) ·P 𝑈) ∈ P)
5250, 14, 51syl2anc 409 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌) ·P 𝑈) ∈ P)
53 addclpr 7451 . . . . . . 7 ((𝑋P𝑊P) → (𝑋 +P 𝑊) ∈ P)
5413, 17, 53syl2anc 409 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑋 +P 𝑊) ∈ P)
55 mulclpr 7486 . . . . . 6 (((𝑋 +P 𝑊) ∈ P𝑉P) → ((𝑋 +P 𝑊) ·P 𝑉) ∈ P)
5654, 6, 55syl2anc 409 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊) ·P 𝑉) ∈ P)
57 addextpr 7535 . . . . 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 1221 . . . 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 7494 . . . . . . . . 9 (((𝑋 +P 𝑊) ∈ P𝑈P) → ((𝑋 +P 𝑊) ·P 𝑈) = (𝑈 ·P (𝑋 +P 𝑊)))
60593adant2 1001 . . . . . . . 8 (((𝑋 +P 𝑊) ∈ P ∧ (𝑍 +P 𝑌) ∈ P𝑈P) → ((𝑋 +P 𝑊) ·P 𝑈) = (𝑈 ·P (𝑋 +P 𝑊)))
61 mulcomprg 7494 . . . . . . . . 9 (((𝑍 +P 𝑌) ∈ P𝑈P) → ((𝑍 +P 𝑌) ·P 𝑈) = (𝑈 ·P (𝑍 +P 𝑌)))
62613adant1 1000 . . . . . . . 8 (((𝑋 +P 𝑊) ∈ P ∧ (𝑍 +P 𝑌) ∈ P𝑈P) → ((𝑍 +P 𝑌) ·P 𝑈) = (𝑈 ·P (𝑍 +P 𝑌)))
6360, 62breq12d 3978 . . . . . . 7 (((𝑋 +P 𝑊) ∈ P ∧ (𝑍 +P 𝑌) ∈ P𝑈P) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) ↔ (𝑈 ·P (𝑋 +P 𝑊))<P (𝑈 ·P (𝑍 +P 𝑌))))
64 ltmprr 7556 . . . . . . 7 (((𝑋 +P 𝑊) ∈ P ∧ (𝑍 +P 𝑌) ∈ P𝑈P) → ((𝑈 ·P (𝑋 +P 𝑊))<P (𝑈 ·P (𝑍 +P 𝑌)) → (𝑋 +P 𝑊)<P (𝑍 +P 𝑌)))
6563, 64sylbid 149 . . . . . 6 (((𝑋 +P 𝑊) ∈ P ∧ (𝑍 +P 𝑌) ∈ P𝑈P) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) → (𝑋 +P 𝑊)<P (𝑍 +P 𝑌)))
6654, 50, 14, 65syl3anc 1220 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 +P 𝑊) ·P 𝑈)<P ((𝑍 +P 𝑌) ·P 𝑈) → (𝑋 +P 𝑊)<P (𝑍 +P 𝑌)))
67 mulcomprg 7494 . . . . . . . 8 (((𝑍 +P 𝑌) ∈ P𝑉P) → ((𝑍 +P 𝑌) ·P 𝑉) = (𝑉 ·P (𝑍 +P 𝑌)))
6850, 6, 67syl2anc 409 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌) ·P 𝑉) = (𝑉 ·P (𝑍 +P 𝑌)))
69 mulcomprg 7494 . . . . . . . 8 (((𝑋 +P 𝑊) ∈ P𝑉P) → ((𝑋 +P 𝑊) ·P 𝑉) = (𝑉 ·P (𝑋 +P 𝑊)))
7054, 6, 69syl2anc 409 . . . . . . 7 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊) ·P 𝑉) = (𝑉 ·P (𝑋 +P 𝑊)))
7168, 70breq12d 3978 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑍 +P 𝑌) ·P 𝑉)<P ((𝑋 +P 𝑊) ·P 𝑉) ↔ (𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊))))
72 ltmprr 7556 . . . . . . 7 (((𝑍 +P 𝑌) ∈ P ∧ (𝑋 +P 𝑊) ∈ P𝑉P) → ((𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊)) → (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)))
7350, 54, 6, 72syl3anc 1220 . . . . . 6 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑉 ·P (𝑍 +P 𝑌))<P (𝑉 ·P (𝑋 +P 𝑊)) → (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)))
7471, 73sylbid 149 . . . . 5 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑍 +P 𝑌) ·P 𝑉)<P ((𝑋 +P 𝑊) ·P 𝑉) → (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)))
7566, 74orim12d 776 . . . 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 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 7492 . . . . 5 ((𝑍P𝑌P) → (𝑍 +P 𝑌) = (𝑌 +P 𝑍))
795, 9, 78syl2anc 409 . . . 4 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑍 +P 𝑌) = (𝑌 +P 𝑍))
8079breq2d 3977 . . 3 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑋 +P 𝑊)<P (𝑍 +P 𝑌) ↔ (𝑋 +P 𝑊)<P (𝑌 +P 𝑍)))
81 addcomprg 7492 . . . . 5 ((𝑋P𝑊P) → (𝑋 +P 𝑊) = (𝑊 +P 𝑋))
8213, 17, 81syl2anc 409 . . . 4 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (𝑋 +P 𝑊) = (𝑊 +P 𝑋))
8382breq2d 3977 . . 3 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → ((𝑍 +P 𝑌)<P (𝑋 +P 𝑊) ↔ (𝑍 +P 𝑌)<P (𝑊 +P 𝑋)))
8480, 83orbi12d 783 . 2 (((𝑋P𝑌P) ∧ (𝑍P𝑊P) ∧ (𝑈P𝑉P)) → (((𝑋 +P 𝑊)<P (𝑍 +P 𝑌) ∨ (𝑍 +P 𝑌)<P (𝑋 +P 𝑊)) ↔ ((𝑋 +P 𝑊)<P (𝑌 +P 𝑍) ∨ (𝑍 +P 𝑌)<P (𝑊 +P 𝑋))))
8577, 84sylibd 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 𝑋))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 698   ∧ w3a 963   = wceq 1335   ∈ wcel 2128   class class class wbr 3965  (class class class)co 5821  Pcnp 7205   +P cpp 7207   ·P cmp 7208
 Copyright terms: Public domain W3C validator