MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylow1lem1 Structured version   Visualization version   GIF version

Theorem sylow1lem1 19147
Description: Lemma for sylow1 19152. The p-adic valuation of the size of 𝑆 is equal to the number of excess powers of 𝑃 in (♯‘𝑋) / (𝑃𝑁). (Contributed by Mario Carneiro, 15-Jan-2015.)
Hypotheses
Ref Expression
sylow1.x 𝑋 = (Base‘𝐺)
sylow1.g (𝜑𝐺 ∈ Grp)
sylow1.f (𝜑𝑋 ∈ Fin)
sylow1.p (𝜑𝑃 ∈ ℙ)
sylow1.n (𝜑𝑁 ∈ ℕ0)
sylow1.d (𝜑 → (𝑃𝑁) ∥ (♯‘𝑋))
sylow1lem.a + = (+g𝐺)
sylow1lem.s 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃𝑁)}
Assertion
Ref Expression
sylow1lem1 (𝜑 → ((♯‘𝑆) ∈ ℕ ∧ (𝑃 pCnt (♯‘𝑆)) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁)))
Distinct variable groups:   𝑁,𝑠   𝑋,𝑠   + ,𝑠   𝐺,𝑠   𝑃,𝑠
Allowed substitution hints:   𝜑(𝑠)   𝑆(𝑠)

