Metamath Proof Explorer

Theorem mulgt0sr

Description: The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996) (New usage is discouraged.)

Ref Expression
Assertion mulgt0sr 
|- ( ( 0R  0R

Proof

Step Hyp Ref Expression
1 ltrelsr 
 |-
2 1 brel 
 |-  ( 0R  ( 0R e. R. /\ A e. R. ) )
3 2 simprd 
 |-  ( 0R  A e. R. )
4 1 brel 
 |-  ( 0R  ( 0R e. R. /\ B e. R. ) )
5 4 simprd 
 |-  ( 0R  B e. R. )
6 3 5 anim12i 
 |-  ( ( 0R  ( A e. R. /\ B e. R. ) )
7 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
8 breq2 
 |-  ( [ <. x , y >. ] ~R = A -> ( 0R . ] ~R <-> 0R
9 8 anbi1d 
 |-  ( [ <. x , y >. ] ~R = A -> ( ( 0R . ] ~R /\ 0R . ] ~R ) <-> ( 0R . ] ~R ) ) )
10 oveq1 
 |-  ( [ <. x , y >. ] ~R = A -> ( [ <. x , y >. ] ~R .R [ <. z , w >. ] ~R ) = ( A .R [ <. z , w >. ] ~R ) )
11 10 breq2d 
 |-  ( [ <. x , y >. ] ~R = A -> ( 0R . ] ~R .R [ <. z , w >. ] ~R ) <-> 0R . ] ~R ) ) )
12 9 11 imbi12d 
 |-  ( [ <. x , y >. ] ~R = A -> ( ( ( 0R . ] ~R /\ 0R . ] ~R ) -> 0R . ] ~R .R [ <. z , w >. ] ~R ) ) <-> ( ( 0R . ] ~R ) -> 0R . ] ~R ) ) ) )
