Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑛 = 1 → (𝑛 · 𝑁) = (1 · 𝑁)) |
2 | 1 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = 1 → ((𝑛 · 𝑁) · 𝑋) = ((1 · 𝑁) · 𝑋)) |
3 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = 1 → (𝑛 · (𝑁 · 𝑋)) = (1 · (𝑁 · 𝑋))) |
4 | 2, 3 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑛 = 1 → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ ((1 · 𝑁) · 𝑋) = (1 · (𝑁 · 𝑋)))) |
5 | 4 | imbi2d 330 |
. . . . 5
⊢ (𝑛 = 1 → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((1 · 𝑁) · 𝑋) = (1 · (𝑁 · 𝑋))))) |
6 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑛 · 𝑁) = (𝑚 · 𝑁)) |
7 | 6 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → ((𝑛 · 𝑁) · 𝑋) = ((𝑚 · 𝑁) · 𝑋)) |
8 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑛 · (𝑁 · 𝑋)) = (𝑚 · (𝑁 · 𝑋))) |
9 | 7, 8 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ ((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)))) |
10 | 9 | imbi2d 330 |
. . . . 5
⊢ (𝑛 = 𝑚 → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋))))) |
11 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑛 = (𝑚 + 1) → (𝑛 · 𝑁) = ((𝑚 + 1) · 𝑁)) |
12 | 11 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → ((𝑛 · 𝑁) · 𝑋) = (((𝑚 + 1) · 𝑁) · 𝑋)) |
13 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → (𝑛 · (𝑁 · 𝑋)) = ((𝑚 + 1) · (𝑁 · 𝑋))) |
14 | 12, 13 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋)))) |
15 | 14 | imbi2d 330 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋))))) |
16 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (𝑛 · 𝑁) = (𝑀 · 𝑁)) |
17 | 16 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → ((𝑛 · 𝑁) · 𝑋) = ((𝑀 · 𝑁) · 𝑋)) |
18 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (𝑛 · (𝑁 · 𝑋)) = (𝑀 · (𝑁 · 𝑋))) |
19 | 17, 18 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑛 = 𝑀 → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
20 | 19 | imbi2d 330 |
. . . . 5
⊢ (𝑛 = 𝑀 → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))))) |
21 | | nncn 11028 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
22 | 21 | mulid2d 10058 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (1
· 𝑁) = 𝑁) |
23 | 22 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → (1 · 𝑁) = 𝑁) |
24 | 23 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((1 · 𝑁) · 𝑋) = (𝑁 · 𝑋)) |
25 | | mulgass.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
26 | | mulgass.t |
. . . . . . . . 9
⊢ · =
(.g‘𝐺) |
27 | 25, 26 | mulgnnclOLD 17557 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
28 | 27 | 3coml 1272 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → (𝑁 · 𝑋) ∈ 𝐵) |
29 | 25, 26 | mulg1 17548 |
. . . . . . 7
⊢ ((𝑁 · 𝑋) ∈ 𝐵 → (1 · (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
30 | 28, 29 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → (1 · (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
31 | 24, 30 | eqtr4d 2659 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((1 · 𝑁) · 𝑋) = (1 · (𝑁 · 𝑋))) |
32 | | oveq1 6657 |
. . . . . . . 8
⊢ (((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)) → (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋))) |
33 | | nncn 11028 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → 𝑚 ∈ ℂ) |
35 | | 1cnd 10056 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → 1 ∈
ℂ) |
36 | | simpr1 1067 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → 𝑁 ∈ ℕ) |
37 | 36 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → 𝑁 ∈ ℂ) |
38 | 34, 35, 37 | adddird 10065 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → ((𝑚 + 1) · 𝑁) = ((𝑚 · 𝑁) + (1 · 𝑁))) |
39 | 23 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → (1 · 𝑁) = 𝑁) |
40 | 39 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → ((𝑚 · 𝑁) + (1 · 𝑁)) = ((𝑚 · 𝑁) + 𝑁)) |
41 | 38, 40 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → ((𝑚 + 1) · 𝑁) = ((𝑚 · 𝑁) + 𝑁)) |
42 | 41 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → (((𝑚 + 1) · 𝑁) · 𝑋) = (((𝑚 · 𝑁) + 𝑁) · 𝑋)) |
43 | | simpr3 1069 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → 𝐺 ∈ Mnd) |
44 | | nnmulcl 11043 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑚 · 𝑁) ∈ ℕ) |
45 | 44 | 3ad2antr1 1226 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → (𝑚 · 𝑁) ∈ ℕ) |
46 | | simpr2 1068 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → 𝑋 ∈ 𝐵) |
47 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) |
48 | 25, 26, 47 | mulgnndirOLD 17570 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ ((𝑚 · 𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (((𝑚 · 𝑁) + 𝑁) · 𝑋) = (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋))) |
49 | 43, 45, 36, 46, 48 | syl13anc 1328 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → (((𝑚 · 𝑁) + 𝑁) · 𝑋) = (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋))) |
50 | 42, 49 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → (((𝑚 + 1) · 𝑁) · 𝑋) = (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋))) |
51 | 25, 26, 47 | mulgnnp1 17549 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 · 𝑋) ∈ 𝐵) → ((𝑚 + 1) · (𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋))) |
52 | 28, 51 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → ((𝑚 + 1) · (𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋))) |
53 | 50, 52 | eqeq12d 2637 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → ((((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋)) ↔ (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋)))) |
54 | 32, 53 | syl5ibr 236 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd)) → (((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋)))) |
55 | 54 | ex 450 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → (((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋))))) |
56 | 55 | a2d 29 |
. . . . 5
⊢ (𝑚 ∈ ℕ → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋))) → ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋))))) |
57 | 5, 10, 15, 20, 31, 56 | nnind 11038 |
. . . 4
⊢ (𝑀 ∈ ℕ → ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Mnd) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
58 | 57 | 3expd 1284 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℕ → (𝑋 ∈ 𝐵 → (𝐺 ∈ Mnd → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))))) |
59 | 58 | com4r 94 |
. 2
⊢ (𝐺 ∈ Mnd → (𝑀 ∈ ℕ → (𝑁 ∈ ℕ → (𝑋 ∈ 𝐵 → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))))) |
60 | 59 | 3imp2 1282 |
1
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |