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}}^{{\log }_{2}9}=3$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2		cxpsqrt	$$⊢2\in ℂ\to 2^{\frac{1}{2}}=\sqrt{2}$$
3	1 2	ax-mp	$$⊢2^{\frac{1}{2}}=\sqrt{2}$$
4	3	eqcomi	$$⊢\sqrt{2}=2^{\frac{1}{2}}$$
5	4	oveq1i	$$⊢{\sqrt{2}}^{{\log }_{2}9}={\left(2^{\frac{1}{2}}\right)}^{{\log }_{2}9}$$
6		2rp	$$⊢2\in {ℝ}^{+}$$
7		halfre	$$⊢\frac{1}{2}\in ℝ$$
8		2z	$$⊢2\in \mathbb{Z}$$
9		uzid	$$⊢2\in \mathbb{Z}\to 2\in {\mathbb{Z}}_{\ge 2}$$
10	8 9	ax-mp	$$⊢2\in {\mathbb{Z}}_{\ge 2}$$
11		9nn	$$⊢9\in \mathbb{N}$$
12		nnrp	$$⊢9\in \mathbb{N}\to 9\in {ℝ}^{+}$$
13	11 12	ax-mp	$$⊢9\in {ℝ}^{+}$$
14		relogbzcl	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge 9\in {ℝ}^{+}\right)\to {\log }_{2}9\in ℝ$$
15	10 13 14	mp2an	$$⊢{\log }_{2}9\in ℝ$$
16		cxpcom	$$⊢\left(2\in {ℝ}^{+}\wedge \frac{1}{2}\in ℝ\wedge {\log }_{2}9\in ℝ\right)\to {\left(2^{\frac{1}{2}}\right)}^{{\log }_{2}9}={\left(2^{{\log }_{2}9}\right)}^{\frac{1}{2}}$$
17	6 7 15 16	mp3an	$$⊢{\left(2^{\frac{1}{2}}\right)}^{{\log }_{2}9}={\left(2^{{\log }_{2}9}\right)}^{\frac{1}{2}}$$
18	15	recni	$$⊢{\log }_{2}9\in ℂ$$
19		cxpcl	$$⊢\left(2\in ℂ\wedge {\log }_{2}9\in ℂ\right)\to 2^{{\log }_{2}9}\in ℂ$$
20	1 18 19	mp2an	$$⊢2^{{\log }_{2}9}\in ℂ$$
21		cxpsqrt	$$⊢2^{{\log }_{2}9}\in ℂ\to {\left(2^{{\log }_{2}9}\right)}^{\frac{1}{2}}=\sqrt{2^{{\log }_{2}9}}$$
22	20 21	ax-mp	$$⊢{\left(2^{{\log }_{2}9}\right)}^{\frac{1}{2}}=\sqrt{2^{{\log }_{2}9}}$$
23	5 17 22	3eqtri	$$⊢{\sqrt{2}}^{{\log }_{2}9}=\sqrt{2^{{\log }_{2}9}}$$
24		2ne0	$$⊢2\ne 0$$
25		1ne2	$$⊢1\ne 2$$
26	25	necomi	$$⊢2\ne 1$$
27		eldifpr	$$⊢2\in \left(ℂ\setminus \left\{0,1\right\}\right)\leftrightarrow \left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)$$
28	1 24 26 27	mpbir3an	$$⊢2\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
29		9cn	$$⊢9\in ℂ$$
30		9re	$$⊢9\in ℝ$$
31		9pos	$$⊢0<9$$
32	30 31	gt0ne0ii	$$⊢9\ne 0$$
33		eldifsn	$$⊢9\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(9\in ℂ\wedge 9\ne 0\right)$$
34	29 32 33	mpbir2an	$$⊢9\in \left(ℂ\setminus \left\{0\right\}\right)$$
35		cxplogb	$$⊢\left(2\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge 9\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to 2^{{\log }_{2}9}=9$$
36	28 34 35	mp2an	$$⊢2^{{\log }_{2}9}=9$$
37	36	fveq2i	$$⊢\sqrt{2^{{\log }_{2}9}}=\sqrt{9}$$
38		sqrt9	$$⊢\sqrt{9}=3$$
39	23 37 38	3eqtri	$$⊢{\sqrt{2}}^{{\log }_{2}9}=3$$