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 <R 𝐴 ∧ 0R <R 𝐵 ) → 0R <R ( 𝐴 ·R 𝐵 ) )

Proof

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