Metamath Proof Explorer

Theorem cos9thpiminplylem2

Description: The polynomial ( ( X ^ 3 ) + ( ( -u 3 x. X ) + 1 ) ) has no rational roots. (Contributed by Thierry Arnoux, 9-Nov-2025)

Ref Expression
Hypothesis cos9thpiminplylem2.1 
|- ( ph -> X e. QQ )
Assertion cos9thpiminplylem2 
|- ( ph -> ( ( X ^ 3 ) + ( ( -u 3 x. X ) + 1 ) ) =/= 0 )

Proof

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