Metamath Proof Explorer

Theorem lamberte

Description: A value of Lambert W (product logarithm) function at _e . (Contributed by Ender Ting, 13-Nov-2025)

Ref Expression
Hypothesis lamberte.1 
|- R = `' ( x e. CC |-> ( x x. ( exp ` x ) ) )
Assertion lamberte 
|- _e R 1

Proof

Step Hyp Ref Expression
1 lamberte.1 
 |-  R = `' ( x e. CC |-> ( x x. ( exp ` x ) ) )
2 1ex 
 |-  1 e. _V
3 epr 
 |-  _e e. RR+
4 3 elexi 
 |-  _e e. _V
5 eqcom 
 |-  ( x = 1 <-> 1 = x )
6 5 biimpi 
 |-  ( x = 1 -> 1 = x )
7 ax-1cn 
 |-  1 e. CC
8 6 7 eqeltrrdi 
 |-  ( x = 1 -> x e. CC )
9 8 adantr 
 |-  ( ( x = 1 /\ y = _e ) -> x e. CC )
10 simpr 
 |-  ( ( x = 1 /\ y = _e ) -> y = _e )
11 df-e 
 |-  _e = ( exp ` 1 )
12 rpssre 
 |-  RR+ C_ RR
13 ax-resscn 
 |-  RR C_ CC
14 12 13 sstri 
 |-  RR+ C_ CC
15 14 3 sselii 
 |-  _e e. CC
16 11 15 eqeltrri 
 |-  ( exp ` 1 ) e. CC
17 16 mullidi 
 |-  ( 1 x. ( exp ` 1 ) ) = ( exp ` 1 )
18 17 11 eqtr4i 
 |-  ( 1 x. ( exp ` 1 ) ) = _e
19 6 fveq2d 
 |-  ( x = 1 -> ( exp ` 1 ) = ( exp ` x ) )
20 6 19 oveq12d 
 |-  ( x = 1 -> ( 1 x. ( exp ` 1 ) ) = ( x x. ( exp ` x ) ) )
21 18 20 eqtr3id 
 |-  ( x = 1 -> _e = ( x x. ( exp ` x ) ) )
22 21 adantr 
 |-  ( ( x = 1 /\ y = _e ) -> _e = ( x x. ( exp ` x ) ) )
23 10 22 eqtrd 
 |-  ( ( x = 1 /\ y = _e ) -> y = ( x x. ( exp ` x ) ) )
24 9 23 jca 
 |-  ( ( x = 1 /\ y = _e ) -> ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) )
25 tbtru 
 |-  ( ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) <-> ( ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) <-> T. ) )
26 24 25 sylib 
 |-  ( ( x = 1 /\ y = _e ) -> ( ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) <-> T. ) )
27 eqid 
 |-  { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } = { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) }
28 2 4 26 27 braba 
 |-  ( 1 { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } _e <-> T. )
29 tbtru 
 |-  ( 1 { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } _e <-> ( 1 { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } _e <-> T. ) )
30 28 29 mpbir 
 |-  1 { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } _e
31 df-mpt 
 |-  ( x e. CC |-> ( x x. ( exp ` x ) ) ) = { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) }
32 31 breqi 
 |-  ( 1 ( x e. CC |-> ( x x. ( exp ` x ) ) ) _e <-> 1 { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } _e )
33 30 32 mpbir 
 |-  1 ( x e. CC |-> ( x x. ( exp ` x ) ) ) _e
34 4 2 brcnv 
 |-  ( _e `' ( x e. CC |-> ( x x. ( exp ` x ) ) ) 1 <-> 1 ( x e. CC |-> ( x x. ( exp ` x ) ) ) _e )
35 33 34 mpbir 
 |-  _e `' ( x e. CC |-> ( x x. ( exp ` x ) ) ) 1
36 1 breqi 
 |-  ( _e R 1 <-> _e `' ( x e. CC |-> ( x x. ( exp ` x ) ) ) 1 )
37 35 36 mpbir 
 |-  _e R 1