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 mulgnn0cl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
36 31 33 34 35 syl3anc ⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
37 simpr32 ⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) ) ) → 𝑛 ∈ ℕ0 )
38 1nn0 ⊢ 1 ∈ ℕ0
39 38 a1i ⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) ) ) → 1 ∈ ℕ0 )
40 37 39 nn0addcld ⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) ) ) → ( 𝑛 + 1 ) ∈ ℕ0 )
41 40 3anassrs ⊢ ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) ) → ( 𝑛 + 1 ) ∈ ℕ0 )
42 41 3anassrs ⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → ( 𝑛 + 1 ) ∈ ℕ0 )
43 1 3 mulgnn0cl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑛 + 1 ) ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑛 + 1 ) · 𝑋 ) ∈ 𝐵 )
44 31 42 34 43 syl3anc ⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → ( ( 𝑛 + 1 ) · 𝑋 ) ∈ 𝐵 )
45 32 36 44 3jca ⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → ( 0 ∈ 𝐵 ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑛 + 1 ) · 𝑋 ) ∈ 𝐵 ) )
46 simpr ⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → 0 ≤ ( 𝑛 · 𝑋 ) )
47 simp-4l ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ oMnd )
48 21 ad4antr ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
49 48 22 syl ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 0 ∈ 𝐵 )
50 simp-4r ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
51 simpr ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
52 48 51 50 35 syl3anc ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
53 simplr ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ 𝑋 )
54 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
55 1 2 54 omndadd ⊢ ( ( 𝑀 ∈ oMnd ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) ≤ ( 𝑋 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) )
56 47 49 50 52 53 55 syl131anc ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) ≤ ( 𝑋 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) )
57 1 54 4 mndlid ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) = ( 𝑛 · 𝑋 ) )
58 48 52 57 syl2anc ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 0 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) = ( 𝑛 · 𝑋 ) )
59 38 a1i ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 1 ∈ ℕ0 )
60 1 3 54 mulgnn0dir ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 1 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 1 + 𝑛 ) · 𝑋 ) = ( ( 1 · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) )
61 48 59 51 50 60 syl13anc ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 + 𝑛 ) · 𝑋 ) = ( ( 1 · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) )
62 1cnd ⊢ ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) → 1 ∈ ℂ )
63 simpr3 ⊢ ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑛 ∈ ℕ0 )
64 63 nn0cnd ⊢ ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑛 ∈ ℂ )
65 62 64 addcomd ⊢ ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) → ( 1 + 𝑛 ) = ( 𝑛 + 1 ) )
66 65 3anassrs ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 1 + 𝑛 ) = ( 𝑛 + 1 ) )
67 66 oveq1d ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 + 𝑛 ) · 𝑋 ) = ( ( 𝑛 + 1 ) · 𝑋 ) )
68 1 3 mulg1 ⊢ ( 𝑋 ∈ 𝐵 → ( 1 · 𝑋 ) = 𝑋 )
69 50 68 syl ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 1 · 𝑋 ) = 𝑋 )
70 69 oveq1d ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 · 𝑋 ) ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) = ( 𝑋 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) )
71 61 67 70 3eqtr3rd ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑋 ( +g ‘ 𝑀 ) ( 𝑛 · 𝑋 ) ) = ( ( 𝑛 + 1 ) · 𝑋 ) )
72 56 58 71 3brtr3d ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · 𝑋 ) ≤ ( ( 𝑛 + 1 ) · 𝑋 ) )
73 72 adantr ⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → ( 𝑛 · 𝑋 ) ≤ ( ( 𝑛 + 1 ) · 𝑋 ) )
74 1 2 postr ⊢ ( ( 𝑀 ∈ Poset ∧ ( 0 ∈ 𝐵 ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑛 + 1 ) · 𝑋 ) ∈ 𝐵 ) ) → ( ( 0 ≤ ( 𝑛 · 𝑋 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) → 0 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) )
75 74 imp ⊢ ( ( ( 𝑀 ∈ Poset ∧ ( 0 ∈ 𝐵 ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑛 + 1 ) · 𝑋 ) ∈ 𝐵 ) ) ∧ ( 0 ≤ ( 𝑛 · 𝑋 ) ∧ ( 𝑛 · 𝑋 ) ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) ) → 0 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) )
76 30 45 46 73 75 syl22anc ⊢ ( ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 0 ≤ ( 𝑛 · 𝑋 ) ) → 0 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) )
77 11 13 15 17 29 76 nn0indd ⊢ ( ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ ( 𝑁 · 𝑋 ) )
78 9 77 mpdan ⊢ ( ( ( ( 𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → 0 ≤ ( 𝑁 · 𝑋 ) )
79 8 78 sylbi ⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) ∧ 0 ≤ 𝑋 ) → 0 ≤ ( 𝑁 · 𝑋 ) )