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	$⊢ φ \to X \in ℚ$
	Assertion	cos9thpiminplylem2	$⊢ φ \to X^{3} + -3 X + 1 \neq 0$

Proof

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

Metamath Proof Explorer

Theorem cos9thpiminplylem2

Proof