Theorem mulgt0sr 4008

Description: The product of two positive signed reals is positive.

Hypotheses

Ref	Expression
mulgt0sr.1	⊢ A ∈ V
mulgt0sr.2	⊢ B ∈ V

Assertion

Ref	Expression
mulgt0sr	⊢ ((0R <R A ∧ 0R <R B) → 0R <R (A ·R B))

Proof of Theorem mulgt0sr

Step	Hyp	Ref	Expression
1		mulgt0sr.1	. . . . 5 ⊢ A ∈ V
2		ltrelsr 3974	. . . . 5 ⊢ <R ⊆ (R × R)
3	1, 2	brel 2459	. . . 4 ⊢ (0R <R A → (0R ∈ R ∧ A ∈ R))
4	3	pm3.27d 262	. . 3 ⊢ (0R <R A → A ∈ R)
5		mulgt0sr.2	. . . . 5 ⊢ B ∈ V
6	5, 2	brel 2459	. . . 4 ⊢ (0R <R B → (0R ∈ R ∧ B ∈ R))
7	6	pm3.27d 262	. . 3 ⊢ (0R <R B → B ∈ R)
8	4, 7	anim12i 268	. 2 ⊢ ((0R <R A ∧ 0R <R B) → (A ∈ R ∧ B ∈ R))
9		df-nr 3961	. . 3 ⊢ R = ((P × P) / ~R )
10		breq2 2066	. . . . 5 ⊢ ([⟨x, y⟩] ~R = A → (0R <R [⟨x, y⟩] ~R ↔ 0R <R A))
11	10	anbi1d 469	. . . 4 ⊢ ([⟨x, y⟩] ~R = A → ((0R <R [⟨x, y⟩] ~R ∧ 0R <R [⟨z, w⟩] ~R ) ↔ (0R <R A ∧ 0R <R [⟨z, w⟩] ~R )))
12		opreq1 3006	. . . . 5 ⊢ ([⟨x, y⟩] ~R = A → ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R ) = (A ·R [⟨z, w⟩] ~R ))
13	12	breq2d 2072	. . . 4 ⊢ ([⟨x, y⟩] ~R = A → (0R <R ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R ) ↔ 0R <R (A ·R [⟨z, w⟩] ~R )))
14	11, 13	imbi12d 474	. . 3 ⊢ ([⟨x, y⟩] ~R = A → (((0R <R [⟨x, y⟩] ~R ∧ 0R <R [⟨z, w⟩] ~R ) → 0R <R ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R )) ↔ ((0R <R A ∧ 0R <R [⟨z, w⟩] ~R ) → 0R <R (A ·R [⟨z, w⟩] ~R ))))
15		breq2 2066	. . . . 5 ⊢ ([⟨z, w⟩] ~R = B → (0R <R [⟨z, w⟩] ~R ↔ 0R <R B))
16	15	anbi2d 468	. . . 4 ⊢ ([⟨z, w⟩] ~R = B → ((0R <R A ∧ 0R <R [⟨z, w⟩] ~R ) ↔ (0R <R A ∧ 0R <R B)))
17		opreq2 3007	. . . . 5 ⊢ ([⟨z, w⟩] ~R = B → (A ·R [⟨z, w⟩] ~R ) = (A ·R B))
18	17	breq2d 2072	. . . 4 ⊢ ([⟨z, w⟩] ~R = B → (0R <R (A ·R [⟨z, w⟩] ~R ) ↔ 0R <R (A ·R B)))
19	16, 18	imbi12d 474	. . 3 ⊢ ([⟨z, w⟩] ~R = B → (((0R <R A ∧ 0R <R [⟨z, w⟩] ~R ) → 0R <R (A ·R [⟨z, w⟩] ~R )) ↔ ((0R <R A ∧ 0R <R B) → 0R <R (A ·R B))))
20		oprex 3018	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ·P z) +P (y ·P w)) ∈ V
21		oprex 3018	. . . . . . . . . . . . . . . . . 18 ⊢ (((x ·P w) +P (y ·P z)) +P (v ·P u)) ∈ V
22	20, 21	addcanpr 3946	. . . . . . . . . . . . . . . . 17 ⊢ (((v ·P w) ∈ P ∧ ((x ·P z) +P (y ·P w)) ∈ P) → (((v ·P w) +P ((x ·P z) +P (y ·P w))) = ((v ·P w) +P (((x ·P w) +P (y ·P z)) +P (v ·P u))) → ((x ·P z) +P (y ·P w)) = (((x ·P w) +P (y ·P z)) +P (v ·P u))))
23		opreq12 3008	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((y +P v) = x ∧ (w +P u) = z) → ((y +P v) ·P (w +P u)) = (x ·P z))
24	23	opreq1d 3012	. . . . . . . . . . . . . . . . . . 19 ⊢ (((y +P v) = x ∧ (w +P u) = z) → (((y +P v) ·P (w +P u)) +P ((y ·P w) +P (v ·P w))) = ((x ·P z) +P ((y ·P w) +P (v ·P w))))
25		opreq2 3007	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((w +P u) = z → (y ·P (w +P u)) = (y ·P z))
26		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ w ∈ V
27		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ u ∈ V
28	26, 27	distrpr 3926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ·P (w +P u)) = ((y ·P w) +P (y ·P u))
29	25, 28	syl5eqr 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((w +P u) = z → ((y ·P w) +P (y ·P u)) = (y ·P z))
30	29	opreq1d 3012	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((w +P u) = z → (((y ·P w) +P (y ·P u)) +P ((v ·P w) +P (v ·P u))) = ((y ·P z) +P ((v ·P w) +P (v ·P u))))
31		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ y ∈ V
32		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ v ∈ V
33		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ f ∈ V
34		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ g ∈ V
35	33, 34	mulcompr 3919	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f ·P g) = (g ·P f)
36		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ h ∈ V
37	34, 36	distrpr 3926	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f ·P (g +P h)) = ((f ·P g) +P (f ·P h))
38	31, 32, 26, 35, 37	caoprdistrr 3081	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y +P v) ·P w) = ((y ·P w) +P (v ·P w))
39	31, 32, 27, 35, 37	caoprdistrr 3081	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y +P v) ·P u) = ((y ·P u) +P (v ·P u))
40	38, 39	opreq12i 3011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((y +P v) ·P w) +P ((y +P v) ·P u)) = (((y ·P w) +P (v ·P w)) +P ((y ·P u) +P (v ·P u)))
41	26, 27	distrpr 3926	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y +P v) ·P (w +P u)) = (((y +P v) ·P w) +P ((y +P v) ·P u))
42		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ·P w) ∈ V
43		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ·P u) ∈ V
44		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (v ·P w) ∈ V
45	33, 34	addcompr 3917	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f +P g) = (g +P f)
46	34, 36	addasspr 3918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f +P g) +P h) = (f +P (g +P h))
47		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (v ·P u) ∈ V
48	42, 43, 44, 45, 46, 47	caopr4 3078	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((y ·P w) +P (y ·P u)) +P ((v ·P w) +P (v ·P u))) = (((y ·P w) +P (v ·P w)) +P ((y ·P u) +P (v ·P u)))
49	40, 41, 48	3eqtr4 1126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y +P v) ·P (w +P u)) = (((y ·P w) +P (y ·P u)) +P ((v ·P w) +P (v ·P u)))
50		oprex 3018	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y ·P z) ∈ V
51	44, 50, 47, 45, 46	caopr12 3075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((v ·P w) +P ((y ·P z) +P (v ·P u))) = ((y ·P z) +P ((v ·P w) +P (v ·P u)))
52	30, 49, 51	3eqtr4g 1147	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((w +P u) = z → ((y +P v) ·P (w +P u)) = ((v ·P w) +P ((y ·P z) +P (v ·P u))))
53		opreq1 3006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y +P v) = x → ((y +P v) ·P w) = (x ·P w))
54	53, 38	syl5eqr 1138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y +P v) = x → ((y ·P w) +P (v ·P w)) = (x ·P w))
55	52, 54	opreqan12rd 3016	. . . . . . . . . . . . . . . . . . 19 ⊢ (((y +P v) = x ∧ (w +P u) = z) → (((y +P v) ·P (w +P u)) +P ((y ·P w) +P (v ·P w))) = (((v ·P w) +P ((y ·P z) +P (v ·P u))) +P (x ·P w)))
56	24, 55	eqtr3d 1130	. . . . . . . . . . . . . . . . . 18 ⊢ (((y +P v) = x ∧ (w +P u) = z) → ((x ·P z) +P ((y ·P w) +P (v ·P w))) = (((v ·P w) +P ((y ·P z) +P (v ·P u))) +P (x ·P w)))
57	42, 44	addasspr 3918	. . . . . . . . . . . . . . . . . . 19 ⊢ (((x ·P z) +P (y ·P w)) +P (v ·P w)) = ((x ·P z) +P ((y ·P w) +P (v ·P w)))
58	20, 44	addcompr 3917	. . . . . . . . . . . . . . . . . . 19 ⊢ (((x ·P z) +P (y ·P w)) +P (v ·P w)) = ((v ·P w) +P ((x ·P z) +P (y ·P w)))
59	57, 58	eqtr3 1121	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ·P z) +P ((y ·P w) +P (v ·P w))) = ((v ·P w) +P ((x ·P z) +P (y ·P w)))
60		oprex 3018	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x ·P w) ∈ V
61		oprex 3018	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ·P z) +P (v ·P u)) ∈ V
62	60, 61	addasspr 3918	. . . . . . . . . . . . . . . . . . 19 ⊢ (((v ·P w) +P (x ·P w)) +P ((y ·P z) +P (v ·P u))) = ((v ·P w) +P ((x ·P w) +P ((y ·P z) +P (v ·P u))))
63	44, 61, 60, 45, 46	caopr32 3074	. . . . . . . . . . . . . . . . . . 19 ⊢ (((v ·P w) +P ((y ·P z) +P (v ·P u))) +P (x ·P w)) = (((v ·P w) +P (x ·P w)) +P ((y ·P z) +P (v ·P u)))
64	50, 47	addasspr 3918	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((x ·P w) +P (y ·P z)) +P (v ·P u)) = ((x ·P w) +P ((y ·P z) +P (v ·P u)))
65	64	opreq2i 3010	. . . . . . . . . . . . . . . . . . 19 ⊢ ((v ·P w) +P (((x ·P w) +P (y ·P z)) +P (v ·P u))) = ((v ·P w) +P ((x ·P w) +P ((y ·P z) +P (v ·P u))))
66	62, 63, 65	3eqtr4 1126	. . . . . . . . . . . . . . . . . 18 ⊢ (((v ·P w) +P ((y ·P z) +P (v ·P u))) +P (x ·P w)) = ((v ·P w) +P (((x ·P w) +P (y ·P z)) +P (v ·P u)))
67	56, 59, 66	3eqtr3g 1146	. . . . . . . . . . . . . . . . 17 ⊢ (((y +P v) = x ∧ (w +P u) = z) → ((v ·P w) +P ((x ·P z) +P (y ·P w))) = ((v ·P w) +P (((x ·P w) +P (y ·P z)) +P (v ·P u))))
68	22, 67	syl5 22	. . . . . . . . . . . . . . . 16 ⊢ (((v ·P w) ∈ P ∧ ((x ·P z) +P (y ·P w)) ∈ P) → (((y +P v) = x ∧ (w +P u) = z) → ((x ·P z) +P (y ·P w)) = (((x ·P w) +P (y ·P z)) +P (v ·P u))))
69	47	ltaddpr2 3935	. . . . . . . . . . . . . . . . . 18 ⊢ (((x ·P z) +P (y ·P w)) ∈ P → ((((x ·P w) +P (y ·P z)) +P (v ·P u)) = ((x ·P z) +P (y ·P w)) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
70		cleqcom 1103	. . . . . . . . . . . . . . . . . 18 ⊢ (((x ·P z) +P (y ·P w)) = (((x ·P w) +P (y ·P z)) +P (v ·P u)) ↔ (((x ·P w) +P (y ·P z)) +P (v ·P u)) = ((x ·P z) +P (y ·P w)))
71	69, 70	syl5ib 181	. . . . . . . . . . . . . . . . 17 ⊢ (((x ·P z) +P (y ·P w)) ∈ P → (((x ·P z) +P (y ·P w)) = (((x ·P w) +P (y ·P z)) +P (v ·P u)) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
72	71	adantl 305	. . . . . . . . . . . . . . . 16 ⊢ (((v ·P w) ∈ P ∧ ((x ·P z) +P (y ·P w)) ∈ P) → (((x ·P z) +P (y ·P w)) = (((x ·P w) +P (y ·P z)) +P (v ·P u)) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
73	68, 72	syld 27	. . . . . . . . . . . . . . 15 ⊢ (((v ·P w) ∈ P ∧ ((x ·P z) +P (y ·P w)) ∈ P) → (((y +P v) = x ∧ (w +P u) = z) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
74		mulclpr 3916	. . . . . . . . . . . . . . 15 ⊢ ((v ∈ P ∧ w ∈ P) → (v ·P w) ∈ P)
75	73, 74	sylan 343	. . . . . . . . . . . . . 14 ⊢ (((v ∈ P ∧ w ∈ P) ∧ ((x ·P z) +P (y ·P w)) ∈ P) → (((y +P v) = x ∧ (w +P u) = z) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
76	75	a1d 14	. . . . . . . . . . . . 13 ⊢ (((v ∈ P ∧ w ∈ P) ∧ ((x ·P z) +P (y ·P w)) ∈ P) → (u ∈ P → (((y +P v) = x ∧ (w +P u) = z) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w)))))
77	76	exp31 293	. . . . . . . . . . . 12 ⊢ (v ∈ P → (w ∈ P → (((x ·P z) +P (y ·P w)) ∈ P → (u ∈ P → (((y +P v) = x ∧ (w +P u) = z) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w)))))))
78	77	com13 33	. . . . . . . . . . 11 ⊢ (((x ·P z) +P (y ·P w)) ∈ P → (w ∈ P → (v ∈ P → (u ∈ P → (((y +P v) = x ∧ (w +P u) = z) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w)))))))
79	78	imp 277	. . . . . . . . . 10 ⊢ ((((x ·P z) +P (y ·P w)) ∈ P ∧ w ∈ P) → (v ∈ P → (u ∈ P → (((y +P v) = x ∧ (w +P u) = z) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))))
80	79	imp4c 284	. . . . . . . . 9 ⊢ ((((x ·P z) +P (y ·P w)) ∈ P ∧ w ∈ P) → (((v ∈ P ∧ u ∈ P) ∧ ((y +P v) = x ∧ (w +P u) = z)) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
81		an4 388	. . . . . . . . 9 ⊢ (((v ∈ P ∧ (y +P v) = x) ∧ (u ∈ P ∧ (w +P u) = z)) ↔ ((v ∈ P ∧ u ∈ P) ∧ ((y +P v) = x ∧ (w +P u) = z)))
82	80, 81	syl5ib 181	. . . . . . . 8 ⊢ ((((x ·P z) +P (y ·P w)) ∈ P ∧ w ∈ P) → (((v ∈ P ∧ (y +P v) = x) ∧ (u ∈ P ∧ (w +P u) = z)) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
83	82	19.23advv 955	. . . . . . 7 ⊢ ((((x ·P z) +P (y ·P w)) ∈ P ∧ w ∈ P) → (∃v∃u((v ∈ P ∧ (y +P v) = x) ∧ (u ∈ P ∧ (w +P u) = z)) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
84		visset 1350	. . . . . . . . . 10 ⊢ x ∈ V
85	84	ltexpri 3943	. . . . . . . . 9 ⊢ (y<P x → ∃v(v ∈ P ∧ (y +P v) = x))
86		visset 1350	. . . . . . . . . 10 ⊢ z ∈ V
87	86	ltexpri 3943	. . . . . . . . 9 ⊢ (w<P z → ∃u(u ∈ P ∧ (w +P u) = z))
88	85, 87	anim12i 268	. . . . . . . 8 ⊢ ((y<P x ∧ w<P z) → (∃v(v ∈ P ∧ (y +P v) = x) ∧ ∃u(u ∈ P ∧ (w +P u) = z)))
89		eeanv 980	. . . . . . . 8 ⊢ (∃v∃u((v ∈ P ∧ (y +P v) = x) ∧ (u ∈ P ∧ (w +P u) = z)) ↔ (∃v(v ∈ P ∧ (y +P v) = x) ∧ ∃u(u ∈ P ∧ (w +P u) = z)))
90	88, 89	sylibr 175	. . . . . . 7 ⊢ ((y<P x ∧ w<P z) → ∃v∃u((v ∈ P ∧ (y +P v) = x) ∧ (u ∈ P ∧ (w +P u) = z)))
91	83, 90	syl5 22	. . . . . 6 ⊢ ((((x ·P z) +P (y ·P w)) ∈ P ∧ w ∈ P) → ((y<P x ∧ w<P z) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
92		addclpr 3914	. . . . . . . 8 ⊢ (((x ·P z) ∈ P ∧ (y ·P w) ∈ P) → ((x ·P z) +P (y ·P w)) ∈ P)
93		mulclpr 3916	. . . . . . . 8 ⊢ ((x ∈ P ∧ z ∈ P) → (x ·P z) ∈ P)
94		mulclpr 3916	. . . . . . . 8 ⊢ ((y ∈ P ∧ w ∈ P) → (y ·P w) ∈ P)
95	92, 93, 94	syl2an 349	. . . . . . 7 ⊢ (((x ∈ P ∧ z ∈ P) ∧ (y ∈ P ∧ w ∈ P)) → ((x ·P z) +P (y ·P w)) ∈ P)
96	95	an4s 390	. . . . . 6 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ((x ·P z) +P (y ·P w)) ∈ P)
97		pm3.27 260	. . . . . . 7 ⊢ ((z ∈ P ∧ w ∈ P) → w ∈ P)
98	97	adantl 305	. . . . . 6 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → w ∈ P)
99	91, 96, 98	sylanc 361	. . . . 5 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ((y<P x ∧ w<P z) → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
100		mulsrpr 3979	. . . . . . 7 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R ) = [⟨((x ·P z) +P (y ·P w)), ((x ·P w) +P (y ·P z))⟩] ~R )
101	100	breq2d 2072	. . . . . 6 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → (0R <R ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R ) ↔ 0R <R [⟨((x ·P z) +P (y ·P w)), ((x ·P w) +P (y ·P z))⟩] ~R ))
102		oprex 3018	. . . . . . 7 ⊢ ((x ·P w) +P (y ·P z)) ∈ V
103	20, 102	gt0srpr 3981	. . . . . 6 ⊢ (0R <R [⟨((x ·P z) +P (y ·P w)), ((x ·P w) +P (y ·P z))⟩] ~R ↔ ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w)))
104	101, 103	syl6bb 414	. . . . 5 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → (0R <R ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R ) ↔ ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
105	99, 104	sylibrd 179	. . . 4 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ((y<P x ∧ w<P z) → 0R <R ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R )))
106	84, 31	gt0srpr 3981	. . . . 5 ⊢ (0R <R [⟨x, y⟩] ~R ↔ y<P x)
107	86, 26	gt0srpr 3981	. . . . 5 ⊢ (0R <R [⟨z, w⟩] ~R ↔ w<P z)
108	106, 107	anbi12i 369	. . . 4 ⊢ ((0R <R [⟨x, y⟩] ~R ∧ 0R <R [⟨z, w⟩] ~R ) ↔ (y<P x ∧ w<P z))
109	105, 108	syl5ib 181	. . 3 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ((0R <R [⟨x, y⟩] ~R ∧ 0R <R [⟨z, w⟩] ~R ) → 0R <R ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R )))
110	9, 14, 19, 109	2ecoptocl 3240	. 2 ⊢ ((A ∈ R ∧ B ∈ R) → ((0R <R A ∧ 0R <R B) → 0R <R (A ·R B)))
111	8, 110	mpcom 49	1 ⊢ ((0R <R A ∧ 0R <R B) → 0R <R (A ·R B))

Syntax hints:   → wi 2   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092  Vcvv 1348  ⟨cop 1810   class class class wbr 2054  (class class class)co 3001  [cec 3198  Pcnp 3779   +_P cpp 3781   ·_P cmp 3782  <_P cltp 3783   ~_R cer 3786  Rcnr 3787  0_Rc0r 3788   ·_R cmr 3792   <_R cltr 3793

This theorem is referenced by:  sqgt0sr 4009  axmulgt0 4086

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1o 3104  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-1p 3881  df-plp 3882  df-mp 3883  df-ltp 3884  df-mpr 3959  df-enr 3960  df-nr 3961  df-mr 3963  df-ltr 3964  df-0r 3965

metamath.org