ply1dg3rt0irred

Description: If a cubic polynomial over a field has no roots, it is irreducible. (Proposed by Saveliy Skresanov, 5-Jun-2025.) (Contributed by Thierry Arnoux, 8-Jun-2025)

	Ref	Expression
Hypotheses	ply1dg3rt0irred.z	$⊢ \underset{˙}{0} = 0_{F}$
	ply1dg3rt0irred.o	$⊢ O = {eval}_{1} (F)$
	ply1dg3rt0irred.d	$⊢ D = \deg_{1} (F)$
	ply1dg3rt0irred.p	$⊢ P = {Poly}_{1} (F)$
	ply1dg3rt0irred.b	$⊢ B = {Base}_{P}$
	ply1dg3rt0irred.f	$⊢ φ \to F \in Field$
	ply1dg3rt0irred.q	$⊢ φ \to Q \in B$
	ply1dg3rt0irred.1	$⊢ φ \to {O (Q)}^{-1} [\{\underset{˙}{0}\}] = \emptyset$
	ply1dg3rt0irred.2	$⊢ φ \to D (Q) = 3$
Assertion	ply1dg3rt0irred	$⊢ φ \to Q \in Irred (P)$

Proof

Step	Hyp	Ref	Expression
1		ply1dg3rt0irred.z	$⊢ \underset{˙}{0} = 0_{F}$
2		ply1dg3rt0irred.o	$⊢ O = {eval}_{1} (F)$
3		ply1dg3rt0irred.d	$⊢ D = \deg_{1} (F)$
4		ply1dg3rt0irred.p	$⊢ P = {Poly}_{1} (F)$
5		ply1dg3rt0irred.b	$⊢ B = {Base}_{P}$
6		ply1dg3rt0irred.f	$⊢ φ \to F \in Field$
7		ply1dg3rt0irred.q	$⊢ φ \to Q \in B$
8		ply1dg3rt0irred.1	$⊢ φ \to {O (Q)}^{-1} [\{\underset{˙}{0}\}] = \emptyset$
9		ply1dg3rt0irred.2	$⊢ φ \to D (Q) = 3$
10		3ne0	$⊢ 3 \neq 0$
11	10	a1i	$⊢ φ \to 3 \neq 0$
12	9 11	eqnetrd	$⊢ φ \to D (Q) \neq 0$
13		eqid	$⊢ algSc (P) = algSc (P)$
14		eqid	$⊢ {Base}_{F} = {Base}_{F}$
15	7 5	eleqtrdi	$⊢ φ \to Q \in {Base}_{P}$
16	4 13 14 1 6 3 15	ply1unit	$⊢ φ \to (Q \in Unit (P) \leftrightarrow D (Q) = 0)$
17	16	necon3bbid	$⊢ φ \to (\neg Q \in Unit (P) \leftrightarrow D (Q) \neq 0)$
18	12 17	mpbird	$⊢ φ \to \neg Q \in Unit (P)$
19	7 18	eldifd	$⊢ φ \to Q \in (B ∖ Unit (P))$
20	6	ad3antrrr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to F \in Field$
21		simpllr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to p \in (B ∖ Unit (P))$
22	21	eldifad	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to p \in B$
23	22 5	eleqtrdi	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to p \in {Base}_{P}$
24	4 13 14 1 20 3 23	ply1unit	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to (p \in Unit (P) \leftrightarrow D (p) = 0)$
25	24	biimpar	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 0) \to p \in Unit (P)$
26	21	eldifbd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to \neg p \in Unit (P)$
27	26	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 0) \to \neg p \in Unit (P)$
28	25 27	pm2.21fal	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 0) \to ⊥$
29	28	adantlr	$⊢ (((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) \in \{0, 1\}) \land D (p) = 0) \to ⊥$
30	6	fldcrngd	$⊢ φ \to F \in CRing$
31	30	ad3antrrr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to F \in CRing$
32		simplr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to q \in (B ∖ Unit (P))$
33	32	eldifad	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to q \in B$
34		eqid	$⊢ \cdot_{P} = \cdot_{P}$
35	4 5 2 3 1 31 22 33 34	ply1mulrtss	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (p)}^{-1} [\{\underset{˙}{0}\}] \subseteq {O (p \cdot_{P} q)}^{-1} [\{\underset{˙}{0}\}]$
36		simpr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to p \cdot_{P} q = Q$
37	36	fveq2d	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to O (p \cdot_{P} q) = O (Q)$
38	37	cnveqd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (p \cdot_{P} q)}^{-1} = {O (Q)}^{-1}$
39	38	imaeq1d	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (p \cdot_{P} q)}^{-1} [\{\underset{˙}{0}\}] = {O (Q)}^{-1} [\{\underset{˙}{0}\}]$
40	35 39	sseqtrd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (p)}^{-1} [\{\underset{˙}{0}\}] \subseteq {O (Q)}^{-1} [\{\underset{˙}{0}\}]$
41	8	ad3antrrr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (Q)}^{-1} [\{\underset{˙}{0}\}] = \emptyset$
42	40 41	sseqtrd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (p)}^{-1} [\{\underset{˙}{0}\}] \subseteq \emptyset$
43		ss0	$⊢ {O (p)}^{-1} [\{\underset{˙}{0}\}] \subseteq \emptyset \to {O (p)}^{-1} [\{\underset{˙}{0}\}] = \emptyset$
44	42 43	syl	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (p)}^{-1} [\{\underset{˙}{0}\}] = \emptyset$
45	44	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 1) \to {O (p)}^{-1} [\{\underset{˙}{0}\}] = \emptyset$
46	20	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 1) \to F \in Field$
47	22	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 1) \to p \in B$
48		simpr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 1) \to D (p) = 1$
49	4 5 2 3 1 46 47 48	ply1dg1rtn0	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 1) \to {O (p)}^{-1} [\{\underset{˙}{0}\}] \neq \emptyset$
50	45 49	pm2.21ddne	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 1) \to ⊥$
51	50	adantlr	$⊢ (((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) \in \{0, 1\}) \land D (p) = 1) \to ⊥$
52		elpri	$⊢ D (p) \in \{0, 1\} \to (D (p) = 0 \lor D (p) = 1)$
53	52	adantl	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) \in \{0, 1\}) \to (D (p) = 0 \lor D (p) = 1)$
54	29 51 53	mpjaodan	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) \in \{0, 1\}) \to ⊥$
55	4 5 2 3 1 31 33 22 34	ply1mulrtss	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (q)}^{-1} [\{\underset{˙}{0}\}] \subseteq {O (q \cdot_{P} p)}^{-1} [\{\underset{˙}{0}\}]$
56		fldidom	$⊢ F \in Field \to F \in IDomn$
57	6 56	syl	$⊢ φ \to F \in IDomn$
58	4	ply1idom	$⊢ F \in IDomn \to P \in IDomn$
59	57 58	syl	$⊢ φ \to P \in IDomn$
60	59	idomcringd	$⊢ φ \to P \in CRing$
61	60	ad3antrrr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to P \in CRing$
62	5 34 61 33 22	crngcomd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to q \cdot_{P} p = p \cdot_{P} q$
63	62 36	eqtrd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to q \cdot_{P} p = Q$
64	63	fveq2d	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to O (q \cdot_{P} p) = O (Q)$
65	64	cnveqd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (q \cdot_{P} p)}^{-1} = {O (Q)}^{-1}$
66	65	imaeq1d	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (q \cdot_{P} p)}^{-1} [\{\underset{˙}{0}\}] = {O (Q)}^{-1} [\{\underset{˙}{0}\}]$
67	66 41	eqtrd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (q \cdot_{P} p)}^{-1} [\{\underset{˙}{0}\}] = \emptyset$
68	55 67	sseqtrd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (q)}^{-1} [\{\underset{˙}{0}\}] \subseteq \emptyset$
69		ss0	$⊢ {O (q)}^{-1} [\{\underset{˙}{0}\}] \subseteq \emptyset \to {O (q)}^{-1} [\{\underset{˙}{0}\}] = \emptyset$
70	68 69	syl	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to {O (q)}^{-1} [\{\underset{˙}{0}\}] = \emptyset$
71	70	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 2) \to {O (q)}^{-1} [\{\underset{˙}{0}\}] = \emptyset$
72	20	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 2) \to F \in Field$
73	33	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 2) \to q \in B$
74	30	crngringd	$⊢ φ \to F \in Ring$
75	74	ad3antrrr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to F \in Ring$
76		eqid	$⊢ 0_{P} = 0_{P}$
77	59	idomdomd	$⊢ φ \to P \in Domn$
78	77	ad3antrrr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to P \in Domn$
79		3nn0	$⊢ 3 \in ℕ_{0}$
80	9 79	eqeltrdi	$⊢ φ \to D (Q) \in ℕ_{0}$
81	3 4 76 5	deg1nn0clb	$⊢ (F \in Ring \land Q \in B) \to (Q \neq 0_{P} \leftrightarrow D (Q) \in ℕ_{0})$
82	81	biimpar	$⊢ ((F \in Ring \land Q \in B) \land D (Q) \in ℕ_{0}) \to Q \neq 0_{P}$
83	74 7 80 82	syl21anc	$⊢ φ \to Q \neq 0_{P}$
84	83	ad3antrrr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to Q \neq 0_{P}$
85	36 84	eqnetrd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to p \cdot_{P} q \neq 0_{P}$
86	5 34 76 78 22 33 85	domnmuln0rd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to (p \neq 0_{P} \land q \neq 0_{P})$
87	86	simpld	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to p \neq 0_{P}$
88	3 4 76 5	deg1nn0cl	$⊢ (F \in Ring \land p \in B \land p \neq 0_{P}) \to D (p) \in ℕ_{0}$
89	75 22 87 88	syl3anc	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (p) \in ℕ_{0}$
90	89	nn0cnd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (p) \in ℂ$
91	86	simprd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to q \neq 0_{P}$
92	3 4 76 5	deg1nn0cl	$⊢ (F \in Ring \land q \in B \land q \neq 0_{P}) \to D (q) \in ℕ_{0}$
93	75 33 91 92	syl3anc	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (q) \in ℕ_{0}$
94	93	nn0cnd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (q) \in ℂ$
95	36	fveq2d	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (p \cdot_{P} q) = D (Q)$
96	57	idomdomd	$⊢ φ \to F \in Domn$
97	96	ad3antrrr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to F \in Domn$
98	3 4 5 34 76 97 22 87 33 91	deg1mul	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (p \cdot_{P} q) = D (p) + D (q)$
99	9	ad3antrrr	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (Q) = 3$
100	95 98 99	3eqtr3d	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (p) + D (q) = 3$
101	90 94 100	mvlladdd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (q) = 3 - D (p)$
102	101	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 2) \to D (q) = 3 - D (p)$
103		simpr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 2) \to D (p) = 2$
104	103	oveq2d	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 2) \to 3 - D (p) = 3 - 2$
105		3cn	$⊢ 3 \in ℂ$
106		2cn	$⊢ 2 \in ℂ$
107		ax-1cn	$⊢ 1 \in ℂ$
108		2p1e3	$⊢ 2 + 1 = 3$
109	105 106 107 108	subaddrii	$⊢ 3 - 2 = 1$
110	109	a1i	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 2) \to 3 - 2 = 1$
111	102 104 110	3eqtrd	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 2) \to D (q) = 1$
112	4 5 2 3 1 72 73 111	ply1dg1rtn0	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 2) \to {O (q)}^{-1} [\{\underset{˙}{0}\}] \neq \emptyset$
113	71 112	pm2.21ddne	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 2) \to ⊥$
114	113	adantlr	$⊢ (((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) \in \{2, 3\}) \land D (p) = 2) \to ⊥$
115	101	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to D (q) = 3 - D (p)$
116		simpr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to D (p) = 3$
117	116	oveq2d	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to 3 - D (p) = 3 - 3$
118	105	subidi	$⊢ 3 - 3 = 0$
119	118	a1i	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to 3 - 3 = 0$
120	115 117 119	3eqtrd	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to D (q) = 0$
121	20	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to F \in Field$
122	33 5	eleqtrdi	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to q \in {Base}_{P}$
123	122	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to q \in {Base}_{P}$
124	4 13 14 1 121 3 123	ply1unit	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to (q \in Unit (P) \leftrightarrow D (q) = 0)$
125	120 124	mpbird	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to q \in Unit (P)$
126	32	eldifbd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to \neg q \in Unit (P)$
127	126	adantr	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to \neg q \in Unit (P)$
128	125 127	pm2.21fal	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) = 3) \to ⊥$
129	128	adantlr	$⊢ (((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) \in \{2, 3\}) \land D (p) = 3) \to ⊥$
130		elpri	$⊢ D (p) \in \{2, 3\} \to (D (p) = 2 \lor D (p) = 3)$
131	130	adantl	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) \in \{2, 3\}) \to (D (p) = 2 \lor D (p) = 3)$
132	114 129 131	mpjaodan	$⊢ ((((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \land D (p) \in \{2, 3\}) \to ⊥$
133	79	a1i	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to 3 \in ℕ_{0}$
134	89	nn0red	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (p) \in ℝ$
135		nn0addge1	$⊢ (D (p) \in ℝ \land D (q) \in ℕ_{0}) \to D (p) \leq D (p) + D (q)$
136	134 93 135	syl2anc	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (p) \leq D (p) + D (q)$
137	136 100	breqtrd	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (p) \leq 3$
138		fznn0	$⊢ 3 \in ℕ_{0} \to (D (p) \in (0 \dots 3) \leftrightarrow (D (p) \in ℕ_{0} \land D (p) \leq 3))$
139	138	biimpar	$⊢ (3 \in ℕ_{0} \land (D (p) \in ℕ_{0} \land D (p) \leq 3)) \to D (p) \in (0 \dots 3)$
140	133 89 137 139	syl12anc	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (p) \in (0 \dots 3)$
141		fz0to3un2pr	$⊢ (0 \dots 3) = \{0, 1\} \cup \{2, 3\}$
142	140 141	eleqtrdi	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to D (p) \in (\{0, 1\} \cup \{2, 3\})$
143		elun	$⊢ D (p) \in (\{0, 1\} \cup \{2, 3\}) \leftrightarrow (D (p) \in \{0, 1\} \lor D (p) \in \{2, 3\})$
144	142 143	sylib	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to (D (p) \in \{0, 1\} \lor D (p) \in \{2, 3\})$
145	54 132 144	mpjaodan	$⊢ (((φ \land p \in (B ∖ Unit (P))) \land q \in (B ∖ Unit (P))) \land p \cdot_{P} q = Q) \to ⊥$
146	145	r19.29ffa	$⊢ (φ \land \exists p \in (B ∖ Unit (P)) \exists q \in (B ∖ Unit (P)) p \cdot_{P} q = Q) \to ⊥$
147	146	inegd	$⊢ φ \to \neg \exists p \in (B ∖ Unit (P)) \exists q \in (B ∖ Unit (P)) p \cdot_{P} q = Q$
148		ralnex2	$⊢ \forall p \in (B ∖ Unit (P)) \forall q \in (B ∖ Unit (P)) \neg p \cdot_{P} q = Q \leftrightarrow \neg \exists p \in (B ∖ Unit (P)) \exists q \in (B ∖ Unit (P)) p \cdot_{P} q = Q$
149	147 148	sylibr	$⊢ φ \to \forall p \in (B ∖ Unit (P)) \forall q \in (B ∖ Unit (P)) \neg p \cdot_{P} q = Q$
150		df-ne	$⊢ p \cdot_{P} q \neq Q \leftrightarrow \neg p \cdot_{P} q = Q$
151	150	2ralbii	$⊢ \forall p \in (B ∖ Unit (P)) \forall q \in (B ∖ Unit (P)) p \cdot_{P} q \neq Q \leftrightarrow \forall p \in (B ∖ Unit (P)) \forall q \in (B ∖ Unit (P)) \neg p \cdot_{P} q = Q$
152	149 151	sylibr	$⊢ φ \to \forall p \in (B ∖ Unit (P)) \forall q \in (B ∖ Unit (P)) p \cdot_{P} q \neq Q$
153		eqid	$⊢ Unit (P) = Unit (P)$
154		eqid	$⊢ Irred (P) = Irred (P)$
155		eqid	$⊢ B ∖ Unit (P) = B ∖ Unit (P)$
156	5 153 154 155 34	isirred	$⊢ Q \in Irred (P) \leftrightarrow (Q \in (B ∖ Unit (P)) \land \forall p \in (B ∖ Unit (P)) \forall q \in (B ∖ Unit (P)) p \cdot_{P} q \neq Q)$
157	19 152 156	sylanbrc	$⊢ φ \to Q \in Irred (P)$

Metamath Proof Explorer

Theorem ply1dg3rt0irred

Proof