Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = 0 → (𝑥(.g‘ℂfld)𝐵) =
(0(.g‘ℂfld)𝐵)) |
2 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = 0 → (𝑥 · 𝐵) = (0 · 𝐵)) |
3 | 1, 2 | eqeq12d 2637 |
. . 3
⊢ (𝑥 = 0 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔
(0(.g‘ℂfld)𝐵) = (0 · 𝐵))) |
4 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥(.g‘ℂfld)𝐵) = (𝑦(.g‘ℂfld)𝐵)) |
5 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥 · 𝐵) = (𝑦 · 𝐵)) |
6 | 4, 5 | eqeq12d 2637 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ (𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵))) |
7 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑥(.g‘ℂfld)𝐵) = ((𝑦 +
1)(.g‘ℂfld)𝐵)) |
8 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝐵) = ((𝑦 + 1) · 𝐵)) |
9 | 7, 8 | eqeq12d 2637 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵))) |
10 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = -𝑦 → (𝑥(.g‘ℂfld)𝐵) = (-𝑦(.g‘ℂfld)𝐵)) |
11 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = -𝑦 → (𝑥 · 𝐵) = (-𝑦 · 𝐵)) |
12 | 10, 11 | eqeq12d 2637 |
. . 3
⊢ (𝑥 = -𝑦 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ (-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵))) |
13 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥(.g‘ℂfld)𝐵) = (𝐴(.g‘ℂfld)𝐵)) |
14 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥 · 𝐵) = (𝐴 · 𝐵)) |
15 | 13, 14 | eqeq12d 2637 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝑥(.g‘ℂfld)𝐵) = (𝑥 · 𝐵) ↔ (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))) |
16 | | cnfldbas 19750 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
17 | | cnfld0 19770 |
. . . . 5
⊢ 0 =
(0g‘ℂfld) |
18 | | eqid 2622 |
. . . . 5
⊢
(.g‘ℂfld) =
(.g‘ℂfld) |
19 | 16, 17, 18 | mulg0 17546 |
. . . 4
⊢ (𝐵 ∈ ℂ →
(0(.g‘ℂfld)𝐵) = 0) |
20 | | mul02 10214 |
. . . 4
⊢ (𝐵 ∈ ℂ → (0
· 𝐵) =
0) |
21 | 19, 20 | eqtr4d 2659 |
. . 3
⊢ (𝐵 ∈ ℂ →
(0(.g‘ℂfld)𝐵) = (0 · 𝐵)) |
22 | | oveq1 6657 |
. . . . 5
⊢ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → ((𝑦(.g‘ℂfld)𝐵) + 𝐵) = ((𝑦 · 𝐵) + 𝐵)) |
23 | | cnring 19768 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
24 | | ringmnd 18556 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
⊢
ℂfld ∈ Mnd |
26 | | cnfldadd 19751 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
27 | 16, 18, 26 | mulgnn0p1 17552 |
. . . . . . 7
⊢
((ℂfld ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℂ) → ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦(.g‘ℂfld)𝐵) + 𝐵)) |
28 | 25, 27 | mp3an1 1411 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦(.g‘ℂfld)𝐵) + 𝐵)) |
29 | | nn0cn 11302 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℂ) |
30 | 29 | adantr 481 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ 𝑦 ∈
ℂ) |
31 | | 1cnd 10056 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ 1 ∈ ℂ) |
32 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ 𝐵 ∈
ℂ) |
33 | 30, 31, 32 | adddird 10065 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦 + 1) ·
𝐵) = ((𝑦 · 𝐵) + (1 · 𝐵))) |
34 | | mulid2 10038 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ → (1
· 𝐵) = 𝐵) |
35 | 34 | adantl 482 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ (1 · 𝐵) =
𝐵) |
36 | 35 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦 · 𝐵) + (1 · 𝐵)) = ((𝑦 · 𝐵) + 𝐵)) |
37 | 33, 36 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦 + 1) ·
𝐵) = ((𝑦 · 𝐵) + 𝐵)) |
38 | 28, 37 | eqeq12d 2637 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ (((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵) ↔ ((𝑦(.g‘ℂfld)𝐵) + 𝐵) = ((𝑦 · 𝐵) + 𝐵))) |
39 | 22, 38 | syl5ibr 236 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ 𝐵 ∈ ℂ)
→ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵))) |
40 | 39 | expcom 451 |
. . 3
⊢ (𝐵 ∈ ℂ → (𝑦 ∈ ℕ0
→ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → ((𝑦 +
1)(.g‘ℂfld)𝐵) = ((𝑦 + 1) · 𝐵)))) |
41 | | fveq2 6191 |
. . . . 5
⊢ ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) →
((invg‘ℂfld)‘(𝑦(.g‘ℂfld)𝐵)) =
((invg‘ℂfld)‘(𝑦 · 𝐵))) |
42 | | eqid 2622 |
. . . . . . 7
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
43 | 16, 18, 42 | mulgnegnn 17551 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-𝑦(.g‘ℂfld)𝐵) =
((invg‘ℂfld)‘(𝑦(.g‘ℂfld)𝐵))) |
44 | | nncn 11028 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
45 | | mulneg1 10466 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝑦 · 𝐵) = -(𝑦 · 𝐵)) |
46 | 44, 45 | sylan 488 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-𝑦 · 𝐵) = -(𝑦 · 𝐵)) |
47 | | mulcl 10020 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑦 · 𝐵) ∈ ℂ) |
48 | 44, 47 | sylan 488 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (𝑦 · 𝐵) ∈ ℂ) |
49 | | cnfldneg 19772 |
. . . . . . . 8
⊢ ((𝑦 · 𝐵) ∈ ℂ →
((invg‘ℂfld)‘(𝑦 · 𝐵)) = -(𝑦 · 𝐵)) |
50 | 48, 49 | syl 17 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
((invg‘ℂfld)‘(𝑦 · 𝐵)) = -(𝑦 · 𝐵)) |
51 | 46, 50 | eqtr4d 2659 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → (-𝑦 · 𝐵) =
((invg‘ℂfld)‘(𝑦 · 𝐵))) |
52 | 43, 51 | eqeq12d 2637 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵) ↔
((invg‘ℂfld)‘(𝑦(.g‘ℂfld)𝐵)) =
((invg‘ℂfld)‘(𝑦 · 𝐵)))) |
53 | 41, 52 | syl5ibr 236 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → (-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵))) |
54 | 53 | expcom 451 |
. . 3
⊢ (𝐵 ∈ ℂ → (𝑦 ∈ ℕ → ((𝑦(.g‘ℂfld)𝐵) = (𝑦 · 𝐵) → (-𝑦(.g‘ℂfld)𝐵) = (-𝑦 · 𝐵)))) |
55 | 3, 6, 9, 12, 15, 21, 40, 54 | zindd 11478 |
. 2
⊢ (𝐵 ∈ ℂ → (𝐴 ∈ ℤ → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))) |
56 | 55 | impcom 446 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵)) |