| Step | Hyp | Ref
| Expression |
| 1 | | oddz 47618 |
. . . . 5
⊢ (𝑁 ∈ Odd → 𝑁 ∈
ℤ) |
| 2 | | odd2np1ALTV 47661 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (𝑁 ∈ Odd ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝑁 ∈ Odd → (𝑁 ∈ Odd ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
| 4 | 3 | ibi 267 |
. . 3
⊢ (𝑁 ∈ Odd → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁) |
| 5 | 4 | 3ad2ant3 1136 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁) |
| 6 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝐴 ∈ ℂ) |
| 7 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((2 · 𝑛) + 1) = 𝑁) |
| 8 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑁 ∈ ℕ) |
| 9 | 8 | nncnd 12282 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑁 ∈ ℂ) |
| 10 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 1 ∈
ℂ) |
| 11 | | 2z 12649 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
| 12 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℤ) |
| 13 | | zmulcl 12666 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 · 𝑛) ∈ ℤ) |
| 14 | 11, 12, 13 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℤ) |
| 15 | 14 | zcnd 12723 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℂ) |
| 16 | 9, 10, 15 | subadd2d 11639 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝑁 − 1) = (2 · 𝑛) ↔ ((2 · 𝑛) + 1) = 𝑁)) |
| 17 | 7, 16 | mpbird 257 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝑁 − 1) = (2 · 𝑛)) |
| 18 | | nnm1nn0 12567 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
| 19 | 8, 18 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝑁 − 1) ∈
ℕ0) |
| 20 | 17, 19 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℕ0) |
| 21 | 6, 20 | expcld 14186 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑(2 · 𝑛)) ∈ ℂ) |
| 22 | 21, 6 | mulneg2d 11717 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · -𝐴) = -((𝐴↑(2 · 𝑛)) · 𝐴)) |
| 23 | | sqneg 14156 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) |
| 24 | 6, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑2) = (𝐴↑2)) |
| 25 | 24 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑2)↑𝑛) = ((𝐴↑2)↑𝑛)) |
| 26 | 6 | negcld 11607 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -𝐴 ∈ ℂ) |
| 27 | | 2rp 13039 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ+ |
| 28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 2 ∈
ℝ+) |
| 29 | 12 | zred 12722 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℝ) |
| 30 | 20 | nn0ge0d 12590 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 0 ≤ (2 ·
𝑛)) |
| 31 | 28, 29, 30 | prodge0rd 13142 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 0 ≤ 𝑛) |
| 32 | | elnn0z 12626 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↔ (𝑛 ∈ ℤ
∧ 0 ≤ 𝑛)) |
| 33 | 12, 31, 32 | sylanbrc 583 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℕ0) |
| 34 | | 2nn0 12543 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
| 35 | 34 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 2 ∈
ℕ0) |
| 36 | 26, 33, 35 | expmuld 14189 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑(2 · 𝑛)) = ((-𝐴↑2)↑𝑛)) |
| 37 | 6, 33, 35 | expmuld 14189 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑(2 · 𝑛)) = ((𝐴↑2)↑𝑛)) |
| 38 | 25, 36, 37 | 3eqtr4d 2787 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑(2 · 𝑛)) = (𝐴↑(2 · 𝑛))) |
| 39 | 38 | oveq1d 7446 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑(2 · 𝑛)) · -𝐴) = ((𝐴↑(2 · 𝑛)) · -𝐴)) |
| 40 | 26, 20 | expp1d 14187 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑((2 · 𝑛) + 1)) = ((-𝐴↑(2 · 𝑛)) · -𝐴)) |
| 41 | 7 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑((2 · 𝑛) + 1)) = (-𝐴↑𝑁)) |
| 42 | 40, 41 | eqtr3d 2779 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑(2 · 𝑛)) · -𝐴) = (-𝐴↑𝑁)) |
| 43 | 39, 42 | eqtr3d 2779 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · -𝐴) = (-𝐴↑𝑁)) |
| 44 | 22, 43 | eqtr3d 2779 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -((𝐴↑(2 · 𝑛)) · 𝐴) = (-𝐴↑𝑁)) |
| 45 | 6, 20 | expp1d 14187 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑((2 · 𝑛) + 1)) = ((𝐴↑(2 · 𝑛)) · 𝐴)) |
| 46 | 7 | oveq2d 7447 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑((2 · 𝑛) + 1)) = (𝐴↑𝑁)) |
| 47 | 45, 46 | eqtr3d 2779 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · 𝐴) = (𝐴↑𝑁)) |
| 48 | 47 | negeqd 11502 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -((𝐴↑(2 · 𝑛)) · 𝐴) = -(𝐴↑𝑁)) |
| 49 | 44, 48 | eqtr3d 2779 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |
| 50 | 5, 49 | rexlimddv 3161 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |