Theorem 2irrexpq

Description: There exist irrational numbers a and b such that ( a ^c b ) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "classical proof" for theorem 1.2 of Bauer, p. 483. This proof is not acceptable in intuitionistic logic, since it is based on the law of excluded middle: Either ( ( sqrt2 ) ^c ( sqrt2 ) ) is rational, in which case ( sqrt2 ) , being irrational (see sqrt2irr ), can be chosen for both a and b , or ( ( sqrt2 ) ^c ( sqrt2 ) ) is irrational, in which case ( ( sqrt2 ) ^c ( sqrt2 ) ) can be chosen for a and ( sqrt2 ) for b , since ( ( ( sqrt2 ) ^c ( sqrt2 ) ) ^c ( sqrt2 ) ) = 2 is rational. For an alternate proof, which can be used in intuitionistic logic, see 2irrexpqALT . (Contributed by AV, 23-Dec-2022)

	Ref	Expression
Assertion	2irrexpq	$$⊢\exists a\in \left(ℝ\setminus \mathbb{Q}\right)\exists b\in \left(ℝ\setminus \mathbb{Q}\right)a^b\in \mathbb{Q}$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢a=\sqrt{2}\to a^b={\sqrt{2}}^b$$
2	1	eleq1d	$$⊢a=\sqrt{2}\to \left(a^b\in \mathbb{Q}\leftrightarrow {\sqrt{2}}^b\in \mathbb{Q}\right)$$
3		oveq2	$$⊢b=\sqrt{2}\to {\sqrt{2}}^b={\sqrt{2}}^{\sqrt{2}}$$
4	3	eleq1d	$$⊢b=\sqrt{2}\to \left({\sqrt{2}}^b\in \mathbb{Q}\leftrightarrow {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\right)$$
5	2 4	rspc2ev	$$⊢\left(\sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\right)\to \exists a\in \left(ℝ\setminus \mathbb{Q}\right)\exists b\in \left(ℝ\setminus \mathbb{Q}\right)a^b\in \mathbb{Q}$$
6		3ianor	$$⊢\neg \left(\sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\right)\leftrightarrow \left(\neg \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\vee \neg \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\vee \neg {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\right)$$
7		sqrt2irr0	$$⊢\sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)$$
8	7	pm2.24i	$$⊢\neg \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\to \left({\sqrt{2}}^{\sqrt{2}}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge {\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}\in \mathbb{Q}\right)$$
9		2rp	$$⊢2\in {ℝ}^{+}$$
10		rpsqrtcl	$$⊢2\in {ℝ}^{+}\to \sqrt{2}\in {ℝ}^{+}$$
11	9 10	ax-mp	$$⊢\sqrt{2}\in {ℝ}^{+}$$
12		rpre	$$⊢\sqrt{2}\in {ℝ}^{+}\to \sqrt{2}\in ℝ$$
13		rpge0	$$⊢\sqrt{2}\in {ℝ}^{+}\to 0\le \sqrt{2}$$
14	12 13 12	recxpcld	$$⊢\sqrt{2}\in {ℝ}^{+}\to {\sqrt{2}}^{\sqrt{2}}\in ℝ$$
15	11 14	ax-mp	$$⊢{\sqrt{2}}^{\sqrt{2}}\in ℝ$$
16	15	a1i	$$⊢\neg {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\to {\sqrt{2}}^{\sqrt{2}}\in ℝ$$
17		id	$$⊢\neg {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\to \neg {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}$$
18	16 17	eldifd	$$⊢\neg {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\to {\sqrt{2}}^{\sqrt{2}}\in \left(ℝ\setminus \mathbb{Q}\right)$$
19	7	a1i	$$⊢\neg {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\to \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)$$
20		sqrt2re	$$⊢\sqrt{2}\in ℝ$$
21	20	recni	$$⊢\sqrt{2}\in ℂ$$
22		cxpmul	$$⊢\left(\sqrt{2}\in {ℝ}^{+}\wedge \sqrt{2}\in ℝ\wedge \sqrt{2}\in ℂ\right)\to {\sqrt{2}}^{\sqrt{2}\sqrt{2}}={\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}$$
23	11 20 21 22	mp3an	$$⊢{\sqrt{2}}^{\sqrt{2}\sqrt{2}}={\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}$$
24		2re	$$⊢2\in ℝ$$
25		0le2	$$⊢0\le 2$$
26		remsqsqrt	$$⊢\left(2\in ℝ\wedge 0\le 2\right)\to \sqrt{2}\sqrt{2}=2$$
27	24 25 26	mp2an	$$⊢\sqrt{2}\sqrt{2}=2$$
28	27	oveq2i	$$⊢{\sqrt{2}}^{\sqrt{2}\sqrt{2}}={\sqrt{2}}^2$$
29		2cn	$$⊢2\in ℂ$$
30		cxpsqrtth	$$⊢2\in ℂ\to {\sqrt{2}}^2=2$$
31	29 30	ax-mp	$$⊢{\sqrt{2}}^2=2$$
32		2z	$$⊢2\in \mathbb{Z}$$
33		zq	$$⊢2\in \mathbb{Z}\to 2\in \mathbb{Q}$$
34	32 33	ax-mp	$$⊢2\in \mathbb{Q}$$
35	31 34	eqeltri	$$⊢{\sqrt{2}}^2\in \mathbb{Q}$$
36	28 35	eqeltri	$$⊢{\sqrt{2}}^{\sqrt{2}\sqrt{2}}\in \mathbb{Q}$$
37	23 36	eqeltrri	$$⊢{\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}\in \mathbb{Q}$$
38	37	a1i	$$⊢\neg {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\to {\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}\in \mathbb{Q}$$
39	18 19 38	3jca	$$⊢\neg {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\to \left({\sqrt{2}}^{\sqrt{2}}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge {\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}\in \mathbb{Q}\right)$$
40	8 8 39	3jaoi	$$⊢\left(\neg \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\vee \neg \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\vee \neg {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\right)\to \left({\sqrt{2}}^{\sqrt{2}}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge {\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}\in \mathbb{Q}\right)$$
41	6 40	sylbi	$$⊢\neg \left(\sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\right)\to \left({\sqrt{2}}^{\sqrt{2}}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge {\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}\in \mathbb{Q}\right)$$
42		oveq1	$$⊢a={\sqrt{2}}^{\sqrt{2}}\to a^b={\left({\sqrt{2}}^{\sqrt{2}}\right)}^b$$
43	42	eleq1d	$$⊢a={\sqrt{2}}^{\sqrt{2}}\to \left(a^b\in \mathbb{Q}\leftrightarrow {\left({\sqrt{2}}^{\sqrt{2}}\right)}^b\in \mathbb{Q}\right)$$
44		oveq2	$$⊢b=\sqrt{2}\to {\left({\sqrt{2}}^{\sqrt{2}}\right)}^b={\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}$$
45	44	eleq1d	$$⊢b=\sqrt{2}\to \left({\left({\sqrt{2}}^{\sqrt{2}}\right)}^b\in \mathbb{Q}\leftrightarrow {\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}\in \mathbb{Q}\right)$$
46	43 45	rspc2ev	$$⊢\left({\sqrt{2}}^{\sqrt{2}}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge {\left({\sqrt{2}}^{\sqrt{2}}\right)}^{\sqrt{2}}\in \mathbb{Q}\right)\to \exists a\in \left(ℝ\setminus \mathbb{Q}\right)\exists b\in \left(ℝ\setminus \mathbb{Q}\right)a^b\in \mathbb{Q}$$
47	41 46	syl	$$⊢\neg \left(\sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge \sqrt{2}\in \left(ℝ\setminus \mathbb{Q}\right)\wedge {\sqrt{2}}^{\sqrt{2}}\in \mathbb{Q}\right)\to \exists a\in \left(ℝ\setminus \mathbb{Q}\right)\exists b\in \left(ℝ\setminus \mathbb{Q}\right)a^b\in \mathbb{Q}$$
48	5 47	pm2.61i	$$⊢\exists a\in \left(ℝ\setminus \mathbb{Q}\right)\exists b\in \left(ℝ\setminus \mathbb{Q}\right)a^b\in \mathbb{Q}$$