Step |
Hyp |
Ref |
Expression |
1 |
|
3nn |
⊢ 3 ∈ ℕ |
2 |
1
|
a1i |
⊢ ( ¬ ( 3 ↑ 3 ) ∈ ℕ → 3 ∈ ℕ ) |
3 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
4 |
3
|
a1i |
⊢ ( ¬ ( 3 ↑ 3 ) ∈ ℕ → 3 ∈ ℕ0 ) |
5 |
2 4
|
nnexpcld |
⊢ ( ¬ ( 3 ↑ 3 ) ∈ ℕ → ( 3 ↑ 3 ) ∈ ℕ ) |
6 |
5
|
pm2.18i |
⊢ ( 3 ↑ 3 ) ∈ ℕ |
7 |
|
nnq |
⊢ ( ( 3 ↑ 3 ) ∈ ℕ → ( 3 ↑ 3 ) ∈ ℚ ) |
8 |
6 7
|
mp1i |
⊢ ( 𝐴 ∈ ℚ → ( 3 ↑ 3 ) ∈ ℚ ) |
9 |
|
qexpcl |
⊢ ( ( 𝐴 ∈ ℚ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ 3 ) ∈ ℚ ) |
10 |
3 9
|
mpan2 |
⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ↑ 3 ) ∈ ℚ ) |
11 |
|
qmulcl |
⊢ ( ( ( 3 ↑ 3 ) ∈ ℚ ∧ ( 𝐴 ↑ 3 ) ∈ ℚ ) → ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) ∈ ℚ ) |
12 |
8 10 11
|
syl2anc |
⊢ ( 𝐴 ∈ ℚ → ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) ∈ ℚ ) |
13 |
|
1nn |
⊢ 1 ∈ ℕ |
14 |
|
nnq |
⊢ ( 1 ∈ ℕ → 1 ∈ ℚ ) |
15 |
13 14
|
ax-mp |
⊢ 1 ∈ ℚ |
16 |
|
qsubcl |
⊢ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) ∈ ℚ ∧ 1 ∈ ℚ ) → ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ∈ ℚ ) |
17 |
12 15 16
|
sylancl |
⊢ ( 𝐴 ∈ ℚ → ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ∈ ℚ ) |
18 |
|
qsqcl |
⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ↑ 2 ) ∈ ℚ ) |
19 |
|
qmulcl |
⊢ ( ( ( 3 ↑ 3 ) ∈ ℚ ∧ ( 𝐴 ↑ 2 ) ∈ ℚ ) → ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) ∈ ℚ ) |
20 |
8 18 19
|
syl2anc |
⊢ ( 𝐴 ∈ ℚ → ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) ∈ ℚ ) |
21 |
|
nnq |
⊢ ( 3 ∈ ℕ → 3 ∈ ℚ ) |
22 |
1 21
|
ax-mp |
⊢ 3 ∈ ℚ |
23 |
|
qsqcl |
⊢ ( 3 ∈ ℚ → ( 3 ↑ 2 ) ∈ ℚ ) |
24 |
22 23
|
mp1i |
⊢ ( 𝐴 ∈ ℚ → ( 3 ↑ 2 ) ∈ ℚ ) |
25 |
|
qmulcl |
⊢ ( ( ( 3 ↑ 2 ) ∈ ℚ ∧ 𝐴 ∈ ℚ ) → ( ( 3 ↑ 2 ) · 𝐴 ) ∈ ℚ ) |
26 |
24 25
|
mpancom |
⊢ ( 𝐴 ∈ ℚ → ( ( 3 ↑ 2 ) · 𝐴 ) ∈ ℚ ) |
27 |
|
qaddcl |
⊢ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) ∈ ℚ ∧ ( ( 3 ↑ 2 ) · 𝐴 ) ∈ ℚ ) → ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ∈ ℚ ) |
28 |
20 26 27
|
syl2anc |
⊢ ( 𝐴 ∈ ℚ → ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ∈ ℚ ) |
29 |
|
qaddcl |
⊢ ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ∈ ℚ ∧ 3 ∈ ℚ ) → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ∈ ℚ ) |
30 |
28 22 29
|
sylancl |
⊢ ( 𝐴 ∈ ℚ → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ∈ ℚ ) |
31 |
|
id |
⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℚ ) |
32 |
31
|
3cubeslem2 |
⊢ ( 𝐴 ∈ ℚ → ¬ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) = 0 ) |
33 |
32
|
neqned |
⊢ ( 𝐴 ∈ ℚ → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ≠ 0 ) |
34 |
|
qdivcl |
⊢ ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ∈ ℚ ∧ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ∈ ℚ ∧ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ≠ 0 ) → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ∈ ℚ ) |
35 |
17 30 33 34
|
syl3anc |
⊢ ( 𝐴 ∈ ℚ → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ∈ ℚ ) |
36 |
|
qnegcl |
⊢ ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) ∈ ℚ → - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) ∈ ℚ ) |
37 |
12 36
|
syl |
⊢ ( 𝐴 ∈ ℚ → - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) ∈ ℚ ) |
38 |
|
qaddcl |
⊢ ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) ∈ ℚ ∧ ( ( 3 ↑ 2 ) · 𝐴 ) ∈ ℚ ) → ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ∈ ℚ ) |
39 |
37 26 38
|
syl2anc |
⊢ ( 𝐴 ∈ ℚ → ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ∈ ℚ ) |
40 |
|
qaddcl |
⊢ ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ∈ ℚ ∧ 1 ∈ ℚ ) → ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ∈ ℚ ) |
41 |
39 15 40
|
sylancl |
⊢ ( 𝐴 ∈ ℚ → ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ∈ ℚ ) |
42 |
|
qdivcl |
⊢ ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ∈ ℚ ∧ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ∈ ℚ ∧ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ≠ 0 ) → ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ∈ ℚ ) |
43 |
41 30 33 42
|
syl3anc |
⊢ ( 𝐴 ∈ ℚ → ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ∈ ℚ ) |
44 |
|
qdivcl |
⊢ ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ∈ ℚ ∧ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ∈ ℚ ∧ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ≠ 0 ) → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ∈ ℚ ) |
45 |
28 30 33 44
|
syl3anc |
⊢ ( 𝐴 ∈ ℚ → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ∈ ℚ ) |
46 |
31
|
3cubeslem4 |
⊢ ( 𝐴 ∈ ℚ → 𝐴 = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) ) |
47 |
|
oveq1 |
⊢ ( 𝑎 = ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( 𝑎 ↑ 3 ) = ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) |
48 |
47
|
oveq1d |
⊢ ( 𝑎 = ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) = ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( 𝑏 ↑ 3 ) ) ) |
49 |
48
|
oveq1d |
⊢ ( 𝑎 = ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ) |
50 |
49
|
eqeq2d |
⊢ ( 𝑎 = ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ↔ 𝐴 = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ) ) |
51 |
|
oveq1 |
⊢ ( 𝑏 = ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( 𝑏 ↑ 3 ) = ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) |
52 |
51
|
oveq2d |
⊢ ( 𝑏 = ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( 𝑏 ↑ 3 ) ) = ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) ) |
53 |
52
|
oveq1d |
⊢ ( 𝑏 = ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ) |
54 |
53
|
eqeq2d |
⊢ ( 𝑏 = ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( 𝐴 = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ↔ 𝐴 = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ) ) |
55 |
|
oveq1 |
⊢ ( 𝑐 = ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( 𝑐 ↑ 3 ) = ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) |
56 |
55
|
oveq2d |
⊢ ( 𝑐 = ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) ) |
57 |
56
|
eqeq2d |
⊢ ( 𝑐 = ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) → ( 𝐴 = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ↔ 𝐴 = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) ) ) |
58 |
50 54 57
|
rspc3ev |
⊢ ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ∈ ℚ ∧ ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ∈ ℚ ∧ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ∈ ℚ ) ∧ 𝐴 = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) ) → ∃ 𝑎 ∈ ℚ ∃ 𝑏 ∈ ℚ ∃ 𝑐 ∈ ℚ 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ) |
59 |
35 43 45 46 58
|
syl31anc |
⊢ ( 𝐴 ∈ ℚ → ∃ 𝑎 ∈ ℚ ∃ 𝑏 ∈ ℚ ∃ 𝑐 ∈ ℚ 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ) |
60 |
|
3anass |
⊢ ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) ↔ ( 𝑎 ∈ ℚ ∧ ( 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) ) ) |
61 |
|
qexpcl |
⊢ ( ( 𝑎 ∈ ℚ ∧ 3 ∈ ℕ0 ) → ( 𝑎 ↑ 3 ) ∈ ℚ ) |
62 |
3 61
|
mpan2 |
⊢ ( 𝑎 ∈ ℚ → ( 𝑎 ↑ 3 ) ∈ ℚ ) |
63 |
|
simprl |
⊢ ( ( 𝑎 ∈ ℚ ∧ ( 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) ) → 𝑏 ∈ ℚ ) |
64 |
|
qexpcl |
⊢ ( ( 𝑏 ∈ ℚ ∧ 3 ∈ ℕ0 ) → ( 𝑏 ↑ 3 ) ∈ ℚ ) |
65 |
63 3 64
|
sylancl |
⊢ ( ( 𝑎 ∈ ℚ ∧ ( 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) ) → ( 𝑏 ↑ 3 ) ∈ ℚ ) |
66 |
|
qaddcl |
⊢ ( ( ( 𝑎 ↑ 3 ) ∈ ℚ ∧ ( 𝑏 ↑ 3 ) ∈ ℚ ) → ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) ∈ ℚ ) |
67 |
62 65 66
|
syl2an2r |
⊢ ( ( 𝑎 ∈ ℚ ∧ ( 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) ) → ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) ∈ ℚ ) |
68 |
|
simprr |
⊢ ( ( 𝑎 ∈ ℚ ∧ ( 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) ) → 𝑐 ∈ ℚ ) |
69 |
|
qexpcl |
⊢ ( ( 𝑐 ∈ ℚ ∧ 3 ∈ ℕ0 ) → ( 𝑐 ↑ 3 ) ∈ ℚ ) |
70 |
68 3 69
|
sylancl |
⊢ ( ( 𝑎 ∈ ℚ ∧ ( 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) ) → ( 𝑐 ↑ 3 ) ∈ ℚ ) |
71 |
|
qaddcl |
⊢ ( ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) ∈ ℚ ∧ ( 𝑐 ↑ 3 ) ∈ ℚ ) → ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ∈ ℚ ) |
72 |
67 70 71
|
syl2anc |
⊢ ( ( 𝑎 ∈ ℚ ∧ ( 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) ) → ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ∈ ℚ ) |
73 |
|
eleq1a |
⊢ ( ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ∈ ℚ → ( 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) → 𝐴 ∈ ℚ ) ) |
74 |
72 73
|
syl |
⊢ ( ( 𝑎 ∈ ℚ ∧ ( 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) ) → ( 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) → 𝐴 ∈ ℚ ) ) |
75 |
74
|
a1i |
⊢ ( ⊤ → ( ( 𝑎 ∈ ℚ ∧ ( 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) ) → ( 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) → 𝐴 ∈ ℚ ) ) ) |
76 |
60 75
|
syl5bi |
⊢ ( ⊤ → ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) → ( 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) → 𝐴 ∈ ℚ ) ) ) |
77 |
76
|
rexlimdv3d |
⊢ ( ⊤ → ( ∃ 𝑎 ∈ ℚ ∃ 𝑏 ∈ ℚ ∃ 𝑐 ∈ ℚ 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) → 𝐴 ∈ ℚ ) ) |
78 |
77
|
mptru |
⊢ ( ∃ 𝑎 ∈ ℚ ∃ 𝑏 ∈ ℚ ∃ 𝑐 ∈ ℚ 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) → 𝐴 ∈ ℚ ) |
79 |
59 78
|
impbii |
⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑎 ∈ ℚ ∃ 𝑏 ∈ ℚ ∃ 𝑐 ∈ ℚ 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) ) |