| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cos9thpiminplylem2.1 |
⊢ ( 𝜑 → 𝑋 ∈ ℚ ) |
| 2 |
|
simpr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → 𝑋 = 0 ) |
| 3 |
2
|
oveq1d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( 𝑋 ↑ 3 ) = ( 0 ↑ 3 ) ) |
| 4 |
|
3nn |
⊢ 3 ∈ ℕ |
| 5 |
4
|
a1i |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → 3 ∈ ℕ ) |
| 6 |
5
|
0expd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( 0 ↑ 3 ) = 0 ) |
| 7 |
3 6
|
eqtrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( 𝑋 ↑ 3 ) = 0 ) |
| 8 |
7
|
oveq1d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = ( 0 + ( ( - 3 · 𝑋 ) + 1 ) ) ) |
| 9 |
2
|
oveq2d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( - 3 · 𝑋 ) = ( - 3 · 0 ) ) |
| 10 |
|
3cn |
⊢ 3 ∈ ℂ |
| 11 |
10
|
negcli |
⊢ - 3 ∈ ℂ |
| 12 |
11
|
a1i |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → - 3 ∈ ℂ ) |
| 13 |
12
|
mul01d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( - 3 · 0 ) = 0 ) |
| 14 |
9 13
|
eqtr2d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → 0 = ( - 3 · 𝑋 ) ) |
| 15 |
14
|
oveq1d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( 0 + 1 ) = ( ( - 3 · 𝑋 ) + 1 ) ) |
| 16 |
|
0p1e1 |
⊢ ( 0 + 1 ) = 1 |
| 17 |
15 16
|
eqtr3di |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( ( - 3 · 𝑋 ) + 1 ) = 1 ) |
| 18 |
14 17
|
oveq12d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( 0 + ( ( - 3 · 𝑋 ) + 1 ) ) = ( ( - 3 · 𝑋 ) + 1 ) ) |
| 19 |
8 18 17
|
3eqtrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 1 ) |
| 20 |
|
ax-1ne0 |
⊢ 1 ≠ 0 |
| 21 |
20
|
a1i |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → 1 ≠ 0 ) |
| 22 |
19 21
|
eqnetrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 = 0 ) → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ≠ 0 ) |
| 23 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) → 𝑋 = ( 𝑝 / 𝑞 ) ) |
| 24 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) → 𝑝 ∈ ℤ ) |
| 25 |
24
|
zcnd |
⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) → 𝑝 ∈ ℂ ) |
| 26 |
25
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) → 𝑝 ∈ ℂ ) |
| 27 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) → 𝑞 ∈ ℕ ) |
| 28 |
27
|
nncnd |
⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) → 𝑞 ∈ ℂ ) |
| 29 |
28
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) → 𝑞 ∈ ℂ ) |
| 30 |
27
|
nnne0d |
⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) → 𝑞 ≠ 0 ) |
| 31 |
30
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) → 𝑞 ≠ 0 ) |
| 32 |
26 29 31
|
divcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) → ( 𝑝 / 𝑞 ) ∈ ℂ ) |
| 33 |
23 32
|
eqeltrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) → 𝑋 ∈ ℂ ) |
| 34 |
33
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑋 ∈ ℂ ) |
| 35 |
|
simplr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑋 ≠ 0 ) |
| 36 |
34 35
|
reccld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 1 / 𝑋 ) ∈ ℂ ) |
| 37 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
| 38 |
37
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 3 ∈ ℕ0 ) |
| 39 |
36 38
|
expcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( 1 / 𝑋 ) ↑ 3 ) ∈ ℂ ) |
| 40 |
11
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → - 3 ∈ ℂ ) |
| 41 |
36
|
sqcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( 1 / 𝑋 ) ↑ 2 ) ∈ ℂ ) |
| 42 |
40 41
|
mulcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) ∈ ℂ ) |
| 43 |
|
1cnd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 1 ∈ ℂ ) |
| 44 |
42 43
|
addcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) + 1 ) ∈ ℂ ) |
| 45 |
37
|
a1i |
⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) → 3 ∈ ℕ0 ) |
| 46 |
33 45
|
expcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) → ( 𝑋 ↑ 3 ) ∈ ℂ ) |
| 47 |
46
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑋 ↑ 3 ) ∈ ℂ ) |
| 48 |
39 44 47
|
adddird |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( ( 1 / 𝑋 ) ↑ 3 ) + ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) + 1 ) ) · ( 𝑋 ↑ 3 ) ) = ( ( ( ( 1 / 𝑋 ) ↑ 3 ) · ( 𝑋 ↑ 3 ) ) + ( ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) + 1 ) · ( 𝑋 ↑ 3 ) ) ) ) |
| 49 |
|
3z |
⊢ 3 ∈ ℤ |
| 50 |
49
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 3 ∈ ℤ ) |
| 51 |
34 35 50
|
exprecd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( 1 / 𝑋 ) ↑ 3 ) = ( 1 / ( 𝑋 ↑ 3 ) ) ) |
| 52 |
51
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( 1 / 𝑋 ) ↑ 3 ) · ( 𝑋 ↑ 3 ) ) = ( ( 1 / ( 𝑋 ↑ 3 ) ) · ( 𝑋 ↑ 3 ) ) ) |
| 53 |
34 35 50
|
expne0d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑋 ↑ 3 ) ≠ 0 ) |
| 54 |
47 53
|
recid2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( 1 / ( 𝑋 ↑ 3 ) ) · ( 𝑋 ↑ 3 ) ) = 1 ) |
| 55 |
52 54
|
eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( 1 / 𝑋 ) ↑ 3 ) · ( 𝑋 ↑ 3 ) ) = 1 ) |
| 56 |
|
2z |
⊢ 2 ∈ ℤ |
| 57 |
56
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 2 ∈ ℤ ) |
| 58 |
34 35 57
|
exprecd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( 1 / 𝑋 ) ↑ 2 ) = ( 1 / ( 𝑋 ↑ 2 ) ) ) |
| 59 |
58
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( 1 / 𝑋 ) ↑ 2 ) · ( 𝑋 ↑ 3 ) ) = ( ( 1 / ( 𝑋 ↑ 2 ) ) · ( 𝑋 ↑ 3 ) ) ) |
| 60 |
34
|
sqcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑋 ↑ 2 ) ∈ ℂ ) |
| 61 |
34 35 57
|
expne0d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑋 ↑ 2 ) ≠ 0 ) |
| 62 |
47 60 61
|
divrec2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( 𝑋 ↑ 3 ) / ( 𝑋 ↑ 2 ) ) = ( ( 1 / ( 𝑋 ↑ 2 ) ) · ( 𝑋 ↑ 3 ) ) ) |
| 63 |
|
2cnd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 2 ∈ ℂ ) |
| 64 |
|
2p1e3 |
⊢ ( 2 + 1 ) = 3 |
| 65 |
64
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 2 + 1 ) = 3 ) |
| 66 |
65
|
eqcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 3 = ( 2 + 1 ) ) |
| 67 |
63 43 66
|
mvrladdd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 3 − 2 ) = 1 ) |
| 68 |
67
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑋 ↑ ( 3 − 2 ) ) = ( 𝑋 ↑ 1 ) ) |
| 69 |
34 35 57 50
|
expsubd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑋 ↑ ( 3 − 2 ) ) = ( ( 𝑋 ↑ 3 ) / ( 𝑋 ↑ 2 ) ) ) |
| 70 |
34
|
exp1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑋 ↑ 1 ) = 𝑋 ) |
| 71 |
68 69 70
|
3eqtr3d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( 𝑋 ↑ 3 ) / ( 𝑋 ↑ 2 ) ) = 𝑋 ) |
| 72 |
59 62 71
|
3eqtr2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( 1 / 𝑋 ) ↑ 2 ) · ( 𝑋 ↑ 3 ) ) = 𝑋 ) |
| 73 |
72
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 3 · ( ( ( 1 / 𝑋 ) ↑ 2 ) · ( 𝑋 ↑ 3 ) ) ) = ( 3 · 𝑋 ) ) |
| 74 |
73
|
negeqd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → - ( 3 · ( ( ( 1 / 𝑋 ) ↑ 2 ) · ( 𝑋 ↑ 3 ) ) ) = - ( 3 · 𝑋 ) ) |
| 75 |
40 41 47
|
mulassd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) · ( 𝑋 ↑ 3 ) ) = ( - 3 · ( ( ( 1 / 𝑋 ) ↑ 2 ) · ( 𝑋 ↑ 3 ) ) ) ) |
| 76 |
10
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 3 ∈ ℂ ) |
| 77 |
41 47
|
mulcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( 1 / 𝑋 ) ↑ 2 ) · ( 𝑋 ↑ 3 ) ) ∈ ℂ ) |
| 78 |
76 77
|
mulneg1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( - 3 · ( ( ( 1 / 𝑋 ) ↑ 2 ) · ( 𝑋 ↑ 3 ) ) ) = - ( 3 · ( ( ( 1 / 𝑋 ) ↑ 2 ) · ( 𝑋 ↑ 3 ) ) ) ) |
| 79 |
75 78
|
eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) · ( 𝑋 ↑ 3 ) ) = - ( 3 · ( ( ( 1 / 𝑋 ) ↑ 2 ) · ( 𝑋 ↑ 3 ) ) ) ) |
| 80 |
76 34
|
mulneg1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( - 3 · 𝑋 ) = - ( 3 · 𝑋 ) ) |
| 81 |
74 79 80
|
3eqtr4d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) · ( 𝑋 ↑ 3 ) ) = ( - 3 · 𝑋 ) ) |
| 82 |
47
|
mullidd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 1 · ( 𝑋 ↑ 3 ) ) = ( 𝑋 ↑ 3 ) ) |
| 83 |
81 82
|
oveq12d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) · ( 𝑋 ↑ 3 ) ) + ( 1 · ( 𝑋 ↑ 3 ) ) ) = ( ( - 3 · 𝑋 ) + ( 𝑋 ↑ 3 ) ) ) |
| 84 |
42 47 43 83
|
joinlmuladdmuld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) + 1 ) · ( 𝑋 ↑ 3 ) ) = ( ( - 3 · 𝑋 ) + ( 𝑋 ↑ 3 ) ) ) |
| 85 |
55 84
|
oveq12d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( ( 1 / 𝑋 ) ↑ 3 ) · ( 𝑋 ↑ 3 ) ) + ( ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) + 1 ) · ( 𝑋 ↑ 3 ) ) ) = ( 1 + ( ( - 3 · 𝑋 ) + ( 𝑋 ↑ 3 ) ) ) ) |
| 86 |
40 34
|
mulcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( - 3 · 𝑋 ) ∈ ℂ ) |
| 87 |
86 47
|
addcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( - 3 · 𝑋 ) + ( 𝑋 ↑ 3 ) ) ∈ ℂ ) |
| 88 |
43 87
|
addcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 1 + ( ( - 3 · 𝑋 ) + ( 𝑋 ↑ 3 ) ) ) = ( ( ( - 3 · 𝑋 ) + ( 𝑋 ↑ 3 ) ) + 1 ) ) |
| 89 |
86 47
|
addcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( - 3 · 𝑋 ) + ( 𝑋 ↑ 3 ) ) = ( ( 𝑋 ↑ 3 ) + ( - 3 · 𝑋 ) ) ) |
| 90 |
89
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( - 3 · 𝑋 ) + ( 𝑋 ↑ 3 ) ) + 1 ) = ( ( ( 𝑋 ↑ 3 ) + ( - 3 · 𝑋 ) ) + 1 ) ) |
| 91 |
47 86 43
|
addassd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( 𝑋 ↑ 3 ) + ( - 3 · 𝑋 ) ) + 1 ) = ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ) |
| 92 |
88 90 91
|
3eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 1 + ( ( - 3 · 𝑋 ) + ( 𝑋 ↑ 3 ) ) ) = ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ) |
| 93 |
48 85 92
|
3eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( ( 1 / 𝑋 ) ↑ 3 ) + ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) + 1 ) ) · ( 𝑋 ↑ 3 ) ) = ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ) |
| 94 |
39 44
|
addcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( 1 / 𝑋 ) ↑ 3 ) + ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) + 1 ) ) ∈ ℂ ) |
| 95 |
|
simpllr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → 𝑋 = ( 𝑝 / 𝑞 ) ) |
| 96 |
95
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑋 = ( 𝑝 / 𝑞 ) ) |
| 97 |
96
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 1 / 𝑋 ) = ( 1 / ( 𝑝 / 𝑞 ) ) ) |
| 98 |
|
simp-6r |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑝 ∈ ℤ ) |
| 99 |
98
|
zcnd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑝 ∈ ℂ ) |
| 100 |
|
simp-5r |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑞 ∈ ℕ ) |
| 101 |
100
|
nncnd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑞 ∈ ℂ ) |
| 102 |
|
simpr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 ) |
| 103 |
95 102
|
eqnetrrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → ( 𝑝 / 𝑞 ) ≠ 0 ) |
| 104 |
25
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → 𝑝 ∈ ℂ ) |
| 105 |
28
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → 𝑞 ∈ ℂ ) |
| 106 |
30
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → 𝑞 ≠ 0 ) |
| 107 |
104 105 106
|
divne0bd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → ( 𝑝 ≠ 0 ↔ ( 𝑝 / 𝑞 ) ≠ 0 ) ) |
| 108 |
103 107
|
mpbird |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → 𝑝 ≠ 0 ) |
| 109 |
108
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑝 ≠ 0 ) |
| 110 |
100
|
nnne0d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑞 ≠ 0 ) |
| 111 |
99 101 109 110
|
recdivd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 1 / ( 𝑝 / 𝑞 ) ) = ( 𝑞 / 𝑝 ) ) |
| 112 |
101 99 109
|
divrecd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑞 / 𝑝 ) = ( 𝑞 · ( 1 / 𝑝 ) ) ) |
| 113 |
99
|
div1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑝 / 1 ) = 𝑝 ) |
| 114 |
|
simpr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( abs ‘ 𝑝 ) = 1 ) |
| 115 |
114
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑝 / ( abs ‘ 𝑝 ) ) = ( 𝑝 / 1 ) ) |
| 116 |
24
|
zred |
⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) → 𝑝 ∈ ℝ ) |
| 117 |
116
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → 𝑝 ∈ ℝ ) |
| 118 |
117 108
|
receqid |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → ( ( 1 / 𝑝 ) = 𝑝 ↔ ( abs ‘ 𝑝 ) = 1 ) ) |
| 119 |
118
|
biimpar |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 1 / 𝑝 ) = 𝑝 ) |
| 120 |
113 115 119
|
3eqtr4d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑝 / ( abs ‘ 𝑝 ) ) = ( 1 / 𝑝 ) ) |
| 121 |
120
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑞 · ( 𝑝 / ( abs ‘ 𝑝 ) ) ) = ( 𝑞 · ( 1 / 𝑝 ) ) ) |
| 122 |
112 121
|
eqtr4d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑞 / 𝑝 ) = ( 𝑞 · ( 𝑝 / ( abs ‘ 𝑝 ) ) ) ) |
| 123 |
97 111 122
|
3eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 1 / 𝑋 ) = ( 𝑞 · ( 𝑝 / ( abs ‘ 𝑝 ) ) ) ) |
| 124 |
98
|
zred |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑝 ∈ ℝ ) |
| 125 |
|
sgnval2 |
⊢ ( ( 𝑝 ∈ ℝ ∧ 𝑝 ≠ 0 ) → ( sgn ‘ 𝑝 ) = ( 𝑝 / ( abs ‘ 𝑝 ) ) ) |
| 126 |
124 109 125
|
syl2anc |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( sgn ‘ 𝑝 ) = ( 𝑝 / ( abs ‘ 𝑝 ) ) ) |
| 127 |
126
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑞 · ( sgn ‘ 𝑝 ) ) = ( 𝑞 · ( 𝑝 / ( abs ‘ 𝑝 ) ) ) ) |
| 128 |
123 127
|
eqtr4d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 1 / 𝑋 ) = ( 𝑞 · ( sgn ‘ 𝑝 ) ) ) |
| 129 |
100
|
nnzd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑞 ∈ ℤ ) |
| 130 |
|
neg1z |
⊢ - 1 ∈ ℤ |
| 131 |
130
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → - 1 ∈ ℤ ) |
| 132 |
|
0zd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 0 ∈ ℤ ) |
| 133 |
|
1zzd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 1 ∈ ℤ ) |
| 134 |
131 132 133
|
tpssd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → { - 1 , 0 , 1 } ⊆ ℤ ) |
| 135 |
124
|
rexrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → 𝑝 ∈ ℝ* ) |
| 136 |
|
sgncl |
⊢ ( 𝑝 ∈ ℝ* → ( sgn ‘ 𝑝 ) ∈ { - 1 , 0 , 1 } ) |
| 137 |
135 136
|
syl |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( sgn ‘ 𝑝 ) ∈ { - 1 , 0 , 1 } ) |
| 138 |
134 137
|
sseldd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( sgn ‘ 𝑝 ) ∈ ℤ ) |
| 139 |
129 138
|
zmulcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 𝑞 · ( sgn ‘ 𝑝 ) ) ∈ ℤ ) |
| 140 |
128 139
|
eqeltrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( 1 / 𝑋 ) ∈ ℤ ) |
| 141 |
140
|
cos9thpiminplylem1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( 1 / 𝑋 ) ↑ 3 ) + ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) + 1 ) ) ≠ 0 ) |
| 142 |
94 47 141 53
|
mulne0d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( ( ( 1 / 𝑋 ) ↑ 3 ) + ( ( - 3 · ( ( 1 / 𝑋 ) ↑ 2 ) ) + 1 ) ) · ( 𝑋 ↑ 3 ) ) ≠ 0 ) |
| 143 |
93 142
|
eqnetrrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) = 1 ) → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ≠ 0 ) |
| 144 |
|
simplr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) → 𝑟 ∈ ℙ ) |
| 145 |
|
1nprm |
⊢ ¬ 1 ∈ ℙ |
| 146 |
145
|
a1i |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) → ¬ 1 ∈ ℙ ) |
| 147 |
|
nelne2 |
⊢ ( ( 𝑟 ∈ ℙ ∧ ¬ 1 ∈ ℙ ) → 𝑟 ≠ 1 ) |
| 148 |
144 146 147
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) → 𝑟 ≠ 1 ) |
| 149 |
|
prmnn |
⊢ ( 𝑟 ∈ ℙ → 𝑟 ∈ ℕ ) |
| 150 |
149
|
ad3antlr |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∈ ℕ ) |
| 151 |
150
|
nnnn0d |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∈ ℕ0 ) |
| 152 |
150
|
nnzd |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∈ ℤ ) |
| 153 |
|
simp-5r |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → 𝑝 ∈ ℤ ) |
| 154 |
153
|
ad4antr |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑝 ∈ ℤ ) |
| 155 |
|
simp-8r |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑞 ∈ ℕ ) |
| 156 |
155
|
nnzd |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑞 ∈ ℤ ) |
| 157 |
|
simplr |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∥ ( abs ‘ 𝑝 ) ) |
| 158 |
|
dvdsabsb |
⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑝 ∈ ℤ ) → ( 𝑟 ∥ 𝑝 ↔ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ) |
| 159 |
158
|
biimpar |
⊢ ( ( ( 𝑟 ∈ ℤ ∧ 𝑝 ∈ ℤ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) → 𝑟 ∥ 𝑝 ) |
| 160 |
152 154 157 159
|
syl21anc |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∥ 𝑝 ) |
| 161 |
|
simpllr |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∈ ℙ ) |
| 162 |
4
|
a1i |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 3 ∈ ℕ ) |
| 163 |
49
|
a1i |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 3 ∈ ℤ ) |
| 164 |
155
|
nnnn0d |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑞 ∈ ℕ0 ) |
| 165 |
|
nn0sqcl |
⊢ ( 𝑞 ∈ ℕ0 → ( 𝑞 ↑ 2 ) ∈ ℕ0 ) |
| 166 |
164 165
|
syl |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑞 ↑ 2 ) ∈ ℕ0 ) |
| 167 |
166
|
nn0zd |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑞 ↑ 2 ) ∈ ℤ ) |
| 168 |
163 167
|
zmulcld |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 3 · ( 𝑞 ↑ 2 ) ) ∈ ℤ ) |
| 169 |
|
zsqcl |
⊢ ( 𝑝 ∈ ℤ → ( 𝑝 ↑ 2 ) ∈ ℤ ) |
| 170 |
154 169
|
syl |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 ↑ 2 ) ∈ ℤ ) |
| 171 |
168 170
|
zsubcld |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ∈ ℤ ) |
| 172 |
152 154 171 160
|
dvdsmultr1d |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∥ ( 𝑝 · ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ) ) |
| 173 |
105
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑞 ∈ ℂ ) |
| 174 |
37
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 3 ∈ ℕ0 ) |
| 175 |
173 174
|
expcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑞 ↑ 3 ) ∈ ℂ ) |
| 176 |
104
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑝 ∈ ℂ ) |
| 177 |
10
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 3 ∈ ℂ ) |
| 178 |
173
|
sqcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑞 ↑ 2 ) ∈ ℂ ) |
| 179 |
177 178
|
mulcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 3 · ( 𝑞 ↑ 2 ) ) ∈ ℂ ) |
| 180 |
176
|
sqcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 ↑ 2 ) ∈ ℂ ) |
| 181 |
179 180
|
subcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ∈ ℂ ) |
| 182 |
176 181
|
mulcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 · ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ) ∈ ℂ ) |
| 183 |
95
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑋 = ( 𝑝 / 𝑞 ) ) |
| 184 |
183
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑋 ↑ 3 ) = ( ( 𝑝 / 𝑞 ) ↑ 3 ) ) |
| 185 |
184
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑋 ↑ 3 ) · ( 𝑞 ↑ 3 ) ) = ( ( ( 𝑝 / 𝑞 ) ↑ 3 ) · ( 𝑞 ↑ 3 ) ) ) |
| 186 |
106
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑞 ≠ 0 ) |
| 187 |
176 173 186 174
|
expdivd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑝 / 𝑞 ) ↑ 3 ) = ( ( 𝑝 ↑ 3 ) / ( 𝑞 ↑ 3 ) ) ) |
| 188 |
187
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( ( 𝑝 / 𝑞 ) ↑ 3 ) · ( 𝑞 ↑ 3 ) ) = ( ( ( 𝑝 ↑ 3 ) / ( 𝑞 ↑ 3 ) ) · ( 𝑞 ↑ 3 ) ) ) |
| 189 |
176 174
|
expcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 ↑ 3 ) ∈ ℂ ) |
| 190 |
49
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 3 ∈ ℤ ) |
| 191 |
173 186 190
|
expne0d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑞 ↑ 3 ) ≠ 0 ) |
| 192 |
189 175 191
|
divcan1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( ( 𝑝 ↑ 3 ) / ( 𝑞 ↑ 3 ) ) · ( 𝑞 ↑ 3 ) ) = ( 𝑝 ↑ 3 ) ) |
| 193 |
185 188 192
|
3eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑋 ↑ 3 ) · ( 𝑞 ↑ 3 ) ) = ( 𝑝 ↑ 3 ) ) |
| 194 |
11
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → - 3 ∈ ℂ ) |
| 195 |
33
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑋 ∈ ℂ ) |
| 196 |
194 195
|
mulcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( - 3 · 𝑋 ) ∈ ℂ ) |
| 197 |
|
1cnd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 1 ∈ ℂ ) |
| 198 |
194 195 175
|
mulassd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( - 3 · 𝑋 ) · ( 𝑞 ↑ 3 ) ) = ( - 3 · ( 𝑋 · ( 𝑞 ↑ 3 ) ) ) ) |
| 199 |
183
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑋 · ( 𝑞 ↑ 3 ) ) = ( ( 𝑝 / 𝑞 ) · ( 𝑞 ↑ 3 ) ) ) |
| 200 |
176 173 175 186
|
div32d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑝 / 𝑞 ) · ( 𝑞 ↑ 3 ) ) = ( 𝑝 · ( ( 𝑞 ↑ 3 ) / 𝑞 ) ) ) |
| 201 |
|
1zzd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 1 ∈ ℤ ) |
| 202 |
173 186 201 190
|
expsubd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑞 ↑ ( 3 − 1 ) ) = ( ( 𝑞 ↑ 3 ) / ( 𝑞 ↑ 1 ) ) ) |
| 203 |
|
3m1e2 |
⊢ ( 3 − 1 ) = 2 |
| 204 |
203
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 3 − 1 ) = 2 ) |
| 205 |
204
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑞 ↑ ( 3 − 1 ) ) = ( 𝑞 ↑ 2 ) ) |
| 206 |
173
|
exp1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑞 ↑ 1 ) = 𝑞 ) |
| 207 |
206
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) / ( 𝑞 ↑ 1 ) ) = ( ( 𝑞 ↑ 3 ) / 𝑞 ) ) |
| 208 |
202 205 207
|
3eqtr3rd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) / 𝑞 ) = ( 𝑞 ↑ 2 ) ) |
| 209 |
208
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 · ( ( 𝑞 ↑ 3 ) / 𝑞 ) ) = ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) |
| 210 |
199 200 209
|
3eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑋 · ( 𝑞 ↑ 3 ) ) = ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) |
| 211 |
210
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( - 3 · ( 𝑋 · ( 𝑞 ↑ 3 ) ) ) = ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) ) |
| 212 |
198 211
|
eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( - 3 · 𝑋 ) · ( 𝑞 ↑ 3 ) ) = ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) ) |
| 213 |
175
|
mullidd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 1 · ( 𝑞 ↑ 3 ) ) = ( 𝑞 ↑ 3 ) ) |
| 214 |
212 213
|
oveq12d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( ( - 3 · 𝑋 ) · ( 𝑞 ↑ 3 ) ) + ( 1 · ( 𝑞 ↑ 3 ) ) ) = ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) ) |
| 215 |
196 175 197 214
|
joinlmuladdmuld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( ( - 3 · 𝑋 ) + 1 ) · ( 𝑞 ↑ 3 ) ) = ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) ) |
| 216 |
193 215
|
oveq12d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( ( 𝑋 ↑ 3 ) · ( 𝑞 ↑ 3 ) ) + ( ( ( - 3 · 𝑋 ) + 1 ) · ( 𝑞 ↑ 3 ) ) ) = ( ( 𝑝 ↑ 3 ) + ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) ) ) |
| 217 |
46
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑋 ↑ 3 ) ∈ ℂ ) |
| 218 |
196 197
|
addcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( - 3 · 𝑋 ) + 1 ) ∈ ℂ ) |
| 219 |
217 218 175
|
adddird |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) · ( 𝑞 ↑ 3 ) ) = ( ( ( 𝑋 ↑ 3 ) · ( 𝑞 ↑ 3 ) ) + ( ( ( - 3 · 𝑋 ) + 1 ) · ( 𝑞 ↑ 3 ) ) ) ) |
| 220 |
176 179 180
|
subdid |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 · ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ) = ( ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) − ( 𝑝 · ( 𝑝 ↑ 2 ) ) ) ) |
| 221 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
| 222 |
221
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 2 ∈ ℕ0 ) |
| 223 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
| 224 |
223
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 1 ∈ ℕ0 ) |
| 225 |
176 222 224
|
expaddd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 ↑ ( 1 + 2 ) ) = ( ( 𝑝 ↑ 1 ) · ( 𝑝 ↑ 2 ) ) ) |
| 226 |
|
1p2e3 |
⊢ ( 1 + 2 ) = 3 |
| 227 |
226
|
a1i |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 1 + 2 ) = 3 ) |
| 228 |
227
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 ↑ ( 1 + 2 ) ) = ( 𝑝 ↑ 3 ) ) |
| 229 |
176
|
exp1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 ↑ 1 ) = 𝑝 ) |
| 230 |
229
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑝 ↑ 1 ) · ( 𝑝 ↑ 2 ) ) = ( 𝑝 · ( 𝑝 ↑ 2 ) ) ) |
| 231 |
225 228 230
|
3eqtr3rd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 · ( 𝑝 ↑ 2 ) ) = ( 𝑝 ↑ 3 ) ) |
| 232 |
231
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) − ( 𝑝 · ( 𝑝 ↑ 2 ) ) ) = ( ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) − ( 𝑝 ↑ 3 ) ) ) |
| 233 |
220 232
|
eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 · ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ) = ( ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) − ( 𝑝 ↑ 3 ) ) ) |
| 234 |
233
|
oveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ) ) = ( ( 𝑞 ↑ 3 ) − ( ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) − ( 𝑝 ↑ 3 ) ) ) ) |
| 235 |
176 179
|
mulcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ∈ ℂ ) |
| 236 |
175 235 189
|
subsub2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) − ( ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) − ( 𝑝 ↑ 3 ) ) ) = ( ( 𝑞 ↑ 3 ) + ( ( 𝑝 ↑ 3 ) − ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) ) ) |
| 237 |
175 189 235
|
addsub12d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) + ( ( 𝑝 ↑ 3 ) − ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) ) = ( ( 𝑝 ↑ 3 ) + ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) ) ) |
| 238 |
175 235
|
subcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) ∈ ℂ ) |
| 239 |
189 238
|
addcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑝 ↑ 3 ) + ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) ) = ( ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) + ( 𝑝 ↑ 3 ) ) ) |
| 240 |
235
|
negcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → - ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ∈ ℂ ) |
| 241 |
175 240
|
addcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) + - ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) = ( - ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) ) |
| 242 |
175 235
|
negsubd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) + - ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) = ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) ) |
| 243 |
176 177 178
|
mul12d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) = ( 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) ) |
| 244 |
243
|
negeqd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → - ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) = - ( 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) ) |
| 245 |
176 178
|
mulcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 · ( 𝑞 ↑ 2 ) ) ∈ ℂ ) |
| 246 |
177 245
|
mulneg1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) = - ( 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) ) |
| 247 |
244 246
|
eqtr4d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → - ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) = ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) ) |
| 248 |
247
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( - ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) = ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) ) |
| 249 |
241 242 248
|
3eqtr3d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) = ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) ) |
| 250 |
249
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) + ( 𝑝 ↑ 3 ) ) = ( ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) + ( 𝑝 ↑ 3 ) ) ) |
| 251 |
239 250
|
eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑝 ↑ 3 ) + ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) ) ) = ( ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) + ( 𝑝 ↑ 3 ) ) ) |
| 252 |
236 237 251
|
3eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) − ( ( 𝑝 · ( 3 · ( 𝑞 ↑ 2 ) ) ) − ( 𝑝 ↑ 3 ) ) ) = ( ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) + ( 𝑝 ↑ 3 ) ) ) |
| 253 |
194 245
|
mulcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) ∈ ℂ ) |
| 254 |
253 175
|
addcld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) ∈ ℂ ) |
| 255 |
254 189
|
addcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) + ( 𝑝 ↑ 3 ) ) = ( ( 𝑝 ↑ 3 ) + ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) ) ) |
| 256 |
234 252 255
|
3eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ) ) = ( ( 𝑝 ↑ 3 ) + ( ( - 3 · ( 𝑝 · ( 𝑞 ↑ 2 ) ) ) + ( 𝑞 ↑ 3 ) ) ) ) |
| 257 |
216 219 256
|
3eqtr4rd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ) ) = ( ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) · ( 𝑞 ↑ 3 ) ) ) |
| 258 |
|
simpr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) |
| 259 |
258
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) · ( 𝑞 ↑ 3 ) ) = ( 0 · ( 𝑞 ↑ 3 ) ) ) |
| 260 |
175
|
mul02d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 0 · ( 𝑞 ↑ 3 ) ) = 0 ) |
| 261 |
257 259 260
|
3eqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( ( 𝑞 ↑ 3 ) − ( 𝑝 · ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ) ) = 0 ) |
| 262 |
175 182 261
|
subeq0d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑞 ↑ 3 ) = ( 𝑝 · ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ) ) |
| 263 |
262
|
ad5ant15 |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑞 ↑ 3 ) = ( 𝑝 · ( ( 3 · ( 𝑞 ↑ 2 ) ) − ( 𝑝 ↑ 2 ) ) ) ) |
| 264 |
172 263
|
breqtrrd |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∥ ( 𝑞 ↑ 3 ) ) |
| 265 |
|
prmdvdsexp |
⊢ ( ( 𝑟 ∈ ℙ ∧ 𝑞 ∈ ℤ ∧ 3 ∈ ℕ ) → ( 𝑟 ∥ ( 𝑞 ↑ 3 ) ↔ 𝑟 ∥ 𝑞 ) ) |
| 266 |
265
|
biimpa |
⊢ ( ( ( 𝑟 ∈ ℙ ∧ 𝑞 ∈ ℤ ∧ 3 ∈ ℕ ) ∧ 𝑟 ∥ ( 𝑞 ↑ 3 ) ) → 𝑟 ∥ 𝑞 ) |
| 267 |
161 156 162 264 266
|
syl31anc |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∥ 𝑞 ) |
| 268 |
|
dvdsgcd |
⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( ( 𝑟 ∥ 𝑝 ∧ 𝑟 ∥ 𝑞 ) → 𝑟 ∥ ( 𝑝 gcd 𝑞 ) ) ) |
| 269 |
268
|
imp |
⊢ ( ( ( 𝑟 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ ( 𝑟 ∥ 𝑝 ∧ 𝑟 ∥ 𝑞 ) ) → 𝑟 ∥ ( 𝑝 gcd 𝑞 ) ) |
| 270 |
152 154 156 160 267 269
|
syl32anc |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∥ ( 𝑝 gcd 𝑞 ) ) |
| 271 |
|
simp-6r |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → ( 𝑝 gcd 𝑞 ) = 1 ) |
| 272 |
270 271
|
breqtrd |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 ∥ 1 ) |
| 273 |
|
dvds1 |
⊢ ( 𝑟 ∈ ℕ0 → ( 𝑟 ∥ 1 ↔ 𝑟 = 1 ) ) |
| 274 |
273
|
biimpa |
⊢ ( ( 𝑟 ∈ ℕ0 ∧ 𝑟 ∥ 1 ) → 𝑟 = 1 ) |
| 275 |
151 272 274
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) ∧ ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) = 0 ) → 𝑟 = 1 ) |
| 276 |
148 275
|
mteqand |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑟 ∥ ( abs ‘ 𝑝 ) ) → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ≠ 0 ) |
| 277 |
|
nnabscl |
⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑝 ≠ 0 ) → ( abs ‘ 𝑝 ) ∈ ℕ ) |
| 278 |
153 108 277
|
syl2anc |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ 𝑝 ) ∈ ℕ ) |
| 279 |
|
eluz2b3 |
⊢ ( ( abs ‘ 𝑝 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( abs ‘ 𝑝 ) ∈ ℕ ∧ ( abs ‘ 𝑝 ) ≠ 1 ) ) |
| 280 |
|
exprmfct |
⊢ ( ( abs ‘ 𝑝 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑟 ∈ ℙ 𝑟 ∥ ( abs ‘ 𝑝 ) ) |
| 281 |
279 280
|
sylbir |
⊢ ( ( ( abs ‘ 𝑝 ) ∈ ℕ ∧ ( abs ‘ 𝑝 ) ≠ 1 ) → ∃ 𝑟 ∈ ℙ 𝑟 ∥ ( abs ‘ 𝑝 ) ) |
| 282 |
278 281
|
sylan |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) → ∃ 𝑟 ∈ ℙ 𝑟 ∥ ( abs ‘ 𝑝 ) ) |
| 283 |
276 282
|
r19.29a |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) ∧ ( abs ‘ 𝑝 ) ≠ 1 ) → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ≠ 0 ) |
| 284 |
143 283
|
pm2.61dane |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ∧ 𝑋 ≠ 0 ) → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ≠ 0 ) |
| 285 |
22 284
|
pm2.61dane |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ 𝑋 = ( 𝑝 / 𝑞 ) ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ≠ 0 ) |
| 286 |
285
|
anasss |
⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℤ ) ∧ 𝑞 ∈ ℕ ) ∧ ( 𝑋 = ( 𝑝 / 𝑞 ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ) → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ≠ 0 ) |
| 287 |
|
elq2 |
⊢ ( 𝑋 ∈ ℚ → ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ ( 𝑋 = ( 𝑝 / 𝑞 ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ) |
| 288 |
1 287
|
syl |
⊢ ( 𝜑 → ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ ( 𝑋 = ( 𝑝 / 𝑞 ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ) |
| 289 |
286 288
|
r19.29vva |
⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · 𝑋 ) + 1 ) ) ≠ 0 ) |