HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem distrlem4pr 5110
Description: Lemma for distributive law for positive reals.
Assertion
Ref Expression
distrlem4pr |- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ ((x e. A /\ f e. A) /\ (y e. B /\ z e. C))) -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C)))
Distinct variable groups:   x,y,z,f,A   x,B,y,z,f   x,C,y,z,f
Proof of Theorem distrlem4pr
StepHypRef Expression
1 distrlem3pr 5109 . . . . 5 |- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ (f e. A /\ (y e. B /\ z e. C))) -> (f e. Q. /\ (y e. Q. /\ z e. Q.)))
2 visset 1809 . . . . . . . 8 |- x e. V
3 visset 1809 . . . . . . . 8 |- f e. V
4 visset 1809 . . . . . . . . 9 |- w e. V
5 visset 1809 . . . . . . . . 9 |- v e. V
64, 5ltmpq 5057 . . . . . . . 8 |- (u e. Q. -> (w <Q v <-> (u .Q w) <Q (u .Q v)))
7 visset 1809 . . . . . . . 8 |- y e. V
84, 5mulcompq 5044 . . . . . . . 8 |- (w .Q v) = (v .Q w)
92, 3, 6, 7, 8caoprord2 4049 . . . . . . 7 |- (y e. Q. -> (x <Q f <-> (x .Q y) <Q (f .Q y)))
10 mulclpq 5040 . . . . . . . 8 |- ((f e. Q. /\ z e. Q.) -> (f .Q z) e. Q.)
11 oprex 3974 . . . . . . . . 9 |- (x .Q y) e. V
12 oprex 3974 . . . . . . . . 9 |- (f .Q y) e. V
134, 5ltapq 5056 . . . . . . . . 9 |- (u e. Q. -> (w <Q v <-> (u +Q w) <Q (u +Q v)))
14 oprex 3974 . . . . . . . . 9 |- (f .Q z) e. V
154, 5addcompq 5042 . . . . . . . . 9 |- (w +Q v) = (v +Q w)
1611, 12, 13, 14, 15caoprord2 4049 . . . . . . . 8 |- ((f .Q z) e. Q. -> ((x .Q y) <Q (f .Q y) <-> ((x .Q y) +Q (f .Q z)) <Q ((f .Q y) +Q (f .Q z))))
1710, 16syl 10 . . . . . . 7 |- ((f e. Q. /\ z e. Q.) -> ((x .Q y) <Q (f .Q y) <-> ((x .Q y) +Q (f .Q z)) <Q ((f .Q y) +Q (f .Q z))))
189, 17sylan9bb 539 . . . . . 6 |- ((y e. Q. /\ (f e. Q. /\ z e. Q.)) -> (x <Q f <-> ((x .Q y) +Q (f .Q z)) <Q ((f .Q y) +Q (f .Q z))))
1918an1s 486 . . . . 5 |- ((f e. Q. /\ (y e. Q. /\ z e. Q.)) -> (x <Q f <-> ((x .Q y) +Q (f .Q z)) <Q ((f .Q y) +Q (f .Q z))))
201, 19syl 10 . . . 4 |- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ (f e. A /\ (y e. B /\ z e. C))) -> (x <Q f <-> ((x .Q y) +Q (f .Q z)) <Q ((f .Q y) +Q (f .Q z))))
21 distrlem2pr 5108 . . . . . 6 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> ((f e. A /\ (y e. B /\ z e. C)) -> ((f .Q y) +Q (f .Q z)) e. (A .P. (B +P. C))))
22 mulclpr 5102 . . . . . . . 8 |- ((A e. P. /\ (B +P. C) e. P.) -> (A .P. (B +P. C)) e. P.)
23 addclpr 5100 . . . . . . . 8 |- ((B e. P. /\ C e. P.) -> (B +P. C) e. P.)
2422, 23sylan2 451 . . . . . . 7 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (A .P. (B +P. C)) e. P.)
25 prcdpq 5077 . . . . . . . 8 |- (((A .P. (B +P. C)) e. P. /\ ((f .Q y) +Q (f .Q z)) e. (A .P. (B +P. C))) -> (((x .Q y) +Q (f .Q z)) <Q ((f .Q y) +Q (f .Q z)) -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C))))
2625ex 373 . . . . . . 7 |- ((A .P. (B +P. C)) e. P. -> (((f .Q y) +Q (f .Q z)) e. (A .P. (B +P. C)) -> (((x .Q y) +Q (f .Q z)) <Q ((f .Q y) +Q (f .Q z)) -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C)))))
2724, 26syl 10 . . . . . 6 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (((f .Q y) +Q (f .Q z)) e. (A .P. (B +P. C)) -> (((x .Q y) +Q (f .Q z)) <Q ((f .Q y) +Q (f .Q z)) -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C)))))
2821, 27syld 27 . . . . 5 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> ((f e. A /\ (y e. B /\ z e. C)) -> (((x .Q y) +Q (f .Q z)) <Q ((f .Q y) +Q (f .Q z)) -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C)))))
2928imp 350 . . . 4 |- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ (f e. A /\ (y e. B /\ z e. C))) -> (((x .Q y) +Q (f .Q z)) <Q ((f .Q y) +Q (f .Q z)) -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C))))
3020, 29sylbid 203 . . 3 |- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ (f e. A /\ (y e. B /\ z e. C))) -> (x <Q f -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C))))
3130adantrll 400 . 2 |- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ ((x e. A /\ f e. A) /\ (y e. B /\ z e. C))) -> (x <Q f -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C))))
32 distrlem3pr 5109 . . . . 5 |- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ (x e. A /\ (y e. B /\ z e. C))) -> (x e. Q. /\ (y e. Q. /\ z e. Q.)))
33 visset 1809 . . . . . . . 8 |- z e. V
343, 2, 6, 33, 8caoprord2 4049 . . . . . . 7 |- (z e. Q. -> (f <Q x <-> (f .Q z) <Q (x .Q z)))
35 mulclpq 5040 . . . . . . . 8 |- ((x e. Q. /\ y e. Q.) -> (x .Q y) e. Q.)
36 oprex 3974 . . . . . . . . 9 |- (x .Q z) e. V
3714, 36ltapq 5056 . . . . . . . 8 |- ((x .Q y) e. Q. -> ((f .Q z) <Q (x .Q z) <-> ((x .Q y) +Q (f .Q z)) <Q ((x .Q y) +Q (x .Q z))))
3835, 37syl 10 . . . . . . 7 |- ((x e. Q. /\ y e. Q.) -> ((f .Q z) <Q (x .Q z) <-> ((x .Q y) +Q (f .Q z)) <Q ((x .Q y) +Q (x .Q z))))
3934, 38sylan9bbr 540 . . . . . 6 |- (((x e. Q. /\ y e. Q.) /\ z e. Q.) -> (f <Q x <-> ((x .Q y) +Q (f .Q z)) <Q ((x .Q y) +Q (x .Q z))))
4039anasss 440 . . . . 5 |- ((x e. Q. /\ (y e. Q. /\ z e. Q.)) -> (f <Q x <-> ((x .Q y) +Q (f .Q z)) <Q ((x .Q y) +Q (x .Q z))))
4132, 40syl 10 . . . 4 |- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ (x e. A /\ (y e. B /\ z e. C))) -> (f <Q x <-> ((x .Q y) +Q (f .Q z)) <Q ((x .Q y) +Q (x .Q z))))
42 distrlem2pr 5108 . . . . . 6 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> ((x e. A /\ (y e. B /\ z e. C)) -> ((x .Q y) +Q (x .Q z)) e. (A .P. (B +P. C))))
43 prcdpq 5077 . . . . . . . 8 |- (((A .P. (B +P. C)) e. P. /\ ((x .Q y) +Q (x .Q z)) e. (A .P. (B +P. C))) -> (((x .Q y) +Q (f .Q z)) <Q ((x .Q y) +Q (x .Q z)) -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C))))
4443ex 373 . . . . . . 7 |- ((A .P. (B +P. C)) e. P. -> (((x .Q y) +Q (x .Q z)) e. (A .P. (B +P. C)) -> (((x .Q y) +Q (f .Q z)) <Q ((x .Q y) +Q (x .Q z)) -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C)))))
4524, 44syl 10 . . . . . 6 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (((x .Q y) +Q (x .Q z)) e. (A .P. (B +P. C)) -> (((x .Q y) +Q (f .Q z)) <Q ((x .Q y) +Q (x .Q z)) -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C)))))
4642, 45syld 27 . . . . 5 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> ((x e. A