13 breq2 
 |-  ( [ <. z , w >. ] ~R = B -> ( 0R . ] ~R <-> 0R
14 13 anbi2d 
 |-  ( [ <. z , w >. ] ~R = B -> ( ( 0R . ] ~R ) <-> ( 0R
15 oveq2 
 |-  ( [ <. z , w >. ] ~R = B -> ( A .R [ <. z , w >. ] ~R ) = ( A .R B ) )
16 15 breq2d 
 |-  ( [ <. z , w >. ] ~R = B -> ( 0R . ] ~R ) <-> 0R
17 14 16 imbi12d 
 |-  ( [ <. z , w >. ] ~R = B -> ( ( ( 0R . ] ~R ) -> 0R . ] ~R ) ) <-> ( ( 0R  0R
18 gt0srpr 
 |-  ( 0R . ] ~R <-> y
19 gt0srpr 
 |-  ( 0R . ] ~R <-> w
20 18 19 anbi12i 
 |-  ( ( 0R . ] ~R /\ 0R . ] ~R ) <-> ( y
21 simprr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> w e. P. )
22 mulclpr 
 |-  ( ( x e. P. /\ z e. P. ) -> ( x .P. z ) e. P. )
23 mulclpr 
 |-  ( ( y e. P. /\ w e. P. ) -> ( y .P. w ) e. P. )
24 addclpr 
 |-  ( ( ( x .P. z ) e. P. /\ ( y .P. w ) e. P. ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
25 22 23 24 syl2an 
 |-  ( ( ( x e. P. /\ z e. P. ) /\ ( y e. P. /\ w e. P. ) ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
26 25 an4s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
27 ltexpri 
 |-  ( y 
 E. v e. P. ( y +P. v ) = x )
28 ltexpri 
 |-  ( w 
 E. u e. P. ( w +P. u ) = z )
29 mulclpr 
 |-  ( ( v e. P. /\ w e. P. ) -> ( v .P. w ) e. P. )
30 oveq12 
 |-  ( ( ( y +P. v ) = x /\ ( w +P. u ) = z ) -> ( ( y +P. v ) .P. ( w +P. u ) ) = ( x .P. z ) )
31 30 oveq1d 
 |-  ( ( ( 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 ) ) ) )
32 distrpr 
 |-  ( y .P. ( w +P. u ) ) = ( ( y .P. w ) +P. ( y .P. u ) )
33 oveq2 
 |-  ( ( w +P. u ) = z -> ( y .P. ( w +P. u ) ) = ( y .P. z ) )
34 32 33 eqtr3id 
 |-  ( ( w +P. u ) = z -> ( ( y .P. w ) +P. ( y .P. u ) ) = ( y .P. z ) )
35 34 oveq1d 
 |-  ( ( 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 ) ) ) )
36 vex 
 |-  y e. _V
37 vex 
 |-  v e. _V
38 vex 
 |-  w e. _V
39 mulcompr 
 |-  ( f .P. g ) = ( g .P. f )
40 distrpr 
 |-  ( f .P. ( g +P. h ) ) = ( ( f .P. g ) +P. ( f .P. h ) )
41 36 37 38 39 40 caovdir 
 |-  ( ( y +P. v ) .P. w ) = ( ( y .P. w ) +P. ( v .P. w ) )
42 vex 
 |-  u e. _V
43 36 37 42 39 40 caovdir 
 |-  ( ( y +P. v ) .P. u ) = ( ( y .P. u ) +P. ( v .P. u ) )
44 41 43 oveq12i 
 |-  ( ( ( 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 ) ) )
45 distrpr 
 |-  ( ( y +P. v ) .P. ( w +P. u ) ) = ( ( ( y +P. v ) .P. w ) +P. ( ( y +P. v ) .P. u ) )
46 ovex 
 |-  ( y .P. w ) e. _V
47 ovex 
 |-  ( y .P. u ) e. _V
48 ovex 
 |-  ( v .P. w ) e. _V
49 addcompr 
 |-  ( f +P. g ) = ( g +P. f )
50 addasspr 
 |-  ( ( f +P. g ) +P. h ) = ( f +P. ( g +P. h ) )
51 ovex 
 |-  ( v .P. u ) e. _V
52 46 47 48 49 50 51 caov4 
 |-  ( ( ( 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 ) ) )
53 44 45 52 3eqtr4i 
 |-  ( ( y +P. v ) .P. ( w +P. u ) ) = ( ( ( y .P. w ) +P. ( y .P. u ) ) +P. ( ( v .P. w ) +P. ( v .P. u ) ) )
54 ovex 
 |-  ( y .P. z ) e. _V
55 48 54 51 49 50 caov12 
 |-  ( ( v .P. w ) +P. ( ( y .P. z ) +P. ( v .P. u ) ) ) = ( ( y .P. z ) +P. ( ( v .P. w ) +P. ( v .P. u ) ) )
56 35 53 55 3eqtr4g 
 |-  ( ( w +P. u ) = z -> ( ( y +P. v ) .P. ( w +P. u ) ) = ( ( v .P. w ) +P. ( ( y .P. z ) +P. ( v .P. u ) ) ) )
57 oveq1 
 |-  ( ( y +P. v ) = x -> ( ( y +P. v ) .P. w ) = ( x .P. w ) )
58 41 57 eqtr3id 
 |-  ( ( y +P. v ) = x -> ( ( y .P. w ) +P. ( v .P. w ) ) = ( x .P. w ) )
59 56 58 oveqan12rd 
 |-  ( ( ( 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 ) ) )
60 31 59 eqtr3d 
 |-  ( ( ( 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 ) ) )
61 addasspr 
 |-  ( ( ( x .P. z ) +P. ( y .P. w ) ) +P. ( v .P. w ) ) = ( ( x .P. z ) +P. ( ( y .P. w ) +P. ( v .P. w ) ) )
62 addcompr 
 |-  ( ( ( x .P. z ) +P. ( y .P. w ) ) +P. ( v .P. w ) ) = ( ( v .P. w ) +P. ( ( x .P. z ) +P. ( y .P. w ) ) )
63 61 62 eqtr3i 
 |-  ( ( x .P. z ) +P. ( ( y .P. w ) +P. ( v .P. w ) ) ) = ( ( v .P. w ) +P. ( ( x .P. z ) +P. ( y .P. w ) ) )
64 addasspr 
 |-  ( ( ( 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 ) ) ) )
65 ovex 
 |-  ( ( y .P. z ) +P. ( v .P. u ) ) e. _V
66 ovex 
 |-  ( x .P. w ) e. _V
67 48 65 66 49 50 caov32 
 |-  ( ( ( v .P. w ) +P. ( ( y .P. z ) +P. ( v .P. u ) ) ) +P. ( x .P. w ) ) = ( ( ( v .P. w ) +P. ( x .P. w ) ) +P. ( ( y .P. z ) +P. ( v .P. u ) ) )
68 addasspr 
 |-  ( ( ( x .P. w ) +P. ( y .P. z ) ) +P. ( v .P. u ) ) = ( ( x .P. w ) +P. ( ( y .P. z ) +P. ( v .P. u ) ) )
69 68 oveq2i 
 |-  ( ( 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 ) ) ) )
70 64 67 69 3eqtr4i 
 |-  ( ( ( v .P. w ) +P. ( ( y .P. z ) +P. ( v .P. u ) ) ) +P. ( x .P. w ) ) = ( ( v .P. w ) +P. ( ( ( x .P. w ) +P. ( y .P. z ) ) +P. ( v .P. u ) ) )
71 60 63 70 3eqtr3g 
 |-  ( ( ( y +P. v ) = x /\ ( w +P. u ) = z ) -> ( ( 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 ) ) ) )
72 addcanpr 
 |-  ( ( ( 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 ) ) ) )
