Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = ( sqrt ` 2 ) -> ( a ^c b ) = ( ( sqrt ` 2 ) ^c b ) )
2 1 eleq1d 
 |-  ( a = ( sqrt ` 2 ) -> ( ( a ^c b ) e. QQ <-> ( ( sqrt ` 2 ) ^c b ) e. QQ ) )
3 oveq2 
 |-  ( b = ( sqrt ` 2 ) -> ( ( sqrt ` 2 ) ^c b ) = ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) )
4 3 eleq1d 
 |-  ( b = ( sqrt ` 2 ) -> ( ( ( sqrt ` 2 ) ^c b ) e. QQ <-> ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ ) )
5 2 4 rspc2ev 
 |-  ( ( ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ ) -> E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ )
6 3ianor 
 |-  ( -. ( ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ ) <-> ( -. ( sqrt ` 2 ) e. ( RR \ QQ ) \/ -. ( sqrt ` 2 ) e. ( RR \ QQ ) \/ -. ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ ) )
7 sqrt2irr0 
 |-  ( sqrt ` 2 ) e. ( RR \ QQ )
8 7 pm2.24i 
 |-  ( -. ( sqrt ` 2 ) e. ( RR \ QQ ) -> ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. ( RR \ QQ ) /\ ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) ) e. QQ ) )
9 2rp 
 |-  2 e. RR+
10 rpsqrtcl 
 |-  ( 2 e. RR+ -> ( sqrt ` 2 ) e. RR+ )
11 9 10 ax-mp 
 |-  ( sqrt ` 2 ) e. RR+
12 rpre 
 |-  ( ( sqrt ` 2 ) e. RR+ -> ( sqrt ` 2 ) e. RR )
13 rpge0 
 |-  ( ( sqrt ` 2 ) e. RR+ -> 0 <_ ( sqrt ` 2 ) )
14 12 13 12 recxpcld 
 |-  ( ( sqrt ` 2 ) e. RR+ -> ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. RR )
15 11 14 ax-mp 
 |-  ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. RR
16 15 a1i 
 |-  ( -. ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ -> ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. RR )
17 id 
 |-  ( -. ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ -> -. ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ )
18 16 17 eldifd 
 |-  ( -. ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ -> ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. ( RR \ QQ ) )
19 7 a1i 
 |-  ( -. ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ -> ( sqrt ` 2 ) e. ( RR \ QQ ) )
20 sqrt2re 
 |-  ( sqrt ` 2 ) e. RR
21 20 recni 
 |-  ( sqrt ` 2 ) e. CC
22 cxpmul 
 |-  ( ( ( sqrt ` 2 ) e. RR+ /\ ( sqrt ` 2 ) e. RR /\ ( sqrt ` 2 ) e. CC ) -> ( ( sqrt ` 2 ) ^c ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) ) = ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) ) )
23 11 20 21 22 mp3an 
 |-  ( ( sqrt ` 2 ) ^c ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) ) = ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) )
24 2re 
 |-  2 e. RR
25 0le2 
 |-  0 <_ 2
26 remsqsqrt 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) = 2 )
27 24 25 26 mp2an 
 |-  ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) = 2
28 27 oveq2i 
 |-  ( ( sqrt ` 2 ) ^c ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) ) = ( ( sqrt ` 2 ) ^c 2 )
29 2cn 
 |-  2 e. CC
30 cxpsqrtth 
 |-  ( 2 e. CC -> ( ( sqrt ` 2 ) ^c 2 ) = 2 )
31 29 30 ax-mp 
 |-  ( ( sqrt ` 2 ) ^c 2 ) = 2
32 2z 
 |-  2 e. ZZ
33 zq 
 |-  ( 2 e. ZZ -> 2 e. QQ )
34 32 33 ax-mp 
 |-  2 e. QQ
35 31 34 eqeltri 
 |-  ( ( sqrt ` 2 ) ^c 2 ) e. QQ
36 28 35 eqeltri 
 |-  ( ( sqrt ` 2 ) ^c ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) ) e. QQ
37 23 36 eqeltrri 
 |-  ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) ) e. QQ
38 37 a1i 
 |-  ( -. ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ -> ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) ) e. QQ )
39 18 19 38 3jca 
 |-  ( -. ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ -> ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. ( RR \ QQ ) /\ ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) ) e. QQ ) )
40 8 8 39 3jaoi 
 |-  ( ( -. ( sqrt ` 2 ) e. ( RR \ QQ ) \/ -. ( sqrt ` 2 ) e. ( RR \ QQ ) \/ -. ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ ) -> ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. ( RR \ QQ ) /\ ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) ) e. QQ ) )
41 6 40 sylbi 
 |-  ( -. ( ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ ) -> ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. ( RR \ QQ ) /\ ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) ) e. QQ ) )
42 oveq1 
 |-  ( a = ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) -> ( a ^c b ) = ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c b ) )
43 42 eleq1d 
 |-  ( a = ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) -> ( ( a ^c b ) e. QQ <-> ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c b ) e. QQ ) )
44 oveq2 
 |-  ( b = ( sqrt ` 2 ) -> ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c b ) = ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) ) )
45 44 eleq1d 
 |-  ( b = ( sqrt ` 2 ) -> ( ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c b ) e. QQ <-> ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) ) e. QQ ) )
46 43 45 rspc2ev 
 |-  ( ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. ( RR \ QQ ) /\ ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) ^c ( sqrt ` 2 ) ) e. QQ ) -> E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ )
47 41 46 syl 
 |-  ( -. ( ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( ( sqrt ` 2 ) ^c ( sqrt ` 2 ) ) e. QQ ) -> E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ )
48 5 47 pm2.61i 
 |-  E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