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 65 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> 3 = ( 2 + 1 ) )
67 63 43 66 mvrladdd 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> ( 3 - 2 ) = 1 )
68 67 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 ) )
69 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 ) ) )
70 34 exp1d 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> ( X ^ 1 ) = X )
71 68 69 70 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 )
72 59 62 71 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 )
73 72 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 ) )
74 73 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 ) )
75 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 ) ) ) )
76 10 a1i 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> 3 e. CC )
77 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 )
78 76 77 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 ) ) ) )
79 75 78 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 ) ) ) )
80 76 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 ) )
81 74 79 80 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 ) )
82 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 ) )
83 81 82 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 ) ) )
84 42 47 43 83 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 ) ) )
85 55 84 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 ) ) ) )
86 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 )
87 86 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 )
88 43 87 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 ) )
89 86 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 ) ) )
90 89 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 ) )
91 47 86 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 ) ) )
92 88 90 91 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 ) ) )
93 48 85 92 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 ) ) )
94 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 )
95 simpllr 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> X = ( p / q ) )
96 95 adantr 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> X = ( p / q ) )
97 96 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 ) ) )
98 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> p e. ZZ )
99 98 zcnd 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> p e. CC )
100 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> q e. NN )
101 100 nncnd 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> q e. CC )
102 simpr 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> X =/= 0 )
103 95 102 eqnetrrd 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> ( p / q ) =/= 0 )
104 25 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> p e. CC )
105 28 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> q e. CC )
106 30 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> q =/= 0 )
107 104 105 106 divne0bd 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> ( p =/= 0 <-> ( p / q ) =/= 0 ) )
108 103 107 mpbird 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> p =/= 0 )
109 108 adantr 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> p =/= 0 )
110 100 nnne0d 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> q =/= 0 )
111 99 101 109 110 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 ) )
112 101 99 109 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 ) ) )
113 99 div1d 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> ( p / 1 ) = p )
114 simpr 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> ( abs ` p ) = 1 )
115 114 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 ) )
116 24 zred 
 |-  ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) -> p e. RR )
117 116 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> p e. RR )
118 117 108 receqid 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> ( ( 1 / p ) = p <-> ( abs ` p ) = 1 ) )
119 118 biimpar 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> ( 1 / p ) = p )
120 113 115 119 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 ) )
121 120 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 ) ) )
122 112 121 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 ) ) ) )
123 97 111 122 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 ) ) ) )
124 98 zred 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> p e. RR )
125 sgnval2 
 |-  ( ( p e. RR /\ p =/= 0 ) -> ( sgn ` p ) = ( p / ( abs ` p ) ) )
126 124 109 125 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 ) ) )
127 126 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 ) ) ) )
128 123 127 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 ) ) )
129 100 nnzd 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> q e. ZZ )
130 neg1z 
 |-  -u 1 e. ZZ
131 130 a1i 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> -u 1 e. ZZ )
132 0zd 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> 0 e. ZZ )
133 1zzd 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> 1 e. ZZ )
134 131 132 133 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 )
135 124 rexrd 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> p e. RR* )
136 sgncl 
 |-  ( p e. RR* -> ( sgn ` p ) e. { -u 1 , 0 , 1 } )
137 135 136 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 } )
138 134 137 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> ( sgn ` p ) e. ZZ )
139 129 138 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 )
140 128 139 eqeltrd 
 |-  ( ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) /\ ( abs ` p ) = 1 ) -> ( 1 / X ) e. ZZ )
141 140 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 )
142 94 47 141 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 )
143 93 142 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 )
144 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 )
145 1nprm 
 |-  -. 1 e. Prime
146 145 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 )
147 nelne2 
 |-  ( ( r e. Prime /\ -. 1 e. Prime ) -> r =/= 1 )
148 144 146 147 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 )
149 prmnn 
 |-  ( r e. Prime -> r e. NN )
150 149 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 )
151 150 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 )
152 150 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 )
153 simp-5r 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> p e. ZZ )
154 153 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 )
155 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 )
156 155 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 )
157 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 ) )
158 dvdsabsb 
 |-  ( ( r e. ZZ /\ p e. ZZ ) -> ( r || p <-> r || ( abs ` p ) ) )