Proof of Theorem sylow1lem1
Dummy variables 𝑥 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sylow1.f . . . . 5 (𝜑𝑋 ∈ Fin)
2 sylow1.p . . . . . . . 8 (𝜑𝑃 ∈ ℙ)
3 prmnn 16323 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
42, 3syl 17 . . . . . . 7 (𝜑𝑃 ∈ ℕ)
5 sylow1.n . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
64, 5nnexpcld 13904 . . . . . 6 (𝜑 → (𝑃𝑁) ∈ ℕ)
76nnzd 12370 . . . . 5 (𝜑 → (𝑃𝑁) ∈ ℤ)
8 hashbc 14109 . . . . 5 ((𝑋 ∈ Fin ∧ (𝑃𝑁) ∈ ℤ) → ((♯‘𝑋)C(𝑃𝑁)) = (♯‘{𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃𝑁)}))
91, 7, 8syl2anc 583 . . . 4 (𝜑 → ((♯‘𝑋)C(𝑃𝑁)) = (♯‘{𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃𝑁)}))
10 sylow1lem.s . . . . 5 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃𝑁)}
1110fveq2i 6764 . . . 4 (♯‘𝑆) = (♯‘{𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃𝑁)})
129, 11eqtr4di 2795 . . 3 (𝜑 → ((♯‘𝑋)C(𝑃𝑁)) = (♯‘𝑆))
13 sylow1.d . . . . . 6 (𝜑 → (𝑃𝑁) ∥ (♯‘𝑋))
14 sylow1.g . . . . . . . . . 10 (𝜑𝐺 ∈ Grp)
15 sylow1.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
1615grpbn0 18552 . . . . . . . . . 10 (𝐺 ∈ Grp → 𝑋 ≠ ∅)
1714, 16syl 17 . . . . . . . . 9 (𝜑𝑋 ≠ ∅)
18 hasheq0 14022 . . . . . . . . . . 11 (𝑋 ∈ Fin → ((♯‘𝑋) = 0 ↔ 𝑋 = ∅))
191, 18syl 17 . . . . . . . . . 10 (𝜑 → ((♯‘𝑋) = 0 ↔ 𝑋 = ∅))
2019necon3bbid 2979 . . . . . . . . 9 (𝜑 → (¬ (♯‘𝑋) = 0 ↔ 𝑋 ≠ ∅))
2117, 20mpbird 256 . . . . . . . 8 (𝜑 → ¬ (♯‘𝑋) = 0)
22 hashcl 14015 . . . . . . . . . . 11 (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ0)
231, 22syl 17 . . . . . . . . . 10 (𝜑 → (♯‘𝑋) ∈ ℕ0)
24 elnn0 12181 . . . . . . . . . 10 ((♯‘𝑋) ∈ ℕ0 ↔ ((♯‘𝑋) ∈ ℕ ∨ (♯‘𝑋) = 0))
2523, 24sylib 217 . . . . . . . . 9 (𝜑 → ((♯‘𝑋) ∈ ℕ ∨ (♯‘𝑋) = 0))
2625ord 860 . . . . . . . 8 (𝜑 → (¬ (♯‘𝑋) ∈ ℕ → (♯‘𝑋) = 0))
2721, 26mt3d 148 . . . . . . 7 (𝜑 → (♯‘𝑋) ∈ ℕ)
28 dvdsle 15963 . . . . . . 7 (((𝑃𝑁) ∈ ℤ ∧ (♯‘𝑋) ∈ ℕ) → ((𝑃𝑁) ∥ (♯‘𝑋) → (𝑃𝑁) ≤ (♯‘𝑋)))
297, 27, 28syl2anc 583 . . . . . 6 (𝜑 → ((𝑃𝑁) ∥ (♯‘𝑋) → (𝑃𝑁) ≤ (♯‘𝑋)))
3013, 29mpd 15 . . . . 5 (𝜑 → (𝑃𝑁) ≤ (♯‘𝑋))
316nnnn0d 12239 . . . . . . 7 (𝜑 → (𝑃𝑁) ∈ ℕ0)
32 nn0uz 12565 . . . . . . 7 0 = (ℤ‘0)
3331, 32eleqtrdi 2847 . . . . . 6 (𝜑 → (𝑃𝑁) ∈ (ℤ‘0))
3423nn0zd 12369 . . . . . 6 (𝜑 → (♯‘𝑋) ∈ ℤ)
35 elfz5 13193 . . . . . 6 (((𝑃𝑁) ∈ (ℤ‘0) ∧ (♯‘𝑋) ∈ ℤ) → ((𝑃𝑁) ∈ (0...(♯‘𝑋)) ↔ (𝑃𝑁) ≤ (♯‘𝑋)))
3633, 34, 35syl2anc 583 . . . . 5 (𝜑 → ((𝑃𝑁) ∈ (0...(♯‘𝑋)) ↔ (𝑃𝑁) ≤ (♯‘𝑋)))
3730, 36mpbird 256 . . . 4 (𝜑 → (𝑃𝑁) ∈ (0...(♯‘𝑋)))
38 bccl2 13981 . . . 4 ((𝑃𝑁) ∈ (0...(♯‘𝑋)) → ((♯‘𝑋)C(𝑃𝑁)) ∈ ℕ)
3937, 38syl 17 . . 3 (𝜑 → ((♯‘𝑋)C(𝑃𝑁)) ∈ ℕ)
4012, 39eqeltrrd 2838 . 2 (𝜑 → (♯‘𝑆) ∈ ℕ)
41 nnuz 12566 . . . . . . . . . . 11 ℕ = (ℤ‘1)
426, 41eleqtrdi 2847 . . . . . . . . . 10 (𝜑 → (𝑃𝑁) ∈ (ℤ‘1))
43 elfz5 13193 . . . . . . . . . 10 (((𝑃𝑁) ∈ (ℤ‘1) ∧ (♯‘𝑋) ∈ ℤ) → ((𝑃𝑁) ∈ (1...(♯‘𝑋)) ↔ (𝑃𝑁) ≤ (♯‘𝑋)))
4442, 34, 43syl2anc 583 . . . . . . . . 9 (𝜑 → ((𝑃𝑁) ∈ (1...(♯‘𝑋)) ↔ (𝑃𝑁) ≤ (♯‘𝑋)))
4530, 44mpbird 256 . . . . . . . 8 (𝜑 → (𝑃𝑁) ∈ (1...(♯‘𝑋)))
46 1zzd 12297 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
47 fzsubel 13237 . . . . . . . . 9 (((1 ∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) ∧ ((𝑃𝑁) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑃𝑁) ∈ (1...(♯‘𝑋)) ↔ ((𝑃𝑁) − 1) ∈ ((1 − 1)...((♯‘𝑋) − 1))))
4846, 34, 7, 46, 47syl22anc 835 . . . . . . . 8 (𝜑 → ((𝑃𝑁) ∈ (1...(♯‘𝑋)) ↔ ((𝑃𝑁) − 1) ∈ ((1 − 1)...((♯‘𝑋) − 1))))
4945, 48mpbid 231 . . . . . . 7 (𝜑 → ((𝑃𝑁) − 1) ∈ ((1 − 1)...((♯‘𝑋) − 1)))
50 1m1e0 11991 . . . . . . . 8 (1 − 1) = 0
5150oveq1i 7270 . . . . . . 7 ((1 − 1)...((♯‘𝑋) − 1)) = (0...((♯‘𝑋) − 1))
5249, 51eleqtrdi 2847 . . . . . 6 (𝜑 → ((𝑃𝑁) − 1) ∈ (0...((♯‘𝑋) − 1)))
53 bcp1nk 13975 . . . . . 6 (((𝑃𝑁) − 1) ∈ (0...((♯‘𝑋) − 1)) → ((((♯‘𝑋) − 1) + 1)C(((𝑃𝑁) − 1) + 1)) = ((((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((((♯‘𝑋) − 1) + 1) / (((𝑃𝑁) − 1) + 1))))
5452, 53syl 17 . . . . 5 (𝜑 → ((((♯‘𝑋) − 1) + 1)C(((𝑃𝑁) − 1) + 1)) = ((((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((((♯‘𝑋) − 1) + 1) / (((𝑃𝑁) − 1) + 1))))
5523nn0cnd 12241 . . . . . . 7 (𝜑 → (♯‘𝑋) ∈ ℂ)
56 ax-1cn 10876 . . . . . . 7 1 ∈ ℂ
57 npcan 11176 . . . . . . 7 (((♯‘𝑋) ∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘𝑋) − 1) + 1) = (♯‘𝑋))
5855, 56, 57sylancl 585 . . . . . 6 (𝜑 → (((♯‘𝑋) − 1) + 1) = (♯‘𝑋))
596nncnd 11935 . . . . . . 7 (𝜑 → (𝑃𝑁) ∈ ℂ)
60 npcan 11176 . . . . . . 7 (((𝑃𝑁) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑃𝑁) − 1) + 1) = (𝑃𝑁))
6159, 56, 60sylancl 585 . . . . . 6 (𝜑 → (((𝑃𝑁) − 1) + 1) = (𝑃𝑁))
6258, 61oveq12d 7278 . . . . 5 (𝜑 → ((((♯‘𝑋) − 1) + 1)C(((𝑃𝑁) − 1) + 1)) = ((♯‘𝑋)C(𝑃𝑁)))
6358, 61oveq12d 7278 . . . . . 6 (𝜑 → ((((♯‘𝑋) − 1) + 1) / (((𝑃𝑁) − 1) + 1)) = ((♯‘𝑋) / (𝑃𝑁)))
6463oveq2d 7276 . . . . 5 (𝜑 → ((((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((((♯‘𝑋) − 1) + 1) / (((𝑃𝑁) − 1) + 1))) = ((((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((♯‘𝑋) / (𝑃𝑁))))
6554, 62, 643eqtr3d 2785 . . . 4 (𝜑 → ((♯‘𝑋)C(𝑃𝑁)) = ((((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((♯‘𝑋) / (𝑃𝑁))))
6665oveq2d 7276 . . 3 (𝜑 → (𝑃 pCnt ((♯‘𝑋)C(𝑃𝑁))) = (𝑃 pCnt ((((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((♯‘𝑋) / (𝑃𝑁)))))
6712oveq2d 7276 . . 3 (𝜑 → (𝑃 pCnt ((♯‘𝑋)C(𝑃𝑁))) = (𝑃 pCnt (♯‘𝑆)))
68 bccl2 13981 . . . . . . 7 (((𝑃𝑁) − 1) ∈ (0...((♯‘𝑋) − 1)) → (((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) ∈ ℕ)
6952, 68syl 17 . . . . . 6 (𝜑 → (((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) ∈ ℕ)
7069nnzd 12370 . . . . 5 (𝜑 → (((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) ∈ ℤ)
7169nnne0d 11969 . . . . 5 (𝜑 → (((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) ≠ 0)
726nnne0d 11969 . . . . . . 7 (𝜑 → (𝑃𝑁) ≠ 0)
73 dvdsval2 15910 . . . . . . 7 (((𝑃𝑁) ∈ ℤ ∧ (𝑃𝑁) ≠ 0 ∧ (♯‘𝑋) ∈ ℤ) → ((𝑃𝑁) ∥ (♯‘𝑋) ↔ ((♯‘𝑋) / (𝑃𝑁)) ∈ ℤ))
747, 72, 34, 73syl3anc 1369 . . . . . 6 (𝜑 → ((𝑃𝑁) ∥ (♯‘𝑋) ↔ ((♯‘𝑋) / (𝑃𝑁)) ∈ ℤ))
7513, 74mpbid 231 . . . . 5 (𝜑 → ((♯‘𝑋) / (𝑃𝑁)) ∈ ℤ)
7627nnne0d 11969 . . . . . 6 (𝜑 → (♯‘𝑋) ≠ 0)
7755, 59, 76, 72divne0d 11713 . . . . 5 (𝜑 → ((♯‘𝑋) / (𝑃𝑁)) ≠ 0)
78 pcmul 16496 . . . . 5 ((𝑃 ∈ ℙ ∧ ((((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) ∈ ℤ ∧ (((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) ≠ 0) ∧ (((♯‘𝑋) / (𝑃𝑁)) ∈ ℤ ∧ ((♯‘𝑋) / (𝑃𝑁)) ≠ 0)) → (𝑃 pCnt ((((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((♯‘𝑋) / (𝑃𝑁)))) = ((𝑃 pCnt (((♯‘𝑋) − 1)C((𝑃𝑁) − 1))) + (𝑃 pCnt ((♯‘𝑋) / (𝑃𝑁)))))
792, 70, 71, 75, 77, 78syl122anc 1377 . . . 4 (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((♯‘𝑋) / (𝑃𝑁)))) = ((𝑃 pCnt (((♯‘𝑋) − 1)C((𝑃𝑁) − 1))) + (𝑃 pCnt ((♯‘𝑋) / (𝑃𝑁)))))
80 1cnd 10917 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
8155, 59, 80npncand 11302 . . . . . . . 8 (𝜑 → (((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1)) = ((♯‘𝑋) − 1))
8281oveq1d 7275 . . . . . . 7 (𝜑 → ((((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1)) = (((♯‘𝑋) − 1)C((𝑃𝑁) − 1)))
8382oveq2d 7276 . . . . . 6 (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = (𝑃 pCnt (((♯‘𝑋) − 1)C((𝑃𝑁) − 1))))
846nnred 11934 . . . . . . . 8 (𝜑 → (𝑃𝑁) ∈ ℝ)
8584ltm1d 11853 . . . . . . 7 (𝜑 → ((𝑃𝑁) − 1) < (𝑃𝑁))
86 nnm1nn0 12220 . . . . . . . . 9 ((𝑃𝑁) ∈ ℕ → ((𝑃𝑁) − 1) ∈ ℕ0)
876, 86syl 17 . . . . . . . 8 (𝜑 → ((𝑃𝑁) − 1) ∈ ℕ0)
88 breq1 5078 . . . . . . . . . . 11 (𝑥 = 0 → (𝑥 < (𝑃𝑁) ↔ 0 < (𝑃𝑁)))
89 bcxmaslem1 15490 . . . . . . . . . . . . 13 (𝑥 = 0 → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥) = ((((♯‘𝑋) − (𝑃𝑁)) + 0)C0))
9089oveq2d 7276 . . . . . . . . . . . 12 (𝑥 = 0 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 0)C0)))
9190eqeq1d 2739 . . . . . . . . . . 11 (𝑥 = 0 → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 0)C0)) = 0))
9288, 91imbi12d 344 . . . . . . . . . 10 (𝑥 = 0 → ((𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0) ↔ (0 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 0)C0)) = 0)))
9392imbi2d 340 . . . . . . . . 9 (𝑥 = 0 → ((𝜑 → (𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (0 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 0)C0)) = 0))))
94 breq1 5078 . . . . . . . . . . 11 (𝑥 = 𝑛 → (𝑥 < (𝑃𝑁) ↔ 𝑛 < (𝑃𝑁)))
95 bcxmaslem1 15490 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥) = ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛))
9695oveq2d 7276 . . . . . . . . . . . 12 (𝑥 = 𝑛 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)))
9796eqeq1d 2739 . . . . . . . . . . 11 (𝑥 = 𝑛 → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0))
9894, 97imbi12d 344 . . . . . . . . . 10 (𝑥 = 𝑛 → ((𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0) ↔ (𝑛 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0)))
9998imbi2d 340 . . . . . . . . 9 (𝑥 = 𝑛 → ((𝜑 → (𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (𝑛 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0))))
100 breq1 5078 . . . . . . . . . . 11 (𝑥 = (𝑛 + 1) → (𝑥 < (𝑃𝑁) ↔ (𝑛 + 1) < (𝑃𝑁)))
101 bcxmaslem1 15490 . . . . . . . . . . . . 13 (𝑥 = (𝑛 + 1) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥) = ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1)))
102101oveq2d 7276 . . . . . . . . . . . 12 (𝑥 = (𝑛 + 1) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))))
103102eqeq1d 2739 . . . . . . . . . . 11 (𝑥 = (𝑛 + 1) → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))
104100, 103imbi12d 344 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → ((𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0) ↔ ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)))
105104imbi2d 340 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))))
106 breq1 5078 . . . . . . . . . . 11 (𝑥 = ((𝑃𝑁) − 1) → (𝑥 < (𝑃𝑁) ↔ ((𝑃𝑁) − 1) < (𝑃𝑁)))
107 bcxmaslem1 15490 . . . . . . . . . . . . 13 (𝑥 = ((𝑃𝑁) − 1) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥) = ((((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1)))
108107oveq2d 7276 . . . . . . . . . . . 12 (𝑥 = ((𝑃𝑁) − 1) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))))
109108eqeq1d 2739 . . . . . . . . . . 11 (𝑥 = ((𝑃𝑁) − 1) → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0))
110106, 109imbi12d 344 . . . . . . . . . 10 (𝑥 = ((𝑃𝑁) − 1) → ((𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0) ↔ (((𝑃𝑁) − 1) < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0)))
111110imbi2d 340 . . . . . . . . 9 (𝑥 = ((𝑃𝑁) − 1) → ((𝜑 → (𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (((𝑃𝑁) − 1) < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0))))
112 znn0sub 12313 . . . . . . . . . . . . . . . 16 (((𝑃𝑁) ∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) → ((𝑃𝑁) ≤ (♯‘𝑋) ↔ ((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ0))
1137, 34, 112syl2anc 583 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑃𝑁) ≤ (♯‘𝑋) ↔ ((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ0))
11430, 113mpbid 231 . . . . . . . . . . . . . 14 (𝜑 → ((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ0)
115 0nn0 12194 . . . . . . . . . . . . . 14 0 ∈ ℕ0
116 nn0addcl 12214 . . . . . . . . . . . . . 14 ((((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ0 ∧ 0 ∈ ℕ0) → (((♯‘𝑋) − (𝑃𝑁)) + 0) ∈ ℕ0)
117114, 115, 116sylancl 585 . . . . . . . . . . . . 13 (𝜑 → (((♯‘𝑋) − (𝑃𝑁)) + 0) ∈ ℕ0)
118 bcn0 13968 . . . . . . . . . . . . 13 ((((♯‘𝑋) − (𝑃𝑁)) + 0) ∈ ℕ0 → ((((♯‘𝑋) − (𝑃𝑁)) + 0)C0) = 1)
119117, 118syl 17 . . . . . . . . . . . 12 (𝜑 → ((((♯‘𝑋) − (𝑃𝑁)) + 0)C0) = 1)
120119oveq2d 7276 . . . . . . . . . . 11 (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 0)C0)) = (𝑃 pCnt 1))
121 pc1 16500 . . . . . . . . . . . 12 (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0)
1222, 121syl 17 . . . . . . . . . . 11 (𝜑 → (𝑃 pCnt 1) = 0)
123120, 122eqtrd 2777 . . . . . . . . . 10 (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 0)C0)) = 0)
124123a1d 25 . . . . . . . . 9 (𝜑 → (0 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 0)C0)) = 0))
125 nn0re 12188 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
126125ad2antrl 724 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ∈ ℝ)
127 nn0p1nn 12218 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ)
128127ad2antrl 724 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) ∈ ℕ)
129128nnred 11934 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) ∈ ℝ)
1306adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃𝑁) ∈ ℕ)
131130nnred 11934 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃𝑁) ∈ ℝ)
132126ltp1d 11851 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 < (𝑛 + 1))
133 simprr 769 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) < (𝑃𝑁))
134126, 129, 131, 132, 133lttrd 11082 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 < (𝑃𝑁))
135134expr 456 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ((𝑛 + 1) < (𝑃𝑁) → 𝑛 < (𝑃𝑁)))
136135imim1d 82 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → ((𝑛 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0) → ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0)))
137 oveq1 7267 . . . . . . . . . . 11 ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0 → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
138114adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ0)
139138nn0cnd 12241 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((♯‘𝑋) − (𝑃𝑁)) ∈ ℂ)
140 nn0cn 12189 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
141140ad2antrl 724 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ∈ ℂ)
142 1cnd 10917 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 1 ∈ ℂ)
143139, 141, 142addassd 10944 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) = (((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1)))
144143oveq1d 7275 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1)))
145 nn0addge2 12226 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℝ ∧ ((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ0) → 𝑛 ≤ (((♯‘𝑋) − (𝑃𝑁)) + 𝑛))
146126, 138, 145syl2anc 583 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ≤ (((♯‘𝑋) − (𝑃𝑁)) + 𝑛))
147 simprl 767 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ∈ ℕ0)
148147, 32eleqtrdi 2847 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ∈ (ℤ‘0))
149138, 147nn0addcld 12243 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((♯‘𝑋) − (𝑃𝑁)) + 𝑛) ∈ ℕ0)
150149nn0zd 12369 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((♯‘𝑋) − (𝑃𝑁)) + 𝑛) ∈ ℤ)
151 elfz5 13193 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘0) ∧ (((♯‘𝑋) − (𝑃𝑁)) + 𝑛) ∈ ℤ) → (𝑛 ∈ (0...(((♯‘𝑋) − (𝑃𝑁)) + 𝑛)) ↔ 𝑛 ≤ (((♯‘𝑋) − (𝑃𝑁)) + 𝑛)))
152148, 150, 151syl2anc 583 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 ∈ (0...(((♯‘𝑋) − (𝑃𝑁)) + 𝑛)) ↔ 𝑛 ≤ (((♯‘𝑋) − (𝑃𝑁)) + 𝑛)))
153146, 152mpbird 256 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ∈ (0...(((♯‘𝑋) − (𝑃𝑁)) + 𝑛)))
154 bcp1nk 13975 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (0...(((♯‘𝑋) − (𝑃𝑁)) + 𝑛)) → (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))))
155153, 154syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))))
156144, 155eqtr3d 2779 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1)) = (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))))
157156oveq2d 7276 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
1582adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑃 ∈ ℙ)
159 bccl2 13981 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (0...(((♯‘𝑋) − (𝑃𝑁)) + 𝑛)) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℕ)
160153, 159syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℕ)
161 nnq 12647 . . . . . . . . . . . . . . 15 (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℕ → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℚ)
162160, 161syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℚ)
163160nnne0d 11969 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ≠ 0)
164150peano2zd 12374 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℤ)
165 znq 12637 . . . . . . . . . . . . . . 15 ((((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) → (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℚ)
166164, 128, 165syl2anc 583 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℚ)
167 nn0p1nn 12218 . . . . . . . . . . . . . . . . 17 ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) ∈ ℕ0 → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℕ)
168149, 167syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℕ)
169 nnrp 12686 . . . . . . . . . . . . . . . . 17 (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℕ → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℝ+)
170 nnrp 12686 . . . . . . . . . . . . . . . . 17 ((𝑛 + 1) ∈ ℕ → (𝑛 + 1) ∈ ℝ+)
171 rpdivcl 12700 . . . . . . . . . . . . . . . . 17 ((((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℝ+ ∧ (𝑛 + 1) ∈ ℝ+) → (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
172169, 170, 171syl2an 595 . . . . . . . . . . . . . . . 16 ((((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) → (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
173168, 128, 172syl2anc 583 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
174173rpne0d 12722 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ≠ 0)
175 pcqmul 16498 . . . . . . . . . . . . . 14 ((𝑃 ∈ ℙ ∧ (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℚ ∧ ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ≠ 0) ∧ ((((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℚ ∧ (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ≠ 0)) → (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
176158, 162, 163, 166, 174, 175syl122anc 1377 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
177157, 176eqtrd 2777 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
178168nnne0d 11969 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ≠ 0)
179 pcdiv 16497 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ ℙ ∧ (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℤ ∧ ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ≠ 0) ∧ (𝑛 + 1) ∈ ℕ) → (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1))))
180158, 164, 178, 128, 179syl121anc 1373 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1))))
181128nncnd 11935 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) ∈ ℂ)
182139, 181, 143comraddd 11135 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) = ((𝑛 + 1) + ((♯‘𝑋) − (𝑃𝑁))))
183182oveq2d 7276 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((♯‘𝑋) − (𝑃𝑁)))))
184 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) = 0) → ((♯‘𝑋) − (𝑃𝑁)) = 0)
185184oveq2d 7276 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) = 0) → ((𝑛 + 1) + ((♯‘𝑋) − (𝑃𝑁))) = ((𝑛 + 1) + 0))
186181addid1d 11121 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑛 + 1) + 0) = (𝑛 + 1))
187186adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) = 0) → ((𝑛 + 1) + 0) = (𝑛 + 1))
188185, 187eqtr2d 2778 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) = 0) → (𝑛 + 1) = ((𝑛 + 1) + ((♯‘𝑋) − (𝑃𝑁))))
189188oveq2d 7276 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) = 0) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((♯‘𝑋) − (𝑃𝑁)))))
1902ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → 𝑃 ∈ ℙ)
191 nnq 12647 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 + 1) ∈ ℕ → (𝑛 + 1) ∈ ℚ)
192128, 191syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) ∈ ℚ)
193192adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑛 + 1) ∈ ℚ)
194138nn0zd 12369 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((♯‘𝑋) − (𝑃𝑁)) ∈ ℤ)
195 zq 12639 . . . . . . . . . . . . . . . . . . . . . 22 (((♯‘𝑋) − (𝑃𝑁)) ∈ ℤ → ((♯‘𝑋) − (𝑃𝑁)) ∈ ℚ)
196194, 195syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((♯‘𝑋) − (𝑃𝑁)) ∈ ℚ)
197196adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → ((♯‘𝑋) − (𝑃𝑁)) ∈ ℚ)
198158, 128pccld 16495 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℕ0)
199198nn0red 12240 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ)
200199adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ)
2015adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑁 ∈ ℕ0)
202201nn0red 12240 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑁 ∈ ℝ)
203202adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → 𝑁 ∈ ℝ)
204 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → ((♯‘𝑋) − (𝑃𝑁)) ≠ 0)
205204neneqd 2946 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → ¬ ((♯‘𝑋) − (𝑃𝑁)) = 0)
206114ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → ((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ0)
207 elnn0 12181 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ0 ↔ (((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ ∨ ((♯‘𝑋) − (𝑃𝑁)) = 0))
208206, 207sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ ∨ ((♯‘𝑋) − (𝑃𝑁)) = 0))
209208ord 860 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (¬ ((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ → ((♯‘𝑋) − (𝑃𝑁)) = 0))
210205, 209mt3d 148 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → ((♯‘𝑋) − (𝑃𝑁)) ∈ ℕ)
211190, 210pccld 16495 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt ((♯‘𝑋) − (𝑃𝑁))) ∈ ℕ0)
212211nn0red 12240 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt ((♯‘𝑋) − (𝑃𝑁))) ∈ ℝ)
213128nnzd 12370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) ∈ ℤ)
214 pcdvdsb 16514 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℙ ∧ (𝑛 + 1) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃𝑁) ∥ (𝑛 + 1)))
215158, 213, 201, 214syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃𝑁) ∥ (𝑛 + 1)))
2167adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃𝑁) ∈ ℤ)
217 dvdsle 15963 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃𝑁) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) → ((𝑃𝑁) ∥ (𝑛 + 1) → (𝑃𝑁) ≤ (𝑛 + 1)))
218216, 128, 217syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑃𝑁) ∥ (𝑛 + 1) → (𝑃𝑁) ≤ (𝑛 + 1)))
219215, 218sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) → (𝑃𝑁) ≤ (𝑛 + 1)))
220202, 199lenltd 11067 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ ¬ (𝑃 pCnt (𝑛 + 1)) < 𝑁))
221131, 129lenltd 11067 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑃𝑁) ≤ (𝑛 + 1) ↔ ¬ (𝑛 + 1) < (𝑃𝑁)))
222219, 220, 2213imtr3d 292 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (¬ (𝑃 pCnt (𝑛 + 1)) < 𝑁 → ¬ (𝑛 + 1) < (𝑃𝑁)))
223133, 222mt4d 117 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (𝑛 + 1)) < 𝑁)
224223adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) < 𝑁)
225 dvdssubr 15958 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑃𝑁) ∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) → ((𝑃𝑁) ∥ (♯‘𝑋) ↔ (𝑃𝑁) ∥ ((♯‘𝑋) − (𝑃𝑁))))
2267, 34, 225syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝑃𝑁) ∥ (♯‘𝑋) ↔ (𝑃𝑁) ∥ ((♯‘𝑋) − (𝑃𝑁))))
22713, 226mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃𝑁) ∥ ((♯‘𝑋) − (𝑃𝑁)))
228227ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃𝑁) ∥ ((♯‘𝑋) − (𝑃𝑁)))
229206nn0zd 12369 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → ((♯‘𝑋) − (𝑃𝑁)) ∈ ℤ)
2305ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → 𝑁 ∈ ℕ0)
231 pcdvdsb 16514 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℙ ∧ ((♯‘𝑋) − (𝑃𝑁)) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ (𝑃 pCnt ((♯‘𝑋) − (𝑃𝑁))) ↔ (𝑃𝑁) ∥ ((♯‘𝑋) − (𝑃𝑁))))
232190, 229, 230, 231syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑁 ≤ (𝑃 pCnt ((♯‘𝑋) − (𝑃𝑁))) ↔ (𝑃𝑁) ∥ ((♯‘𝑋) − (𝑃𝑁))))
233228, 232mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → 𝑁 ≤ (𝑃 pCnt ((♯‘𝑋) − (𝑃𝑁))))
234200, 203, 212, 224, 233ltletrd 11081 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) < (𝑃 pCnt ((♯‘𝑋) − (𝑃𝑁))))
235190, 193, 197, 234pcadd2 16535 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((♯‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((♯‘𝑋) − (𝑃𝑁)))))
236189, 235pm2.61dane 3030 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((♯‘𝑋) − (𝑃𝑁)))))
237183, 236eqtr4d 2780 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) = (𝑃 pCnt (𝑛 + 1)))
238198nn0cnd 12241 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℂ)
239237, 238eqeltrd 2837 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) ∈ ℂ)
240239, 237subeq0bd 11347 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1))) = 0)
241180, 240eqtrd 2777 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = 0)
242241oveq2d 7276 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (0 + (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + 0))
243 00id 11096 . . . . . . . . . . . . 13 (0 + 0) = 0
244242, 243eqtr2di 2794 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 0 = (0 + (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
245177, 244eqeq12d 2753 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0 ↔ ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + (𝑃 pCnt (((((♯‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))))))
246137, 245syl5ibr 245 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))
247136, 246animpimp2impd 842 . . . . . . . . 9 (𝑛 ∈ ℕ0 → ((𝜑 → (𝑛 < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0)) → (𝜑 → ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))))
24893, 99, 105, 111, 124, 247nn0ind 12361 . . . . . . . 8 (((𝑃𝑁) − 1) ∈ ℕ0 → (𝜑 → (((𝑃𝑁) − 1) < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0)))
24987, 248mpcom 38 . . . . . . 7 (𝜑 → (((𝑃𝑁) − 1) < (𝑃𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0))
25085, 249mpd 15 . . . . . 6 (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0)
25183, 250eqtr3d 2779 . . . . 5 (𝜑 → (𝑃 pCnt (((♯‘𝑋) − 1)C((𝑃𝑁) − 1))) = 0)
252 pcdiv 16497 . . . . . . 7 ((𝑃 ∈ ℙ ∧ ((♯‘𝑋) ∈ ℤ ∧ (♯‘𝑋) ≠ 0) ∧ (𝑃𝑁) ∈ ℕ) → (𝑃 pCnt ((♯‘𝑋) / (𝑃𝑁))) = ((𝑃 pCnt (♯‘𝑋)) − (𝑃 pCnt (𝑃𝑁))))
2532, 34, 76, 6, 252syl121anc 1373 . . . . . 6 (𝜑 → (𝑃 pCnt ((♯‘𝑋) / (𝑃𝑁))) = ((𝑃 pCnt (♯‘𝑋)) − (𝑃 pCnt (𝑃𝑁))))
2545nn0zd 12369 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
255 pcid 16518 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝑃𝑁)) = 𝑁)
2562, 254, 255syl2anc 583 . . . . . . 7 (𝜑 → (𝑃 pCnt (𝑃𝑁)) = 𝑁)
257256oveq2d 7276 . . . . . 6 (𝜑 → ((𝑃 pCnt (♯‘𝑋)) − (𝑃 pCnt (𝑃𝑁))) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁))
258253, 257eqtrd 2777 . . . . 5 (𝜑 → (𝑃 pCnt ((♯‘𝑋) / (𝑃𝑁))) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁))
259251, 258oveq12d 7278 . . . 4 (𝜑 → ((𝑃 pCnt (((♯‘𝑋) − 1)C((𝑃𝑁) − 1))) + (𝑃 pCnt ((♯‘𝑋) / (𝑃𝑁)))) = (0 + ((𝑃 pCnt (♯‘𝑋)) − 𝑁)))
2602, 27pccld 16495 . . . . . . . 8 (𝜑 → (𝑃 pCnt (♯‘𝑋)) ∈ ℕ0)
261260nn0zd 12369 . . . . . . 7 (𝜑 → (𝑃 pCnt (♯‘𝑋)) ∈ ℤ)
262261, 254zsubcld 12376 . . . . . 6 (𝜑 → ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ∈ ℤ)
263262zcnd 12372 . . . . 5 (𝜑 → ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ∈ ℂ)
264263addid2d 11122 . . . 4 (𝜑 → (0 + ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁))
26579, 259, 2643eqtrd 2781 . . 3 (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((♯‘𝑋) / (𝑃𝑁)))) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁))
26666, 67, 2653eqtr3d 2785 . 2 (𝜑 → (𝑃 pCnt (♯‘𝑆)) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁))
26740, 266jca 511 1 (𝜑 → ((♯‘𝑆) ∈ ℕ ∧ (𝑃 pCnt (♯‘𝑆)) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 843   = wceq 1539  wcel 2107  wne 2941  {crab 3066  c0 4258  𝒫 cpw 4535   class class class wbr 5075  cfv 6423  (class class class)co 7260  Fincfn 8696  cc 10816  cr 10817  0cc0 10818  1c1 10819   + caddc 10821   · cmul 10823   < clt 10956  cle 10957  cmin 11151   / cdiv 11578  cn 11919  0cn0 12179  cz 12265  cuz 12527  cq 12633  +crp 12675  ...cfz 13184  cexp 13726  Ccbc 13960  chash 13988  cdvds 15907  cprime 16320   pCnt cpc 16481  Basecbs 16856  +gcplusg 16906  Grpcgrp 18521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571  ax-cnex 10874  ax-resscn 10875  ax-1cn 10876  ax-icn 10877  ax-addcl 10878  ax-addrcl 10879  ax-mulcl 10880  ax-mulrcl 10881  ax-mulcom 10882  ax-addass 10883  ax-mulass 10884  ax-distr 10885  ax-i2m1 10886  ax-1ne0 10887  ax-1rid 10888  ax-rnegex 10889  ax-rrecex 10890  ax-cnre 10891  ax-pre-lttri 10892  ax-pre-lttrn 10893  ax-pre-ltadd 10894  ax-pre-mulgt0 10895  ax-pre-sup 10896
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4842  df-int 4882  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5485  df-eprel 5491  df-po 5499  df-so 5500  df-fr 5540  df-we 5542  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-pred 6196  df-ord 6259  df-on 6260  df-lim 6261  df-suc 6262  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-riota 7217  df-ov 7263  df-oprab 7264  df-mpo 7265  df-om 7693  df-1st 7809  df-2nd 7810  df-frecs 8073  df-wrecs 8104  df-recs 8178  df-rdg 8217  df-1o 8272  df-2o 8273  df-oadd 8276  df-er 8461  df-en 8697  df-dom 8698  df-sdom 8699  df-fin 8700  df-sup 9147  df-inf 9148  df-dju 9606  df-card 9644  df-pnf 10958  df-mnf 10959  df-xr 10960  df-ltxr 10961  df-le 10962  df-sub 11153  df-neg 11154  df-div 11579  df-nn 11920  df-2 11982  df-3 11983  df-n0 12180  df-z 12266  df-uz 12528  df-q 12634  df-rp 12676  df-fz 13185  df-fl 13456  df-mod 13534  df-seq 13666  df-exp 13727  df-fac 13932  df-bc 13961  df-hash 13989  df-cj 14754  df-re 14755  df-im 14756  df-sqrt 14890  df-abs 14891  df-dvds 15908  df-gcd 16146  df-prm 16321  df-pc 16482  df-0g 17096  df-mgm 18270  df-sgrp 18319  df-mnd 18330  df-grp 18524
This theorem is referenced by:  sylow1lem3  19149
  Copyright terms: Public domain W3C validator