cos9thpiminplylem2 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cos9thpiminplylem2		Structured version Visualization version GIF version

Theorem cos9thpiminplylem2 34415

Description: The polynomial ((𝑋↑3) + (( -3 · 𝑋) + 1)) has no rational roots. (Contributed by Thierry Arnoux, 9-Nov-2025.)

**Hypothesis**
Ref	Expression
cos9thpiminplylem2.1	⊢ (𝜑 → 𝑋 ∈ ℚ)

**Assertion**
Ref	Expression
cos9thpiminplylem2	⊢ (𝜑 → ((𝑋↑3) + (( -3 · 𝑋) + 1)) ≠ 0)

Proof of Theorem cos9thpiminplylem2 Dummy variables 𝑝 𝑞 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 490	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → 𝑋 = 0)
2	1	oveq1d 7435	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → (𝑋↑3) = (0↑3))
3		3nn 12422	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
4	3	a1i 11	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → 3 ∈ ℕ)
5	4	0expd 14282	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → (0↑3) = 0)
6	2, 5	eqtrd 2796	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → (𝑋↑3) = 0)
7	6	oveq1d 7435	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → ((𝑋↑3) + (( -3 · 𝑋) + 1)) = (0 + (( -3 · 𝑋) + 1)))
8	1	oveq2d 7436	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → ( -3 · 𝑋) = ( -3 · 0))
9		3cn 12424	. . . . . . . . . . 11 ⊢ 3 ∈ ℂ
10	9	negcli 11626	. . . . . . . . . 10 ⊢ -3 ∈ ℂ
11	10	a1i 11	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → -3 ∈ ℂ)
12	11	mul01d 11509	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → ( -3 · 0) = 0)
13	8, 12	eqtr2d 2797	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → 0 = ( -3 · 𝑋))
14	13	oveq1d 7435	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → (0 + 1) = (( -3 · 𝑋) + 1))
15		0p1e1 12463	. . . . . . . 8 ⊢ (0 + 1) = 1
16	14, 15	eqtr3di 2811	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → (( -3 · 𝑋) + 1) = 1)
17	13, 16	oveq12d 7438	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → (0 + (( -3 · 𝑋) + 1)) = (( -3 · 𝑋) + 1))
18	7, 17, 16	3eqtrd 2800	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 1)
19		ax-1ne0 11269	. . . . . 6 ⊢ 1 ≠ 0
20	19	a1i 11	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → 1 ≠ 0)
21	18, 20	eqnetrd 3023	. . . 4 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 = 0) → ((𝑋↑3) + (( -3 · 𝑋) + 1)) ≠ 0)
22		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) → 𝑋 = (𝑝 / 𝑞))
23		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) → 𝑝 ∈ ℤ)
24	23	zcnd 12804	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) → 𝑝 ∈ ℂ)
25	24	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) → 𝑝 ∈ ℂ)
26		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) → 𝑞 ∈ ℕ)
27	26	nncnd 12351	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) → 𝑞 ∈ ℂ)
28	27	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) → 𝑞 ∈ ℂ)
29	26	nnne0d 12388	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) → 𝑞 ≠ 0)
30	29	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) → 𝑞 ≠ 0)
31	25, 28, 30	divcld 12093	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) → (𝑝 / 𝑞) ∈ ℂ)
32	22, 31	eqeltrd 2861	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) → 𝑋 ∈ ℂ)
33	32	ad3antrrr 743	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑋 ∈ ℂ)
34		simplr 781	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑋 ≠ 0)
35	33, 34	reccld 12086	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (1 / 𝑋) ∈ ℂ)
36		3nn0 12624	. . . . . . . . . 10 ⊢ 3 ∈ ℕ₀
37	36	a1i 11	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 3 ∈ ℕ₀)
38	35, 37	expcld 14289	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((1 / 𝑋)↑3) ∈ ℂ)
39	10	a1i 11	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → -3 ∈ ℂ)
40	35	sqcld 14287	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((1 / 𝑋)↑2) ∈ ℂ)
41	39, 40	mulcld 11329	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ( -3 · ((1 / 𝑋)↑2)) ∈ ℂ)
42		1cnd 11302	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 1 ∈ ℂ)
43	41, 42	addcld 11328	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (( -3 · ((1 / 𝑋)↑2)) + 1) ∈ ℂ)
44	36	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) → 3 ∈ ℕ₀)
45	32, 44	expcld 14289	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) → (𝑋↑3) ∈ ℂ)
46	45	ad3antrrr 743	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑋↑3) ∈ ℂ)
47	38, 43, 46	adddird 11334	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((((1 / 𝑋)↑3) + (( -3 · ((1 / 𝑋)↑2)) + 1)) · (𝑋↑3)) = ((((1 / 𝑋)↑3) · (𝑋↑3)) + ((( -3 · ((1 / 𝑋)↑2)) + 1) · (𝑋↑3))))
48		3z 12729	. . . . . . . . . . . 12 ⊢ 3 ∈ ℤ
49	48	a1i 11	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 3 ∈ ℤ)
50	33, 34, 49	exprecd 14297	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((1 / 𝑋)↑3) = (1 / (𝑋↑3)))
51	50	oveq1d 7435	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (((1 / 𝑋)↑3) · (𝑋↑3)) = ((1 / (𝑋↑3)) · (𝑋↑3)))
52	33, 34, 49	expne0d 14295	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑋↑3) ≠ 0)
53	46, 52	recid2d 12089	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((1 / (𝑋↑3)) · (𝑋↑3)) = 1)
54	51, 53	eqtrd 2796	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (((1 / 𝑋)↑3) · (𝑋↑3)) = 1)
55		2z 12728	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℤ
56	55	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 2 ∈ ℤ)
57	33, 34, 56	exprecd 14297	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((1 / 𝑋)↑2) = (1 / (𝑋↑2)))
58	57	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (((1 / 𝑋)↑2) · (𝑋↑3)) = ((1 / (𝑋↑2)) · (𝑋↑3)))
59	33	sqcld 14287	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑋↑2) ∈ ℂ)
60	33, 34, 56	expne0d 14295	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑋↑2) ≠ 0)
61	46, 59, 60	divrec2d 12097	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((𝑋↑3) / (𝑋↑2)) = ((1 / (𝑋↑2)) · (𝑋↑3)))
62		2cnd 12421	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 2 ∈ ℂ)
63		2p1e3 12484	. . . . . . . . . . . . . . . . . 18 ⊢ (2 + 1) = 3
64	63	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (2 + 1) = 3)
65	62, 42, 64	mvlladdcd 11726	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (3 − 2) = 1)
66	65	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑋↑(3 − 2)) = (𝑋↑1))
67	33, 34, 56, 49	expsubd 14300	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑋↑(3 − 2)) = ((𝑋↑3) / (𝑋↑2)))
68	33	exp1d 14284	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑋↑1) = 𝑋)
69	66, 67, 68	3eqtr3d 2804	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((𝑋↑3) / (𝑋↑2)) = 𝑋)
70	58, 61, 69	3eqtr2d 2802	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (((1 / 𝑋)↑2) · (𝑋↑3)) = 𝑋)
71	70	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (3 · (((1 / 𝑋)↑2) · (𝑋↑3))) = (3 · 𝑋))
72	71	negeqd 11551	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → -(3 · (((1 / 𝑋)↑2) · (𝑋↑3))) = -(3 · 𝑋))
73	39, 40, 46	mulassd 11332	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (( -3 · ((1 / 𝑋)↑2)) · (𝑋↑3)) = ( -3 · (((1 / 𝑋)↑2) · (𝑋↑3))))
74	9	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 3 ∈ ℂ)
75	40, 46	mulcld 11329	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (((1 / 𝑋)↑2) · (𝑋↑3)) ∈ ℂ)
76	74, 75	mulneg1d 11769	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ( -3 · (((1 / 𝑋)↑2) · (𝑋↑3))) = -(3 · (((1 / 𝑋)↑2) · (𝑋↑3))))
77	73, 76	eqtrd 2796	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (( -3 · ((1 / 𝑋)↑2)) · (𝑋↑3)) = -(3 · (((1 / 𝑋)↑2) · (𝑋↑3))))
78	74, 33	mulneg1d 11769	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ( -3 · 𝑋) = -(3 · 𝑋))
79	72, 77, 78	3eqtr4d 2806	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (( -3 · ((1 / 𝑋)↑2)) · (𝑋↑3)) = ( -3 · 𝑋))
80	46	mullidd 11327	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (1 · (𝑋↑3)) = (𝑋↑3))
81	79, 80	oveq12d 7438	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((( -3 · ((1 / 𝑋)↑2)) · (𝑋↑3)) + (1 · (𝑋↑3))) = (( -3 · 𝑋) + (𝑋↑3)))
82	41, 46, 42, 81	joinlmuladdmuld 11336	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((( -3 · ((1 / 𝑋)↑2)) + 1) · (𝑋↑3)) = (( -3 · 𝑋) + (𝑋↑3)))
83	54, 82	oveq12d 7438	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((((1 / 𝑋)↑3) · (𝑋↑3)) + ((( -3 · ((1 / 𝑋)↑2)) + 1) · (𝑋↑3))) = (1 + (( -3 · 𝑋) + (𝑋↑3))))
84	39, 33	mulcld 11329	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ( -3 · 𝑋) ∈ ℂ)
85	84, 46	addcld 11328	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (( -3 · 𝑋) + (𝑋↑3)) ∈ ℂ)
86	42, 85	addcomd 11512	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (1 + (( -3 · 𝑋) + (𝑋↑3))) = ((( -3 · 𝑋) + (𝑋↑3)) + 1))
87	84, 46	addcomd 11512	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (( -3 · 𝑋) + (𝑋↑3)) = ((𝑋↑3) + ( -3 · 𝑋)))
88	87	oveq1d 7435	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((( -3 · 𝑋) + (𝑋↑3)) + 1) = (((𝑋↑3) + ( -3 · 𝑋)) + 1))
89	46, 84, 42	addassd 11331	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (((𝑋↑3) + ( -3 · 𝑋)) + 1) = ((𝑋↑3) + (( -3 · 𝑋) + 1)))
90	86, 88, 89	3eqtrd 2800	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (1 + (( -3 · 𝑋) + (𝑋↑3))) = ((𝑋↑3) + (( -3 · 𝑋) + 1)))
91	47, 83, 90	3eqtrd 2800	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((((1 / 𝑋)↑3) + (( -3 · ((1 / 𝑋)↑2)) + 1)) · (𝑋↑3)) = ((𝑋↑3) + (( -3 · 𝑋) + 1)))
92	38, 43	addcld 11328	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (((1 / 𝑋)↑3) + (( -3 · ((1 / 𝑋)↑2)) + 1)) ∈ ℂ)
93		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → 𝑋 = (𝑝 / 𝑞))
94	93	adantr 486	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑋 = (𝑝 / 𝑞))
95	94	oveq2d 7436	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (1 / 𝑋) = (1 / (𝑝 / 𝑞)))
96		simp-6r 800	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑝 ∈ ℤ)
97	96	zcnd 12804	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑝 ∈ ℂ)
98		simp-5r 798	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑞 ∈ ℕ)
99	98	nncnd 12351	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑞 ∈ ℂ)
100		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → 𝑋 ≠ 0)
101	93, 100	eqnetrrd 3024	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → (𝑝 / 𝑞) ≠ 0)
102	24	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → 𝑝 ∈ ℂ)
103	27	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → 𝑞 ∈ ℂ)
104	29	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → 𝑞 ≠ 0)
105	102, 103, 104	divne0bd 12105	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → (𝑝 ≠ 0 ↔ (𝑝 / 𝑞) ≠ 0))
106	101, 105	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → 𝑝 ≠ 0)
107	106	adantr 486	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑝 ≠ 0)
108	98	nnne0d 12388	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑞 ≠ 0)
109	97, 99, 107, 108	recdivd 12110	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (1 / (𝑝 / 𝑞)) = (𝑞 / 𝑝))
110	99, 97, 107	divrecd 12096	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑞 / 𝑝) = (𝑞 · (1 / 𝑝)))
111	97	div1d 12085	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑝 / 1) = 𝑝)
112		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (abs‘𝑝) = 1)
113	112	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑝 / (abs‘𝑝)) = (𝑝 / 1))
114	23	zred 12803	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) → 𝑝 ∈ ℝ)
115	114	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → 𝑝 ∈ ℝ)
116	115, 106	receqid 33336	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → ((1 / 𝑝) = 𝑝 ↔ (abs‘𝑝) = 1))
117	116	biimpar 483	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (1 / 𝑝) = 𝑝)
118	111, 113, 117	3eqtr4d 2806	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑝 / (abs‘𝑝)) = (1 / 𝑝))
119	118	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑞 · (𝑝 / (abs‘𝑝))) = (𝑞 · (1 / 𝑝)))
120	110, 119	eqtr4d 2799	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑞 / 𝑝) = (𝑞 · (𝑝 / (abs‘𝑝))))
121	95, 109, 120	3eqtrd 2800	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (1 / 𝑋) = (𝑞 · (𝑝 / (abs‘𝑝))))
122	96	zred 12803	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑝 ∈ ℝ)
123		sgnval2 33327	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ ℝ ∧ 𝑝 ≠ 0) → (sgn‘𝑝) = (𝑝 / (abs‘𝑝)))
124	122, 107, 123	syl2anc 596	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (sgn‘𝑝) = (𝑝 / (abs‘𝑝)))
125	124	oveq2d 7436	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑞 · (sgn‘𝑝)) = (𝑞 · (𝑝 / (abs‘𝑝))))
126	121, 125	eqtr4d 2799	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (1 / 𝑋) = (𝑞 · (sgn‘𝑝)))
127	98	nnzd 12719	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑞 ∈ ℤ)
128		neg1z 12732	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℤ
129	128	a1i 11	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → -1 ∈ ℤ)
130		0zd 12705	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 0 ∈ ℤ)
131		1zzd 12727	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 1 ∈ ℤ)
132	129, 130, 131	tpssd 33134	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → { -1, 0, 1} ⊆ ℤ)
133	122	rexrd 11359	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → 𝑝 ∈ ℝ^*)
134		sgncl 15250	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℝ^* → (sgn‘𝑝) ∈ { -1, 0, 1})
135	133, 134	syl 18	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (sgn‘𝑝) ∈ { -1, 0, 1})
136	132, 135	sseldd 3932	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (sgn‘𝑝) ∈ ℤ)
137	127, 136	zmulcld 12809	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (𝑞 · (sgn‘𝑝)) ∈ ℤ)
138	126, 137	eqeltrd 2861	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (1 / 𝑋) ∈ ℤ)
139	138	cos9thpiminplylem1 34414	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → (((1 / 𝑋)↑3) + (( -3 · ((1 / 𝑋)↑2)) + 1)) ≠ 0)
140	92, 46, 139, 52	mulne0d 11968	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((((1 / 𝑋)↑3) + (( -3 · ((1 / 𝑋)↑2)) + 1)) · (𝑋↑3)) ≠ 0)
141	91, 140	eqnetrrd 3024	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) = 1) → ((𝑋↑3) + (( -3 · 𝑋) + 1)) ≠ 0)
142		simplr 781	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) → 𝑟 ∈ ℙ)
143		1nprm 16854	. . . . . . . . 9 ⊢ ¬ 1 ∈ ℙ
144	143	a1i 11	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) → ¬ 1 ∈ ℙ)
145		nelne2 3054	. . . . . . . 8 ⊢ ((𝑟 ∈ ℙ ∧ ¬ 1 ∈ ℙ) → 𝑟 ≠ 1)
146	142, 144, 145	syl2anc 596	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) → 𝑟 ≠ 1)
147		prmnn 16849	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℙ → 𝑟 ∈ ℕ)
148	147	ad3antlr 744	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∈ ℕ)
149	148	nnnn0d 12667	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∈ ℕ₀)
150	148	nnzd 12719	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∈ ℤ)
151		simp-5r 798	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → 𝑝 ∈ ℤ)
152	151	ad4antr 745	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑝 ∈ ℤ)
153		simp-8r 804	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑞 ∈ ℕ)
154	153	nnzd 12719	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑞 ∈ ℤ)
155		simplr 781	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∥ (abs‘𝑝))
156		dvdsabsb 16445	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ ℤ ∧ 𝑝 ∈ ℤ) → (𝑟 ∥ 𝑝 ↔ 𝑟 ∥ (abs‘𝑝)))
157	156	biimpar 483	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ ℤ ∧ 𝑝 ∈ ℤ) ∧ 𝑟 ∥ (abs‘𝑝)) → 𝑟 ∥ 𝑝)
158	150, 152, 155, 157	syl21anc 851	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∥ 𝑝)
159		simpllr 788	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∈ ℙ)
160	3	a1i 11	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 3 ∈ ℕ)
161	48	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 3 ∈ ℤ)
162	153	nnnn0d 12667	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑞 ∈ ℕ₀)
163		nn0sqcl 14232	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ ℕ₀ → (𝑞↑2) ∈ ℕ₀)
164	162, 163	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑞↑2) ∈ ℕ₀)
165	164	nn0zd 12718	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑞↑2) ∈ ℤ)
166	161, 165	zmulcld 12809	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (3 · (𝑞↑2)) ∈ ℤ)
167		zsqcl 14272	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℤ → (𝑝↑2) ∈ ℤ)
168	152, 167	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝↑2) ∈ ℤ)
169	166, 168	zsubcld 12808	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((3 · (𝑞↑2)) − (𝑝↑2)) ∈ ℤ)
170	150, 152, 169, 158	dvdsmultr1d 16467	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∥ (𝑝 · ((3 · (𝑞↑2)) − (𝑝↑2))))
171	103	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑞 ∈ ℂ)
172	36	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 3 ∈ ℕ₀)
173	171, 172	expcld 14289	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑞↑3) ∈ ℂ)
174	102	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑝 ∈ ℂ)
175	9	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 3 ∈ ℂ)
176	171	sqcld 14287	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑞↑2) ∈ ℂ)
177	175, 176	mulcld 11329	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (3 · (𝑞↑2)) ∈ ℂ)
178	174	sqcld 14287	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝↑2) ∈ ℂ)
179	177, 178	subcld 11669	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((3 · (𝑞↑2)) − (𝑝↑2)) ∈ ℂ)
180	174, 179	mulcld 11329	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝 · ((3 · (𝑞↑2)) − (𝑝↑2))) ∈ ℂ)
181	93	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑋 = (𝑝 / 𝑞))
182	181	oveq1d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑋↑3) = ((𝑝 / 𝑞)↑3))
183	182	oveq1d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑋↑3) · (𝑞↑3)) = (((𝑝 / 𝑞)↑3) · (𝑞↑3)))
184	104	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑞 ≠ 0)
185	174, 171, 184, 172	expdivd 14303	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑝 / 𝑞)↑3) = ((𝑝↑3) / (𝑞↑3)))
186	185	oveq1d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (((𝑝 / 𝑞)↑3) · (𝑞↑3)) = (((𝑝↑3) / (𝑞↑3)) · (𝑞↑3)))
187	174, 172	expcld 14289	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝↑3) ∈ ℂ)
188	48	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 3 ∈ ℤ)
189	171, 184, 188	expne0d 14295	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑞↑3) ≠ 0)
190	187, 173, 189	divcan1d 12094	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (((𝑝↑3) / (𝑞↑3)) · (𝑞↑3)) = (𝑝↑3))
191	183, 186, 190	3eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑋↑3) · (𝑞↑3)) = (𝑝↑3))
192	10	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → -3 ∈ ℂ)
193	32	ad3antrrr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑋 ∈ ℂ)
194	192, 193	mulcld 11329	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ( -3 · 𝑋) ∈ ℂ)
195		1cnd 11302	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 1 ∈ ℂ)
196	192, 193, 173	mulassd 11332	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (( -3 · 𝑋) · (𝑞↑3)) = ( -3 · (𝑋 · (𝑞↑3))))
197	181	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑋 · (𝑞↑3)) = ((𝑝 / 𝑞) · (𝑞↑3)))
198	174, 171, 173, 184	div32d 12116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑝 / 𝑞) · (𝑞↑3)) = (𝑝 · ((𝑞↑3) / 𝑞)))
199		1zzd 12727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 1 ∈ ℤ)
200	171, 184, 199, 188	expsubd 14300	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑞↑(3 − 1)) = ((𝑞↑3) / (𝑞↑1)))
201		3m1e2 12470	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (3 − 1) = 2
202	201	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (3 − 1) = 2)
203	202	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑞↑(3 − 1)) = (𝑞↑2))
204	171	exp1d 14284	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑞↑1) = 𝑞)
205	204	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) / (𝑞↑1)) = ((𝑞↑3) / 𝑞))
206	200, 203, 205	3eqtr3rd 2805	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) / 𝑞) = (𝑞↑2))
207	206	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝 · ((𝑞↑3) / 𝑞)) = (𝑝 · (𝑞↑2)))
208	197, 198, 207	3eqtrd 2800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑋 · (𝑞↑3)) = (𝑝 · (𝑞↑2)))
209	208	oveq2d 7436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ( -3 · (𝑋 · (𝑞↑3))) = ( -3 · (𝑝 · (𝑞↑2))))
210	196, 209	eqtrd 2796	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (( -3 · 𝑋) · (𝑞↑3)) = ( -3 · (𝑝 · (𝑞↑2))))
211	173	mullidd 11327	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (1 · (𝑞↑3)) = (𝑞↑3))
212	210, 211	oveq12d 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((( -3 · 𝑋) · (𝑞↑3)) + (1 · (𝑞↑3))) = (( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3)))
213	194, 173, 195, 212	joinlmuladdmuld 11336	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((( -3 · 𝑋) + 1) · (𝑞↑3)) = (( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3)))
214	191, 213	oveq12d 7438	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (((𝑋↑3) · (𝑞↑3)) + ((( -3 · 𝑋) + 1) · (𝑞↑3))) = ((𝑝↑3) + (( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3))))
215	45	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑋↑3) ∈ ℂ)
216	194, 195	addcld 11328	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (( -3 · 𝑋) + 1) ∈ ℂ)
217	215, 216, 173	adddird 11334	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (((𝑋↑3) + (( -3 · 𝑋) + 1)) · (𝑞↑3)) = (((𝑋↑3) · (𝑞↑3)) + ((( -3 · 𝑋) + 1) · (𝑞↑3))))
218	174, 177, 178	subdid 11772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝 · ((3 · (𝑞↑2)) − (𝑝↑2))) = ((𝑝 · (3 · (𝑞↑2))) − (𝑝 · (𝑝↑2))))
219		2nn0 12623	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℕ₀
220	219	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 2 ∈ ℕ₀)
221		1nn0 12622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℕ₀
222	221	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 1 ∈ ℕ₀)
223	174, 220, 222	expaddd 14291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝↑(1 + 2)) = ((𝑝↑1) · (𝑝↑2)))
224		1p2e3 12485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 + 2) = 3
225	224	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (1 + 2) = 3)
226	225	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝↑(1 + 2)) = (𝑝↑3))
227	174	exp1d 14284	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝↑1) = 𝑝)
228	227	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑝↑1) · (𝑝↑2)) = (𝑝 · (𝑝↑2)))
229	223, 226, 228	3eqtr3rd 2805	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝 · (𝑝↑2)) = (𝑝↑3))
230	229	oveq2d 7436	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑝 · (3 · (𝑞↑2))) − (𝑝 · (𝑝↑2))) = ((𝑝 · (3 · (𝑞↑2))) − (𝑝↑3)))
231	218, 230	eqtrd 2796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝 · ((3 · (𝑞↑2)) − (𝑝↑2))) = ((𝑝 · (3 · (𝑞↑2))) − (𝑝↑3)))
232	231	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) − (𝑝 · ((3 · (𝑞↑2)) − (𝑝↑2)))) = ((𝑞↑3) − ((𝑝 · (3 · (𝑞↑2))) − (𝑝↑3))))
233	174, 177	mulcld 11329	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝 · (3 · (𝑞↑2))) ∈ ℂ)
234	173, 233, 187	subsub2d 11698	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) − ((𝑝 · (3 · (𝑞↑2))) − (𝑝↑3))) = ((𝑞↑3) + ((𝑝↑3) − (𝑝 · (3 · (𝑞↑2))))))
235	173, 187, 233	addsub12d 11692	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) + ((𝑝↑3) − (𝑝 · (3 · (𝑞↑2))))) = ((𝑝↑3) + ((𝑞↑3) − (𝑝 · (3 · (𝑞↑2))))))
236	173, 233	subcld 11669	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) − (𝑝 · (3 · (𝑞↑2)))) ∈ ℂ)
237	187, 236	addcomd 11512	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑝↑3) + ((𝑞↑3) − (𝑝 · (3 · (𝑞↑2))))) = (((𝑞↑3) − (𝑝 · (3 · (𝑞↑2)))) + (𝑝↑3)))
238	233	negcld 11656	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → -(𝑝 · (3 · (𝑞↑2))) ∈ ℂ)
239	173, 238	addcomd 11512	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) + -(𝑝 · (3 · (𝑞↑2)))) = ( -(𝑝 · (3 · (𝑞↑2))) + (𝑞↑3)))
240	173, 233	negsubd 11675	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) + -(𝑝 · (3 · (𝑞↑2)))) = ((𝑞↑3) − (𝑝 · (3 · (𝑞↑2)))))
241	174, 175, 176	mul12d 11519	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝 · (3 · (𝑞↑2))) = (3 · (𝑝 · (𝑞↑2))))
242	241	negeqd 11551	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → -(𝑝 · (3 · (𝑞↑2))) = -(3 · (𝑝 · (𝑞↑2))))
243	174, 176	mulcld 11329	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝 · (𝑞↑2)) ∈ ℂ)
244	175, 243	mulneg1d 11769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ( -3 · (𝑝 · (𝑞↑2))) = -(3 · (𝑝 · (𝑞↑2))))
245	242, 244	eqtr4d 2799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → -(𝑝 · (3 · (𝑞↑2))) = ( -3 · (𝑝 · (𝑞↑2))))
246	245	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ( -(𝑝 · (3 · (𝑞↑2))) + (𝑞↑3)) = (( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3)))
247	239, 240, 246	3eqtr3d 2804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) − (𝑝 · (3 · (𝑞↑2)))) = (( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3)))
248	247	oveq1d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (((𝑞↑3) − (𝑝 · (3 · (𝑞↑2)))) + (𝑝↑3)) = ((( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3)) + (𝑝↑3)))
249	237, 248	eqtrd 2796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑝↑3) + ((𝑞↑3) − (𝑝 · (3 · (𝑞↑2))))) = ((( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3)) + (𝑝↑3)))
250	234, 235, 249	3eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) − ((𝑝 · (3 · (𝑞↑2))) − (𝑝↑3))) = ((( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3)) + (𝑝↑3)))
251	192, 243	mulcld 11329	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ( -3 · (𝑝 · (𝑞↑2))) ∈ ℂ)
252	251, 173	addcld 11328	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3)) ∈ ℂ)
253	252, 187	addcomd 11512	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3)) + (𝑝↑3)) = ((𝑝↑3) + (( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3))))
254	232, 250, 253	3eqtrd 2800	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) − (𝑝 · ((3 · (𝑞↑2)) − (𝑝↑2)))) = ((𝑝↑3) + (( -3 · (𝑝 · (𝑞↑2))) + (𝑞↑3))))
255	214, 217, 254	3eqtr4rd 2807	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) − (𝑝 · ((3 · (𝑞↑2)) − (𝑝↑2)))) = (((𝑋↑3) + (( -3 · 𝑋) + 1)) · (𝑞↑3)))
256		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0)
257	256	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (((𝑋↑3) + (( -3 · 𝑋) + 1)) · (𝑞↑3)) = (0 · (𝑞↑3)))
258	173	mul02d 11508	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (0 · (𝑞↑3)) = 0)
259	255, 257, 258	3eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → ((𝑞↑3) − (𝑝 · ((3 · (𝑞↑2)) − (𝑝↑2)))) = 0)
260	173, 180, 259	subeq0d 11678	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑞↑3) = (𝑝 · ((3 · (𝑞↑2)) − (𝑝↑2))))
261	260	ad5ant15 771	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑞↑3) = (𝑝 · ((3 · (𝑞↑2)) − (𝑝↑2))))
262	170, 261	breqtrrd 5133	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∥ (𝑞↑3))
263		prmdvdsexp 16891	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ ℙ ∧ 𝑞 ∈ ℤ ∧ 3 ∈ ℕ) → (𝑟 ∥ (𝑞↑3) ↔ 𝑟 ∥ 𝑞))
264	263	biimpa 482	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ ℙ ∧ 𝑞 ∈ ℤ ∧ 3 ∈ ℕ) ∧ 𝑟 ∥ (𝑞↑3)) → 𝑟 ∥ 𝑞)
265	159, 154, 160, 262, 264	syl31anc 1400	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∥ 𝑞)
266		dvdsgcd 16717	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → ((𝑟 ∥ 𝑝 ∧ 𝑟 ∥ 𝑞) → 𝑟 ∥ (𝑝 gcd 𝑞)))
267	266	imp 412	. . . . . . . . . 10 ⊢ (((𝑟 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ (𝑟 ∥ 𝑝 ∧ 𝑟 ∥ 𝑞)) → 𝑟 ∥ (𝑝 gcd 𝑞))
268	150, 152, 154, 158, 265, 267	syl32anc 1405	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∥ (𝑝 gcd 𝑞))
269		simp-6r 800	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → (𝑝 gcd 𝑞) = 1)
270	268, 269	breqtrd 5131	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 ∥ 1)
271		dvds1 16489	. . . . . . . . 9 ⊢ (𝑟 ∈ ℕ₀ → (𝑟 ∥ 1 ↔ 𝑟 = 1))
272	271	biimpa 482	. . . . . . . 8 ⊢ ((𝑟 ∈ ℕ₀ ∧ 𝑟 ∥ 1) → 𝑟 = 1)
273	149, 270, 272	syl2anc 596	. . . . . . 7 ⊢ ((((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) ∧ ((𝑋↑3) + (( -3 · 𝑋) + 1)) = 0) → 𝑟 = 1)
274	146, 273	mteqand 3047	. . . . . 6 ⊢ (((((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) ∧ 𝑟 ∈ ℙ) ∧ 𝑟 ∥ (abs‘𝑝)) → ((𝑋↑3) + (( -3 · 𝑋) + 1)) ≠ 0)
275		nnabscl 15493	. . . . . . . 8 ⊢ ((𝑝 ∈ ℤ ∧ 𝑝 ≠ 0) → (abs‘𝑝) ∈ ℕ)
276	151, 106, 275	syl2anc 596	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → (abs‘𝑝) ∈ ℕ)
277		eluz2b3 13049	. . . . . . . 8 ⊢ ((abs‘𝑝) ∈ (ℤ_≥‘2) ↔ ((abs‘𝑝) ∈ ℕ ∧ (abs‘𝑝) ≠ 1))
278		exprmfct 16880	. . . . . . . 8 ⊢ ((abs‘𝑝) ∈ (ℤ_≥‘2) → ∃𝑟 ∈ ℙ 𝑟 ∥ (abs‘𝑝))
279	277, 278	sylbir 238	. . . . . . 7 ⊢ (((abs‘𝑝) ∈ ℕ ∧ (abs‘𝑝) ≠ 1) → ∃𝑟 ∈ ℙ 𝑟 ∥ (abs‘𝑝))
280	276, 279	sylan 592	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) → ∃𝑟 ∈ ℙ 𝑟 ∥ (abs‘𝑝))
281	274, 280	r19.29a 3171	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) ∧ (abs‘𝑝) ≠ 1) → ((𝑋↑3) + (( -3 · 𝑋) + 1)) ≠ 0)
282	141, 281	pm2.61dane 3043	. . . 4 ⊢ ((((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) ∧ 𝑋 ≠ 0) → ((𝑋↑3) + (( -3 · 𝑋) + 1)) ≠ 0)
283	21, 282	pm2.61dane 3043	. . 3 ⊢ (((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ 𝑋 = (𝑝 / 𝑞)) ∧ (𝑝 gcd 𝑞) = 1) → ((𝑋↑3) + (( -3 · 𝑋) + 1)) ≠ 0)
284	283	anasss 472	. 2 ⊢ ((((𝜑 ∧ 𝑝 ∈ ℤ) ∧ 𝑞 ∈ ℕ) ∧ (𝑋 = (𝑝 / 𝑞) ∧ (𝑝 gcd 𝑞) = 1)) → ((𝑋↑3) + (( -3 · 𝑋) + 1)) ≠ 0)
285		cos9thpiminplylem2.1	. . 3 ⊢ (𝜑 → 𝑋 ∈ ℚ)
286		elq2 33403	. . 3 ⊢ (𝑋 ∈ ℚ → ∃𝑝 ∈ ℤ ∃𝑞 ∈ ℕ (𝑋 = (𝑝 / 𝑞) ∧ (𝑝 gcd 𝑞) = 1))
287	285, 286	syl 18	. 2 ⊢ (𝜑 → ∃𝑝 ∈ ℤ ∃𝑞 ∈ ℕ (𝑋 = (𝑝 / 𝑞) ∧ (𝑝 gcd 𝑞) = 1))
288	284, 287	r19.29vva 3223	1 ⊢ (𝜑 → ((𝑋↑3) + (( -3 · 𝑋) + 1)) ≠ 0)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∃wrex 3087 {ctp 4588 class class class wbr 5103 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 ℝ^*cxr 11342 − cmin 11541 -cneg 11542 / cdiv 11973 ℕcn 12335 2c2 12397 3c3 12398 ℕ₀cn0 12606 ℤcz 12693 ℤ_≥cuz 12965 ℚcq 13075 ↑cexp 14204 sgncsgn 15239 abscabs 15401 ∥ cdvds 16422 gcd cgcd 16664 ℙcprime 16846

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-er 8717 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-sup 9434 df-inf 9435 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-z 12694 df-dec 12815 df-uz 12966 df-q 13076 df-rp 13121 df-fz 13640 df-fzo 13789 df-fl 13932 df-mod 14010 df-seq 14145 df-exp 14205 df-sgn 15240 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-dvds 16423 df-gcd 16665 df-prm 16847

This theorem is used by: cos9thpiminply 34420

W3C validator