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 𝐵 ) )