Proof of Theorem logrec
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reccl 11930 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℂ) | 
| 2 |  | recne0 11936 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ≠ 0) | 
| 3 |  | eflog 26619 | . . . . . . . 8
⊢ (((1 /
𝐴) ∈ ℂ ∧ (1
/ 𝐴) ≠ 0) →
(exp‘(log‘(1 / 𝐴))) = (1 / 𝐴)) | 
| 4 | 1, 2, 3 | syl2anc 584 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘(1 / 𝐴))) = (1 / 𝐴)) | 
| 5 | 4 | eqcomd 2742 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) = (exp‘(log‘(1 /
𝐴)))) | 
| 6 | 5 | oveq2d 7448 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / (1 / 𝐴)) = (1 /
(exp‘(log‘(1 / 𝐴))))) | 
| 7 |  | eflog 26619 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
𝐴) | 
| 8 |  | recrec 11965 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / (1 / 𝐴)) = 𝐴) | 
| 9 | 7, 8 | eqtr4d 2779 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
(1 / (1 / 𝐴))) | 
| 10 | 1, 2 | logcld 26613 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘(1 /
𝐴)) ∈
ℂ) | 
| 11 |  | efneg 16135 | . . . . . 6
⊢
((log‘(1 / 𝐴))
∈ ℂ → (exp‘-(log‘(1 / 𝐴))) = (1 / (exp‘(log‘(1 / 𝐴))))) | 
| 12 | 10, 11 | syl 17 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘-(log‘(1 / 𝐴))) = (1 / (exp‘(log‘(1 / 𝐴))))) | 
| 13 | 6, 9, 12 | 3eqtr4d 2786 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
(exp‘-(log‘(1 / 𝐴)))) | 
| 14 | 13 | 3adant3 1132 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) →
(exp‘(log‘𝐴)) =
(exp‘-(log‘(1 / 𝐴)))) | 
| 15 | 14 | fveq2d 6909 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) →
(log‘(exp‘(log‘𝐴))) = (log‘(exp‘-(log‘(1 /
𝐴))))) | 
| 16 |  | logrncl 26610 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ran
log) | 
| 17 | 16 | 3adant3 1132 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) → (log‘𝐴) ∈ ran
log) | 
| 18 |  | logef 26624 | . . 3
⊢
((log‘𝐴)
∈ ran log → (log‘(exp‘(log‘𝐴))) = (log‘𝐴)) | 
| 19 | 17, 18 | syl 17 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) →
(log‘(exp‘(log‘𝐴))) = (log‘𝐴)) | 
| 20 |  | df-ne 2940 | . . . . 5
⊢
((ℑ‘(log‘𝐴)) ≠ π ↔ ¬
(ℑ‘(log‘𝐴)) = π) | 
| 21 |  | lognegb 26633 | . . . . . . . . . . . 12
⊢ (((1 /
𝐴) ∈ ℂ ∧ (1
/ 𝐴) ≠ 0) → (-(1 /
𝐴) ∈
ℝ+ ↔ (ℑ‘(log‘(1 / 𝐴))) = π)) | 
| 22 | 1, 2, 21 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-(1 / 𝐴) ∈ ℝ+
↔ (ℑ‘(log‘(1 / 𝐴))) = π)) | 
| 23 | 22 | biimprd 248 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((ℑ‘(log‘(1 / 𝐴))) = π → -(1 / 𝐴) ∈
ℝ+)) | 
| 24 |  | ax-1cn 11214 | . . . . . . . . . . . 12
⊢ 1 ∈
ℂ | 
| 25 |  | divneg2 11992 | . . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ ∧ 𝐴 ≠
0) → -(1 / 𝐴) = (1 /
-𝐴)) | 
| 26 | 24, 25 | mp3an1 1449 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -(1 / 𝐴) = (1 / -𝐴)) | 
| 27 | 26 | eleq1d 2825 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-(1 / 𝐴) ∈ ℝ+
↔ (1 / -𝐴) ∈
ℝ+)) | 
| 28 | 23, 27 | sylibd 239 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((ℑ‘(log‘(1 / 𝐴))) = π → (1 / -𝐴) ∈
ℝ+)) | 
| 29 |  | negcl 11509 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) | 
| 30 |  | negeq0 11564 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (𝐴 = 0 ↔ -𝐴 = 0)) | 
| 31 | 30 | necon3bid 2984 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ -𝐴 ≠ 0)) | 
| 32 | 31 | biimpa 476 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -𝐴 ≠ 0) | 
| 33 |  | rpreccl 13062 | . . . . . . . . . . 11
⊢ ((1 /
-𝐴) ∈
ℝ+ → (1 / (1 / -𝐴)) ∈
ℝ+) | 
| 34 |  | recrec 11965 | . . . . . . . . . . . 12
⊢ ((-𝐴 ∈ ℂ ∧ -𝐴 ≠ 0) → (1 / (1 / -𝐴)) = -𝐴) | 
| 35 | 34 | eleq1d 2825 | . . . . . . . . . . 11
⊢ ((-𝐴 ∈ ℂ ∧ -𝐴 ≠ 0) → ((1 / (1 /
-𝐴)) ∈
ℝ+ ↔ -𝐴 ∈
ℝ+)) | 
| 36 | 33, 35 | imbitrid 244 | . . . . . . . . . 10
⊢ ((-𝐴 ∈ ℂ ∧ -𝐴 ≠ 0) → ((1 / -𝐴) ∈ ℝ+
→ -𝐴 ∈
ℝ+)) | 
| 37 | 29, 32, 36 | syl2an2r 685 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((1 / -𝐴) ∈ ℝ+
→ -𝐴 ∈
ℝ+)) | 
| 38 | 28, 37 | syld 47 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((ℑ‘(log‘(1 / 𝐴))) = π → -𝐴 ∈
ℝ+)) | 
| 39 |  | lognegb 26633 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-𝐴 ∈ ℝ+
↔ (ℑ‘(log‘𝐴)) = π)) | 
| 40 | 38, 39 | sylibd 239 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((ℑ‘(log‘(1 / 𝐴))) = π →
(ℑ‘(log‘𝐴)) = π)) | 
| 41 | 40 | con3d 152 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (¬
(ℑ‘(log‘𝐴)) = π → ¬
(ℑ‘(log‘(1 / 𝐴))) = π)) | 
| 42 | 41 | 3impia 1117 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ¬
(ℑ‘(log‘𝐴)) = π) → ¬
(ℑ‘(log‘(1 / 𝐴))) = π) | 
| 43 | 20, 42 | syl3an3b 1406 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) → ¬
(ℑ‘(log‘(1 / 𝐴))) = π) | 
| 44 |  | logrncl 26610 | . . . . . 6
⊢ (((1 /
𝐴) ∈ ℂ ∧ (1
/ 𝐴) ≠ 0) →
(log‘(1 / 𝐴)) ∈
ran log) | 
| 45 | 1, 2, 44 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘(1 /
𝐴)) ∈ ran
log) | 
| 46 |  | logreclem 26806 | . . . . 5
⊢
(((log‘(1 / 𝐴)) ∈ ran log ∧ ¬
(ℑ‘(log‘(1 / 𝐴))) = π) → -(log‘(1 / 𝐴)) ∈ ran
log) | 
| 47 | 45, 46 | stoic3 1775 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ¬
(ℑ‘(log‘(1 / 𝐴))) = π) → -(log‘(1 / 𝐴)) ∈ ran
log) | 
| 48 | 43, 47 | syld3an3 1410 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) → -(log‘(1 / 𝐴)) ∈ ran
log) | 
| 49 |  | logef 26624 | . . 3
⊢
(-(log‘(1 / 𝐴)) ∈ ran log →
(log‘(exp‘-(log‘(1 / 𝐴)))) = -(log‘(1 / 𝐴))) | 
| 50 | 48, 49 | syl 17 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) →
(log‘(exp‘-(log‘(1 / 𝐴)))) = -(log‘(1 / 𝐴))) | 
| 51 | 15, 19, 50 | 3eqtr3d 2784 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) → (log‘𝐴) = -(log‘(1 / 𝐴))) |