Proof of Theorem tanatan
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | atancl 26924 | . . 3
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) ∈
ℂ) | 
| 2 |  | 2efiatan 26961 | . . . . . 6
⊢ (𝐴 ∈ dom arctan →
(exp‘(2 · (i · (arctan‘𝐴)))) = (((2 · i) / (𝐴 + i)) − 1)) | 
| 3 | 2 | oveq1d 7446 | . . . . 5
⊢ (𝐴 ∈ dom arctan →
((exp‘(2 · (i · (arctan‘𝐴)))) + 1) = ((((2 · i) / (𝐴 + i)) − 1) +
1)) | 
| 4 |  | 2mulicn 12489 | . . . . . . . 8
⊢ (2
· i) ∈ ℂ | 
| 5 | 4 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan → (2
· i) ∈ ℂ) | 
| 6 |  | atandm 26919 | . . . . . . . . 9
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i)) | 
| 7 | 6 | simp1bi 1146 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan → 𝐴 ∈
ℂ) | 
| 8 |  | ax-icn 11214 | . . . . . . . 8
⊢ i ∈
ℂ | 
| 9 |  | addcl 11237 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (𝐴 + i)
∈ ℂ) | 
| 10 | 7, 8, 9 | sylancl 586 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan → (𝐴 + i) ∈
ℂ) | 
| 11 |  | subneg 11558 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (𝐴 −
-i) = (𝐴 +
i)) | 
| 12 | 7, 8, 11 | sylancl 586 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan → (𝐴 − -i) = (𝐴 + i)) | 
| 13 | 6 | simp2bi 1147 | . . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → 𝐴 ≠ -i) | 
| 14 | 8 | negcli 11577 | . . . . . . . . . 10
⊢ -i ∈
ℂ | 
| 15 |  | subeq0 11535 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ -i ∈
ℂ) → ((𝐴 −
-i) = 0 ↔ 𝐴 =
-i)) | 
| 16 | 15 | necon3bid 2985 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ -i ∈
ℂ) → ((𝐴 −
-i) ≠ 0 ↔ 𝐴 ≠
-i)) | 
| 17 | 7, 14, 16 | sylancl 586 | . . . . . . . . 9
⊢ (𝐴 ∈ dom arctan →
((𝐴 − -i) ≠ 0
↔ 𝐴 ≠
-i)) | 
| 18 | 13, 17 | mpbird 257 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan → (𝐴 − -i) ≠
0) | 
| 19 | 12, 18 | eqnetrrd 3009 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan → (𝐴 + i) ≠ 0) | 
| 20 | 5, 10, 19 | divcld 12043 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → ((2
· i) / (𝐴 + i))
∈ ℂ) | 
| 21 |  | ax-1cn 11213 | . . . . . 6
⊢ 1 ∈
ℂ | 
| 22 |  | npcan 11517 | . . . . . 6
⊢ ((((2
· i) / (𝐴 + i))
∈ ℂ ∧ 1 ∈ ℂ) → ((((2 · i) / (𝐴 + i)) − 1) + 1) = ((2
· i) / (𝐴 +
i))) | 
| 23 | 20, 21, 22 | sylancl 586 | . . . . 5
⊢ (𝐴 ∈ dom arctan → ((((2
· i) / (𝐴 + i))
− 1) + 1) = ((2 · i) / (𝐴 + i))) | 
| 24 | 3, 23 | eqtrd 2777 | . . . 4
⊢ (𝐴 ∈ dom arctan →
((exp‘(2 · (i · (arctan‘𝐴)))) + 1) = ((2 · i) / (𝐴 + i))) | 
| 25 |  | 2muline0 12490 | . . . . . 6
⊢ (2
· i) ≠ 0 | 
| 26 | 25 | a1i 11 | . . . . 5
⊢ (𝐴 ∈ dom arctan → (2
· i) ≠ 0) | 
| 27 | 5, 10, 26, 19 | divne0d 12059 | . . . 4
⊢ (𝐴 ∈ dom arctan → ((2
· i) / (𝐴 + i)) ≠
0) | 
| 28 | 24, 27 | eqnetrd 3008 | . . 3
⊢ (𝐴 ∈ dom arctan →
((exp‘(2 · (i · (arctan‘𝐴)))) + 1) ≠ 0) | 
| 29 |  | tanval3 16170 | . . 3
⊢
(((arctan‘𝐴)
∈ ℂ ∧ ((exp‘(2 · (i · (arctan‘𝐴)))) + 1) ≠ 0) →
(tan‘(arctan‘𝐴)) = (((exp‘(2 · (i ·
(arctan‘𝐴)))) −
1) / (i · ((exp‘(2 · (i · (arctan‘𝐴)))) + 1)))) | 
| 30 | 1, 28, 29 | syl2anc 584 | . 2
⊢ (𝐴 ∈ dom arctan →
(tan‘(arctan‘𝐴)) = (((exp‘(2 · (i ·
(arctan‘𝐴)))) −
1) / (i · ((exp‘(2 · (i · (arctan‘𝐴)))) + 1)))) | 
| 31 | 2 | oveq1d 7446 | . . . . . 6
⊢ (𝐴 ∈ dom arctan →
((exp‘(2 · (i · (arctan‘𝐴)))) − 1) = ((((2 · i) / (𝐴 + i)) − 1) −
1)) | 
| 32 | 21 | a1i 11 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan → 1
∈ ℂ) | 
| 33 | 20, 32, 32 | subsub4d 11651 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan → ((((2
· i) / (𝐴 + i))
− 1) − 1) = (((2 · i) / (𝐴 + i)) − (1 + 1))) | 
| 34 |  | df-2 12329 | . . . . . . . 8
⊢ 2 = (1 +
1) | 
| 35 | 34 | oveq2i 7442 | . . . . . . 7
⊢ (((2
· i) / (𝐴 + i))
− 2) = (((2 · i) / (𝐴 + i)) − (1 + 1)) | 
| 36 | 33, 35 | eqtr4di 2795 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → ((((2
· i) / (𝐴 + i))
− 1) − 1) = (((2 · i) / (𝐴 + i)) − 2)) | 
| 37 | 31, 36 | eqtrd 2777 | . . . . 5
⊢ (𝐴 ∈ dom arctan →
((exp‘(2 · (i · (arctan‘𝐴)))) − 1) = (((2 · i) / (𝐴 + i)) −
2)) | 
| 38 |  | 2cn 12341 | . . . . . . . 8
⊢ 2 ∈
ℂ | 
| 39 |  | mulcl 11239 | . . . . . . . 8
⊢ ((2
∈ ℂ ∧ (𝐴 +
i) ∈ ℂ) → (2 · (𝐴 + i)) ∈ ℂ) | 
| 40 | 38, 10, 39 | sylancr 587 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan → (2
· (𝐴 + i)) ∈
ℂ) | 
| 41 | 5, 40, 10, 19 | divsubdird 12082 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → (((2
· i) − (2 · (𝐴 + i))) / (𝐴 + i)) = (((2 · i) / (𝐴 + i)) − ((2 ·
(𝐴 + i)) / (𝐴 + i)))) | 
| 42 |  | mulneg12 11701 | . . . . . . . . 9
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℂ) → (-2 · 𝐴) = (2 · -𝐴)) | 
| 43 | 38, 7, 42 | sylancr 587 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan → (-2
· 𝐴) = (2 ·
-𝐴)) | 
| 44 |  | negsub 11557 | . . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i + -𝐴) = (i − 𝐴)) | 
| 45 | 8, 7, 44 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → (i +
-𝐴) = (i − 𝐴)) | 
| 46 | 45 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → ((i +
-𝐴) − i) = ((i
− 𝐴) −
i)) | 
| 47 | 7 | negcld 11607 | . . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → -𝐴 ∈
ℂ) | 
| 48 |  | pncan2 11515 | . . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ -𝐴
∈ ℂ) → ((i + -𝐴) − i) = -𝐴) | 
| 49 | 8, 47, 48 | sylancr 587 | . . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → ((i +
-𝐴) − i) = -𝐴) | 
| 50 | 8 | a1i 11 | . . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → i
∈ ℂ) | 
| 51 | 50, 7, 50 | subsub4d 11651 | . . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → ((i
− 𝐴) − i) = (i
− (𝐴 +
i))) | 
| 52 | 46, 49, 51 | 3eqtr3rd 2786 | . . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → (i
− (𝐴 + i)) = -𝐴) | 
| 53 | 52 | oveq2d 7447 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan → (2
· (i − (𝐴 +
i))) = (2 · -𝐴)) | 
| 54 | 38 | a1i 11 | . . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → 2
∈ ℂ) | 
| 55 | 54, 50, 10 | subdid 11719 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan → (2
· (i − (𝐴 +
i))) = ((2 · i) − (2 · (𝐴 + i)))) | 
| 56 | 43, 53, 55 | 3eqtr2rd 2784 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan → ((2
· i) − (2 · (𝐴 + i))) = (-2 · 𝐴)) | 
| 57 | 56 | oveq1d 7446 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → (((2
· i) − (2 · (𝐴 + i))) / (𝐴 + i)) = ((-2 · 𝐴) / (𝐴 + i))) | 
| 58 | 54, 10, 19 | divcan4d 12049 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan → ((2
· (𝐴 + i)) / (𝐴 + i)) = 2) | 
| 59 | 58 | oveq2d 7447 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → (((2
· i) / (𝐴 + i))
− ((2 · (𝐴 +
i)) / (𝐴 + i))) = (((2
· i) / (𝐴 + i))
− 2)) | 
| 60 | 41, 57, 59 | 3eqtr3d 2785 | . . . . 5
⊢ (𝐴 ∈ dom arctan → ((-2
· 𝐴) / (𝐴 + i)) = (((2 · i) /
(𝐴 + i)) −
2)) | 
| 61 | 37, 60 | eqtr4d 2780 | . . . 4
⊢ (𝐴 ∈ dom arctan →
((exp‘(2 · (i · (arctan‘𝐴)))) − 1) = ((-2 · 𝐴) / (𝐴 + i))) | 
| 62 | 24 | oveq2d 7447 | . . . . 5
⊢ (𝐴 ∈ dom arctan → (i
· ((exp‘(2 · (i · (arctan‘𝐴)))) + 1)) = (i · ((2 · i) /
(𝐴 + i)))) | 
| 63 | 8, 38, 8 | mul12i 11456 | . . . . . . . 8
⊢ (i
· (2 · i)) = (2 · (i · i)) | 
| 64 |  | ixi 11892 | . . . . . . . . 9
⊢ (i
· i) = -1 | 
| 65 | 64 | oveq2i 7442 | . . . . . . . 8
⊢ (2
· (i · i)) = (2 · -1) | 
| 66 | 21 | negcli 11577 | . . . . . . . . 9
⊢ -1 ∈
ℂ | 
| 67 | 38 | mulm1i 11708 | . . . . . . . . 9
⊢ (-1
· 2) = -2 | 
| 68 | 66, 38, 67 | mulcomli 11270 | . . . . . . . 8
⊢ (2
· -1) = -2 | 
| 69 | 63, 65, 68 | 3eqtri 2769 | . . . . . . 7
⊢ (i
· (2 · i)) = -2 | 
| 70 | 69 | oveq1i 7441 | . . . . . 6
⊢ ((i
· (2 · i)) / (𝐴 + i)) = (-2 / (𝐴 + i)) | 
| 71 | 50, 5, 10, 19 | divassd 12078 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → ((i
· (2 · i)) / (𝐴 + i)) = (i · ((2 · i) /
(𝐴 + i)))) | 
| 72 | 70, 71 | eqtr3id 2791 | . . . . 5
⊢ (𝐴 ∈ dom arctan → (-2 /
(𝐴 + i)) = (i · ((2
· i) / (𝐴 +
i)))) | 
| 73 | 62, 72 | eqtr4d 2780 | . . . 4
⊢ (𝐴 ∈ dom arctan → (i
· ((exp‘(2 · (i · (arctan‘𝐴)))) + 1)) = (-2 / (𝐴 + i))) | 
| 74 | 61, 73 | oveq12d 7449 | . . 3
⊢ (𝐴 ∈ dom arctan →
(((exp‘(2 · (i · (arctan‘𝐴)))) − 1) / (i · ((exp‘(2
· (i · (arctan‘𝐴)))) + 1))) = (((-2 · 𝐴) / (𝐴 + i)) / (-2 / (𝐴 + i)))) | 
| 75 | 38 | negcli 11577 | . . . . . 6
⊢ -2 ∈
ℂ | 
| 76 |  | mulcl 11239 | . . . . . 6
⊢ ((-2
∈ ℂ ∧ 𝐴
∈ ℂ) → (-2 · 𝐴) ∈ ℂ) | 
| 77 | 75, 7, 76 | sylancr 587 | . . . . 5
⊢ (𝐴 ∈ dom arctan → (-2
· 𝐴) ∈
ℂ) | 
| 78 | 75 | a1i 11 | . . . . 5
⊢ (𝐴 ∈ dom arctan → -2
∈ ℂ) | 
| 79 |  | 2ne0 12370 | . . . . . . 7
⊢ 2 ≠
0 | 
| 80 | 38, 79 | negne0i 11584 | . . . . . 6
⊢ -2 ≠
0 | 
| 81 | 80 | a1i 11 | . . . . 5
⊢ (𝐴 ∈ dom arctan → -2
≠ 0) | 
| 82 | 77, 78, 10, 81, 19 | divcan7d 12071 | . . . 4
⊢ (𝐴 ∈ dom arctan → (((-2
· 𝐴) / (𝐴 + i)) / (-2 / (𝐴 + i))) = ((-2 · 𝐴) / -2)) | 
| 83 | 7, 78, 81 | divcan3d 12048 | . . . 4
⊢ (𝐴 ∈ dom arctan → ((-2
· 𝐴) / -2) = 𝐴) | 
| 84 | 82, 83 | eqtrd 2777 | . . 3
⊢ (𝐴 ∈ dom arctan → (((-2
· 𝐴) / (𝐴 + i)) / (-2 / (𝐴 + i))) = 𝐴) | 
| 85 | 74, 84 | eqtrd 2777 | . 2
⊢ (𝐴 ∈ dom arctan →
(((exp‘(2 · (i · (arctan‘𝐴)))) − 1) / (i · ((exp‘(2
· (i · (arctan‘𝐴)))) + 1))) = 𝐴) | 
| 86 | 30, 85 | eqtrd 2777 | 1
⊢ (𝐴 ∈ dom arctan →
(tan‘(arctan‘𝐴)) = 𝐴) |