Metamath Proof Explorer

Theorem eflogeq

Description: Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion eflogeq ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( exp ‘ 𝐴 ) = 𝐵 ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 efcl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ )
2 efne0 ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ≠ 0 )
3 1 2 logcld ⊢ ( 𝐴 ∈ ℂ → ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ )
4 efsub ⊢ ( ( 𝐴 ∈ ℂ ∧ ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ ) → ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) ) )
5 3 4 mpdan ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) ) )
6 eflog ⊢ ( ( ( exp ‘ 𝐴 ) ∈ ℂ ∧ ( exp ‘ 𝐴 ) ≠ 0 ) → ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) = ( exp ‘ 𝐴 ) )
7 1 2 6 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) = ( exp ‘ 𝐴 ) )
8 7 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) / ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐴 ) ) )
9 1 2 dividd ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐴 ) ) = 1 )
10 5 8 9 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 1 )
11 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ ) → ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ∈ ℂ )
12 3 11 mpdan ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ∈ ℂ )
13 efeq1 ⊢ ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ∈ ℂ → ( ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 1 ↔ ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
14 12 13 syl ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 1 ↔ ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
15 10 14 mpbid ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ )
16 ax-icn ⊢ i ∈ ℂ
17 2cn ⊢ 2 ∈ ℂ
18 picn ⊢ π ∈ ℂ
19 17 18 mulcli ⊢ ( 2 · π ) ∈ ℂ
20 16 19 mulcli ⊢ ( i · ( 2 · π ) ) ∈ ℂ
21 20 a1i ⊢ ( 𝐴 ∈ ℂ → ( i · ( 2 · π ) ) ∈ ℂ )
22 ine0 ⊢ i ≠ 0
23 2ne0 ⊢ 2 ≠ 0
24 pire ⊢ π ∈ ℝ
25 pipos ⊢ 0 < π
26 24 25 gt0ne0ii ⊢ π ≠ 0
27 17 18 23 26 mulne0i ⊢ ( 2 · π ) ≠ 0
28 16 19 22 27 mulne0i ⊢ ( i · ( 2 · π ) ) ≠ 0
29 28 a1i ⊢ ( 𝐴 ∈ ℂ → ( i · ( 2 · π ) ) ≠ 0 )
30 12 21 29 divcan2d ⊢ ( 𝐴 ∈ ℂ → ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) = ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) )
31 30 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) )
32 pncan3 ⊢ ( ( ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 𝐴 )
33 3 32 mpancom ⊢ ( 𝐴 ∈ ℂ → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 𝐴 )
34 31 33 eqtr2d ⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) )
35 oveq2 ⊢ ( 𝑛 = ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) → ( ( i · ( 2 · π ) ) · 𝑛 ) = ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) )
36 35 oveq2d ⊢ ( 𝑛 = ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) )
37 36 rspceeqv ⊢ ( ( ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ∧ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) ) → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) )
38 15 34 37 syl2anc ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) )
39 38 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) )
40 fveq2 ⊢ ( ( exp ‘ 𝐴 ) = 𝐵 → ( log ‘ ( exp ‘ 𝐴 ) ) = ( log ‘ 𝐵 ) )
41 40 oveq1d ⊢ ( ( exp ‘ 𝐴 ) = 𝐵 → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) )
42 41 eqeq2d ⊢ ( ( exp ‘ 𝐴 ) = 𝐵 → ( 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
43 42 rexbidv ⊢ ( ( exp ‘ 𝐴 ) = 𝐵 → ( ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
44 39 43 syl5ibcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( exp ‘ 𝐴 ) = 𝐵 → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
45 logcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
46 45 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
47 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
48 47 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℂ )
49 mulcl ⊢ ( ( ( i · ( 2 · π ) ) ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ )
50 20 48 49 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ )
51 efadd ⊢ ( ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = ( ( exp ‘ ( log ‘ 𝐵 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
52 46 50 51 syl2an2r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = ( ( exp ‘ ( log ‘ 𝐵 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
53 eflog ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
54 53 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
55 ef2kpi ⊢ ( 𝑛 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) = 1 )
56 54 55 oveqan12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( ( exp ‘ ( log ‘ 𝐵 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = ( 𝐵 · 1 ) )
57 simpl2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → 𝐵 ∈ ℂ )
58 57 mulid1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( 𝐵 · 1 ) = 𝐵 )
59 52 56 58 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = 𝐵 )
60 fveqeq2 ⊢ ( 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) → ( ( exp ‘ 𝐴 ) = 𝐵 ↔ ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = 𝐵 ) )
61 59 60 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) → ( exp ‘ 𝐴 ) = 𝐵 ) )
62 61 rexlimdva ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) → ( exp ‘ 𝐴 ) = 𝐵 ) )
63 44 62 impbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( exp ‘ 𝐴 ) = 𝐵 ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )