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 0 𝑹 < 𝑹 A 0 𝑹 < 𝑹 B 0 𝑹 < 𝑹 A 𝑹 B

Proof

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