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 ) ) ) ) )