Metamath Proof Explorer


Theorem cxp112d

Description: General condition for complex exponentiation to be one-to-one with respect to the second argument. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses cxp112d.c
|- ( ph -> C e. CC )
cxp112d.a
|- ( ph -> A e. CC )
cxp112d.b
|- ( ph -> B e. CC )
cxp112d.0
|- ( ph -> C =/= 0 )
cxp112d.1
|- ( ph -> C =/= 1 )
Assertion cxp112d
|- ( ph -> ( ( C ^c A ) = ( C ^c B ) <-> E. n e. ZZ A = ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` C ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cxp112d.c
 |-  ( ph -> C e. CC )
2 cxp112d.a
 |-  ( ph -> A e. CC )
3 cxp112d.b
 |-  ( ph -> B e. CC )
4 cxp112d.0
 |-  ( ph -> C =/= 0 )
5 cxp112d.1
 |-  ( ph -> C =/= 1 )
6 1 4 2 cxpefd
 |-  ( ph -> ( C ^c A ) = ( exp ` ( A x. ( log ` C ) ) ) )
7 1 4 3 cxpefd
 |-  ( ph -> ( C ^c B ) = ( exp ` ( B x. ( log ` C ) ) ) )
8 6 7 eqeq12d
 |-  ( ph -> ( ( C ^c A ) = ( C ^c B ) <-> ( exp ` ( A x. ( log ` C ) ) ) = ( exp ` ( B x. ( log ` C ) ) ) ) )
9 1 4 logcld
 |-  ( ph -> ( log ` C ) e. CC )
10 2 9 mulcld
 |-  ( ph -> ( A x. ( log ` C ) ) e. CC )
11 3 9 mulcld
 |-  ( ph -> ( B x. ( log ` C ) ) e. CC )
12 10 11 ef11d
 |-  ( ph -> ( ( exp ` ( A x. ( log ` C ) ) ) = ( exp ` ( B x. ( log ` C ) ) ) <-> E. n e. ZZ ( A x. ( log ` C ) ) = ( ( B x. ( log ` C ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )
13 2 adantr
 |-  ( ( ph /\ n e. ZZ ) -> A e. CC )
14 9 adantr
 |-  ( ( ph /\ n e. ZZ ) -> ( log ` C ) e. CC )
15 11 adantr
 |-  ( ( ph /\ n e. ZZ ) -> ( B x. ( log ` C ) ) e. CC )
16 ax-icn
 |-  _i e. CC
17 2cn
 |-  2 e. CC
18 picn
 |-  _pi e. CC
19 17 18 mulcli
 |-  ( 2 x. _pi ) e. CC
20 16 19 mulcli
 |-  ( _i x. ( 2 x. _pi ) ) e. CC
21 20 a1i
 |-  ( ( ph /\ n e. ZZ ) -> ( _i x. ( 2 x. _pi ) ) e. CC )
22 zcn
 |-  ( n e. ZZ -> n e. CC )
23 22 adantl
 |-  ( ( ph /\ n e. ZZ ) -> n e. CC )
24 21 23 mulcld
 |-  ( ( ph /\ n e. ZZ ) -> ( ( _i x. ( 2 x. _pi ) ) x. n ) e. CC )
25 15 24 addcld
 |-  ( ( ph /\ n e. ZZ ) -> ( ( B x. ( log ` C ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) e. CC )
26 1 4 5 logccne0d
 |-  ( ph -> ( log ` C ) =/= 0 )
27 26 adantr
 |-  ( ( ph /\ n e. ZZ ) -> ( log ` C ) =/= 0 )
28 13 14 25 27 ldiv
 |-  ( ( ph /\ n e. ZZ ) -> ( ( A x. ( log ` C ) ) = ( ( B x. ( log ` C ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> A = ( ( ( B x. ( log ` C ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) / ( log ` C ) ) ) )
29 15 24 14 27 divdird
 |-  ( ( ph /\ n e. ZZ ) -> ( ( ( B x. ( log ` C ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) / ( log ` C ) ) = ( ( ( B x. ( log ` C ) ) / ( log ` C ) ) + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` C ) ) ) )
30 3 9 26 divcan4d
 |-  ( ph -> ( ( B x. ( log ` C ) ) / ( log ` C ) ) = B )
31 30 adantr
 |-  ( ( ph /\ n e. ZZ ) -> ( ( B x. ( log ` C ) ) / ( log ` C ) ) = B )
32 31 oveq1d
 |-  ( ( ph /\ n e. ZZ ) -> ( ( ( B x. ( log ` C ) ) / ( log ` C ) ) + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` C ) ) ) = ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` C ) ) ) )
33 29 32 eqtrd
 |-  ( ( ph /\ n e. ZZ ) -> ( ( ( B x. ( log ` C ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) / ( log ` C ) ) = ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` C ) ) ) )
34 33 eqeq2d
 |-  ( ( ph /\ n e. ZZ ) -> ( A = ( ( ( B x. ( log ` C ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) / ( log ` C ) ) <-> A = ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` C ) ) ) ) )
35 28 34 bitrd
 |-  ( ( ph /\ n e. ZZ ) -> ( ( A x. ( log ` C ) ) = ( ( B x. ( log ` C ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> A = ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` C ) ) ) ) )
36 35 rexbidva
 |-  ( ph -> ( E. n e. ZZ ( A x. ( log ` C ) ) = ( ( B x. ( log ` C ) ) + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> E. n e. ZZ A = ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` C ) ) ) ) )
37 8 12 36 3bitrd
 |-  ( ph -> ( ( C ^c A ) = ( C ^c B ) <-> E. n e. ZZ A = ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` C ) ) ) ) )