Metamath Proof Explorer

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 ≤ ( 𝑁 · 𝑋 ) )