Proof of Theorem ang180lem4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ang.1 | . . . . . . 7
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0})
↦ (ℑ‘(log‘(𝑦 / 𝑥)))) | 
| 2 |  | 1cnd 11257 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 1 ∈
ℂ) | 
| 3 |  | simp1 1136 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ∈ ℂ) | 
| 4 | 2, 3 | subcld 11621 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 − 𝐴) ∈ ℂ) | 
| 5 |  | simp3 1138 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ≠ 1) | 
| 6 | 5 | necomd 2995 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 1 ≠ 𝐴) | 
| 7 | 2, 3, 6 | subne0d 11630 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 − 𝐴) ≠ 0) | 
| 8 |  | ax-1ne0 11225 | . . . . . . . 8
⊢ 1 ≠
0 | 
| 9 | 8 | a1i 11 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 1 ≠ 0) | 
| 10 | 1, 4, 7, 2, 9 | angvald 26848 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴)𝐹1) = (ℑ‘(log‘(1 / (1
− 𝐴))))) | 
| 11 |  | simp2 1137 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ≠ 0) | 
| 12 | 3, 2 | subcld 11621 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 − 1) ∈ ℂ) | 
| 13 | 3, 2, 5 | subne0d 11630 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 − 1) ≠ 0) | 
| 14 | 1, 3, 11, 12, 13 | angvald 26848 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴𝐹(𝐴 − 1)) =
(ℑ‘(log‘((𝐴 − 1) / 𝐴)))) | 
| 15 | 10, 14 | oveq12d 7450 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((1 − 𝐴)𝐹1) + (𝐴𝐹(𝐴 − 1))) =
((ℑ‘(log‘(1 / (1 − 𝐴)))) + (ℑ‘(log‘((𝐴 − 1) / 𝐴))))) | 
| 16 | 2, 4, 7 | divcld 12044 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / (1 − 𝐴)) ∈
ℂ) | 
| 17 | 4, 7 | recne0d 12038 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / (1 − 𝐴)) ≠ 0) | 
| 18 | 16, 17 | logcld 26613 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘(1 / (1 −
𝐴))) ∈
ℂ) | 
| 19 | 12, 3, 11 | divcld 12044 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) / 𝐴) ∈ ℂ) | 
| 20 | 12, 3, 13, 11 | divne0d 12060 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) / 𝐴) ≠ 0) | 
| 21 | 19, 20 | logcld 26613 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘((𝐴 − 1) / 𝐴)) ∈ ℂ) | 
| 22 | 18, 21 | imaddd 15255 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) = ((ℑ‘(log‘(1 / (1
− 𝐴)))) +
(ℑ‘(log‘((𝐴 − 1) / 𝐴))))) | 
| 23 | 15, 22 | eqtr4d 2779 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((1 − 𝐴)𝐹1) + (𝐴𝐹(𝐴 − 1))) =
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) | 
| 24 | 1, 2, 9, 3, 11 | angvald 26848 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1𝐹𝐴) = (ℑ‘(log‘(𝐴 / 1)))) | 
| 25 | 3 | div1d 12036 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 / 1) = 𝐴) | 
| 26 | 25 | fveq2d 6909 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘(𝐴 / 1)) = (log‘𝐴)) | 
| 27 | 26 | fveq2d 6909 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘(𝐴 / 1))) = (ℑ‘(log‘𝐴))) | 
| 28 | 24, 27 | eqtrd 2776 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1𝐹𝐴) = (ℑ‘(log‘𝐴))) | 
| 29 | 23, 28 | oveq12d 7450 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((1 − 𝐴)𝐹1) + (𝐴𝐹(𝐴 − 1))) + (1𝐹𝐴)) = ((ℑ‘((log‘(1 / (1
− 𝐴))) +
(log‘((𝐴 − 1) /
𝐴)))) +
(ℑ‘(log‘𝐴)))) | 
| 30 | 18, 21 | addcld 11281 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) ∈ ℂ) | 
| 31 | 3, 11 | logcld 26613 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘𝐴) ∈ ℂ) | 
| 32 | 30, 31 | imaddd 15255 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = ((ℑ‘((log‘(1 / (1
− 𝐴))) +
(log‘((𝐴 − 1) /
𝐴)))) +
(ℑ‘(log‘𝐴)))) | 
| 33 | 29, 32 | eqtr4d 2779 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((1 − 𝐴)𝐹1) + (𝐴𝐹(𝐴 − 1))) + (1𝐹𝐴)) = (ℑ‘(((log‘(1 / (1
− 𝐴))) +
(log‘((𝐴 − 1) /
𝐴))) + (log‘𝐴)))) | 
| 34 |  | eqid 2736 | . . . 4
⊢
(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) = (((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) | 
| 35 |  | eqid 2736 | . . . 4
⊢
((((((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) / i) / (2 · π)) − (1 /
2)) = ((((((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) / i) / (2 · π)) − (1 /
2)) | 
| 36 | 1, 34, 35 | ang180lem3 26855 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) ∈ {-(i · π), (i ·
π)}) | 
| 37 |  | fveq2 6905 | . . . . . 6
⊢
((((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) = -(i · π) →
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = (ℑ‘-(i ·
π))) | 
| 38 |  | ax-icn 11215 | . . . . . . . . 9
⊢ i ∈
ℂ | 
| 39 |  | picn 26502 | . . . . . . . . 9
⊢ π
∈ ℂ | 
| 40 | 38, 39 | mulcli 11269 | . . . . . . . 8
⊢ (i
· π) ∈ ℂ | 
| 41 | 40 | imnegi 15221 | . . . . . . 7
⊢
(ℑ‘-(i · π)) = -(ℑ‘(i ·
π)) | 
| 42 | 40 | addlidi 11450 | . . . . . . . . . 10
⊢ (0 + (i
· π)) = (i · π) | 
| 43 | 42 | fveq2i 6908 | . . . . . . . . 9
⊢
(ℑ‘(0 + (i · π))) = (ℑ‘(i ·
π)) | 
| 44 |  | 0re 11264 | . . . . . . . . . 10
⊢ 0 ∈
ℝ | 
| 45 |  | pire 26501 | . . . . . . . . . 10
⊢ π
∈ ℝ | 
| 46 | 44, 45 | crimi 15233 | . . . . . . . . 9
⊢
(ℑ‘(0 + (i · π))) = π | 
| 47 | 43, 46 | eqtr3i 2766 | . . . . . . . 8
⊢
(ℑ‘(i · π)) = π | 
| 48 | 47 | negeqi 11502 | . . . . . . 7
⊢
-(ℑ‘(i · π)) = -π | 
| 49 | 41, 48 | eqtri 2764 | . . . . . 6
⊢
(ℑ‘-(i · π)) = -π | 
| 50 | 37, 49 | eqtrdi 2792 | . . . . 5
⊢
((((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) = -(i · π) →
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = -π) | 
| 51 |  | fveq2 6905 | . . . . . 6
⊢
((((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) = (i · π) →
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = (ℑ‘(i ·
π))) | 
| 52 | 51, 47 | eqtrdi 2792 | . . . . 5
⊢
((((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) = (i · π) →
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = π) | 
| 53 | 50, 52 | orim12i 908 | . . . 4
⊢
(((((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) = -(i · π) ∨ (((log‘(1
/ (1 − 𝐴))) +
(log‘((𝐴 − 1) /
𝐴))) + (log‘𝐴)) = (i · π)) →
((ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = -π ∨
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = π)) | 
| 54 |  | ovex 7465 | . . . . 5
⊢
(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) ∈ V | 
| 55 | 54 | elpr 4649 | . . . 4
⊢
((((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) ∈ {-(i · π), (i ·
π)} ↔ ((((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) = -(i · π) ∨ (((log‘(1
/ (1 − 𝐴))) +
(log‘((𝐴 − 1) /
𝐴))) + (log‘𝐴)) = (i ·
π))) | 
| 56 |  | fvex 6918 | . . . . 5
⊢
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) ∈ V | 
| 57 | 56 | elpr 4649 | . . . 4
⊢
((ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) ∈ {-π, π} ↔
((ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = -π ∨
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = π)) | 
| 58 | 53, 55, 57 | 3imtr4i 292 | . . 3
⊢
((((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) ∈ {-(i · π), (i ·
π)} → (ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) ∈ {-π, π}) | 
| 59 | 36, 58 | syl 17 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) ∈ {-π, π}) | 
| 60 | 33, 59 | eqeltrd 2840 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((1 − 𝐴)𝐹1) + (𝐴𝐹(𝐴 − 1))) + (1𝐹𝐴)) ∈ {-π, π}) |