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 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 ∈ 𝑷 → 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 biimtrid ⊢ 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