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