Step | Hyp | Ref
| Expression |
1 | | nnz 9187 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
2 | | odd2np1 11768 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
3 | 1, 2 | syl 14 |
. . . 4
⊢ (𝑁 ∈ ℕ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
4 | 3 | biimpa 294 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁) |
5 | 4 | 3adant1 1000 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁) |
6 | | simpl1 985 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝐴 ∈ ℂ) |
7 | | simprr 522 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((2 · 𝑛) + 1) = 𝑁) |
8 | | simpl2 986 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑁 ∈ ℕ) |
9 | 8 | nncnd 8848 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑁 ∈ ℂ) |
10 | | 1cnd 7895 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 1 ∈
ℂ) |
11 | | 2z 9196 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
12 | | simprl 521 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℤ) |
13 | | zmulcl 9221 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 · 𝑛) ∈ ℤ) |
14 | 11, 12, 13 | sylancr 411 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℤ) |
15 | 14 | zcnd 9288 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℂ) |
16 | 9, 10, 15 | subadd2d 8206 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝑁 − 1) = (2 · 𝑛) ↔ ((2 · 𝑛) + 1) = 𝑁)) |
17 | 7, 16 | mpbird 166 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝑁 − 1) = (2 · 𝑛)) |
18 | | nnm1nn0 9132 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
19 | 8, 18 | syl 14 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝑁 − 1) ∈
ℕ0) |
20 | 17, 19 | eqeltrrd 2235 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℕ0) |
21 | 6, 20 | expcld 10555 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑(2 · 𝑛)) ∈ ℂ) |
22 | 21, 6 | mulneg2d 8288 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · -𝐴) = -((𝐴↑(2 · 𝑛)) · 𝐴)) |
23 | | sqneg 10482 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) |
24 | 6, 23 | syl 14 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑2) = (𝐴↑2)) |
25 | 24 | oveq1d 5840 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑2)↑𝑛) = ((𝐴↑2)↑𝑛)) |
26 | 6 | negcld 8174 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -𝐴 ∈ ℂ) |
27 | | 2re 8904 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
28 | 27 | a1i 9 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 2 ∈
ℝ) |
29 | 12 | zred 9287 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℝ) |
30 | | 2pos 8925 |
. . . . . . . . . . 11
⊢ 0 <
2 |
31 | 30 | a1i 9 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 0 <
2) |
32 | 20 | nn0ge0d 9147 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 0 ≤ (2 ·
𝑛)) |
33 | | prodge0 8726 |
. . . . . . . . . 10
⊢ (((2
∈ ℝ ∧ 𝑛
∈ ℝ) ∧ (0 < 2 ∧ 0 ≤ (2 · 𝑛))) → 0 ≤ 𝑛) |
34 | 28, 29, 31, 32, 33 | syl22anc 1221 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 0 ≤ 𝑛) |
35 | | elnn0z 9181 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↔ (𝑛 ∈ ℤ
∧ 0 ≤ 𝑛)) |
36 | 12, 34, 35 | sylanbrc 414 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℕ0) |
37 | | 2nn0 9108 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
38 | 37 | a1i 9 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 2 ∈
ℕ0) |
39 | 26, 36, 38 | expmuld 10558 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑(2 · 𝑛)) = ((-𝐴↑2)↑𝑛)) |
40 | 6, 36, 38 | expmuld 10558 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑(2 · 𝑛)) = ((𝐴↑2)↑𝑛)) |
41 | 25, 39, 40 | 3eqtr4d 2200 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑(2 · 𝑛)) = (𝐴↑(2 · 𝑛))) |
42 | 41 | oveq1d 5840 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑(2 · 𝑛)) · -𝐴) = ((𝐴↑(2 · 𝑛)) · -𝐴)) |
43 | 26, 20 | expp1d 10556 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑((2 · 𝑛) + 1)) = ((-𝐴↑(2 · 𝑛)) · -𝐴)) |
44 | 7 | oveq2d 5841 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑((2 · 𝑛) + 1)) = (-𝐴↑𝑁)) |
45 | 43, 44 | eqtr3d 2192 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑(2 · 𝑛)) · -𝐴) = (-𝐴↑𝑁)) |
46 | 42, 45 | eqtr3d 2192 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · -𝐴) = (-𝐴↑𝑁)) |
47 | 22, 46 | eqtr3d 2192 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -((𝐴↑(2 · 𝑛)) · 𝐴) = (-𝐴↑𝑁)) |
48 | 6, 20 | expp1d 10556 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑((2 · 𝑛) + 1)) = ((𝐴↑(2 · 𝑛)) · 𝐴)) |
49 | 7 | oveq2d 5841 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑((2 · 𝑛) + 1)) = (𝐴↑𝑁)) |
50 | 48, 49 | eqtr3d 2192 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · 𝐴) = (𝐴↑𝑁)) |
51 | 50 | negeqd 8071 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -((𝐴↑(2 · 𝑛)) · 𝐴) = -(𝐴↑𝑁)) |
52 | 47, 51 | eqtr3d 2192 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |
53 | 5, 52 | rexlimddv 2579 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |