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	⊢ ∃ 𝑎 ∈ ( ℝ ∖ ℚ ) ∃ 𝑏 ∈ ( ℝ ∖ ℚ ) ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑎 = ( √ ‘ 2 ) → ( 𝑎 ↑𝑐 𝑏 ) = ( ( √ ‘ 2 ) ↑𝑐 𝑏 ) )
2	1	eleq1d	⊢ ( 𝑎 = ( √ ‘ 2 ) → ( ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ ↔ ( ( √ ‘ 2 ) ↑𝑐 𝑏 ) ∈ ℚ ) )
3		oveq2	⊢ ( 𝑏 = ( √ ‘ 2 ) → ( ( √ ‘ 2 ) ↑𝑐 𝑏 ) = ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) )
4	3	eleq1d	⊢ ( 𝑏 = ( √ ‘ 2 ) → ( ( ( √ ‘ 2 ) ↑𝑐 𝑏 ) ∈ ℚ ↔ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) )
5	2 4	rspc2ev	⊢ ( ( ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) → ∃ 𝑎 ∈ ( ℝ ∖ ℚ ) ∃ 𝑏 ∈ ( ℝ ∖ ℚ ) ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ )
6		3ianor	⊢ ( ¬ ( ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) ↔ ( ¬ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∨ ¬ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∨ ¬ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) )
7		sqrt2irr0	⊢ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ )
8	7	pm2.24i	⊢ ( ¬ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) → ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ( ℝ ∖ ℚ ) ∧ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) )
9		2rp	⊢ 2 ∈ ℝ+
10		rpsqrtcl	⊢ ( 2 ∈ ℝ+ → ( √ ‘ 2 ) ∈ ℝ+ )
11	9 10	ax-mp	⊢ ( √ ‘ 2 ) ∈ ℝ+
12		rpre	⊢ ( ( √ ‘ 2 ) ∈ ℝ+ → ( √ ‘ 2 ) ∈ ℝ )
13		rpge0	⊢ ( ( √ ‘ 2 ) ∈ ℝ+ → 0 ≤ ( √ ‘ 2 ) )
14	12 13 12	recxpcld	⊢ ( ( √ ‘ 2 ) ∈ ℝ+ → ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℝ )
15	11 14	ax-mp	⊢ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℝ
16	15	a1i	⊢ ( ¬ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ → ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℝ )
17		id	⊢ ( ¬ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ → ¬ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ )
18	16 17	eldifd	⊢ ( ¬ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ → ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ( ℝ ∖ ℚ ) )
19	7	a1i	⊢ ( ¬ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ → ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) )
20		sqrt2re	⊢ ( √ ‘ 2 ) ∈ ℝ
21	20	recni	⊢ ( √ ‘ 2 ) ∈ ℂ
22		cxpmul	⊢ ( ( ( √ ‘ 2 ) ∈ ℝ+ ∧ ( √ ‘ 2 ) ∈ ℝ ∧ ( √ ‘ 2 ) ∈ ℂ ) → ( ( √ ‘ 2 ) ↑𝑐 ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) ) = ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) ) )
23	11 20 21 22	mp3an	⊢ ( ( √ ‘ 2 ) ↑𝑐 ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) ) = ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) )
24		2re	⊢ 2 ∈ ℝ
25		0le2	⊢ 0 ≤ 2
26		remsqsqrt	⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) = 2 )
27	24 25 26	mp2an	⊢ ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) = 2
28	27	oveq2i	⊢ ( ( √ ‘ 2 ) ↑𝑐 ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) ) = ( ( √ ‘ 2 ) ↑𝑐 2 )
29		2cn	⊢ 2 ∈ ℂ
30		cxpsqrtth	⊢ ( 2 ∈ ℂ → ( ( √ ‘ 2 ) ↑𝑐 2 ) = 2 )
31	29 30	ax-mp	⊢ ( ( √ ‘ 2 ) ↑𝑐 2 ) = 2
32		2z	⊢ 2 ∈ ℤ
33		zq	⊢ ( 2 ∈ ℤ → 2 ∈ ℚ )
34	32 33	ax-mp	⊢ 2 ∈ ℚ
35	31 34	eqeltri	⊢ ( ( √ ‘ 2 ) ↑𝑐 2 ) ∈ ℚ
36	28 35	eqeltri	⊢ ( ( √ ‘ 2 ) ↑𝑐 ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) ) ∈ ℚ
37	23 36	eqeltrri	⊢ ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ
38	37	a1i	⊢ ( ¬ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ → ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ )
39	18 19 38	3jca	⊢ ( ¬ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ → ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ( ℝ ∖ ℚ ) ∧ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) )
40	8 8 39	3jaoi	⊢ ( ( ¬ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∨ ¬ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∨ ¬ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) → ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ( ℝ ∖ ℚ ) ∧ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) )
41	6 40	sylbi	⊢ ( ¬ ( ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) → ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ( ℝ ∖ ℚ ) ∧ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) )
42		oveq1	⊢ ( 𝑎 = ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) → ( 𝑎 ↑𝑐 𝑏 ) = ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 𝑏 ) )
43	42	eleq1d	⊢ ( 𝑎 = ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) → ( ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ ↔ ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 𝑏 ) ∈ ℚ ) )
44		oveq2	⊢ ( 𝑏 = ( √ ‘ 2 ) → ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 𝑏 ) = ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) ) )
45	44	eleq1d	⊢ ( 𝑏 = ( √ ‘ 2 ) → ( ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 𝑏 ) ∈ ℚ ↔ ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) )
46	43 45	rspc2ev	⊢ ( ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ( ℝ ∖ ℚ ) ∧ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) → ∃ 𝑎 ∈ ( ℝ ∖ ℚ ) ∃ 𝑏 ∈ ( ℝ ∖ ℚ ) ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ )
47	41 46	syl	⊢ ( ¬ ( ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( ( √ ‘ 2 ) ↑𝑐 ( √ ‘ 2 ) ) ∈ ℚ ) → ∃ 𝑎 ∈ ( ℝ ∖ ℚ ) ∃ 𝑏 ∈ ( ℝ ∖ ℚ ) ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ )
48	5 47	pm2.61i	⊢ ∃ 𝑎 ∈ ( ℝ ∖ ℚ ) ∃ 𝑏 ∈ ( ℝ ∖ ℚ ) ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