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

Metamath Proof Explorer

Theorem cos9thpiminplylem2

Proof