Step | Hyp | Ref
| Expression |
1 | | df-3an 1089 |
. . 3
⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ↔ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0)) ∧ 0 ≤ 𝑋)) |
2 | | anass 469 |
. . . 4
⊢ (((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ↔ (𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈
ℕ0))) |
3 | 2 | anbi1i 624 |
. . 3
⊢ ((((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ↔ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0)) ∧ 0 ≤ 𝑋)) |
4 | 1, 3 | bitr4i 277 |
. 2
⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ↔ (((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋)) |
5 | | simplr 767 |
. . 3
⊢ ((((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) → 𝑁 ∈
ℕ0) |
6 | | oveq1 7364 |
. . . . 5
⊢ (𝑚 = 0 → (𝑚 · 𝑋) = (0 · 𝑋)) |
7 | 6 | breq2d 5117 |
. . . 4
⊢ (𝑚 = 0 → ( 0 ≤ (𝑚 · 𝑋) ↔ 0 ≤ (0 · 𝑋))) |
8 | | oveq1 7364 |
. . . . 5
⊢ (𝑚 = 𝑛 → (𝑚 · 𝑋) = (𝑛 · 𝑋)) |
9 | 8 | breq2d 5117 |
. . . 4
⊢ (𝑚 = 𝑛 → ( 0 ≤ (𝑚 · 𝑋) ↔ 0 ≤ (𝑛 · 𝑋))) |
10 | | oveq1 7364 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (𝑚 · 𝑋) = ((𝑛 + 1) · 𝑋)) |
11 | 10 | breq2d 5117 |
. . . 4
⊢ (𝑚 = (𝑛 + 1) → ( 0 ≤ (𝑚 · 𝑋) ↔ 0 ≤ ((𝑛 + 1) · 𝑋))) |
12 | | oveq1 7364 |
. . . . 5
⊢ (𝑚 = 𝑁 → (𝑚 · 𝑋) = (𝑁 · 𝑋)) |
13 | 12 | breq2d 5117 |
. . . 4
⊢ (𝑚 = 𝑁 → ( 0 ≤ (𝑚 · 𝑋) ↔ 0 ≤ (𝑁 · 𝑋))) |
14 | | omndtos 31913 |
. . . . . . . 8
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) |
15 | | tospos 18309 |
. . . . . . . 8
⊢ (𝑀 ∈ Toset → 𝑀 ∈ Poset) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Poset) |
17 | | omndmnd 31912 |
. . . . . . . 8
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd) |
18 | | omndmul.0 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑀) |
19 | | omndmul2.3 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑀) |
20 | 18, 19 | mndidcl 18571 |
. . . . . . . 8
⊢ (𝑀 ∈ Mnd → 0 ∈ 𝐵) |
21 | 17, 20 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ oMnd → 0 ∈ 𝐵) |
22 | | omndmul.1 |
. . . . . . . 8
⊢ ≤ =
(le‘𝑀) |
23 | 18, 22 | posref 18207 |
. . . . . . 7
⊢ ((𝑀 ∈ Poset ∧ 0 ∈ 𝐵) → 0 ≤ 0 ) |
24 | 16, 21, 23 | syl2anc 584 |
. . . . . 6
⊢ (𝑀 ∈ oMnd → 0 ≤ 0
) |
25 | 24 | ad3antrrr 728 |
. . . . 5
⊢ ((((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) → 0 ≤ 0 ) |
26 | | omndmul2.2 |
. . . . . . 7
⊢ · =
(.g‘𝑀) |
27 | 18, 19, 26 | mulg0 18879 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 ) |
28 | 27 | ad3antlr 729 |
. . . . 5
⊢ ((((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) → (0 · 𝑋) = 0 ) |
29 | 25, 28 | breqtrrd 5133 |
. . . 4
⊢ ((((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) → 0 ≤ (0 · 𝑋)) |
30 | 16 | ad5antr 732 |
. . . . 5
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → 𝑀 ∈ Poset) |
31 | 17 | ad5antr 732 |
. . . . . . 7
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → 𝑀 ∈ Mnd) |
32 | 31, 20 | syl 17 |
. . . . . 6
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → 0 ∈ 𝐵) |
33 | | simplr 767 |
. . . . . . 7
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → 𝑛 ∈ ℕ0) |
34 | | simp-5r 784 |
. . . . . . 7
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → 𝑋 ∈ 𝐵) |
35 | 18, 26, 31, 33, 34 | mulgnn0cld 18897 |
. . . . . 6
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → (𝑛 · 𝑋) ∈ 𝐵) |
36 | | simpr32 1264 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ (𝑛 · 𝑋)))) → 𝑛 ∈ ℕ0) |
37 | | 1nn0 12429 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
38 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ (𝑛 · 𝑋)))) → 1 ∈
ℕ0) |
39 | 36, 38 | nn0addcld 12477 |
. . . . . . . . 9
⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ (𝑛 · 𝑋)))) → (𝑛 + 1) ∈
ℕ0) |
40 | 39 | 3anassrs 1360 |
. . . . . . . 8
⊢ ((((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ ( 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0 ∧ 0 ≤ (𝑛 · 𝑋))) → (𝑛 + 1) ∈
ℕ0) |
41 | 40 | 3anassrs 1360 |
. . . . . . 7
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → (𝑛 + 1) ∈
ℕ0) |
42 | 18, 26, 31, 41, 34 | mulgnn0cld 18897 |
. . . . . 6
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → ((𝑛 + 1) · 𝑋) ∈ 𝐵) |
43 | 32, 35, 42 | 3jca 1128 |
. . . . 5
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → ( 0 ∈ 𝐵 ∧ (𝑛 · 𝑋) ∈ 𝐵 ∧ ((𝑛 + 1) · 𝑋) ∈ 𝐵)) |
44 | | simpr 485 |
. . . . 5
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → 0 ≤ (𝑛 · 𝑋)) |
45 | | simp-4l 781 |
. . . . . . . 8
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → 𝑀 ∈ oMnd) |
46 | 17 | ad4antr 730 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → 𝑀 ∈ Mnd) |
47 | 46, 20 | syl 17 |
. . . . . . . 8
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → 0 ∈ 𝐵) |
48 | | simp-4r 782 |
. . . . . . . 8
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
49 | | simpr 485 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
50 | 18, 26, 46, 49, 48 | mulgnn0cld 18897 |
. . . . . . . 8
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → (𝑛 · 𝑋) ∈ 𝐵) |
51 | | simplr 767 |
. . . . . . . 8
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → 0 ≤ 𝑋) |
52 | | eqid 2736 |
. . . . . . . . 9
⊢
(+g‘𝑀) = (+g‘𝑀) |
53 | 18, 22, 52 | omndadd 31914 |
. . . . . . . 8
⊢ ((𝑀 ∈ oMnd ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑛 · 𝑋) ∈ 𝐵) ∧ 0 ≤ 𝑋) → ( 0 (+g‘𝑀)(𝑛 · 𝑋)) ≤ (𝑋(+g‘𝑀)(𝑛 · 𝑋))) |
54 | 45, 47, 48, 50, 51, 53 | syl131anc 1383 |
. . . . . . 7
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → ( 0
(+g‘𝑀)(𝑛 · 𝑋)) ≤ (𝑋(+g‘𝑀)(𝑛 · 𝑋))) |
55 | 18, 52, 19 | mndlid 18576 |
. . . . . . . 8
⊢ ((𝑀 ∈ Mnd ∧ (𝑛 · 𝑋) ∈ 𝐵) → ( 0 (+g‘𝑀)(𝑛 · 𝑋)) = (𝑛 · 𝑋)) |
56 | 46, 50, 55 | syl2anc 584 |
. . . . . . 7
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → ( 0
(+g‘𝑀)(𝑛 · 𝑋)) = (𝑛 · 𝑋)) |
57 | 37 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → 1 ∈
ℕ0) |
58 | 18, 26, 52 | mulgnn0dir 18906 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ (1 ∈
ℕ0 ∧ 𝑛
∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((1 + 𝑛) · 𝑋) = ((1 · 𝑋)(+g‘𝑀)(𝑛 · 𝑋))) |
59 | 46, 57, 49, 48, 58 | syl13anc 1372 |
. . . . . . . 8
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → ((1 +
𝑛) · 𝑋) = ((1 · 𝑋)(+g‘𝑀)(𝑛 · 𝑋))) |
60 | | 1cnd 11150 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ (𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0)) → 1 ∈
ℂ) |
61 | | simpr3 1196 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ (𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0)) → 𝑛 ∈
ℕ0) |
62 | 61 | nn0cnd 12475 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ (𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0)) → 𝑛 ∈
ℂ) |
63 | 60, 62 | addcomd 11357 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ (𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑋 ∧ 𝑛 ∈ ℕ0)) → (1 +
𝑛) = (𝑛 + 1)) |
64 | 63 | 3anassrs 1360 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → (1 +
𝑛) = (𝑛 + 1)) |
65 | 64 | oveq1d 7372 |
. . . . . . . 8
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → ((1 +
𝑛) · 𝑋) = ((𝑛 + 1) · 𝑋)) |
66 | 18, 26 | mulg1 18883 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝐵 → (1 · 𝑋) = 𝑋) |
67 | 48, 66 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → (1 · 𝑋) = 𝑋) |
68 | 67 | oveq1d 7372 |
. . . . . . . 8
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → ((1 · 𝑋)(+g‘𝑀)(𝑛 · 𝑋)) = (𝑋(+g‘𝑀)(𝑛 · 𝑋))) |
69 | 59, 65, 68 | 3eqtr3rd 2785 |
. . . . . . 7
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → (𝑋(+g‘𝑀)(𝑛 · 𝑋)) = ((𝑛 + 1) · 𝑋)) |
70 | 54, 56, 69 | 3brtr3d 5136 |
. . . . . 6
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) → (𝑛 · 𝑋) ≤ ((𝑛 + 1) · 𝑋)) |
71 | 70 | adantr 481 |
. . . . 5
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → (𝑛 · 𝑋) ≤ ((𝑛 + 1) · 𝑋)) |
72 | 18, 22 | postr 18209 |
. . . . . 6
⊢ ((𝑀 ∈ Poset ∧ ( 0 ∈ 𝐵 ∧ (𝑛 · 𝑋) ∈ 𝐵 ∧ ((𝑛 + 1) · 𝑋) ∈ 𝐵)) → (( 0 ≤ (𝑛 · 𝑋) ∧ (𝑛 · 𝑋) ≤ ((𝑛 + 1) · 𝑋)) → 0 ≤ ((𝑛 + 1) · 𝑋))) |
73 | 72 | imp 407 |
. . . . 5
⊢ (((𝑀 ∈ Poset ∧ ( 0 ∈ 𝐵 ∧ (𝑛 · 𝑋) ∈ 𝐵 ∧ ((𝑛 + 1) · 𝑋) ∈ 𝐵)) ∧ ( 0 ≤ (𝑛 · 𝑋) ∧ (𝑛 · 𝑋) ≤ ((𝑛 + 1) · 𝑋))) → 0 ≤ ((𝑛 + 1) · 𝑋)) |
74 | 30, 43, 44, 71, 73 | syl22anc 837 |
. . . 4
⊢
((((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑛 ∈ ℕ0) ∧ 0 ≤ (𝑛 · 𝑋)) → 0 ≤ ((𝑛 + 1) · 𝑋)) |
75 | 7, 9, 11, 13, 29, 74 | nn0indd 12600 |
. . 3
⊢
(((((𝑀 ∈ oMnd
∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) ∧ 𝑁 ∈ ℕ0) → 0 ≤ (𝑁 · 𝑋)) |
76 | 5, 75 | mpdan 685 |
. 2
⊢ ((((𝑀 ∈ oMnd ∧ 𝑋 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) → 0 ≤ (𝑁 · 𝑋)) |
77 | 4, 76 | sylbi 216 |
1
⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) → 0 ≤ (𝑁 · 𝑋)) |