Theorem mulgt0sr 5226

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 5192	. . . . 5 ⊢ <R ⊆ (R × R)
3	1, 2	brel 3229	. . . 4 ⊢ (0R <R A → (0R ∈ R ⋀ A ∈ R))
4	3	pm3.27d 325	. . 3 ⊢ (0R <R A → A ∈ R)
5		mulgt0sr.2	. . . . 5 ⊢ B ∈ V
6	5, 2	brel 3229	. . . 4 ⊢ (0R <R B → (0R ∈ R ⋀ B ∈ R))
7	6	pm3.27d 325	. . 3 ⊢ (0R <R B → B ∈ R)
8	4, 7	anim12i 333	. 2 ⊢ ((0R <R A ⋀ 0R <R B) → (A ∈ R ⋀ B ∈ R))
9		df-nr 5179	. . 3 ⊢ R = ((P × P) / ~R )
10		breq2 2628	. . . . 5 ⊢ ([⟨x, y⟩] ~R = A → (0R <R [⟨x, y⟩] ~R ↔ 0R <R A))
11	10	anbi1d 619	. . . 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 3974	. . . . 5 ⊢ ([⟨x, y⟩] ~R = A → ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R ) = (A ·R [⟨z, w⟩] ~R ))
13	12	breq2d 2635	. . . 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 628	. . 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 2628	. . . . 5 ⊢ ([⟨z, w⟩] ~R = B → (0R <R [⟨z, w⟩] ~R ↔ 0R <R B))
16	15	anbi2d 618	. . . 4 ⊢ ([⟨z, w⟩] ~R = B → ((0R <R A ⋀ 0R <R [⟨z, w⟩] ~R ) ↔ (0R <R A ⋀ 0R <R B)))
17		opreq2 3975	. . . . 5 ⊢ ([⟨z, w⟩] ~R = B → (A ·R [⟨z, w⟩] ~R ) = (A ·R B))
18	17	breq2d 2635	. . . 4 ⊢ ([⟨z, w⟩] ~R = B → (0R <R (A ·R [⟨z, w⟩] ~R ) ↔ 0R <R (A ·R B)))
19	16, 18	imbi12d 628	. . 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 3989	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ·P z) +P (y ·P w)) ∈ V
21		oprex 3989	. . . . . . . . . . . . . . . . . 18 ⊢ (((x ·P w) +P (y ·P z)) +P (v ·P u)) ∈ V
22	20, 21	addcanpr 5164	. . . . . . . . . . . . . . . . 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 3976	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((y +P v) = x ⋀ (w +P u) = z) → ((y +P v) ·P (w +P u)) = (x ·P z))
24	23	opreq1d 3981	. . . . . . . . . . . . . . . . . . 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 3975	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((w +P u) = z → (y ·P (w +P u)) = (y ·P z))
26		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ w ∈ V
27		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ u ∈ V
28	26, 27	distrpr 5144	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ·P (w +P u)) = ((y ·P w) +P (y ·P u))
29	25, 28	syl5eqr 1524	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((w +P u) = z → ((y ·P w) +P (y ·P u)) = (y ·P z))
30	29	opreq1d 3981	. . . . . . . . . . . . . . . . . . . . 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 1816	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ y ∈ V
32		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ v ∈ V
33		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ f ∈ V
34		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ g ∈ V
35	33, 34	mulcompr 5137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f ·P g) = (g ·P f)
36		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ h ∈ V
37	34, 36	distrpr 5144	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f ·P (g +P h)) = ((f ·P g) +P (f ·P h))
38	31, 32, 26, 35, 37	caoprdistrr 4073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y +P v) ·P w) = ((y ·P w) +P (v ·P w))
39	31, 32, 27, 35, 37	caoprdistrr 4073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y +P v) ·P u) = ((y ·P u) +P (v ·P u))
40	38, 39	opreq12i 3979	. . . . . . . . . . . . . . . . . . . . . 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 5144	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y +P v) ·P (w +P u)) = (((y +P v) ·P w) +P ((y +P v) ·P u))
42		oprex 3989	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ·P w) ∈ V
43		oprex 3989	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ·P u) ∈ V
44		oprex 3989	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (v ·P w) ∈ V
45	33, 34	addcompr 5135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f +P g) = (g +P f)
46	34, 36	addasspr 5136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f +P g) +P h) = (f +P (g +P h))
47		oprex 3989	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (v ·P u) ∈ V
48	42, 43, 44, 45, 46, 47	caopr4 4070	. . . . . . . . . . . . . . . . . . . . . 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 1508	. . . . . . . . . . . . . . . . . . . . 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 3989	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y ·P z) ∈ V
51	44, 50, 47, 45, 46	caopr12 4067	. . . . . . . . . . . . . . . . . . . . 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 1534	. . . . . . . . . . . . . . . . . . . 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 3974	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y +P v) = x → ((y +P v) ·P w) = (x ·P w))
54	53, 38	syl5eqr 1524	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y +P v) = x → ((y ·P w) +P (v ·P w)) = (x ·P w))
55	52, 54	opreqan12rd 3986	. . . . . . . . . . . . . . . . . . 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 1512	. . . . . . . . . . . . . . . . . 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 5136	. . . . . . . . . . . . . . . . . . 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 5135	. . . . . . . . . . . . . . . . . . 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 1500	. . . . . . . . . . . . . . . . . 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 3989	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x ·P w) ∈ V
61		oprex 3989	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ·P z) +P (v ·P u)) ∈ V
62	60, 61	addasspr 5136	. . . . . . . . . . . . . . . . . . 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 4066	. . . . . . . . . . . . . . . . . . 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 5136	. . . . . . . . . . . . . . . . . . . 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 3978	. . . . . . . . . . . . . . . . . . 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 1508	. . . . . . . . . . . . . . . . . 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 1533	. . . . . . . . . . . . . . . . 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 21	. . . . . . . . . . . . . . . 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 5153	. . . . . . . . . . . . . . . . . 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		eqcom 1480	. . . . . . . . . . . . . . . . . 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 206	. . . . . . . . . . . . . . . . 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 390	. . . . . . . . . . . . . . . 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 5134	. . . . . . . . . . . . . . 15 ⊢ ((v ∈ P ⋀ w ∈ P) → (v ·P w) ∈ P)
75	73, 74	sylan 450	. . . . . . . . . . . . . 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 12	. . . . . . . . . . . . 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 378	. . . . . . . . . . . 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 350	. . . . . . . . . 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 366	. . . . . . . . 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 508	. . . . . . . . 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 206	. . . . . . . 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 1299	. . . . . . 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 1816	. . . . . . . . . 10 ⊢ x ∈ V
85	84	ltexpri 5161	. . . . . . . . 9 ⊢ (y<P x → ∃v(v ∈ P ⋀ (y +P v) = x))
86		visset 1816	. . . . . . . . . 10 ⊢ z ∈ V
87	86	ltexpri 5161	. . . . . . . . 9 ⊢ (w<P z → ∃u(u ∈ P ⋀ (w +P u) = z))
88	85, 87	anim12i 333	. . . . . . . 8 ⊢ ((y<P x ⋀ w<P z) → (∃v(v ∈ P ⋀ (y +P v) = x) ⋀ ∃u(u ∈ P ⋀ (w +P u) = z)))
89		eeanv 1325	. . . . . . . 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 200	. . . . . . 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 21	. . . . . 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 5132	. . . . . . . 8 ⊢ (((x ·P z) ∈ P ⋀ (y ·P w) ∈ P) → ((x ·P z) +P (y ·P w)) ∈ P)
93		mulclpr 5134	. . . . . . . 8 ⊢ ((x ∈ P ⋀ z ∈ P) → (x ·P z) ∈ P)
94		mulclpr 5134	. . . . . . . 8 ⊢ ((y ∈ P ⋀ w ∈ P) → (y ·P w) ∈ P)
95	92, 93, 94	syl2an 456	. . . . . . 7 ⊢ (((x ∈ P ⋀ z ∈ P) ⋀ (y ∈ P ⋀ w ∈ P)) → ((x ·P z) +P (y ·P w)) ∈ P)
96	95	an4s 510	. . . . . 6 ⊢ (((x ∈ P ⋀ y ∈ P) ⋀ (z ∈ P ⋀ w ∈ P)) → ((x ·P z) +P (y ·P w)) ∈ P)
97		simprr 417	. . . . . 6 ⊢ (((x ∈ P ⋀ y ∈ P) ⋀ (z ∈ P ⋀ w ∈ P)) → w ∈ P)
98	91, 96, 97	sylanc 473	. . . . 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))))
99		mulsrpr 5197	. . . . . . 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 )
100	99	breq2d 2635	. . . . . 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 ))
101		oprex 3989	. . . . . . 7 ⊢ ((x ·P w) +P (y ·P z)) ∈ V
102	20, 101	gt0srpr 5199	. . . . . 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)))
103	100, 102	syl6bb 538	. . . . 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))))
104	98, 103	sylibrd 204	. . . 4 ⊢ (((x ∈ P ⋀ y ∈ P) ⋀ (z ∈ P ⋀ w ∈ P)) → ((y<P x ⋀ w<P z) → 0R <R ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R )))
105	84, 31	gt0srpr 5199	. . . . 5 ⊢ (0R <R [⟨x, y⟩] ~R ↔ y<P x)
106	86, 26	gt0srpr 5199	. . . . 5 ⊢ (0R <R [⟨z, w⟩] ~R ↔ w<P z)
107	105, 106	anbi12i 484	. . . 4 ⊢ ((0R <R [⟨x, y⟩] ~R ⋀ 0R <R [⟨z, w⟩] ~R ) ↔ (y<P x ⋀ w<P z))
108	104, 107	syl5ib 206	. . 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 )))
109	9, 14, 19, 108	2ecoptocl 4310	. 2 ⊢ ((A ∈ R ⋀ B ∈ R) → ((0R <R A ⋀ 0R <R B) → 0R <R (A ·R B)))
110	8, 109	mpcom 49	1 ⊢ ((0R <R A ⋀ 0R <R B) → 0R <R (A ·R B))

Syntax hints:   → wi 3   ⋀ wa 223   = wceq 958   ∈ wcel 960  ∃wex 982  Vcvv 1814  ⟨cop 2415   class class class wbr 2624  (class class class)co 3969  [cec 4265  Pcnp 4997   +_P cpp 4999   ·_P cmp 5000  <_P cltp 5001   ~_R cer 5004  Rcnr 5005  0_Rc0r 5006   ·_R cmr 5010   <_R cltr 5011

This theorem is referenced by:  sqgt0sr 5227  pre-axmulgt0 5302

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if