Theorem mulgt0sr 5214

Description: The product of two positive signed reals is positive.

Hypotheses

Ref	Expression
mulgt0sr.1	|- A e. V
mulgt0sr.2	|- B e. V

Assertion

Ref	Expression
mulgt0sr	|- ((0R <R A /\ 0R <R B) -> 0R <R (A .R B))

Proof of Theorem mulgt0sr

Step	Hyp	Ref	Expression
1		mulgt0sr.1	. . . . 5 |- A e. V
2		ltrelsr 5180	. . . . 5 |- <R (_ (R. X. R.)
3	1, 2	brel 3223	. . . 4 |- (0R <R A -> (0R e. R. /\ A e. R.))
4	3	pm3.27d 325	. . 3 |- (0R <R A -> A e. R.)
5		mulgt0sr.2	. . . . 5 |- B e. V
6	5, 2	brel 3223	. . . 4 |- (0R <R B -> (0R e. R. /\ B e. R.))
7	6	pm3.27d 325	. . 3 |- (0R <R B -> B e. R.)
8	4, 7	anim12i 333	. 2 |- ((0R <R A /\ 0R <R B) -> (A e. R. /\ B e. R.))
9		df-nr 5167	. . 3 |- R. = ((P. X. P.)/. ~R )
10		breq2 2623	. . . . 5 |- ([<.x, y>.] ~R = A -> (0R <R [<.x, y>.] ~R <-> 0R <R A))
11	10	anbi1d 617	. . . 4 |- ([<.x, y>.] ~R = A -> ((0R <R [<.x, y>.] ~R /\ 0R <R [<.z, w>.] ~R ) <-> (0R <R A /\ 0R <R [<.z, w>.] ~R )))
12		opreq1 3968	. . . . 5 |- ([<.x, y>.] ~R = A -> ([<.x, y>.] ~R .R [<.z, w>.] ~R ) = (A .R [<.z, w>.] ~R ))
13	12	breq2d 2630	. . . 4 |- ([<.x, y>.] ~R = A -> (0R <R ([<.x, y>.] ~R .R [<.z, w>.] ~R ) <-> 0R <R (A .R [<.z, w>.] ~R )))
14	11, 13	imbi12d 626	. . 3 |- ([<.x, y>.] ~R = A -> (((0R <R [<.x, y>.] ~R /\ 0R <R [<.z, w>.] ~R ) -> 0R <R ([<.x, y>.] ~R .R [<.z, w>.] ~R )) <-> ((0R <R A /\ 0R <R [<.z, w>.] ~R ) -> 0R <R (A .R [<.z, w>.] ~R ))))
15		breq2 2623	. . . . 5 |- ([<.z, w>.] ~R = B -> (0R <R [<.z, w>.] ~R <-> 0R <R B))
16	15	anbi2d 616	. . . 4 |- ([<.z, w>.] ~R = B -> ((0R <R A /\ 0R <R [<.z, w>.] ~R ) <-> (0R <R A /\ 0R <R B)))
17		opreq2 3969	. . . . 5 |- ([<.z, w>.] ~R = B -> (A .R [<.z, w>.] ~R ) = (A .R B))
18	17	breq2d 2630	. . . 4 |- ([<.z, w>.] ~R = B -> (0R <R (A .R [<.z, w>.] ~R ) <-> 0R <R (A .R B)))
19	16, 18	imbi12d 626	. . 3 |- ([<.z, w>.] ~R = B -> (((0R <R A /\ 0R <R [<.z, w>.] ~R ) -> 0R <R (A .R [<.z, w>.] ~R )) <-> ((0R <R A /\ 0R <R B) -> 0R <R (A .R B))))
20		oprex 3983	. . . . . . . . . . . . . . . . . 18 |- ((x .P. z) +P. (y .P. w)) e. V
21		oprex 3983	. . . . . . . . . . . . . . . . . 18 |- (((x .P. w) +P. (y .P. z)) +P. (v .P. u)) e. V
22	20, 21	addcanpr 5152	. . . . . . . . . . . . . . . . 17 |- (((v .P. w) e. P. /\ ((x .P. z) +P. (y .P. w)) e. P.) -> (((v .P. w) +P. ((x .P. z) +P. (y .P. w))) = ((v .P. w) +P. (((x .P. w) +P. (y .P. z)) +P. (v .P. u))) -> ((x .P. z) +P. (y .P. w)) = (((x .P. w) +P. (y .P. z)) +P. (v .P. u))))
23		opreq12 3970	. . . . . . . . . . . . . . . . . . . 20 |- (((y +P. v) = x /\ (w +P. u) = z) -> ((y +P. v) .P. (w +P. u)) = (x .P. z))
24	23	opreq1d 3975	. . . . . . . . . . . . . . . . . . 19 |- (((y +P. v) = x /\ (w +P. u) = z) -> (((y +P. v) .P. (w +P. u)) +P. ((y .P. w) +P. (v .P. w))) = ((x .P. z) +P. ((y .P. w) +P. (v .P. w))))
25		opreq2 3969	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((w +P. u) = z -> (y .P. (w +P. u)) = (y .P. z))
26		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . 24 |- w e. V
27		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . 24 |- u e. V
28	26, 27	distrpr 5132	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y .P. (w +P. u)) = ((y .P. w) +P. (y .P. u))
29	25, 28	syl5eqr 1521	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w +P. u) = z -> ((y .P. w) +P. (y .P. u)) = (y .P. z))
30	29	opreq1d 3975	. . . . . . . . . . . . . . . . . . . . 21 |- ((w +P. u) = z -> (((y .P. w) +P. (y .P. u)) +P. ((v .P. w) +P. (v .P. u))) = ((y .P. z) +P. ((v .P. w) +P. (v .P. u))))
31		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . 24 |- y e. V
32		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . 24 |- v e. V
33		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- f e. V
34		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- g e. V
35	33, 34	mulcompr 5125	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f .P. g) = (g .P. f)
36		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- h e. V
37	34, 36	distrpr 5132	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f .P. (g +P. h)) = ((f .P. g) +P. (f .P. h))
38	31, 32, 26, 35, 37	caoprdistrr 4067	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y +P. v) .P. w) = ((y .P. w) +P. (v .P. w))
39	31, 32, 27, 35, 37	caoprdistrr 4067	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y +P. v) .P. u) = ((y .P. u) +P. (v .P. u))
40	38, 39	opreq12i 3973	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y +P. v) .P. w) +P. ((y +P. v) .P. u)) = (((y .P. w) +P. (v .P. w)) +P. ((y .P. u) +P. (v .P. u)))
41	26, 27	distrpr 5132	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y +P. v) .P. (w +P. u)) = (((y +P. v) .P. w) +P. ((y +P. v) .P. u))
42		oprex 3983	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y .P. w) e. V
43		oprex 3983	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y .P. u) e. V
44		oprex 3983	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v .P. w) e. V
45	33, 34	addcompr 5123	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f +P. g) = (g +P. f)
46	34, 36	addasspr 5124	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f +P. g) +P. h) = (f +P. (g +P. h))
47		oprex 3983	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v .P. u) e. V
48	42, 43, 44, 45, 46, 47	caopr4 4064	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y .P. w) +P. (y .P. u)) +P. ((v .P. w) +P. (v .P. u))) = (((y .P. w) +P. (v .P. w)) +P. ((y .P. u) +P. (v .P. u)))
49	40, 41, 48	3eqtr4 1505	. . . . . . . . . . . . . . . . . . . . 21 |- ((y +P. v) .P. (w +P. u)) = (((y .P. w) +P. (y .P. u)) +P. ((v .P. w) +P. (v .P. u)))
50		oprex 3983	. . . . . . . . . . . . . . . . . . . . . 22 |- (y .P. z) e. V
51	44, 50, 47, 45, 46	caopr12 4061	. . . . . . . . . . . . . . . . . . . . 21 |- ((v .P. w) +P. ((y .P. z) +P. (v .P. u))) = ((y .P. z) +P. ((v .P. w) +P. (v .P. u)))
52	30, 49, 51	3eqtr4g 1531	. . . . . . . . . . . . . . . . . . . 20 |- ((w +P. u) = z -> ((y +P. v) .P. (w +P. u)) = ((v .P. w) +P. ((y .P. z) +P. (v .P. u))))
53		opreq1 3968	. . . . . . . . . . . . . . . . . . . . 21 |- ((y +P. v) = x -> ((y +P. v) .P. w) = (x .P. w))
54	53, 38	syl5eqr 1521	. . . . . . . . . . . . . . . . . . . 20 |- ((y +P. v) = x -> ((y .P. w) +P. (v .P. w)) = (x .P. w))
55	52, 54	opreqan12rd 3980	. . . . . . . . . . . . . . . . . . 19 |- (((y +P. v) = x /\ (w +P. u) = z) -> (((y +P. v) .P. (w +P. u)) +P. ((y .P. w) +P. (v .P. w))) = (((v .P. w) +P. ((y .P. z) +P. (v .P. u))) +P. (x .P. w)))
56	24, 55	eqtr3d 1509	. . . . . . . . . . . . . . . . . 18 |- (((y +P. v) = x /\ (w +P. u) = z) -> ((x .P. z) +P. ((y .P. w) +P. (v .P. w))) = (((v .P. w) +P. ((y .P. z) +P. (v .P. u))) +P. (x .P. w)))
57	42, 44	addasspr 5124	. . . . . . . . . . . . . . . . . . 19 |- (((x .P. z) +P. (y .P. w)) +P. (v .P. w)) = ((x .P. z) +P. ((y .P. w) +P. (v .P. w)))
58	20, 44	addcompr 5123	. . . . . . . . . . . . . . . . . . 19 |- (((x .P. z) +P. (y .P. w)) +P. (v .P. w)) = ((v .P. w) +P. ((x .P. z) +P. (y .P. w)))
59	57, 58	eqtr3 1497	. . . . . . . . . . . . . . . . . 18 |- ((x .P. z) +P. ((y .P. w) +P. (v .P. w))) = ((v .P. w) +P. ((x .P. z) +P. (y .P. w)))
60		oprex 3983	. . . . . . . . . . . . . . . . . . . 20 |- (x .P. w) e. V
61		oprex 3983	. . . . . . . . . . . . . . . . . . . 20 |- ((y .P. z) +P. (v .P. u)) e. V
62	60, 61	addasspr 5124	. . . . . . . . . . . . . . . . . . 19 |- (((v .P. w) +P. (x .P. w)) +P. ((y .P. z) +P. (v .P. u))) = ((v .P. w) +P. ((x .P. w) +P. ((y .P. z) +P. (v .P. u))))
63	44, 61, 60, 45, 46	caopr32 4060	. . . . . . . . . . . . . . . . . . 19 |- (((v .P. w) +P. ((y .P. z) +P. (v .P. u))) +P. (x .P. w)) = (((v .P. w) +P. (x .P. w)) +P. ((