159 158 biimpar 
 |-  ( ( ( r e. ZZ /\ p e. ZZ ) /\ r || ( abs ` p ) ) -> r || p )
160 152 154 157 159 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 )
161 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 )
162 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 )
163 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 )
164 155 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 )
165 nn0sqcl 
 |-  ( q e. NN0 -> ( q ^ 2 ) e. NN0 )
166 164 165 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 )
167 166 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 )
168 163 167 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 )
169 zsqcl 
 |-  ( p e. ZZ -> ( p ^ 2 ) e. ZZ )
170 154 169 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 )
171 168 170 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 )
172 152 154 171 160 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 ) ) ) )
173 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 e. CC )
174 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 )
175 173 174 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 )
176 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 ) -> p e. CC )
177 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 )
178 173 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 )
179 177 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 ) -> ( 3 x. ( q ^ 2 ) ) e. CC )
180 176 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 )
181 179 180 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 )
182 176 181 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 )
183 95 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 ) )
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 ) = ( ( p / q ) ^ 3 ) )
185 184 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 ) ) )
186 106 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 )
187 176 173 186 174 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 ) ) )
188 187 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 ) ) )
189 176 174 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 )
190 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 )
191 173 186 190 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 )
192 189 175 191 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 ) )
193 185 188 192 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 ) )
194 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 )
195 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 )
196 194 195 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 )
197 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 )
198 194 195 175 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 ) ) ) )
199 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 x. ( q ^ 3 ) ) = ( ( p / q ) x. ( q ^ 3 ) ) )
200 176 173 175 186 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 ) ) )
201 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 )
202 173 186 201 190 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 ) ) )
203 3m1e2 
 |-  ( 3 - 1 ) = 2
204 203 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 )
205 204 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 ) )
206 173 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 )
207 206 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 ) )
208 202 205 207 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 ) )
209 208 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 ) ) )
210 199 200 209 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 ) ) )
211 210 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 ) ) ) )
212 198 211 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 ) ) ) )
213 175 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 ) )
214 212 213 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 ) ) )
215 196 175 197 214 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 ) ) )
216 193 215 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 ) ) ) )
217 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 )
218 196 197 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 )
219 217 218 175 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 ) ) ) )
220 176 179 180 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 ) ) ) )
221 2nn0 
 |-  2 e. NN0
222 221 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 )
223 1nn0 
 |-  1 e. NN0
224 223 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 )
225 176 222 224 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 ) ) )
226 1p2e3 
 |-  ( 1 + 2 ) = 3
227 226 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 )
228 227 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 ) )
229 176 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 )
230 229 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 ) ) )
231 225 228 230 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 ) )
232 231 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 ) ) )
233 220 232 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 ) ) )
234 233 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 ) ) ) )
235 176 179 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 )
236 175 235 189 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 ) ) ) ) ) )
237 175 189 235 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 ) ) ) ) ) )
238 175 235 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 )
239 189 238 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 ) ) )
240 235 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 )
241 175 240 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 ) ) )
242 175 235 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 ) ) ) ) )
243 176 177 178 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 ) ) ) )
244 243 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 ) ) ) )
245 176 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. ( q ^ 2 ) ) e. CC )
246 177 245 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 ) ) ) )
247 244 246 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 ) ) ) )
248 247 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 ) ) )
249 241 242 248 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 ) ) )
250 249 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 ) ) )
251 239 250 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 ) ) )
252 236 237 251 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 ) ) )
253 194 245 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 )
254 253 175 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 )
255 254 189 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 ) ) ) )
256 234 252 255 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 ) ) ) )
257 216 219 256 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 ) ) )
258 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 )
259 258 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 ) ) )
260 175 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 )
261 257 259 260 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 )
262 175 182 261 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 ) ) ) )
263 262 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 ) ) ) )
264 172 263 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 ) )
265 prmdvdsexp 
 |-  ( ( r e. Prime /\ q e. ZZ /\ 3 e. NN ) -> ( r || ( q ^ 3 ) <-> r || q ) )
266 265 biimpa 
 |-  ( ( ( r e. Prime /\ q e. ZZ /\ 3 e. NN ) /\ r || ( q ^ 3 ) ) -> r || q )
267 161 156 162 264 266 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 )
268 dvdsgcd 
 |-  ( ( r e. ZZ /\ p e. ZZ /\ q e. ZZ ) -> ( ( r || p /\ r || q ) -> r || ( p gcd q ) ) )
269 268 imp 
 |-  ( ( ( r e. ZZ /\ p e. ZZ /\ q e. ZZ ) /\ ( r || p /\ r || q ) ) -> r || ( p gcd q ) )
270 152 154 156 160 267 269 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 ) )
271 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 )
272 270 271 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 )
273 dvds1 
 |-  ( r e. NN0 -> ( r || 1 <-> r = 1 ) )
274 273 biimpa 
 |-  ( ( r e. NN0 /\ r || 1 ) -> r = 1 )
275 151 272 274 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 )
276 148 275 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 )
277 nnabscl 
 |-  ( ( p e. ZZ /\ p =/= 0 ) -> ( abs ` p ) e. NN )
278 153 108 277 syl2anc 
 |-  ( ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) /\ X =/= 0 ) -> ( abs ` p ) e. NN )
279 eluz2b3 
 |-  ( ( abs ` p ) e. ( ZZ>= ` 2 ) <-> ( ( abs ` p ) e. NN /\ ( abs ` p ) =/= 1 ) )
280 exprmfct 
 |-  ( ( abs ` p ) e. ( ZZ>= ` 2 ) -> E. r e. Prime r || ( abs ` p ) )
281 279 280 sylbir 
 |-  ( ( ( abs ` p ) e. NN /\ ( abs ` p ) =/= 1 ) -> E. r e. Prime r || ( abs ` p ) )
282 278 281 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 ) )
283 276 282 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 )
284 143 283 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 )
285 22 284 pm2.61dane 
 |-  ( ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ X = ( p / q ) ) /\ ( p gcd q ) = 1 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. X ) + 1 ) ) =/= 0 )
286 285 anasss 
 |-  ( ( ( ( ph /\ p e. ZZ ) /\ q e. NN ) /\ ( X = ( p / q ) /\ ( p gcd q ) = 1 ) ) -> ( ( X ^ 3 ) + ( ( -u 3 x. X ) + 1 ) ) =/= 0 )
287 elq2 
 |-  ( X e. QQ -> E. p e. ZZ E. q e. NN ( X = ( p / q ) /\ ( p gcd q ) = 1 ) )
288 1 287 syl 
 |-  ( ph -> E. p e. ZZ E. q e. NN ( X = ( p / q ) /\ ( p gcd q ) = 1 ) )
289 286 288 r19.29vva 
 |-  ( ph -> ( ( X ^ 3 ) + ( ( -u 3 x. X ) + 1 ) ) =/= 0 )