This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 → ( 0R ∈ R ∧ 𝐴 ∈ R ) )
3 2 simprd ⊢ ( 0R <R 𝐴 → 𝐴 ∈ R )
4 1 brel ⊢ ( 0R <R 𝐵 → ( 0R ∈ R ∧ 𝐵 ∈ 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 biimtrid ⊢ ( ( ( 𝑥 ·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 biimtrid ⊢ ( ( ( 𝑥 ∈ 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 𝐵 ) )