Theorem mulgt0sr 6704

Description: The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.)

Assertion

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

Proof of Theorem mulgt0sr

Dummy variables x y z w v u f g ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltrelsr 6666	. . . . 5 ⊢ <R ⊆ (R × R)
2	1	brel 4335	. . . 4 ⊢ (0R <R A → (0R ∈ R ∧ A ∈ R))
3	2	simprd 107	. . 3 ⊢ (0R <R A → A ∈ R)
4	1	brel 4335	. . . 4 ⊢ (0R <R B → (0R ∈ R ∧ B ∈ R))
5	4	simprd 107	. . 3 ⊢ (0R <R B → B ∈ R)
6	3, 5	anim12i 321	. 2 ⊢ ((0R <R A ∧ 0R <R B) → (A ∈ R ∧ B ∈ R))
7		df-nr 6655	. . 3 ⊢ R = ((P × P) / ~R )
8		breq2 3759	. . . . 5 ⊢ ([⟨x, y⟩] ~R = A → (0R <R [⟨x, y⟩] ~R ↔ 0R <R A))
9	8	anbi1d 438	. . . 4 ⊢ ([⟨x, y⟩] ~R = A → ((0R <R [⟨x, y⟩] ~R ∧ 0R <R [⟨z, w⟩] ~R ) ↔ (0R <R A ∧ 0R <R [⟨z, w⟩] ~R )))
10		oveq1 5462	. . . . 5 ⊢ ([⟨x, y⟩] ~R = A → ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R ) = (A ·R [⟨z, w⟩] ~R ))
11	10	breq2d 3767	. . . 4 ⊢ ([⟨x, y⟩] ~R = A → (0R <R ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R ) ↔ 0R <R (A ·R [⟨z, w⟩] ~R )))
12	9, 11	imbi12d 223	. . 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 ))))
13		breq2 3759	. . . . 5 ⊢ ([⟨z, w⟩] ~R = B → (0R <R [⟨z, w⟩] ~R ↔ 0R <R B))
14	13	anbi2d 437	. . . 4 ⊢ ([⟨z, w⟩] ~R = B → ((0R <R A ∧ 0R <R [⟨z, w⟩] ~R ) ↔ (0R <R A ∧ 0R <R B)))
15		oveq2 5463	. . . . 5 ⊢ ([⟨z, w⟩] ~R = B → (A ·R [⟨z, w⟩] ~R ) = (A ·R B))
16	15	breq2d 3767	. . . 4 ⊢ ([⟨z, w⟩] ~R = B → (0R <R (A ·R [⟨z, w⟩] ~R ) ↔ 0R <R (A ·R B)))
17	14, 16	imbi12d 223	. . 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))))
18		gt0srpr 6676	. . . . 5 ⊢ (0R <R [⟨x, y⟩] ~R ↔ y<P x)
19		gt0srpr 6676	. . . . 5 ⊢ (0R <R [⟨z, w⟩] ~R ↔ w<P z)
20	18, 19	anbi12i 433	. . . 4 ⊢ ((0R <R [⟨x, y⟩] ~R ∧ 0R <R [⟨z, w⟩] ~R ) ↔ (y<P x ∧ w<P z))
21		ltexpri 6587	. . . . . . 7 ⊢ (y<P x → ∃v ∈ P (y +P v) = x)
22		ltexpri 6587	. . . . . . . . 9 ⊢ (w<P z → ∃u ∈ P (w +P u) = z)
23		addclpr 6520	. . . . . . . . . . . . . 14 ⊢ ((f ∈ P ∧ g ∈ P) → (f +P g) ∈ P)
24	23	adantl 262	. . . . . . . . . . . . 13 ⊢ ((((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) ∧ (f ∈ P ∧ g ∈ P)) → (f +P g) ∈ P)
25		simplrr 488	. . . . . . . . . . . . . . 15 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (y +P v) = x)
26		simplr 482	. . . . . . . . . . . . . . . . 17 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → y ∈ P)
27	26	ad2antrr 457	. . . . . . . . . . . . . . . 16 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → y ∈ P)
28		simplrl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → v ∈ P)
29	24, 27, 28	caovcld 5596	. . . . . . . . . . . . . . 15 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (y +P v) ∈ P)
30	25, 29	eqeltrrd 2112	. . . . . . . . . . . . . 14 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → x ∈ P)
31		simplrr 488	. . . . . . . . . . . . . . 15 ⊢ ((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) → w ∈ P)
32	31	adantr 261	. . . . . . . . . . . . . 14 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → w ∈ P)
33		mulclpr 6553	. . . . . . . . . . . . . 14 ⊢ ((x ∈ P ∧ w ∈ P) → (x ·P w) ∈ P)
34	30, 32, 33	syl2anc 391	. . . . . . . . . . . . 13 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (x ·P w) ∈ P)
35		simplrl 487	. . . . . . . . . . . . . . 15 ⊢ ((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) → z ∈ P)
36	35	adantr 261	. . . . . . . . . . . . . 14 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → z ∈ P)
37		mulclpr 6553	. . . . . . . . . . . . . 14 ⊢ ((y ∈ P ∧ z ∈ P) → (y ·P z) ∈ P)
38	27, 36, 37	syl2anc 391	. . . . . . . . . . . . 13 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (y ·P z) ∈ P)
39	24, 34, 38	caovcld 5596	. . . . . . . . . . . 12 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((x ·P w) +P (y ·P z)) ∈ P)
40		simprl 483	. . . . . . . . . . . . 13 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → u ∈ P)
41		mulclpr 6553	. . . . . . . . . . . . 13 ⊢ ((v ∈ P ∧ u ∈ P) → (v ·P u) ∈ P)
42	28, 40, 41	syl2anc 391	. . . . . . . . . . . 12 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (v ·P u) ∈ P)
43		ltaddpr 6571	. . . . . . . . . . . 12 ⊢ ((((x ·P w) +P (y ·P z)) ∈ P ∧ (v ·P u) ∈ P) → ((x ·P w) +P (y ·P z))<P (((x ·P w) +P (y ·P z)) +P (v ·P u)))
44	39, 42, 43	syl2anc 391	. . . . . . . . . . 11 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ 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 w) +P (y ·P z)) +P (v ·P u)))
45		simprr 484	. . . . . . . . . . . . . . 15 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (w +P u) = z)
46		oveq12 5464	. . . . . . . . . . . . . . . 16 ⊢ (((y +P v) = x ∧ (w +P u) = z) → ((y +P v) ·P (w +P u)) = (x ·P z))
47	46	oveq1d 5470	. . . . . . . . . . . . . . 15 ⊢ (((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))))
48	25, 45, 47	syl2anc 391	. . . . . . . . . . . . . 14 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (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))))
49		distrprg 6564	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ P ∧ w ∈ P ∧ u ∈ P) → (y ·P (w +P u)) = ((y ·P w) +P (y ·P u)))
50	27, 32, 40, 49	syl3anc 1134	. . . . . . . . . . . . . . . . . 18 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (y ·P (w +P u)) = ((y ·P w) +P (y ·P u)))
51		oveq2 5463	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((w +P u) = z → (y ·P (w +P u)) = (y ·P z))
52	51	adantl 262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((u ∈ P ∧ (w +P u) = z) → (y ·P (w +P u)) = (y ·P z))
53	52	adantl 262	. . . . . . . . . . . . . . . . . 18 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (y ·P (w +P u)) = (y ·P z))
54	50, 53	eqtr3d 2071	. . . . . . . . . . . . . . . . 17 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((y ·P w) +P (y ·P u)) = (y ·P z))
55	54	oveq1d 5470	. . . . . . . . . . . . . . . 16 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (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))))
56		distrprg 6564	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → (f ·P (g +P ℎ)) = ((f ·P g) +P (f ·P ℎ)))
57	56	adantl 262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) ∧ (f ∈ P ∧ g ∈ P ∧ ℎ ∈ P)) → (f ·P (g +P ℎ)) = ((f ·P g) +P (f ·P ℎ)))
58		mulcomprg 6556	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((f ∈ P ∧ g ∈ P) → (f ·P g) = (g ·P f))
59	58	adantl 262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) ∧ (f ∈ P ∧ g ∈ P)) → (f ·P g) = (g ·P f))
60	57, 27, 28, 32, 24, 59	caovdir2d 5619	. . . . . . . . . . . . . . . . . 18 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((y +P v) ·P w) = ((y ·P w) +P (v ·P w)))
61	57, 27, 28, 40, 24, 59	caovdir2d 5619	. . . . . . . . . . . . . . . . . 18 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((y +P v) ·P u) = ((y ·P u) +P (v ·P u)))
62	60, 61	oveq12d 5473	. . . . . . . . . . . . . . . . 17 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (((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))))
63		distrprg 6564	. . . . . . . . . . . . . . . . . 18 ⊢ (((y +P v) ∈ P ∧ w ∈ P ∧ u ∈ P) → ((y +P v) ·P (w +P u)) = (((y +P v) ·P w) +P ((y +P v) ·P u)))
64	29, 32, 40, 63	syl3anc 1134	. . . . . . . . . . . . . . . . 17 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((y +P v) ·P (w +P u)) = (((y +P v) ·P w) +P ((y +P v) ·P u)))
65		mulclpr 6553	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ P ∧ w ∈ P) → (y ·P w) ∈ P)
66	27, 32, 65	syl2anc 391	. . . . . . . . . . . . . . . . . 18 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (y ·P w) ∈ P)
67		mulclpr 6553	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ P ∧ u ∈ P) → (y ·P u) ∈ P)
68	27, 40, 67	syl2anc 391	. . . . . . . . . . . . . . . . . 18 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (y ·P u) ∈ P)
69		mulclpr 6553	. . . . . . . . . . . . . . . . . . 19 ⊢ ((v ∈ P ∧ w ∈ P) → (v ·P w) ∈ P)
70	28, 32, 69	syl2anc 391	. . . . . . . . . . . . . . . . . 18 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (v ·P w) ∈ P)
71		addcomprg 6554	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f ∈ P ∧ g ∈ P) → (f +P g) = (g +P f))
72	71	adantl 262	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) ∧ (f ∈ P ∧ g ∈ P)) → (f +P g) = (g +P f))
73		addassprg 6555	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → ((f +P g) +P ℎ) = (f +P (g +P ℎ)))
74	73	adantl 262	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) ∧ (f ∈ P ∧ g ∈ P ∧ ℎ ∈ P)) → ((f +P g) +P ℎ) = (f +P (g +P ℎ)))
75	66, 68, 70, 72, 74, 42, 24	caov4d 5627	. . . . . . . . . . . . . . . . 17 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (((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))))
76	62, 64, 75	3eqtr4d 2079	. . . . . . . . . . . . . . . 16 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((y +P v) ·P (w +P u)) = (((y ·P w) +P (y ·P u)) +P ((v ·P w) +P (v ·P u))))
77	70, 38, 42, 72, 74	caov12d 5624	. . . . . . . . . . . . . . . 16 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((v ·P w) +P ((y ·P z) +P (v ·P u))) = ((y ·P z) +P ((v ·P w) +P (v ·P u))))
78	55, 76, 77	3eqtr4d 2079	. . . . . . . . . . . . . . 15 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((y +P v) ·P (w +P u)) = ((v ·P w) +P ((y ·P z) +P (v ·P u))))
79		oveq1 5462	. . . . . . . . . . . . . . . . . 18 ⊢ ((y +P v) = x → ((y +P v) ·P w) = (x ·P w))
80	79	adantl 262	. . . . . . . . . . . . . . . . 17 ⊢ ((v ∈ P ∧ (y +P v) = x) → ((y +P v) ·P w) = (x ·P w))
81	80	ad2antlr 458	. . . . . . . . . . . . . . . 16 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((y +P v) ·P w) = (x ·P w))
82	60, 81	eqtr3d 2071	. . . . . . . . . . . . . . 15 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((y ·P w) +P (v ·P w)) = (x ·P w))
83	78, 82	oveq12d 5473	. . . . . . . . . . . . . 14 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (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)))
84	48, 83	eqtr3d 2071	. . . . . . . . . . . . 13 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (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)))
85		mulclpr 6553	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ P ∧ z ∈ P) → (x ·P z) ∈ P)
86	30, 36, 85	syl2anc 391	. . . . . . . . . . . . . . 15 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (x ·P z) ∈ P)
87		addassprg 6555	. . . . . . . . . . . . . . 15 ⊢ (((x ·P z) ∈ P ∧ (y ·P w) ∈ P ∧ (v ·P w) ∈ P) → (((x ·P z) +P (y ·P w)) +P (v ·P w)) = ((x ·P z) +P ((y ·P w) +P (v ·P w))))
88	86, 66, 70, 87	syl3anc 1134	. . . . . . . . . . . . . 14 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (((x ·P z) +P (y ·P w)) +P (v ·P w)) = ((x ·P z) +P ((y ·P w) +P (v ·P w))))
89		addclpr 6520	. . . . . . . . . . . . . . . 16 ⊢ (((x ·P z) ∈ P ∧ (y ·P w) ∈ P) → ((x ·P z) +P (y ·P w)) ∈ P)
90	86, 66, 89	syl2anc 391	. . . . . . . . . . . . . . 15 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((x ·P z) +P (y ·P w)) ∈ P)
91		addcomprg 6554	. . . . . . . . . . . . . . 15 ⊢ ((((x ·P z) +P (y ·P w)) ∈ P ∧ (v ·P w) ∈ P) → (((x ·P z) +P (y ·P w)) +P (v ·P w)) = ((v ·P w) +P ((x ·P z) +P (y ·P w))))
92	90, 70, 91	syl2anc 391	. . . . . . . . . . . . . 14 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (((x ·P z) +P (y ·P w)) +P (v ·P w)) = ((v ·P w) +P ((x ·P z) +P (y ·P w))))
93	88, 92	eqtr3d 2071	. . . . . . . . . . . . 13 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((x ·P z) +P ((y ·P w) +P (v ·P w))) = ((v ·P w) +P ((x ·P z) +P (y ·P w))))
94	24, 38, 42	caovcld 5596	. . . . . . . . . . . . . . 15 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((y ·P z) +P (v ·P u)) ∈ P)
95		addassprg 6555	. . . . . . . . . . . . . . 15 ⊢ (((v ·P w) ∈ P ∧ (x ·P w) ∈ P ∧ ((y ·P z) +P (v ·P u)) ∈ P) → (((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)))))
96	70, 34, 94, 95	syl3anc 1134	. . . . . . . . . . . . . 14 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (((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)))))
97	70, 94, 34, 72, 74	caov32d 5623	. . . . . . . . . . . . . 14 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (((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))))
98		addassprg 6555	. . . . . . . . . . . . . . . 16 ⊢ (((x ·P w) ∈ P ∧ (y ·P z) ∈ P ∧ (v ·P u) ∈ P) → (((x ·P w) +P (y ·P z)) +P (v ·P u)) = ((x ·P w) +P ((y ·P z) +P (v ·P u))))
99	34, 38, 42, 98	syl3anc 1134	. . . . . . . . . . . . . . 15 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (((x ·P w) +P (y ·P z)) +P (v ·P u)) = ((x ·P w) +P ((y ·P z) +P (v ·P u))))
100	99	oveq2d 5471	. . . . . . . . . . . . . 14 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((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)))))
101	96, 97, 100	3eqtr4d 2079	. . . . . . . . . . . . 13 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (((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))))
102	84, 93, 101	3eqtr3d 2077	. . . . . . . . . . . 12 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (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))))
103	24, 39, 42	caovcld 5596	. . . . . . . . . . . . 13 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → (((x ·P w) +P (y ·P z)) +P (v ·P u)) ∈ P)
104		addcanprg 6590	. . . . . . . . . . . . 13 ⊢ (((v ·P w) ∈ P ∧ ((x ·P z) +P (y ·P w)) ∈ P ∧ (((x ·P w) +P (y ·P z)) +P (v ·P u)) ∈ 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))))
105	70, 90, 103, 104	syl3anc 1134	. . . . . . . . . . . 12 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (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))) → ((x ·P z) +P (y ·P w)) = (((x ·P w) +P (y ·P z)) +P (v ·P u))))
106	102, 105	mpd 13	. . . . . . . . . . 11 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) ∧ (u ∈ P ∧ (w +P u) = z)) → ((x ·P z) +P (y ·P w)) = (((x ·P w) +P (y ·P z)) +P (v ·P u)))
107	44, 106	breqtrrd 3781	. . . . . . . . . 10 ⊢ (((((x ∈ P ∧ y ∈ P) ∧ (z ∈ 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)))
108	107	rexlimdvaa 2428	. . . . . . . . 9 ⊢ ((((x ∈ P ∧ y ∈ P) ∧ (z ∈ 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))))
109	22, 108	syl5 28	. . . . . . . 8 ⊢ ((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) ∧ (v ∈ P ∧ (y +P v) = x)) → (w<P z → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w))))
110	109	rexlimdvaa 2428	. . . . . . 7 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → (∃v ∈ P (y +P v) = x → (w<P z → ((x ·P w) +P (y ·P z))<P ((x ·P z) +P (y ·P w)))))
111	21, 110	syl5 28	. . . . . 6 ⊢ (((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)))))
112	111	impd 242	. . . . 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))))
113		mulsrpr 6674	. . . . . . 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 )
114	113	breq2d 3767	. . . . . 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 ))
115		gt0srpr 6676	. . . . . 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)))
116	114, 115	syl6bb 185	. . . . 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))))
117	112, 116	sylibrd 158	. . . 4 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ((y<P x ∧ w<P z) → 0R <R ([⟨x, y⟩] ~R ·R [⟨z, w⟩] ~R )))
118	20, 117	syl5bi 141	. . 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 )))
119	7, 12, 17, 118	2ecoptocl 6130	. 2 ⊢ ((A ∈ R ∧ B ∈ R) → ((0R <R A ∧ 0R <R B) → 0R <R (A ·R B)))
120	6, 119	mpcom 32	1 ⊢ ((0R <R A ∧ 0R <R B) → 0R <R (A ·R B))

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ∃wrex 2301  ⟨cop 3370   class class class wbr 3755  (class class class)co 5455  [cec 6040  Pcnp 6275   +_P cpp 6277   ·_P cmp 6278  <_P cltp 6279   ~_R cer 6280  Rcnr 6281  0_Rc0r 6282   ·_R cmr 6286   <_R cltr 6287

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-po 4024  df-iso 4025  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-2o 5941  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-pli 6289  df-mi 6290  df-lti 6291  df-plpq 6328  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-plqqs 6333  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337  df-enq0 6407  df-nq0 6408  df-0nq0 6409  df-plq0 6410  df-mq0 6411  df-inp 6449  df-i1p 6450  df-iplp 6451  df-imp 6452  df-iltp 6453  df-enr 6654  df-nr 6655  df-mr 6657  df-ltr 6658  df-0r 6659

This theorem is referenced by:  axpre-mulgt0  6771