Theorem recxpf1lem

Description: Complex exponentiation on positive real numbers is a one-to-one function. (Contributed by Thierry Arnoux, 1-Apr-2025)

	Ref	Expression
Hypotheses	recxpf1.1	|- ( ph -> A e. RR )
	recxpf1.2	|- ( ph -> 0 <_ A )
	recxpf1.3	|- ( ph -> B e. RR )
	recxpf1.4	|- ( ph -> 0 <_ B )
	recxpf1.5	|- ( ph -> C e. RR+ )
Assertion	recxpf1lem	|- ( ph -> ( A = B <-> ( A ^c C ) = ( B ^c C ) ) )

Proof

Step	Hyp	Ref	Expression
1		recxpf1.1	|- ( ph -> A e. RR )
2		recxpf1.2	|- ( ph -> 0 <_ A )
3		recxpf1.3	|- ( ph -> B e. RR )
4		recxpf1.4	|- ( ph -> 0 <_ B )
5		recxpf1.5	|- ( ph -> C e. RR+ )
6	1 2 3 4 5	cxple2d	|- ( ph -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
7	3 4 1 2 5	cxple2d	|- ( ph -> ( B <_ A <-> ( B ^c C ) <_ ( A ^c C ) ) )
8	6 7	anbi12d	|- ( ph -> ( ( A <_ B /\ B <_ A ) <-> ( ( A ^c C ) <_ ( B ^c C ) /\ ( B ^c C ) <_ ( A ^c C ) ) ) )
9	1 3	letri3d	|- ( ph -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
10	5	rpred	|- ( ph -> C e. RR )
11	1 2 10	recxpcld	|- ( ph -> ( A ^c C ) e. RR )
12	3 4 10	recxpcld	|- ( ph -> ( B ^c C ) e. RR )
13	11 12	letri3d	|- ( ph -> ( ( A ^c C ) = ( B ^c C ) <-> ( ( A ^c C ) <_ ( B ^c C ) /\ ( B ^c C ) <_ ( A ^c C ) ) ) )
14	8 9 13	3bitr4d	|- ( ph -> ( A = B <-> ( A ^c C ) = ( B ^c C ) ) )