Theorem 2irrexpqALT

Description: Alternate proof of 2irrexpq : There exist irrational numbers a and b such that ( a ^ b ) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of Bauer, p. 483. In contrast to 2irrexpq , this is a constructive proof because it is based on two explicitly named irrational numbers ( sqrt2 ) and ( 2 logb 9 ) , see sqrt2irr0 , 2logb9irr and sqrt2cxp2logb9e3 . Therefore, this proof is also acceptable/usable in intuitionistic logic. (Contributed by AV, 23-Dec-2022) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	2irrexpqALT	⊢ ∃ 𝑎 ∈ ( ℝ ∖ ℚ ) ∃ 𝑏 ∈ ( ℝ ∖ ℚ ) ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ

Proof

Step	Hyp	Ref	Expression
1		sqrt2irr0	⊢ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ )
2		2logb9irr	⊢ ( 2 logb 9 ) ∈ ( ℝ ∖ ℚ )
3		sqrt2cxp2logb9e3	⊢ ( ( √ ‘ 2 ) ↑𝑐 ( 2 logb 9 ) ) = 3
4		3z	⊢ 3 ∈ ℤ
5		zq	⊢ ( 3 ∈ ℤ → 3 ∈ ℚ )
6	4 5	ax-mp	⊢ 3 ∈ ℚ
7	3 6	eqeltri	⊢ ( ( √ ‘ 2 ) ↑𝑐 ( 2 logb 9 ) ) ∈ ℚ
8		oveq1	⊢ ( 𝑎 = ( √ ‘ 2 ) → ( 𝑎 ↑𝑐 𝑏 ) = ( ( √ ‘ 2 ) ↑𝑐 𝑏 ) )
9	8	eleq1d	⊢ ( 𝑎 = ( √ ‘ 2 ) → ( ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ ↔ ( ( √ ‘ 2 ) ↑𝑐 𝑏 ) ∈ ℚ ) )
10		oveq2	⊢ ( 𝑏 = ( 2 logb 9 ) → ( ( √ ‘ 2 ) ↑𝑐 𝑏 ) = ( ( √ ‘ 2 ) ↑𝑐 ( 2 logb 9 ) ) )
11	10	eleq1d	⊢ ( 𝑏 = ( 2 logb 9 ) → ( ( ( √ ‘ 2 ) ↑𝑐 𝑏 ) ∈ ℚ ↔ ( ( √ ‘ 2 ) ↑𝑐 ( 2 logb 9 ) ) ∈ ℚ ) )
12	9 11	rspc2ev	⊢ ( ( ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) ∧ ( 2 logb 9 ) ∈ ( ℝ ∖ ℚ ) ∧ ( ( √ ‘ 2 ) ↑𝑐 ( 2 logb 9 ) ) ∈ ℚ ) → ∃ 𝑎 ∈ ( ℝ ∖ ℚ ) ∃ 𝑏 ∈ ( ℝ ∖ ℚ ) ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ )
13	1 2 7 12	mp3an	⊢ ∃ 𝑎 ∈ ( ℝ ∖ ℚ ) ∃ 𝑏 ∈ ( ℝ ∖ ℚ ) ( 𝑎 ↑𝑐 𝑏 ) ∈ ℚ