Metamath Proof Explorer

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 ⊢ ∃ a ∈ ℝ ∖ ℚ ∃ b ∈ ℝ ∖ ℚ a b ∈ ℚ

Proof

Step Hyp Ref Expression
1 sqrt2irr0 ⊢ 2 ∈ ℝ ∖ ℚ
2 2logb9irr ⊢ log 2 9 ∈ ℝ ∖ ℚ
3 sqrt2cxp2logb9e3 ⊢ 2 log 2 9 = 3
4 3z ⊢ 3 ∈ ℤ
5 zq ⊢ 3 ∈ ℤ → 3 ∈ ℚ
6 4 5 ax-mp ⊢ 3 ∈ ℚ
7 3 6 eqeltri ⊢ 2 log 2 9 ∈ ℚ
8 oveq1 ⊢ a = 2 → a b = 2 b
9 8 eleq1d ⊢ a = 2 → a b ∈ ℚ ↔ 2 b ∈ ℚ
10 oveq2 ⊢ b = log 2 9 → 2 b = 2 log 2 9
11 10 eleq1d ⊢ b = log 2 9 → 2 b ∈ ℚ ↔ 2 log 2 9 ∈ ℚ
12 9 11 rspc2ev ⊢ 2 ∈ ℝ ∖ ℚ ∧ log 2 9 ∈ ℝ ∖ ℚ ∧ 2 log 2 9 ∈ ℚ → ∃ a ∈ ℝ ∖ ℚ ∃ b ∈ ℝ ∖ ℚ a b ∈ ℚ
13 1 2 7 12 mp3an ⊢ ∃ a ∈ ℝ ∖ ℚ ∃ b ∈ ℝ ∖ ℚ a b ∈ ℚ