Metamath Proof Explorer

Theorem lambert0

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

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

Proof

Step Hyp Ref Expression
1 lambert0.1 
 |-  R = `' ( x e. CC |-> ( x x. ( exp ` x ) ) )
2 c0ex 
 |-  0 e. _V
3 eqcom 
 |-  ( x = 0 <-> 0 = x )
4 3 biimpi 
 |-  ( x = 0 -> 0 = x )
5 0cnd 
 |-  ( x = 0 -> 0 e. CC )
6 4 5 eqeltrrd 
 |-  ( x = 0 -> x e. CC )
7 6 adantr 
 |-  ( ( x = 0 /\ y = 0 ) -> x e. CC )
8 simpr 
 |-  ( ( x = 0 /\ y = 0 ) -> y = 0 )
9 ef0 
 |-  ( exp ` 0 ) = 1
10 ax-1cn 
 |-  1 e. CC
11 9 10 eqeltri 
 |-  ( exp ` 0 ) e. CC
12 11 mul02i 
 |-  ( 0 x. ( exp ` 0 ) ) = 0
13 4 fveq2d 
 |-  ( x = 0 -> ( exp ` 0 ) = ( exp ` x ) )
14 4 13 oveq12d 
 |-  ( x = 0 -> ( 0 x. ( exp ` 0 ) ) = ( x x. ( exp ` x ) ) )
15 12 14 eqtr3id 
 |-  ( x = 0 -> 0 = ( x x. ( exp ` x ) ) )
16 15 adantr 
 |-  ( ( x = 0 /\ y = 0 ) -> 0 = ( x x. ( exp ` x ) ) )
17 8 16 eqtrd 
 |-  ( ( x = 0 /\ y = 0 ) -> y = ( x x. ( exp ` x ) ) )
18 7 17 jca 
 |-  ( ( x = 0 /\ y = 0 ) -> ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) )
19 tbtru 
 |-  ( ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) <-> ( ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) <-> T. ) )
20 18 19 sylib 
 |-  ( ( x = 0 /\ y = 0 ) -> ( ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) <-> T. ) )
21 eqid 
 |-  { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } = { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) }
22 2 2 20 21 braba 
 |-  ( 0 { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } 0 <-> T. )
23 tbtru 
 |-  ( 0 { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } 0 <-> ( 0 { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } 0 <-> T. ) )
24 22 23 mpbir 
 |-  0 { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } 0
25 df-mpt 
 |-  ( x e. CC |-> ( x x. ( exp ` x ) ) ) = { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) }
26 25 breqi 
 |-  ( 0 ( x e. CC |-> ( x x. ( exp ` x ) ) ) 0 <-> 0 { <. x , y >. | ( x e. CC /\ y = ( x x. ( exp ` x ) ) ) } 0 )
27 24 26 mpbir 
 |-  0 ( x e. CC |-> ( x x. ( exp ` x ) ) ) 0
28 2 2 brcnv 
 |-  ( 0 `' ( x e. CC |-> ( x x. ( exp ` x ) ) ) 0 <-> 0 ( x e. CC |-> ( x x. ( exp ` x ) ) ) 0 )
29 27 28 mpbir 
 |-  0 `' ( x e. CC |-> ( x x. ( exp ` x ) ) ) 0
30 1 breqi 
 |-  ( 0 R 0 <-> 0 `' ( x e. CC |-> ( x x. ( exp ` x ) ) ) 0 )
31 29 30 mpbir 
 |-  0 R 0