Proof of Theorem logrec
Step | Hyp | Ref
| Expression |
1 | | reccl 11017 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℂ) |
2 | | recne0 11023 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ≠ 0) |
3 | | eflog 24722 |
. . . . . . . 8
⊢ (((1 /
𝐴) ∈ ℂ ∧ (1
/ 𝐴) ≠ 0) →
(exp‘(log‘(1 / 𝐴))) = (1 / 𝐴)) |
4 | 1, 2, 3 | syl2anc 579 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘(1 / 𝐴))) = (1 / 𝐴)) |
5 | 4 | eqcomd 2831 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) = (exp‘(log‘(1 /
𝐴)))) |
6 | 5 | oveq2d 6921 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / (1 / 𝐴)) = (1 /
(exp‘(log‘(1 / 𝐴))))) |
7 | | eflog 24722 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
𝐴) |
8 | | recrec 11048 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / (1 / 𝐴)) = 𝐴) |
9 | 7, 8 | eqtr4d 2864 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
(1 / (1 / 𝐴))) |
10 | 1, 2 | logcld 24716 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘(1 /
𝐴)) ∈
ℂ) |
11 | | efneg 15200 |
. . . . . 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 2871 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
(exp‘-(log‘(1 / 𝐴)))) |
14 | 13 | 3adant3 1166 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) →
(exp‘(log‘𝐴)) =
(exp‘-(log‘(1 / 𝐴)))) |
15 | 14 | fveq2d 6437 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) →
(log‘(exp‘(log‘𝐴))) = (log‘(exp‘-(log‘(1 /
𝐴))))) |
16 | | logrncl 24713 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ran
log) |
17 | 16 | 3adant3 1166 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) → (log‘𝐴) ∈ ran
log) |
18 | | logef 24727 |
. . 3
⊢
((log‘𝐴)
∈ ran log → (log‘(exp‘(log‘𝐴))) = (log‘𝐴)) |
19 | 17, 18 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) →
(log‘(exp‘(log‘𝐴))) = (log‘𝐴)) |
20 | | df-ne 3000 |
. . . . 5
⊢
((ℑ‘(log‘𝐴)) ≠ π ↔ ¬
(ℑ‘(log‘𝐴)) = π) |
21 | | lognegb 24735 |
. . . . . . . . . . . 12
⊢ (((1 /
𝐴) ∈ ℂ ∧ (1
/ 𝐴) ≠ 0) → (-(1 /
𝐴) ∈
ℝ+ ↔ (ℑ‘(log‘(1 / 𝐴))) = π)) |
22 | 1, 2, 21 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-(1 / 𝐴) ∈ ℝ+
↔ (ℑ‘(log‘(1 / 𝐴))) = π)) |
23 | 22 | biimprd 240 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((ℑ‘(log‘(1 / 𝐴))) = π → -(1 / 𝐴) ∈
ℝ+)) |
24 | | ax-1cn 10310 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
25 | | divneg2 11075 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ ∧ 𝐴 ≠
0) → -(1 / 𝐴) = (1 /
-𝐴)) |
26 | 24, 25 | mp3an1 1576 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -(1 / 𝐴) = (1 / -𝐴)) |
27 | 26 | eleq1d 2891 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-(1 / 𝐴) ∈ ℝ+
↔ (1 / -𝐴) ∈
ℝ+)) |
28 | 23, 27 | sylibd 231 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((ℑ‘(log‘(1 / 𝐴))) = π → (1 / -𝐴) ∈
ℝ+)) |
29 | | negcl 10601 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) |
30 | 29 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -𝐴 ∈
ℂ) |
31 | | negeq0 10656 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (𝐴 = 0 ↔ -𝐴 = 0)) |
32 | 31 | necon3bid 3043 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ -𝐴 ≠ 0)) |
33 | 32 | biimpa 470 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -𝐴 ≠ 0) |
34 | | rpreccl 12140 |
. . . . . . . . . . 11
⊢ ((1 /
-𝐴) ∈
ℝ+ → (1 / (1 / -𝐴)) ∈
ℝ+) |
35 | | recrec 11048 |
. . . . . . . . . . . 12
⊢ ((-𝐴 ∈ ℂ ∧ -𝐴 ≠ 0) → (1 / (1 / -𝐴)) = -𝐴) |
36 | 35 | eleq1d 2891 |
. . . . . . . . . . 11
⊢ ((-𝐴 ∈ ℂ ∧ -𝐴 ≠ 0) → ((1 / (1 /
-𝐴)) ∈
ℝ+ ↔ -𝐴 ∈
ℝ+)) |
37 | 34, 36 | syl5ib 236 |
. . . . . . . . . 10
⊢ ((-𝐴 ∈ ℂ ∧ -𝐴 ≠ 0) → ((1 / -𝐴) ∈ ℝ+
→ -𝐴 ∈
ℝ+)) |
38 | 30, 33, 37 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((1 / -𝐴) ∈ ℝ+
→ -𝐴 ∈
ℝ+)) |
39 | 28, 38 | syld 47 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((ℑ‘(log‘(1 / 𝐴))) = π → -𝐴 ∈
ℝ+)) |
40 | | lognegb 24735 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-𝐴 ∈ ℝ+
↔ (ℑ‘(log‘𝐴)) = π)) |
41 | 39, 40 | sylibd 231 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((ℑ‘(log‘(1 / 𝐴))) = π →
(ℑ‘(log‘𝐴)) = π)) |
42 | 41 | con3d 150 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (¬
(ℑ‘(log‘𝐴)) = π → ¬
(ℑ‘(log‘(1 / 𝐴))) = π)) |
43 | 42 | 3impia 1149 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ¬
(ℑ‘(log‘𝐴)) = π) → ¬
(ℑ‘(log‘(1 / 𝐴))) = π) |
44 | 20, 43 | syl3an3b 1528 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) → ¬
(ℑ‘(log‘(1 / 𝐴))) = π) |
45 | | logrncl 24713 |
. . . . . 6
⊢ (((1 /
𝐴) ∈ ℂ ∧ (1
/ 𝐴) ≠ 0) →
(log‘(1 / 𝐴)) ∈
ran log) |
46 | 1, 2, 45 | syl2anc 579 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘(1 /
𝐴)) ∈ ran
log) |
47 | | logreclem 24902 |
. . . . 5
⊢
(((log‘(1 / 𝐴)) ∈ ran log ∧ ¬
(ℑ‘(log‘(1 / 𝐴))) = π) → -(log‘(1 / 𝐴)) ∈ ran
log) |
48 | 46, 47 | stoic3 1875 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ¬
(ℑ‘(log‘(1 / 𝐴))) = π) → -(log‘(1 / 𝐴)) ∈ ran
log) |
49 | 44, 48 | syld3an3 1532 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) → -(log‘(1 / 𝐴)) ∈ ran
log) |
50 | | logef 24727 |
. . 3
⊢
(-(log‘(1 / 𝐴)) ∈ ran log →
(log‘(exp‘-(log‘(1 / 𝐴)))) = -(log‘(1 / 𝐴))) |
51 | 49, 50 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) →
(log‘(exp‘-(log‘(1 / 𝐴)))) = -(log‘(1 / 𝐴))) |
52 | 15, 19, 51 | 3eqtr3d 2869 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧
(ℑ‘(log‘𝐴)) ≠ π) → (log‘𝐴) = -(log‘(1 / 𝐴))) |