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 ( ( √ ‘ 2 ) ↑𝑐 ( 2 logb 9 ) ) = 3

Proof

Step Hyp Ref Expression
1 2cn ⊢ 2 ∈ ℂ
2 cxpsqrt ⊢ ( 2 ∈ ℂ → ( 2 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 2 ) )
3 1 2 ax-mp ⊢ ( 2 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 2 )
4 3 eqcomi ⊢ ( √ ‘ 2 ) = ( 2 ↑𝑐 ( 1 / 2 ) )
5 4 oveq1i ⊢ ( ( √ ‘ 2 ) ↑𝑐 ( 2 logb 9 ) ) = ( ( 2 ↑𝑐 ( 1 / 2 ) ) ↑𝑐 ( 2 logb 9 ) )
6 2rp ⊢ 2 ∈ ℝ+
7 halfre ⊢ ( 1 / 2 ) ∈ ℝ
8 2z ⊢ 2 ∈ ℤ
9 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
10 8 9 ax-mp ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
11 9nn ⊢ 9 ∈ ℕ
12 nnrp ⊢ ( 9 ∈ ℕ → 9 ∈ ℝ+ )
13 11 12 ax-mp ⊢ 9 ∈ ℝ+
14 relogbzcl ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 9 ∈ ℝ+ ) → ( 2 logb 9 ) ∈ ℝ )
15 10 13 14 mp2an ⊢ ( 2 logb 9 ) ∈ ℝ
16 cxpcom ⊢ ( ( 2 ∈ ℝ+ ∧ ( 1 / 2 ) ∈ ℝ ∧ ( 2 logb 9 ) ∈ ℝ ) → ( ( 2 ↑𝑐 ( 1 / 2 ) ) ↑𝑐 ( 2 logb 9 ) ) = ( ( 2 ↑𝑐 ( 2 logb 9 ) ) ↑𝑐 ( 1 / 2 ) ) )
17 6 7 15 16 mp3an ⊢ ( ( 2 ↑𝑐 ( 1 / 2 ) ) ↑𝑐 ( 2 logb 9 ) ) = ( ( 2 ↑𝑐 ( 2 logb 9 ) ) ↑𝑐 ( 1 / 2 ) )
18 15 recni ⊢ ( 2 logb 9 ) ∈ ℂ
19 cxpcl ⊢ ( ( 2 ∈ ℂ ∧ ( 2 logb 9 ) ∈ ℂ ) → ( 2 ↑𝑐 ( 2 logb 9 ) ) ∈ ℂ )
20 1 18 19 mp2an ⊢ ( 2 ↑𝑐 ( 2 logb 9 ) ) ∈ ℂ
21 cxpsqrt ⊢ ( ( 2 ↑𝑐 ( 2 logb 9 ) ) ∈ ℂ → ( ( 2 ↑𝑐 ( 2 logb 9 ) ) ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ ( 2 ↑𝑐 ( 2 logb 9 ) ) ) )
22 20 21 ax-mp ⊢ ( ( 2 ↑𝑐 ( 2 logb 9 ) ) ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ ( 2 ↑𝑐 ( 2 logb 9 ) ) )
23 5 17 22 3eqtri ⊢ ( ( √ ‘ 2 ) ↑𝑐 ( 2 logb 9 ) ) = ( √ ‘ ( 2 ↑𝑐 ( 2 logb 9 ) ) )
24 2ne0 ⊢ 2 ≠ 0
25 1ne2 ⊢ 1 ≠ 2
26 25 necomi ⊢ 2 ≠ 1
27 eldifpr ⊢ ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) )
28 1 24 26 27 mpbir3an ⊢ 2 ∈ ( ℂ ∖ { 0 , 1 } )
29 9cn ⊢ 9 ∈ ℂ
30 9re ⊢ 9 ∈ ℝ
31 9pos ⊢ 0 < 9
32 30 31 gt0ne0ii ⊢ 9 ≠ 0
33 eldifsn ⊢ ( 9 ∈ ( ℂ ∖ { 0 } ) ↔ ( 9 ∈ ℂ ∧ 9 ≠ 0 ) )
34 29 32 33 mpbir2an ⊢ 9 ∈ ( ℂ ∖ { 0 } )
35 cxplogb ⊢ ( ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 9 ∈ ( ℂ ∖ { 0 } ) ) → ( 2 ↑𝑐 ( 2 logb 9 ) ) = 9 )
36 28 34 35 mp2an ⊢ ( 2 ↑𝑐 ( 2 logb 9 ) ) = 9
37 36 fveq2i ⊢ ( √ ‘ ( 2 ↑𝑐 ( 2 logb 9 ) ) ) = ( √ ‘ 9 )
38 sqrt9 ⊢ ( √ ‘ 9 ) = 3
39 23 37 38 3eqtri ⊢ ( ( √ ‘ 2 ) ↑𝑐 ( 2 logb 9 ) ) = 3