This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 log 2 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 log 2 9 = 2 1 2 log 2 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 ∈ ℝ + → log 2 9 ∈ ℝ
15 10 13 14 mp2an ⊢ log 2 9 ∈ ℝ
16 cxpcom ⊢ 2 ∈ ℝ + ∧ 1 2 ∈ ℝ ∧ log 2 9 ∈ ℝ → 2 1 2 log 2 9 = 2 log 2 9 1 2
17 6 7 15 16 mp3an ⊢ 2 1 2 log 2 9 = 2 log 2 9 1 2
18 15 recni ⊢ log 2 9 ∈ ℂ
19 cxpcl ⊢ 2 ∈ ℂ ∧ log 2 9 ∈ ℂ → 2 log 2 9 ∈ ℂ
20 1 18 19 mp2an ⊢ 2 log 2 9 ∈ ℂ
21 cxpsqrt ⊢ 2 log 2 9 ∈ ℂ → 2 log 2 9 1 2 = 2 log 2 9
22 20 21 ax-mp ⊢ 2 log 2 9 1 2 = 2 log 2 9
23 5 17 22 3eqtri ⊢ 2 log 2 9 = 2 log 2 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 log 2 9 = 9
36 28 34 35 mp2an ⊢ 2 log 2 9 = 9
37 36 fveq2i ⊢ 2 log 2 9 = 9
38 sqrt9 ⊢ 9 = 3
39 23 37 38 3eqtri ⊢ 2 log 2 9 = 3