Metamath Proof Explorer

Theorem cxp111d

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

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

Proof

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