This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → A ∈ ℝ
recxpf1.2 ⊢ φ → 0 ≤ A
recxpf1.3 ⊢ φ → B ∈ ℝ
recxpf1.4 ⊢ φ → 0 ≤ B
recxpf1.5 ⊢ φ → C ∈ ℝ +
Assertion recxpf1lem ⊢ φ → A = B ↔ A C = B C

Proof

Step Hyp Ref Expression
1 recxpf1.1 ⊢ φ → A ∈ ℝ
2 recxpf1.2 ⊢ φ → 0 ≤ A
3 recxpf1.3 ⊢ φ → B ∈ ℝ
4 recxpf1.4 ⊢ φ → 0 ≤ B
5 recxpf1.5 ⊢ φ → C ∈ ℝ +
6 1 2 3 4 5 cxple2d ⊢ φ → A ≤ B ↔ A C ≤ B C
7 3 4 1 2 5 cxple2d ⊢ φ → B ≤ A ↔ B C ≤ A C
8 6 7 anbi12d ⊢ φ → A ≤ B ∧ B ≤ A ↔ A C ≤ B C ∧ B C ≤ A C
9 1 3 letri3d ⊢ φ → A = B ↔ A ≤ B ∧ B ≤ A
10 5 rpred ⊢ φ → C ∈ ℝ
11 1 2 10 recxpcld ⊢ φ → A C ∈ ℝ
12 3 4 10 recxpcld ⊢ φ → B C ∈ ℝ
13 11 12 letri3d ⊢ φ → A C = B C ↔ A C ≤ B C ∧ B C ≤ A C
14 8 9 13 3bitr4d ⊢ φ → A = B ↔ A C = B C