Theorem omndmul2

Description: In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018)

	Ref	Expression
Hypotheses	omndmul.0	⊢ 𝐵 = ( Base ‘ 𝑀 )
	omndmul.1	⊢ ≤ = ( le ‘ 𝑀 )
	omndmul2.2	⊢ · = ( .g ‘ 𝑀 )
	omndmul2.3	⊢ 0 = ( 0g ‘ 𝑀 )
Assertion	omndmul2	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → 0 ≤ ( 𝑁 · 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		omndmul.0	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		omndmul.1	⊢ ≤ = ( le ‘ 𝑀 )
3		omndmul2.2	⊢ · = ( .g ‘ 𝑀 )
4		omndmul2.3	⊢ 0 = ( 0g ‘ 𝑀 )
5		df-3an	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ↔ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) ) ∧ 0 ≤ 𝑋 ) )
6		anass	⊢ ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ↔ ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) ) )
7	6	anbi1i	⊢ ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ↔ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) ) ∧ 0 ≤ 𝑋 ) )
8	5 7	bitr4i	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ↔ ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) )
9		simplr	⊢ ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → 𝑁 ∈ ℕ0 )
10		oveq1	⊢ ( 𝑚 = 0 → ( 𝑚 · 𝑋 ) = ( 0 · 𝑋 ) )
11	10	breq2d	⊢ ( 𝑚 = 0 → ( 0 ≤ ( 𝑚 · 𝑋 ) ↔ 0 ≤ ( 0 · 𝑋 ) ) )
12		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 · 𝑋 ) = ( 𝑛 · 𝑋 ) )
13	12	breq2d	⊢ ( 𝑚 = 𝑛 → ( 0 ≤ ( 𝑚 · 𝑋 ) ↔ 0 ≤ ( 𝑛 · 𝑋 ) ) )
14		oveq1	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 · 𝑋 ) = ( ( 𝑛 + 1 ) · 𝑋 ) )
15	14	breq2d	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 0 ≤ ( 𝑚 · 𝑋 ) ↔ 0 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) )
16		oveq1	⊢ ( 𝑚 = 𝑁 → ( 𝑚 · 𝑋 ) = ( 𝑁 · 𝑋 ) )
17	16	breq2d	⊢ ( 𝑚 = 𝑁 → ( 0 ≤ ( 𝑚 · 𝑋 ) ↔ 0 ≤ ( 𝑁 · 𝑋 ) ) )
18		omndtos	⊢ ( 𝑀 ∈ oMnd → 𝑀 ∈ Toset )
19		tospos	⊢ ( 𝑀 ∈ Toset → 𝑀 ∈ Poset )
20	18 19	syl	⊢ ( 𝑀 ∈ oMnd → 𝑀 ∈ Poset )
21		omndmnd	⊢ ( 𝑀 ∈ oMnd → 𝑀 ∈ Mnd )
22	1 4	mndidcl	⊢ ( 𝑀 ∈ Mnd → 0 ∈ 𝐵 )
23	21 22	syl	⊢ ( 𝑀 ∈ oMnd → 0 ∈ 𝐵 )
24	1 2	posref	⊢ ( ( 𝑀 ∈ Poset ∧ 0 ∈ 𝐵 ) → 0 ≤ 0 )
25	20 23 24	syl2anc	⊢ ( 𝑀 ∈ oMnd → 0 ≤ 0 )
26	25	ad3antrrr	⊢ ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → 0 ≤ 0 )
27	1 4 3	mulg0	⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = 0 )
28	27	ad3antlr	⊢ ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → ( 0 · 𝑋 ) = 0 )
29	26 28	breqtrrd	⊢ ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → 0 ≤ ( 0 · 𝑋 ) )
30	20	ad5antr	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → 𝑀 ∈ Poset )
31	21	ad5antr	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → 𝑀 ∈ Mnd )
32	31 22	syl	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → 0 ∈ 𝐵 )
33		simplr	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → 𝑛 ∈ ℕ0 )
34		simp-5r	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → 𝑋 ∈ 𝐵 )
35	1 3 31 33 34	mulgnn0cld	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
36		simpr32	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) ) ) → 𝑛 ∈ ℕ0 )
37		1nn0	⊢ 1 ∈ ℕ0
38	37	a1i	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) ) ) → 1 ∈ ℕ0 )
39	36 38	nn0addcld	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) ) ) → ( 𝑛 + 1 ) ∈ ℕ0 )
40	39	3anassrs	⊢ ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) ) → ( 𝑛 + 1 ) ∈ ℕ0 )
41	40	3anassrs	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → ( 𝑛 + 1 ) ∈ ℕ0 )
42	1 3 31 41 34	mulgnn0cld	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → ( ( 𝑛 + 1 ) · 𝑋 ) ∈ 𝐵 )
43	32 35 42	3jca	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → ( 0 ∈ 𝐵 ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑛 + 1 ) · 𝑋 ) ∈ 𝐵 ) )
44		simpr	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → 0 ≤ ( 𝑛 · 𝑋 ) )
45		simp-4l	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ oMnd )
46	21	ad4antr	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
47	46 22	syl	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 0 ∈ 𝐵 )
48		simp-4r	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
49		simpr	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
50	1 3 46 49 48	mulgnn0cld	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
51		simplr	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ 𝑋 )
52		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
53	1 2 52	omndadd	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) ≤ ( 𝑋 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) )
54	45 47 48 50 51 53	syl131anc	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) ≤ ( 𝑋 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) )
55	1 52 4	mndlid	⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) = ( 𝑛 · 𝑋 ) )
56	46 50 55	syl2anc	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) = ( 𝑛 · 𝑋 ) )
57	37	a1i	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 1 ∈ ℕ0 )
58	1 3 52	mulgnn0dir	⊢ ( ( 𝑀 ∈ Mnd ∧ ( 1 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 1 + 𝑛 ) · 𝑋 ) = ( ( 1 · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) )
59	46 57 49 48 58	syl13anc	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 + 𝑛 ) · 𝑋 ) = ( ( 1 · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) )
60		1cnd	⊢ ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) → 1 ∈ ℂ )
61		simpr3	⊢ ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑛 ∈ ℕ0 )
62	61	nn0cnd	⊢ ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑛 ∈ ℂ )
63	60 62	addcomd	⊢ ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) → ( 1 + 𝑛 ) = ( 𝑛 + 1 ) )
64	63	3anassrs	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 1 + 𝑛 ) = ( 𝑛 + 1 ) )
65	64	oveq1d	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 + 𝑛 ) · 𝑋 ) = ( ( 𝑛 + 1 ) · 𝑋 ) )
66	1 3	mulg1	⊢ ( 𝑋 ∈ 𝐵 → ( 1 · 𝑋 ) = 𝑋 )
67	48 66	syl	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 1 · 𝑋 ) = 𝑋 )
68	67	oveq1d	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) = ( 𝑋 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) )
69	59 65 68	3eqtr3rd	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑋 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) = ( ( 𝑛 + 1 ) · 𝑋 ) )
70	54 56 69	3brtr3d	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · 𝑋 ) ≤ ( ( 𝑛 + 1 ) · 𝑋 ) )
71	70	adantr	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → ( 𝑛 · 𝑋 ) ≤ ( ( 𝑛 + 1 ) · 𝑋 ) )
72	1 2	postr	⊢ ( ( 𝑀 ∈ Poset ∧ ( 0 ∈ 𝐵 ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑛 + 1 ) · 𝑋 ) ∈ 𝐵 ) ) → ( ( 0 ≤ ( 𝑛 · 𝑋 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) → 0 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) )
73	72	imp	⊢ ( ( ( 𝑀 ∈ Poset ∧ ( 0 ∈ 𝐵 ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑛 + 1 ) · 𝑋 ) ∈ 𝐵 ) ) ∧ ( 0 ≤ ( 𝑛 · 𝑋 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) ) → 0 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) )
74	30 43 44 71 73	syl22anc	⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → 0 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) )
75	11 13 15 17 29 74	nn0indd	⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ ( 𝑁 · 𝑋 ) )
76	9 75	mpdan	⊢ ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → 0 ≤ ( 𝑁 · 𝑋 ) )
77	8 76	sylbi	⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → 0 ≤ ( 𝑁 · 𝑋 ) )