73 71 72 syl5 
 |-  ( ( ( v .P. w ) e. P. /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( ( ( y +P. v ) = x /\ ( w +P. u ) = z ) -> ( ( x .P. z ) +P. ( y .P. w ) ) = ( ( ( x .P. w ) +P. ( y .P. z ) ) +P. ( v .P. u ) ) ) )
74 eqcom 
 |-  ( ( ( x .P. z ) +P. ( y .P. w ) ) = ( ( ( x .P. w ) +P. ( y .P. z ) ) +P. ( v .P. u ) ) <-> ( ( ( x .P. w ) +P. ( y .P. z ) ) +P. ( v .P. u ) ) = ( ( x .P. z ) +P. ( y .P. w ) ) )
75 ltaddpr2 
 |-  ( ( ( x .P. z ) +P. ( y .P. w ) ) e. 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 ) )
76 74 75 syl5bi 
 |-  ( ( ( x .P. z ) +P. ( y .P. w ) ) e. P. -> ( ( ( x .P. z ) +P. ( y .P. w ) ) = ( ( ( x .P. w ) +P. ( y .P. z ) ) +P. ( v .P. u ) ) -> ( ( x .P. w ) +P. ( y .P. z ) )
77 76 adantl 
 |-  ( ( ( v .P. w ) e. P. /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( ( ( x .P. z ) +P. ( y .P. w ) ) = ( ( ( x .P. w ) +P. ( y .P. z ) ) +P. ( v .P. u ) ) -> ( ( x .P. w ) +P. ( y .P. z ) )
78 73 77 syld 
 |-  ( ( ( v .P. w ) e. P. /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( ( ( y +P. v ) = x /\ ( w +P. u ) = z ) -> ( ( x .P. w ) +P. ( y .P. z ) )
79 29 78 sylan 
 |-  ( ( ( v e. P. /\ w e. P. ) /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( ( ( y +P. v ) = x /\ ( w +P. u ) = z ) -> ( ( x .P. w ) +P. ( y .P. z ) )
80 79 a1d 
 |-  ( ( ( v e. P. /\ w e. P. ) /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( u e. P. -> ( ( ( y +P. v ) = x /\ ( w +P. u ) = z ) -> ( ( x .P. w ) +P. ( y .P. z ) )
81 80 exp4a 
 |-  ( ( ( v e. P. /\ w e. P. ) /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( u e. P. -> ( ( y +P. v ) = x -> ( ( w +P. u ) = z -> ( ( x .P. w ) +P. ( y .P. z ) )
82 81 com34 
 |-  ( ( ( v e. P. /\ w e. P. ) /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( u e. P. -> ( ( w +P. u ) = z -> ( ( y +P. v ) = x -> ( ( x .P. w ) +P. ( y .P. z ) )
83 82 rexlimdv 
 |-  ( ( ( v e. P. /\ w e. P. ) /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( E. u e. P. ( w +P. u ) = z -> ( ( y +P. v ) = x -> ( ( x .P. w ) +P. ( y .P. z ) )
84 83 expl 
 |-  ( v e. P. -> ( ( w e. P. /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( E. u e. P. ( w +P. u ) = z -> ( ( y +P. v ) = x -> ( ( x .P. w ) +P. ( y .P. z ) )
85 84 com24 
 |-  ( v e. P. -> ( ( y +P. v ) = x -> ( E. u e. P. ( w +P. u ) = z -> ( ( w e. P. /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( ( x .P. w ) +P. ( y .P. z ) )
86 85 rexlimiv 
 |-  ( E. v e. P. ( y +P. v ) = x -> ( E. u e. P. ( w +P. u ) = z -> ( ( w e. P. /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( ( x .P. w ) +P. ( y .P. z ) )
87 27 28 86 syl2im 
 |-  ( y 
 ( w 
 ( ( w e. P. /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( ( x .P. w ) +P. ( y .P. z ) )
88 87 imp 
 |-  ( ( y 
 ( ( w e. P. /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( ( x .P. w ) +P. ( y .P. z ) )
89 88 com12 
 |-  ( ( w e. P. /\ ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) -> ( ( y 
 ( ( x .P. w ) +P. ( y .P. z ) )
90 21 26 89 syl2anc 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( y 
 ( ( x .P. w ) +P. ( y .P. z ) )
91 mulsrpr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R .R [ <. z , w >. ] ~R ) = [ <. ( ( x .P. z ) +P. ( y .P. w ) ) , ( ( x .P. w ) +P. ( y .P. z ) ) >. ] ~R )
92 91 breq2d 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( 0R . ] ~R .R [ <. z , w >. ] ~R ) <-> 0R . ] ~R ) )
93 gt0srpr 
 |-  ( 0R . ] ~R <-> ( ( x .P. w ) +P. ( y .P. z ) )
94 92 93 bitrdi 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( 0R . ] ~R .R [ <. z , w >. ] ~R ) <-> ( ( x .P. w ) +P. ( y .P. z ) )
95 90 94 sylibrd 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( y 
 0R . ] ~R .R [ <. z , w >. ] ~R ) ) )
96 20 95 syl5bi 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( 0R . ] ~R /\ 0R . ] ~R ) -> 0R . ] ~R .R [ <. z , w >. ] ~R ) ) )
97 7 12 17 96 2ecoptocl 
 |-  ( ( A e. R. /\ B e. R. ) -> ( ( 0R  0R
98 6 97 mpcom 
 |-  ( ( 0R  0R