Proof of Theorem ang180lem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ang180lem1.3 | . . . . . . . . . 10
⊢ 𝑁 = (((𝑇 / i) / (2 · π)) − (1 /
2)) | 
| 2 |  | ang.1 | . . . . . . . . . . . . . . . 16
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0})
↦ (ℑ‘(log‘(𝑦 / 𝑥)))) | 
| 3 |  | ang180lem1.2 | . . . . . . . . . . . . . . . 16
⊢ 𝑇 = (((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) | 
| 4 | 2, 3, 1 | ang180lem2 26854 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-2 < 𝑁 ∧ 𝑁 < 1)) | 
| 5 | 4 | simprd 495 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑁 < 1) | 
| 6 |  | 1e0p1 12777 | . . . . . . . . . . . . . 14
⊢ 1 = (0 +
1) | 
| 7 | 5, 6 | breqtrdi 5183 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑁 < (0 + 1)) | 
| 8 | 2, 3, 1 | ang180lem1 26853 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑁 ∈ ℤ ∧ (𝑇 / i) ∈ ℝ)) | 
| 9 | 8 | simpld 494 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑁 ∈ ℤ) | 
| 10 |  | 0z 12626 | . . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ | 
| 11 |  | zleltp1 12670 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 0 ∈
ℤ) → (𝑁 ≤ 0
↔ 𝑁 < (0 +
1))) | 
| 12 | 9, 10, 11 | sylancl 586 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑁 ≤ 0 ↔ 𝑁 < (0 + 1))) | 
| 13 | 7, 12 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑁 ≤ 0) | 
| 14 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → 𝑁 ≤ 0) | 
| 15 |  | zlem1lt 12671 | . . . . . . . . . . . . . 14
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 ≤ 𝑁 ↔ (0 − 1) < 𝑁)) | 
| 16 | 10, 9, 15 | sylancr 587 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (0 ≤ 𝑁 ↔ (0 − 1) < 𝑁)) | 
| 17 |  | df-neg 11496 | . . . . . . . . . . . . . 14
⊢ -1 = (0
− 1) | 
| 18 | 17 | breq1i 5149 | . . . . . . . . . . . . 13
⊢ (-1 <
𝑁 ↔ (0 − 1) <
𝑁) | 
| 19 | 16, 18 | bitr4di 289 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (0 ≤ 𝑁 ↔ -1 < 𝑁)) | 
| 20 | 19 | biimpar 477 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → 0 ≤ 𝑁) | 
| 21 | 9 | zred 12724 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑁 ∈ ℝ) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → 𝑁 ∈ ℝ) | 
| 23 |  | 0re 11264 | . . . . . . . . . . . 12
⊢ 0 ∈
ℝ | 
| 24 |  | letri3 11347 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 0 ∈
ℝ) → (𝑁 = 0
↔ (𝑁 ≤ 0 ∧ 0
≤ 𝑁))) | 
| 25 | 22, 23, 24 | sylancl 586 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → (𝑁 = 0 ↔ (𝑁 ≤ 0 ∧ 0 ≤ 𝑁))) | 
| 26 | 14, 20, 25 | mpbir2and 713 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → 𝑁 = 0) | 
| 27 | 1, 26 | eqtr3id 2790 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → (((𝑇 / i) / (2 · π)) − (1 / 2))
= 0) | 
| 28 |  | ax-1cn 11214 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ | 
| 29 |  | simp1 1136 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ∈ ℂ) | 
| 30 |  | subcl 11508 | . . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − 𝐴) ∈ ℂ) | 
| 31 | 28, 29, 30 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 − 𝐴) ∈ ℂ) | 
| 32 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ≠ 1) | 
| 33 | 32 | necomd 2995 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 1 ≠ 𝐴) | 
| 34 |  | subeq0 11536 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) | 
| 35 | 28, 29, 34 | sylancr 587 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) | 
| 36 | 35 | necon3bid 2984 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) ≠ 0 ↔ 1 ≠ 𝐴)) | 
| 37 | 33, 36 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 − 𝐴) ≠ 0) | 
| 38 | 31, 37 | reccld 12037 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / (1 − 𝐴)) ∈
ℂ) | 
| 39 | 31, 37 | recne0d 12038 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / (1 − 𝐴)) ≠ 0) | 
| 40 | 38, 39 | logcld 26613 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘(1 / (1 −
𝐴))) ∈
ℂ) | 
| 41 |  | subcl 11508 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) ∈ ℂ) | 
| 42 | 29, 28, 41 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 − 1) ∈ ℂ) | 
| 43 |  | simp2 1137 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ≠ 0) | 
| 44 | 42, 29, 43 | divcld 12044 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) / 𝐴) ∈ ℂ) | 
| 45 |  | subeq0 11536 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 −
1) = 0 ↔ 𝐴 =
1)) | 
| 46 | 29, 28, 45 | sylancl 586 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) = 0 ↔ 𝐴 = 1)) | 
| 47 | 46 | necon3bid 2984 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) ≠ 0 ↔ 𝐴 ≠ 1)) | 
| 48 | 32, 47 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 − 1) ≠ 0) | 
| 49 | 42, 29, 48, 43 | divne0d 12060 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) / 𝐴) ≠ 0) | 
| 50 | 44, 49 | logcld 26613 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘((𝐴 − 1) / 𝐴)) ∈ ℂ) | 
| 51 | 40, 50 | addcld 11281 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) ∈ ℂ) | 
| 52 |  | logcl 26611 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) | 
| 53 | 52 | 3adant3 1132 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘𝐴) ∈ ℂ) | 
| 54 | 51, 53 | addcld 11281 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) ∈ ℂ) | 
| 55 | 3, 54 | eqeltrid 2844 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑇 ∈ ℂ) | 
| 56 |  | ax-icn 11215 | . . . . . . . . . . . . . 14
⊢ i ∈
ℂ | 
| 57 | 56 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → i ∈
ℂ) | 
| 58 |  | ine0 11699 | . . . . . . . . . . . . . 14
⊢ i ≠
0 | 
| 59 | 58 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → i ≠ 0) | 
| 60 | 55, 57, 59 | divcld 12044 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) ∈ ℂ) | 
| 61 |  | 2cn 12342 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ | 
| 62 |  | picn 26502 | . . . . . . . . . . . . . 14
⊢ π
∈ ℂ | 
| 63 | 61, 62 | mulcli 11269 | . . . . . . . . . . . . 13
⊢ (2
· π) ∈ ℂ | 
| 64 | 63 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ∈
ℂ) | 
| 65 |  | 2ne0 12371 | . . . . . . . . . . . . . 14
⊢ 2 ≠
0 | 
| 66 |  | pire 26501 | . . . . . . . . . . . . . . 15
⊢ π
∈ ℝ | 
| 67 |  | pipos 26503 | . . . . . . . . . . . . . . 15
⊢ 0 <
π | 
| 68 | 66, 67 | gt0ne0ii 11800 | . . . . . . . . . . . . . 14
⊢ π ≠
0 | 
| 69 | 61, 62, 65, 68 | mulne0i 11907 | . . . . . . . . . . . . 13
⊢ (2
· π) ≠ 0 | 
| 70 | 69 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ≠
0) | 
| 71 | 60, 64, 70 | divcld 12044 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) / (2 · π)) ∈
ℂ) | 
| 72 | 71 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → ((𝑇 / i) / (2 · π)) ∈
ℂ) | 
| 73 |  | halfcn 12482 | . . . . . . . . . 10
⊢ (1 / 2)
∈ ℂ | 
| 74 |  | subeq0 11536 | . . . . . . . . . 10
⊢ ((((𝑇 / i) / (2 · π))
∈ ℂ ∧ (1 / 2) ∈ ℂ) → ((((𝑇 / i) / (2 · π)) − (1 / 2))
= 0 ↔ ((𝑇 / i) / (2
· π)) = (1 / 2))) | 
| 75 | 72, 73, 74 | sylancl 586 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → ((((𝑇 / i) / (2 · π)) − (1 / 2))
= 0 ↔ ((𝑇 / i) / (2
· π)) = (1 / 2))) | 
| 76 | 27, 75 | mpbid 232 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → ((𝑇 / i) / (2 · π)) = (1 /
2)) | 
| 77 | 60 | adantr 480 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → (𝑇 / i) ∈ ℂ) | 
| 78 | 63 | a1i 11 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → (2 · π) ∈
ℂ) | 
| 79 | 73 | a1i 11 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → (1 / 2) ∈
ℂ) | 
| 80 | 69 | a1i 11 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → (2 · π) ≠
0) | 
| 81 | 77, 78, 79, 80 | divmuld 12066 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → (((𝑇 / i) / (2 · π)) = (1 / 2) ↔
((2 · π) · (1 / 2)) = (𝑇 / i))) | 
| 82 | 76, 81 | mpbid 232 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → ((2 · π) · (1 /
2)) = (𝑇 /
i)) | 
| 83 | 63, 61, 65 | divreci 12013 | . . . . . . . 8
⊢ ((2
· π) / 2) = ((2 · π) · (1 / 2)) | 
| 84 | 62, 61, 65 | divcan3i 12014 | . . . . . . . 8
⊢ ((2
· π) / 2) = π | 
| 85 | 83, 84 | eqtr3i 2766 | . . . . . . 7
⊢ ((2
· π) · (1 / 2)) = π | 
| 86 | 82, 85 | eqtr3di 2791 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → (𝑇 / i) = π) | 
| 87 | 55 | adantr 480 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → 𝑇 ∈ ℂ) | 
| 88 | 56 | a1i 11 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → i ∈ ℂ) | 
| 89 | 62 | a1i 11 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → π ∈
ℂ) | 
| 90 | 58 | a1i 11 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → i ≠ 0) | 
| 91 | 87, 88, 89, 90 | divmuld 12066 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → ((𝑇 / i) = π ↔ (i · π) =
𝑇)) | 
| 92 | 86, 91 | mpbid 232 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → (i · π) = 𝑇) | 
| 93 | 92 | eqcomd 2742 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → 𝑇 = (i · π)) | 
| 94 | 93 | olcd 874 | . . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 < 𝑁) → (𝑇 = -(i · π) ∨ 𝑇 = (i · π))) | 
| 95 | 62, 56 | mulneg1i 11710 | . . . . . . 7
⊢ (-π
· i) = -(π · i) | 
| 96 | 62, 56 | mulcomi 11270 | . . . . . . . 8
⊢ (π
· i) = (i · π) | 
| 97 | 96 | negeqi 11502 | . . . . . . 7
⊢ -(π
· i) = -(i · π) | 
| 98 | 95, 97 | eqtri 2764 | . . . . . 6
⊢ (-π
· i) = -(i · π) | 
| 99 | 73, 63 | mulneg1i 11710 | . . . . . . . . . 10
⊢ (-(1 / 2)
· (2 · π)) = -((1 / 2) · (2 ·
π)) | 
| 100 | 28, 61, 65 | divcan1i 12012 | . . . . . . . . . . . . 13
⊢ ((1 / 2)
· 2) = 1 | 
| 101 | 100 | oveq1i 7442 | . . . . . . . . . . . 12
⊢ (((1 / 2)
· 2) · π) = (1 · π) | 
| 102 | 73, 61, 62 | mulassi 11273 | . . . . . . . . . . . 12
⊢ (((1 / 2)
· 2) · π) = ((1 / 2) · (2 ·
π)) | 
| 103 | 62 | mullidi 11267 | . . . . . . . . . . . 12
⊢ (1
· π) = π | 
| 104 | 101, 102,
103 | 3eqtr3i 2772 | . . . . . . . . . . 11
⊢ ((1 / 2)
· (2 · π)) = π | 
| 105 | 104 | negeqi 11502 | . . . . . . . . . 10
⊢ -((1 / 2)
· (2 · π)) = -π | 
| 106 | 99, 105 | eqtri 2764 | . . . . . . . . 9
⊢ (-(1 / 2)
· (2 · π)) = -π | 
| 107 | 28, 73 | negsubdii 11595 | . . . . . . . . . . . . 13
⊢ -(1
− (1 / 2)) = (-1 + (1 / 2)) | 
| 108 |  | 1mhlfehlf 12487 | . . . . . . . . . . . . . 14
⊢ (1
− (1 / 2)) = (1 / 2) | 
| 109 | 108 | negeqi 11502 | . . . . . . . . . . . . 13
⊢ -(1
− (1 / 2)) = -(1 / 2) | 
| 110 | 107, 109 | eqtr3i 2766 | . . . . . . . . . . . 12
⊢ (-1 + (1
/ 2)) = -(1 / 2) | 
| 111 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → -1 = 𝑁) | 
| 112 | 111, 1 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → -1 = (((𝑇 / i) / (2 · π)) − (1 /
2))) | 
| 113 | 112 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → (-1 + (1 / 2)) = ((((𝑇 / i) / (2 · π))
− (1 / 2)) + (1 / 2))) | 
| 114 | 110, 113 | eqtr3id 2790 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → -(1 / 2) = ((((𝑇 / i) / (2 · π)) − (1 / 2))
+ (1 / 2))) | 
| 115 |  | npcan 11518 | . . . . . . . . . . . . 13
⊢ ((((𝑇 / i) / (2 · π))
∈ ℂ ∧ (1 / 2) ∈ ℂ) → ((((𝑇 / i) / (2 · π)) − (1 / 2))
+ (1 / 2)) = ((𝑇 / i) / (2
· π))) | 
| 116 | 71, 73, 115 | sylancl 586 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((𝑇 / i) / (2 · π)) − (1 / 2))
+ (1 / 2)) = ((𝑇 / i) / (2
· π))) | 
| 117 | 116 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → ((((𝑇 / i) / (2 · π)) − (1 / 2))
+ (1 / 2)) = ((𝑇 / i) / (2
· π))) | 
| 118 | 114, 117 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → -(1 / 2) = ((𝑇 / i) / (2 · π))) | 
| 119 | 118 | oveq1d 7447 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → (-(1 / 2) · (2 ·
π)) = (((𝑇 / i) / (2
· π)) · (2 · π))) | 
| 120 | 106, 119 | eqtr3id 2790 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → -π = (((𝑇 / i) / (2 · π)) · (2
· π))) | 
| 121 | 60, 64, 70 | divcan1d 12045 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((𝑇 / i) / (2 · π)) · (2
· π)) = (𝑇 /
i)) | 
| 122 | 121 | adantr 480 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → (((𝑇 / i) / (2 · π)) · (2
· π)) = (𝑇 /
i)) | 
| 123 | 120, 122 | eqtrd 2776 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → -π = (𝑇 / i)) | 
| 124 | 123 | oveq1d 7447 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → (-π · i) = ((𝑇 / i) ·
i)) | 
| 125 | 98, 124 | eqtr3id 2790 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → -(i · π) = ((𝑇 / i) ·
i)) | 
| 126 | 55, 57, 59 | divcan1d 12045 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) · i) = 𝑇) | 
| 127 | 126 | adantr 480 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → ((𝑇 / i) · i) = 𝑇) | 
| 128 | 125, 127 | eqtr2d 2777 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → 𝑇 = -(i · π)) | 
| 129 | 128 | orcd 873 | . . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ -1 = 𝑁) → (𝑇 = -(i · π) ∨ 𝑇 = (i · π))) | 
| 130 |  | df-2 12330 | . . . . . . . 8
⊢ 2 = (1 +
1) | 
| 131 | 130 | negeqi 11502 | . . . . . . 7
⊢ -2 = -(1
+ 1) | 
| 132 |  | negdi2 11568 | . . . . . . . 8
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ) → -(1 + 1) = (-1 −
1)) | 
| 133 | 28, 28, 132 | mp2an 692 | . . . . . . 7
⊢ -(1 + 1)
= (-1 − 1) | 
| 134 | 131, 133 | eqtri 2764 | . . . . . 6
⊢ -2 = (-1
− 1) | 
| 135 | 4 | simpld 494 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -2 < 𝑁) | 
| 136 | 134, 135 | eqbrtrrid 5178 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-1 − 1) < 𝑁) | 
| 137 |  | neg1z 12655 | . . . . . 6
⊢ -1 ∈
ℤ | 
| 138 |  | zlem1lt 12671 | . . . . . 6
⊢ ((-1
∈ ℤ ∧ 𝑁
∈ ℤ) → (-1 ≤ 𝑁 ↔ (-1 − 1) < 𝑁)) | 
| 139 | 137, 9, 138 | sylancr 587 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-1 ≤ 𝑁 ↔ (-1 − 1) < 𝑁)) | 
| 140 | 136, 139 | mpbird 257 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -1 ≤ 𝑁) | 
| 141 |  | neg1rr 12382 | . . . . 5
⊢ -1 ∈
ℝ | 
| 142 |  | leloe 11348 | . . . . 5
⊢ ((-1
∈ ℝ ∧ 𝑁
∈ ℝ) → (-1 ≤ 𝑁 ↔ (-1 < 𝑁 ∨ -1 = 𝑁))) | 
| 143 | 141, 21, 142 | sylancr 587 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-1 ≤ 𝑁 ↔ (-1 < 𝑁 ∨ -1 = 𝑁))) | 
| 144 | 140, 143 | mpbid 232 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-1 < 𝑁 ∨ -1 = 𝑁)) | 
| 145 | 94, 129, 144 | mpjaodan 960 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 = -(i · π) ∨ 𝑇 = (i · π))) | 
| 146 | 3 | ovexi 7466 | . . 3
⊢ 𝑇 ∈ V | 
| 147 | 146 | elpr 4649 | . 2
⊢ (𝑇 ∈ {-(i · π), (i
· π)} ↔ (𝑇 =
-(i · π) ∨ 𝑇 =
(i · π))) | 
| 148 | 145, 147 | sylibr 234 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑇 ∈ {-(i · π), (i ·
π)}) |