Step |
Hyp |
Ref |
Expression |
1 |
|
seff.s |
⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } ) |
2 |
|
elpri |
⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) ) |
3 |
|
reeff1 |
⊢ ( exp ↾ ℝ ) : ℝ –1-1→ ℝ+ |
4 |
|
f1f |
⊢ ( ( exp ↾ ℝ ) : ℝ –1-1→ ℝ+ → ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ ) |
5 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
6 |
|
fss |
⊢ ( ( ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ ∧ ℝ+ ⊆ ℝ ) → ( exp ↾ ℝ ) : ℝ ⟶ ℝ ) |
7 |
5 6
|
mpan2 |
⊢ ( ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ → ( exp ↾ ℝ ) : ℝ ⟶ ℝ ) |
8 |
3 4 7
|
mp2b |
⊢ ( exp ↾ ℝ ) : ℝ ⟶ ℝ |
9 |
|
feq23 |
⊢ ( ( 𝑆 = ℝ ∧ 𝑆 = ℝ ) → ( ( exp ↾ ℝ ) : 𝑆 ⟶ 𝑆 ↔ ( exp ↾ ℝ ) : ℝ ⟶ ℝ ) ) |
10 |
9
|
anidms |
⊢ ( 𝑆 = ℝ → ( ( exp ↾ ℝ ) : 𝑆 ⟶ 𝑆 ↔ ( exp ↾ ℝ ) : ℝ ⟶ ℝ ) ) |
11 |
8 10
|
mpbiri |
⊢ ( 𝑆 = ℝ → ( exp ↾ ℝ ) : 𝑆 ⟶ 𝑆 ) |
12 |
|
reseq2 |
⊢ ( 𝑆 = ℝ → ( exp ↾ 𝑆 ) = ( exp ↾ ℝ ) ) |
13 |
12
|
feq1d |
⊢ ( 𝑆 = ℝ → ( ( exp ↾ 𝑆 ) : 𝑆 ⟶ 𝑆 ↔ ( exp ↾ ℝ ) : 𝑆 ⟶ 𝑆 ) ) |
14 |
11 13
|
mpbird |
⊢ ( 𝑆 = ℝ → ( exp ↾ 𝑆 ) : 𝑆 ⟶ 𝑆 ) |
15 |
|
eff |
⊢ exp : ℂ ⟶ ℂ |
16 |
|
frel |
⊢ ( exp : ℂ ⟶ ℂ → Rel exp ) |
17 |
|
resdm |
⊢ ( Rel exp → ( exp ↾ dom exp ) = exp ) |
18 |
15 16 17
|
mp2b |
⊢ ( exp ↾ dom exp ) = exp |
19 |
15
|
fdmi |
⊢ dom exp = ℂ |
20 |
19
|
reseq2i |
⊢ ( exp ↾ dom exp ) = ( exp ↾ ℂ ) |
21 |
18 20
|
eqtr3i |
⊢ exp = ( exp ↾ ℂ ) |
22 |
21
|
feq1i |
⊢ ( exp : ℂ ⟶ ℂ ↔ ( exp ↾ ℂ ) : ℂ ⟶ ℂ ) |
23 |
15 22
|
mpbi |
⊢ ( exp ↾ ℂ ) : ℂ ⟶ ℂ |
24 |
|
feq23 |
⊢ ( ( 𝑆 = ℂ ∧ 𝑆 = ℂ ) → ( ( exp ↾ ℂ ) : 𝑆 ⟶ 𝑆 ↔ ( exp ↾ ℂ ) : ℂ ⟶ ℂ ) ) |
25 |
24
|
anidms |
⊢ ( 𝑆 = ℂ → ( ( exp ↾ ℂ ) : 𝑆 ⟶ 𝑆 ↔ ( exp ↾ ℂ ) : ℂ ⟶ ℂ ) ) |
26 |
23 25
|
mpbiri |
⊢ ( 𝑆 = ℂ → ( exp ↾ ℂ ) : 𝑆 ⟶ 𝑆 ) |
27 |
|
reseq2 |
⊢ ( 𝑆 = ℂ → ( exp ↾ 𝑆 ) = ( exp ↾ ℂ ) ) |
28 |
27
|
feq1d |
⊢ ( 𝑆 = ℂ → ( ( exp ↾ 𝑆 ) : 𝑆 ⟶ 𝑆 ↔ ( exp ↾ ℂ ) : 𝑆 ⟶ 𝑆 ) ) |
29 |
26 28
|
mpbird |
⊢ ( 𝑆 = ℂ → ( exp ↾ 𝑆 ) : 𝑆 ⟶ 𝑆 ) |
30 |
14 29
|
jaoi |
⊢ ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → ( exp ↾ 𝑆 ) : 𝑆 ⟶ 𝑆 ) |
31 |
1 2 30
|
3syl |
⊢ ( 𝜑 → ( exp ↾ 𝑆 ) : 𝑆 ⟶ 𝑆 ) |