This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )