Metamath Proof Explorer

Theorem sqrt2cxp2logb9e3

Description: The square root of two to the power of the logarithm of nine to base two is three. ( sqrt2 ) and ( 2 logb 9 ) are irrational numbers (see sqrt2irr0 resp. 2logb9irr ), satisfying the statement in 2irrexpqALT . (Contributed by AV, 29-Dec-2022)

Ref Expression
Assertion sqrt2cxp2logb9e3 
|- ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) = 3

Proof

Step Hyp Ref Expression
1 2cn 
 |-  2 e. CC
2 cxpsqrt 
 |-  ( 2 e. CC -> ( 2 ^c ( 1 / 2 ) ) = ( sqrt ` 2 ) )
3 1 2 ax-mp 
 |-  ( 2 ^c ( 1 / 2 ) ) = ( sqrt ` 2 )
4 3 eqcomi 
 |-  ( sqrt ` 2 ) = ( 2 ^c ( 1 / 2 ) )
5 4 oveq1i 
 |-  ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) = ( ( 2 ^c ( 1 / 2 ) ) ^c ( 2 logb 9 ) )
6 2rp 
 |-  2 e. RR+
7 halfre 
 |-  ( 1 / 2 ) e. RR
8 2z 
 |-  2 e. ZZ
9 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
10 8 9 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
11 9nn 
 |-  9 e. NN
12 nnrp 
 |-  ( 9 e. NN -> 9 e. RR+ )
13 11 12 ax-mp 
 |-  9 e. RR+
14 relogbzcl 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ 9 e. RR+ ) -> ( 2 logb 9 ) e. RR )
15 10 13 14 mp2an 
 |-  ( 2 logb 9 ) e. RR
16 cxpcom 
 |-  ( ( 2 e. RR+ /\ ( 1 / 2 ) e. RR /\ ( 2 logb 9 ) e. RR ) -> ( ( 2 ^c ( 1 / 2 ) ) ^c ( 2 logb 9 ) ) = ( ( 2 ^c ( 2 logb 9 ) ) ^c ( 1 / 2 ) ) )
17 6 7 15 16 mp3an 
 |-  ( ( 2 ^c ( 1 / 2 ) ) ^c ( 2 logb 9 ) ) = ( ( 2 ^c ( 2 logb 9 ) ) ^c ( 1 / 2 ) )
18 15 recni 
 |-  ( 2 logb 9 ) e. CC
19 cxpcl 
 |-  ( ( 2 e. CC /\ ( 2 logb 9 ) e. CC ) -> ( 2 ^c ( 2 logb 9 ) ) e. CC )
20 1 18 19 mp2an 
 |-  ( 2 ^c ( 2 logb 9 ) ) e. CC
21 cxpsqrt 
 |-  ( ( 2 ^c ( 2 logb 9 ) ) e. CC -> ( ( 2 ^c ( 2 logb 9 ) ) ^c ( 1 / 2 ) ) = ( sqrt ` ( 2 ^c ( 2 logb 9 ) ) ) )
22 20 21 ax-mp 
 |-  ( ( 2 ^c ( 2 logb 9 ) ) ^c ( 1 / 2 ) ) = ( sqrt ` ( 2 ^c ( 2 logb 9 ) ) )
23 5 17 22 3eqtri 
 |-  ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) = ( sqrt ` ( 2 ^c ( 2 logb 9 ) ) )
24 2ne0 
 |-  2 =/= 0
25 1ne2 
 |-  1 =/= 2
26 25 necomi 
 |-  2 =/= 1
27 eldifpr 
 |-  ( 2 e. ( CC \ { 0 , 1 } ) <-> ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) )
28 1 24 26 27 mpbir3an 
 |-  2 e. ( CC \ { 0 , 1 } )
29 9cn 
 |-  9 e. CC
30 9re 
 |-  9 e. RR
31 9pos 
 |-  0 < 9
32 30 31 gt0ne0ii 
 |-  9 =/= 0
33 eldifsn 
 |-  ( 9 e. ( CC \ { 0 } ) <-> ( 9 e. CC /\ 9 =/= 0 ) )
34 29 32 33 mpbir2an 
 |-  9 e. ( CC \ { 0 } )
35 cxplogb 
 |-  ( ( 2 e. ( CC \ { 0 , 1 } ) /\ 9 e. ( CC \ { 0 } ) ) -> ( 2 ^c ( 2 logb 9 ) ) = 9 )
36 28 34 35 mp2an 
 |-  ( 2 ^c ( 2 logb 9 ) ) = 9
37 36 fveq2i 
 |-  ( sqrt ` ( 2 ^c ( 2 logb 9 ) ) ) = ( sqrt ` 9 )
38 sqrt9 
 |-  ( sqrt ` 9 ) = 3
39 23 37 38 3eqtri 
 |-  ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) = 3