| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oddz 47618 | . . . . . 6
⊢ (𝑁 ∈ Odd → 𝑁 ∈
ℤ) | 
| 2 |  | odd2np1ALTV 47661 | . . . . . 6
⊢ (𝑁 ∈ ℤ → (𝑁 ∈ Odd ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) | 
| 3 | 1, 2 | syl 17 | . . . . 5
⊢ (𝑁 ∈ Odd → (𝑁 ∈ Odd ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) | 
| 4 | 3 | biimpd 229 | . . . 4
⊢ (𝑁 ∈ Odd → (𝑁 ∈ Odd → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) | 
| 5 | 4 | pm2.43i 52 | . . 3
⊢ (𝑁 ∈ Odd → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁) | 
| 6 | 5 | 3ad2ant3 1136 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁) | 
| 7 |  | simpl1 1192 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → 𝐴 ∈ ℂ) | 
| 8 |  | simpl2 1193 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → 𝐴 ≠ 0) | 
| 9 |  | 2z 12649 | . . . . . . 7
⊢ 2 ∈
ℤ | 
| 10 |  | simprl 771 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℤ) | 
| 11 |  | zmulcl 12666 | . . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 · 𝑛) ∈ ℤ) | 
| 12 | 9, 10, 11 | sylancr 587 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈ ℤ) | 
| 13 | 7, 8, 12 | expclzd 14191 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (𝐴↑(2 · 𝑛)) ∈ ℂ) | 
| 14 | 13, 7 | mulneg2d 11717 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · -𝐴) = -((𝐴↑(2 · 𝑛)) · 𝐴)) | 
| 15 |  | sqneg 14156 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) | 
| 16 | 7, 15 | syl 17 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (-𝐴↑2) = (𝐴↑2)) | 
| 17 | 16 | oveq1d 7446 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → ((-𝐴↑2)↑𝑛) = ((𝐴↑2)↑𝑛)) | 
| 18 | 7 | negcld 11607 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → -𝐴 ∈ ℂ) | 
| 19 | 7, 8 | negne0d 11618 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → -𝐴 ≠ 0) | 
| 20 | 9 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁) → 2 ∈
ℤ) | 
| 21 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁) → 𝑛 ∈ ℤ) | 
| 22 | 20, 21 | jca 511 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁) → (2 ∈ ℤ ∧
𝑛 ∈
ℤ)) | 
| 23 | 22 | adantl 481 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (2 ∈ ℤ ∧ 𝑛 ∈
ℤ)) | 
| 24 | 18, 19, 23 | jca31 514 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → ((-𝐴 ∈ ℂ ∧ -𝐴 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝑛 ∈
ℤ))) | 
| 25 |  | expmulz 14149 | . . . . . . . 8
⊢ (((-𝐴 ∈ ℂ ∧ -𝐴 ≠ 0) ∧ (2 ∈ ℤ
∧ 𝑛 ∈ ℤ))
→ (-𝐴↑(2 ·
𝑛)) = ((-𝐴↑2)↑𝑛)) | 
| 26 | 24, 25 | syl 17 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (-𝐴↑(2 · 𝑛)) = ((-𝐴↑2)↑𝑛)) | 
| 27 | 7, 8, 23 | jca31 514 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝑛 ∈
ℤ))) | 
| 28 |  | expmulz 14149 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (2 ∈ ℤ
∧ 𝑛 ∈ ℤ))
→ (𝐴↑(2 ·
𝑛)) = ((𝐴↑2)↑𝑛)) | 
| 29 | 27, 28 | syl 17 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (𝐴↑(2 · 𝑛)) = ((𝐴↑2)↑𝑛)) | 
| 30 | 17, 26, 29 | 3eqtr4d 2787 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (-𝐴↑(2 · 𝑛)) = (𝐴↑(2 · 𝑛))) | 
| 31 | 30 | oveq1d 7446 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → ((-𝐴↑(2 · 𝑛)) · -𝐴) = ((𝐴↑(2 · 𝑛)) · -𝐴)) | 
| 32 | 18, 19, 12 | expp1zd 14195 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (-𝐴↑((2 · 𝑛) + 1)) = ((-𝐴↑(2 · 𝑛)) · -𝐴)) | 
| 33 |  | simprr 773 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → ((2 · 𝑛) + 1) = 𝑁) | 
| 34 | 33 | oveq2d 7447 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (-𝐴↑((2 · 𝑛) + 1)) = (-𝐴↑𝑁)) | 
| 35 | 32, 34 | eqtr3d 2779 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → ((-𝐴↑(2 · 𝑛)) · -𝐴) = (-𝐴↑𝑁)) | 
| 36 | 31, 35 | eqtr3d 2779 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · -𝐴) = (-𝐴↑𝑁)) | 
| 37 | 14, 36 | eqtr3d 2779 | . . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → -((𝐴↑(2 · 𝑛)) · 𝐴) = (-𝐴↑𝑁)) | 
| 38 | 7, 8, 12 | expp1zd 14195 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (𝐴↑((2 · 𝑛) + 1)) = ((𝐴↑(2 · 𝑛)) · 𝐴)) | 
| 39 | 33 | oveq2d 7447 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (𝐴↑((2 · 𝑛) + 1)) = (𝐴↑𝑁)) | 
| 40 | 38, 39 | eqtr3d 2779 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · 𝐴) = (𝐴↑𝑁)) | 
| 41 | 40 | negeqd 11502 | . . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → -((𝐴↑(2 · 𝑛)) · 𝐴) = -(𝐴↑𝑁)) | 
| 42 | 37, 41 | eqtr3d 2779 | . 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = 𝑁)) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) | 
| 43 | 6, 42 | rexlimddv 3161 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |