Step | Hyp | Ref
| Expression |
1 | | nnz 12342 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
2 | | odd2np1 16048 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝑁 ∈ ℕ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
4 | 3 | biimpa 477 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁) |
5 | 4 | 3adant1 1129 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁) |
6 | | simpl1 1190 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝐴 ∈ ℂ) |
7 | | simprr 770 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((2 · 𝑛) + 1) = 𝑁) |
8 | | simpl2 1191 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑁 ∈ ℕ) |
9 | 8 | nncnd 11989 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑁 ∈ ℂ) |
10 | | 1cnd 10971 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 1 ∈
ℂ) |
11 | | 2z 12352 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
12 | | simprl 768 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℤ) |
13 | | zmulcl 12369 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝑛
∈ ℤ) → (2 · 𝑛) ∈ ℤ) |
14 | 11, 12, 13 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℤ) |
15 | 14 | zcnd 12426 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℂ) |
16 | 9, 10, 15 | subadd2d 11351 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝑁 − 1) = (2 · 𝑛) ↔ ((2 · 𝑛) + 1) = 𝑁)) |
17 | 7, 16 | mpbird 256 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝑁 − 1) = (2 · 𝑛)) |
18 | | nnm1nn0 12274 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
19 | 8, 18 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝑁 − 1) ∈
ℕ0) |
20 | 17, 19 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (2 · 𝑛) ∈
ℕ0) |
21 | 6, 20 | expcld 13862 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑(2 · 𝑛)) ∈ ℂ) |
22 | 21, 6 | mulneg2d 11429 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · -𝐴) = -((𝐴↑(2 · 𝑛)) · 𝐴)) |
23 | | sqneg 13834 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) |
24 | 6, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑2) = (𝐴↑2)) |
25 | 24 | oveq1d 7286 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑2)↑𝑛) = ((𝐴↑2)↑𝑛)) |
26 | 6 | negcld 11319 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -𝐴 ∈ ℂ) |
27 | | 2rp 12734 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ+ |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 2 ∈
ℝ+) |
29 | 12 | zred 12425 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℝ) |
30 | 20 | nn0ge0d 12296 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 0 ≤ (2 ·
𝑛)) |
31 | 28, 29, 30 | prodge0rd 12836 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 0 ≤ 𝑛) |
32 | | elnn0z 12332 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↔ (𝑛 ∈ ℤ
∧ 0 ≤ 𝑛)) |
33 | 12, 31, 32 | sylanbrc 583 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 𝑛 ∈ ℕ0) |
34 | | 2nn0 12250 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
35 | 34 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → 2 ∈
ℕ0) |
36 | 26, 33, 35 | expmuld 13865 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑(2 · 𝑛)) = ((-𝐴↑2)↑𝑛)) |
37 | 6, 33, 35 | expmuld 13865 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑(2 · 𝑛)) = ((𝐴↑2)↑𝑛)) |
38 | 25, 36, 37 | 3eqtr4d 2790 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑(2 · 𝑛)) = (𝐴↑(2 · 𝑛))) |
39 | 38 | oveq1d 7286 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑(2 · 𝑛)) · -𝐴) = ((𝐴↑(2 · 𝑛)) · -𝐴)) |
40 | 26, 20 | expp1d 13863 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑((2 · 𝑛) + 1)) = ((-𝐴↑(2 · 𝑛)) · -𝐴)) |
41 | 7 | oveq2d 7287 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑((2 · 𝑛) + 1)) = (-𝐴↑𝑁)) |
42 | 40, 41 | eqtr3d 2782 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((-𝐴↑(2 · 𝑛)) · -𝐴) = (-𝐴↑𝑁)) |
43 | 39, 42 | eqtr3d 2782 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · -𝐴) = (-𝐴↑𝑁)) |
44 | 22, 43 | eqtr3d 2782 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -((𝐴↑(2 · 𝑛)) · 𝐴) = (-𝐴↑𝑁)) |
45 | 6, 20 | expp1d 13863 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑((2 · 𝑛) + 1)) = ((𝐴↑(2 · 𝑛)) · 𝐴)) |
46 | 7 | oveq2d 7287 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (𝐴↑((2 · 𝑛) + 1)) = (𝐴↑𝑁)) |
47 | 45, 46 | eqtr3d 2782 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → ((𝐴↑(2 · 𝑛)) · 𝐴) = (𝐴↑𝑁)) |
48 | 47 | negeqd 11215 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → -((𝐴↑(2 · 𝑛)) · 𝐴) = -(𝐴↑𝑁)) |
49 | 44, 48 | eqtr3d 2782 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁)) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |
50 | 5, 49 | rexlimddv 3222 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |