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 ⊢xy~𝑹=A→0𝑹<𝑹xy~𝑹↔0𝑹<𝑹A
9 8 anbi1d ⊢xy~𝑹=A→0𝑹<𝑹xy~𝑹∧0𝑹<𝑹zw~𝑹↔0𝑹<𝑹A∧0𝑹<𝑹zw~𝑹
10 oveq1 ⊢xy~𝑹=A→xy~𝑹⋅𝑹zw~𝑹=A⋅𝑹zw~𝑹
11 10 breq2d ⊢xy~𝑹=A→0𝑹<𝑹xy~𝑹⋅𝑹zw~𝑹↔0𝑹<𝑹A⋅𝑹zw~𝑹
12 9 11 imbi12d ⊢xy~𝑹=A→0𝑹<𝑹xy~𝑹∧0𝑹<𝑹zw~𝑹→0𝑹<𝑹xy~𝑹⋅𝑹zw~𝑹↔0𝑹<𝑹A∧0𝑹<𝑹zw~𝑹→0𝑹<𝑹A⋅𝑹zw~𝑹
13 breq2 ⊢zw~𝑹=B→0𝑹<𝑹zw~𝑹↔0𝑹<𝑹B
14 13 anbi2d ⊢zw~𝑹=B→0𝑹<𝑹A∧0𝑹<𝑹zw~𝑹↔0𝑹<𝑹A∧0𝑹<𝑹B
15 oveq2 ⊢zw~𝑹=B→A⋅𝑹zw~𝑹=A⋅𝑹B
16 15 breq2d ⊢zw~𝑹=B→0𝑹<𝑹A⋅𝑹zw~𝑹↔0𝑹<𝑹A⋅𝑹B
17 14 16 imbi12d ⊢zw~𝑹=B→0𝑹<𝑹A∧0𝑹<𝑹zw~𝑹→0𝑹<𝑹A⋅𝑹zw~𝑹↔0𝑹<𝑹A∧0𝑹<𝑹B→0𝑹<𝑹A⋅𝑹B
18 gt0srpr ⊢0𝑹<𝑹xy~𝑹↔y<𝑷x
19 gt0srpr ⊢0𝑹<𝑹zw~𝑹↔w<𝑷z
20 18 19 anbi12i ⊢0𝑹<𝑹xy~𝑹∧0𝑹<𝑹zw~𝑹↔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 biimtrid ⊢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∈𝑷→xy~𝑹⋅𝑹zw~𝑹=x⋅𝑷z+𝑷y⋅𝑷wx⋅𝑷w+𝑷y⋅𝑷z~𝑹
92 91 breq2d ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→0𝑹<𝑹xy~𝑹⋅𝑹zw~𝑹↔0𝑹<𝑹x⋅𝑷z+𝑷y⋅𝑷wx⋅𝑷w+𝑷y⋅𝑷z~𝑹
93 gt0srpr ⊢0𝑹<𝑹x⋅𝑷z+𝑷y⋅𝑷wx⋅𝑷w+𝑷y⋅𝑷z~𝑹↔x⋅𝑷w+𝑷y⋅𝑷z<𝑷x⋅𝑷z+𝑷y⋅𝑷w
94 92 93 bitrdi ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→0𝑹<𝑹xy~𝑹⋅𝑹zw~𝑹↔x⋅𝑷w+𝑷y⋅𝑷z<𝑷x⋅𝑷z+𝑷y⋅𝑷w
95 90 94 sylibrd ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→y<𝑷x∧w<𝑷z→0𝑹<𝑹xy~𝑹⋅𝑹zw~𝑹
96 20 95 biimtrid ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→0𝑹<𝑹xy~𝑹∧0𝑹<𝑹zw~𝑹→0𝑹<𝑹xy~𝑹⋅𝑹zw~𝑹
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