This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ

Proof

Step Hyp Ref Expression
1 sqrt2irr0 
 |-  ( sqrt ` 2 ) e. ( RR \ QQ )
2 2logb9irr 
 |-  ( 2 logb 9 ) e. ( RR \ QQ )
3 sqrt2cxp2logb9e3 
 |-  ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) = 3
4 3z 
 |-  3 e. ZZ
5 zq 
 |-  ( 3 e. ZZ -> 3 e. QQ )
6 4 5 ax-mp 
 |-  3 e. QQ
7 3 6 eqeltri 
 |-  ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) e. QQ
8 oveq1 
 |-  ( a = ( sqrt ` 2 ) -> ( a ^c b ) = ( ( sqrt ` 2 ) ^c b ) )
9 8 eleq1d 
 |-  ( a = ( sqrt ` 2 ) -> ( ( a ^c b ) e. QQ <-> ( ( sqrt ` 2 ) ^c b ) e. QQ ) )
10 oveq2 
 |-  ( b = ( 2 logb 9 ) -> ( ( sqrt ` 2 ) ^c b ) = ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) )
11 10 eleq1d 
 |-  ( b = ( 2 logb 9 ) -> ( ( ( sqrt ` 2 ) ^c b ) e. QQ <-> ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) e. QQ ) )
12 9 11 rspc2ev 
 |-  ( ( ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( 2 logb 9 ) e. ( RR \ QQ ) /\ ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) e. QQ ) -> E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ )
13 1 2 7 12 mp3an 
 |-  E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