Theorem sylow1lem3

Description: Lemma for sylow1 . One of the orbits of the group action has p-adic valuation less than the prime count of the set S . (Contributed by Mario Carneiro, 15-Jan-2015)

	Ref	Expression
Hypotheses	sylow1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow1.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	sylow1.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow1.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	sylow1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	sylow1.d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
	sylow1lem.a	⊢ + = ( +g ‘ 𝐺 )
	sylow1lem.s	⊢ 𝑆 = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
	sylow1lem.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑆 ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
	sylow1lem3.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑆 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
Assertion	sylow1lem3	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑆 ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		sylow1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow1.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		sylow1.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
4		sylow1.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		sylow1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		sylow1.d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
7		sylow1lem.a	⊢ + = ( +g ‘ 𝐺 )
8		sylow1lem.s	⊢ 𝑆 = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
9		sylow1lem.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑆 ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
10		sylow1lem3.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑆 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
11	1 2 3 4 5 6 7 8	sylow1lem1	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑆 ) ∈ ℕ ∧ ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
12	11	simpld	⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ℕ )
13		pcndvds	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑆 ) ∈ ℕ ) → ¬ ( 𝑃 ↑ ( ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) + 1 ) ) ∥ ( ♯ ‘ 𝑆 ) )
14	4 12 13	syl2anc	⊢ ( 𝜑 → ¬ ( 𝑃 ↑ ( ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) + 1 ) ) ∥ ( ♯ ‘ 𝑆 ) )
15	11	simprd	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) = ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
16	15	oveq1d	⊢ ( 𝜑 → ( ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) + 1 ) = ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) )
17	16	oveq2d	⊢ ( 𝜑 → ( 𝑃 ↑ ( ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) + 1 ) ) = ( 𝑃 ↑ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ) )
18	1 2 3 4 5 6 7 8 9	sylow1lem2	⊢ ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct 𝑆 ) )
19	10 1	gaorber	⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑆 ) → ∼ Er 𝑆 )
20	18 19	syl	⊢ ( 𝜑 → ∼ Er 𝑆 )
21		pwfi	⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
22	3 21	sylib	⊢ ( 𝜑 → 𝒫 𝑋 ∈ Fin )
23	8	ssrab3	⊢ 𝑆 ⊆ 𝒫 𝑋
24		ssfi	⊢ ( ( 𝒫 𝑋 ∈ Fin ∧ 𝑆 ⊆ 𝒫 𝑋 ) → 𝑆 ∈ Fin )
25	22 23 24	sylancl	⊢ ( 𝜑 → 𝑆 ∈ Fin )
26	20 25	qshash	⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = Σ 𝑧 ∈ ( 𝑆 / ∼ ) ( ♯ ‘ 𝑧 ) )
27	17 26	breq12d	⊢ ( 𝜑 → ( ( 𝑃 ↑ ( ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) + 1 ) ) ∥ ( ♯ ‘ 𝑆 ) ↔ ( 𝑃 ↑ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ) ∥ Σ 𝑧 ∈ ( 𝑆 / ∼ ) ( ♯ ‘ 𝑧 ) ) )
28	14 27	mtbid	⊢ ( 𝜑 → ¬ ( 𝑃 ↑ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ) ∥ Σ 𝑧 ∈ ( 𝑆 / ∼ ) ( ♯ ‘ 𝑧 ) )
29		pwfi	⊢ ( 𝑆 ∈ Fin ↔ 𝒫 𝑆 ∈ Fin )
30	25 29	sylib	⊢ ( 𝜑 → 𝒫 𝑆 ∈ Fin )
31	20	qsss	⊢ ( 𝜑 → ( 𝑆 / ∼ ) ⊆ 𝒫 𝑆 )
32	30 31	ssfid	⊢ ( 𝜑 → ( 𝑆 / ∼ ) ∈ Fin )
33	32	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) → ( 𝑆 / ∼ ) ∈ Fin )
34		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
35	4 34	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
36	4 12	pccld	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑆 ) ) ∈ ℕ0 )
37	15 36	eqeltrrd	⊢ ( 𝜑 → ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ∈ ℕ0 )
38		peano2nn0	⊢ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ∈ ℕ0 → ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ∈ ℕ0 )
39	37 38	syl	⊢ ( 𝜑 → ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ∈ ℕ0 )
40	35 39	nnexpcld	⊢ ( 𝜑 → ( 𝑃 ↑ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ) ∈ ℕ )
41	40	nnzd	⊢ ( 𝜑 → ( 𝑃 ↑ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ) ∈ ℤ )
42	41	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) → ( 𝑃 ↑ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ) ∈ ℤ )
43		erdm	⊢ ( ∼ Er 𝑆 → dom ∼ = 𝑆 )
44	20 43	syl	⊢ ( 𝜑 → dom ∼ = 𝑆 )
45		elqsn0	⊢ ( ( dom ∼ = 𝑆 ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → 𝑧 ≠ ∅ )
46	44 45	sylan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → 𝑧 ≠ ∅ )
47	25	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → 𝑆 ∈ Fin )
48	31	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → 𝑧 ∈ 𝒫 𝑆 )
49	48	elpwid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → 𝑧 ⊆ 𝑆 )
50	47 49	ssfid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → 𝑧 ∈ Fin )
51		hashnncl	⊢ ( 𝑧 ∈ Fin → ( ( ♯ ‘ 𝑧 ) ∈ ℕ ↔ 𝑧 ≠ ∅ ) )
52	50 51	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ( ♯ ‘ 𝑧 ) ∈ ℕ ↔ 𝑧 ≠ ∅ ) )
53	46 52	mpbird	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ )
54	53	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ )
55	54	nnzd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ♯ ‘ 𝑧 ) ∈ ℤ )
56		fveq2	⊢ ( 𝑎 = 𝑧 → ( ♯ ‘ 𝑎 ) = ( ♯ ‘ 𝑧 ) )
57	56	oveq2d	⊢ ( 𝑎 = 𝑧 → ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) = ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) )
58	57	breq1d	⊢ ( 𝑎 = 𝑧 → ( ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ↔ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
59	58	notbid	⊢ ( 𝑎 = 𝑧 → ( ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ↔ ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
60	59	rspccva	⊢ ( ( ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
61	60	adantll	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
62	1	grpbn0	⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
63	2 62	syl	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
64		hashnncl	⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
65	3 64	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
66	63 65	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ )
67	4 66	pccld	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 )
68	67	nn0zd	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℤ )
69	5	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
70	68 69	zsubcld	⊢ ( 𝜑 → ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ∈ ℤ )
71	70	ad2antrr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ∈ ℤ )
72	71	zred	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ∈ ℝ )
73	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → 𝑃 ∈ ℙ )
74	73 54	pccld	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ∈ ℕ0 )
75	74	nn0zd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ∈ ℤ )
76	75	zred	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ∈ ℝ )
77	72 76	ltnled	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) < ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ↔ ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
78	61 77	mpbird	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) < ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) )
79		zltp1le	⊢ ( ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ∈ ℤ ∧ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ∈ ℤ ) → ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) < ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ↔ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ) )
80	71 75 79	syl2anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) < ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ↔ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ) )
81	78 80	mpbid	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) )
82	39	ad2antrr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ∈ ℕ0 )
83		pcdvdsb	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ∈ ℕ0 ) → ( ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ↔ ( 𝑃 ↑ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ) ∥ ( ♯ ‘ 𝑧 ) ) )
84	73 55 82 83	syl3anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑧 ) ) ↔ ( 𝑃 ↑ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ) ∥ ( ♯ ‘ 𝑧 ) ) )
85	81 84	mpbid	⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ∧ 𝑧 ∈ ( 𝑆 / ∼ ) ) → ( 𝑃 ↑ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ) ∥ ( ♯ ‘ 𝑧 ) )
86	33 42 55 85	fsumdvds	⊢ ( ( 𝜑 ∧ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) → ( 𝑃 ↑ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) + 1 ) ) ∥ Σ 𝑧 ∈ ( 𝑆 / ∼ ) ( ♯ ‘ 𝑧 ) )
87	28 86	mtand	⊢ ( 𝜑 → ¬ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
88		dfrex2	⊢ ( ∃ 𝑎 ∈ ( 𝑆 / ∼ ) ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ↔ ¬ ∀ 𝑎 ∈ ( 𝑆 / ∼ ) ¬ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
89	87 88	sylibr	⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝑆 / ∼ ) ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
90		eqid	⊢ ( 𝑆 / ∼ ) = ( 𝑆 / ∼ )
91		fveq2	⊢ ( [ 𝑧 ] ∼ = 𝑎 → ( ♯ ‘ [ 𝑧 ] ∼ ) = ( ♯ ‘ 𝑎 ) )
92	91	oveq2d	⊢ ( [ 𝑧 ] ∼ = 𝑎 → ( 𝑃 pCnt ( ♯ ‘ [ 𝑧 ] ∼ ) ) = ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) )
93	92	breq1d	⊢ ( [ 𝑧 ] ∼ = 𝑎 → ( ( 𝑃 pCnt ( ♯ ‘ [ 𝑧 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ↔ ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
94	93	imbi1d	⊢ ( [ 𝑧 ] ∼ = 𝑎 → ( ( ( 𝑃 pCnt ( ♯ ‘ [ 𝑧 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) → ∃ 𝑤 ∈ 𝑆 ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ↔ ( ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) → ∃ 𝑤 ∈ 𝑆 ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) )
95		eceq1	⊢ ( 𝑤 = 𝑧 → [ 𝑤 ] ∼ = [ 𝑧 ] ∼ )
96	95	fveq2d	⊢ ( 𝑤 = 𝑧 → ( ♯ ‘ [ 𝑤 ] ∼ ) = ( ♯ ‘ [ 𝑧 ] ∼ ) )
97	96	oveq2d	⊢ ( 𝑤 = 𝑧 → ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) = ( 𝑃 pCnt ( ♯ ‘ [ 𝑧 ] ∼ ) ) )
98	97	breq1d	⊢ ( 𝑤 = 𝑧 → ( ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ↔ ( 𝑃 pCnt ( ♯ ‘ [ 𝑧 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
99	98	rspcev	⊢ ( ( 𝑧 ∈ 𝑆 ∧ ( 𝑃 pCnt ( ♯ ‘ [ 𝑧 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) → ∃ 𝑤 ∈ 𝑆 ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
100	99	ex	⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝑃 pCnt ( ♯ ‘ [ 𝑧 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) → ∃ 𝑤 ∈ 𝑆 ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
101	100	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑃 pCnt ( ♯ ‘ [ 𝑧 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) → ∃ 𝑤 ∈ 𝑆 ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
102	90 94 101	ectocld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑆 / ∼ ) ) → ( ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) → ∃ 𝑤 ∈ 𝑆 ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
103	102	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝑆 / ∼ ) ( 𝑃 pCnt ( ♯ ‘ 𝑎 ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) → ∃ 𝑤 ∈ 𝑆 ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
104	89 103	mpd	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑆 ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )