Step | Hyp | Ref
| Expression |
1 | | oddz 41544 |
. . . . . . 7
⊢ (𝑁 ∈ Odd → 𝑁 ∈
ℤ) |
2 | | odd2np1ALTV 41585 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (𝑁 ∈ Odd ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ Odd → (𝑁 ∈ Odd ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
4 | 3 | biimpd 219 |
. . . . 5
⊢ (𝑁 ∈ Odd → (𝑁 ∈ Odd → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
5 | 4 | pm2.43i 52 |
. . . 4
⊢ (𝑁 ∈ Odd → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁) |
6 | 5 | adantl 482 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁) |
7 | 6 | 3adant1 1079 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁) |
8 | | simpl1 1064 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝐴 ∈ ℂ) |
9 | | simprr 796 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((2 · 𝑛) + 1) = 𝑁) |
10 | | simpl2 1065 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑁 ∈ ℕ) |
11 | 10 | nncnd 11036 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑁 ∈ ℂ) |
12 | | 1cnd 10056 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 1 ∈
ℂ) |
13 | | 2z 11409 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
14 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℤ) |
15 | | zmulcl 11426 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 · 𝑛) ∈ ℤ) |
16 | 13, 14, 15 | sylancr 695 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℤ) |
17 | 16 | zcnd 11483 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℂ) |
18 | 11, 12, 17 | subadd2d 10411 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝑁 − 1) = (2 · 𝑛) ↔ ((2 · 𝑛) + 1) = 𝑁)) |
19 | 9, 18 | mpbird 247 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝑁 − 1) = (2 · 𝑛)) |
20 | | nnm1nn0 11334 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
21 | 10, 20 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝑁 − 1) ∈
ℕ0) |
22 | 19, 21 | eqeltrrd 2702 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℕ0) |
23 | 8, 22 | expcld 13008 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑(2 · 𝑛)) ∈ ℂ) |
24 | 23, 8 | mulneg2d 10484 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · -𝐴) = -((𝐴↑(2 · 𝑛)) · 𝐴)) |
25 | | sqneg 12923 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) |
26 | 8, 25 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑2) = (𝐴↑2)) |
27 | 26 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑2)↑𝑛) = ((𝐴↑2)↑𝑛)) |
28 | 8 | negcld 10379 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -𝐴 ∈ ℂ) |
29 | | 2re 11090 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 2 ∈
ℝ) |
31 | 14 | zred 11482 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℝ) |
32 | | 2pos 11112 |
. . . . . . . . . . 11
⊢ 0 <
2 |
33 | 32 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 0 <
2) |
34 | 22 | nn0ge0d 11354 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 0 ≤ (2 ·
𝑛)) |
35 | | prodge0 10870 |
. . . . . . . . . 10
⊢ (((2
∈ ℝ ∧ 𝑛
∈ ℝ) ∧ (0 < 2 ∧ 0 ≤ (2 · 𝑛))) → 0 ≤ 𝑛) |
36 | 30, 31, 33, 34, 35 | syl22anc 1327 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 0 ≤ 𝑛) |
37 | | elnn0z 11390 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↔ (𝑛 ∈ ℤ
∧ 0 ≤ 𝑛)) |
38 | 14, 36, 37 | sylanbrc 698 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℕ0) |
39 | | 2nn0 11309 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
40 | 39 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 2 ∈
ℕ0) |
41 | 28, 38, 40 | expmuld 13011 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑(2 · 𝑛)) = ((-𝐴↑2)↑𝑛)) |
42 | 8, 38, 40 | expmuld 13011 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑(2 · 𝑛)) = ((𝐴↑2)↑𝑛)) |
43 | 27, 41, 42 | 3eqtr4d 2666 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑(2 · 𝑛)) = (𝐴↑(2 · 𝑛))) |
44 | 43 | oveq1d 6665 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑(2 · 𝑛)) · -𝐴) = ((𝐴↑(2 · 𝑛)) · -𝐴)) |
45 | 28, 22 | expp1d 13009 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑((2 · 𝑛) + 1)) = ((-𝐴↑(2 · 𝑛)) · -𝐴)) |
46 | 9 | oveq2d 6666 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑((2 · 𝑛) + 1)) = (-𝐴↑𝑁)) |
47 | 45, 46 | eqtr3d 2658 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑(2 · 𝑛)) · -𝐴) = (-𝐴↑𝑁)) |
48 | 44, 47 | eqtr3d 2658 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · -𝐴) = (-𝐴↑𝑁)) |
49 | 24, 48 | eqtr3d 2658 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -((𝐴↑(2 · 𝑛)) · 𝐴) = (-𝐴↑𝑁)) |
50 | 8, 22 | expp1d 13009 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑((2 · 𝑛) + 1)) = ((𝐴↑(2 · 𝑛)) · 𝐴)) |
51 | 9 | oveq2d 6666 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑((2 · 𝑛) + 1)) = (𝐴↑𝑁)) |
52 | 50, 51 | eqtr3d 2658 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · 𝐴) = (𝐴↑𝑁)) |
53 | 52 | negeqd 10275 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -((𝐴↑(2 · 𝑛)) · 𝐴) = -(𝐴↑𝑁)) |
54 | 49, 53 | eqtr3d 2658 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |
55 | 7, 54 | rexlimddv 3035 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |