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