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