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

Theorem sylow1lem1 18059
Description: Lemma for sylow1 18064. 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 15435 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
42, 3syl 17 . . . . . . 7 (𝜑𝑃 ∈ ℕ)
5 sylow1.n . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
64, 5nnexpcld 13070 . . . . . 6 (𝜑 → (𝑃𝑁) ∈ ℕ)
76nnzd 11519 . . . . 5 (𝜑 → (𝑃𝑁) ∈ ℤ)
8 hashbc 13275 . . . . 5 ((𝑋 ∈ Fin ∧ (𝑃𝑁) ∈ ℤ) → ((#‘𝑋)C(𝑃𝑁)) = (#‘{𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃𝑁)}))
91, 7, 8syl2anc 694 . . . 4 (𝜑 → ((#‘𝑋)C(𝑃𝑁)) = (#‘{𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃𝑁)}))
10 sylow1lem.s . . . . 5 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃𝑁)}
1110fveq2i 6232 . . . 4 (#‘𝑆) = (#‘{𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃𝑁)})
129, 11syl6eqr 2703 . . 3 (𝜑 → ((#‘𝑋)C(𝑃𝑁)) = (#‘𝑆))
13 sylow1.d . . . . . 6 (𝜑 → (𝑃𝑁) ∥ (#‘𝑋))
14 sylow1.g . . . . . . . . . 10 (𝜑𝐺 ∈ Grp)
15 sylow1.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
1615grpbn0 17498 . . . . . . . . . 10 (𝐺 ∈ Grp → 𝑋 ≠ ∅)
1714, 16syl 17 . . . . . . . . 9 (𝜑𝑋 ≠ ∅)
18 hasheq0 13192 . . . . . . . . . . 11 (𝑋 ∈ Fin → ((#‘𝑋) = 0 ↔ 𝑋 = ∅))
191, 18syl 17 . . . . . . . . . 10 (𝜑 → ((#‘𝑋) = 0 ↔ 𝑋 = ∅))
2019necon3bbid 2860 . . . . . . . . 9 (𝜑 → (¬ (#‘𝑋) = 0 ↔ 𝑋 ≠ ∅))
2117, 20mpbird 247 . . . . . . . 8 (𝜑 → ¬ (#‘𝑋) = 0)
22 hashcl 13185 . . . . . . . . . . 11 (𝑋 ∈ Fin → (#‘𝑋) ∈ ℕ0)
231, 22syl 17 . . . . . . . . . 10 (𝜑 → (#‘𝑋) ∈ ℕ0)
24 elnn0 11332 . . . . . . . . . 10 ((#‘𝑋) ∈ ℕ0 ↔ ((#‘𝑋) ∈ ℕ ∨ (#‘𝑋) = 0))
2523, 24sylib 208 . . . . . . . . 9 (𝜑 → ((#‘𝑋) ∈ ℕ ∨ (#‘𝑋) = 0))
2625ord 391 . . . . . . . 8 (𝜑 → (¬ (#‘𝑋) ∈ ℕ → (#‘𝑋) = 0))
2721, 26mt3d 140 . . . . . . 7 (𝜑 → (#‘𝑋) ∈ ℕ)
28 dvdsle 15079 . . . . . . 7 (((𝑃𝑁) ∈ ℤ ∧ (#‘𝑋) ∈ ℕ) → ((𝑃𝑁) ∥ (#‘𝑋) → (𝑃𝑁) ≤ (#‘𝑋)))
297, 27, 28syl2anc 694 . . . . . 6 (𝜑 → ((𝑃𝑁) ∥ (#‘𝑋) → (𝑃𝑁) ≤ (#‘𝑋)))
3013, 29mpd 15 . . . . 5 (𝜑 → (𝑃𝑁) ≤ (#‘𝑋))
316nnnn0d 11389 . . . . . . 7 (𝜑 → (𝑃𝑁) ∈ ℕ0)
32 nn0uz 11760 . . . . . . 7 0 = (ℤ‘0)
3331, 32syl6eleq 2740 . . . . . 6 (𝜑 → (𝑃𝑁) ∈ (ℤ‘0))
3423nn0zd 11518 . . . . . 6 (𝜑 → (#‘𝑋) ∈ ℤ)
35 elfz5 12372 . . . . . 6 (((𝑃𝑁) ∈ (ℤ‘0) ∧ (#‘𝑋) ∈ ℤ) → ((𝑃𝑁) ∈ (0...(#‘𝑋)) ↔ (𝑃𝑁) ≤ (#‘𝑋)))
3633, 34, 35syl2anc 694 . . . . 5 (𝜑 → ((𝑃𝑁) ∈ (0...(#‘𝑋)) ↔ (𝑃𝑁) ≤ (#‘𝑋)))
3730, 36mpbird 247 . . . 4 (𝜑 → (𝑃𝑁) ∈ (0...(#‘𝑋)))
38 bccl2 13150 . . . 4 ((𝑃𝑁) ∈ (0...(#‘𝑋)) → ((#‘𝑋)C(𝑃𝑁)) ∈ ℕ)
3937, 38syl 17 . . 3 (𝜑 → ((#‘𝑋)C(𝑃𝑁)) ∈ ℕ)
4012, 39eqeltrrd 2731 . 2 (𝜑 → (#‘𝑆) ∈ ℕ)
41 nnuz 11761 . . . . . . . . . . 11 ℕ = (ℤ‘1)
426, 41syl6eleq 2740 . . . . . . . . . 10 (𝜑 → (𝑃𝑁) ∈ (ℤ‘1))
43 elfz5 12372 . . . . . . . . . 10 (((𝑃𝑁) ∈ (ℤ‘1) ∧ (#‘𝑋) ∈ ℤ) → ((𝑃𝑁) ∈ (1...(#‘𝑋)) ↔ (𝑃𝑁) ≤ (#‘𝑋)))
4442, 34, 43syl2anc 694 . . . . . . . . 9 (𝜑 → ((𝑃𝑁) ∈ (1...(#‘𝑋)) ↔ (𝑃𝑁) ≤ (#‘𝑋)))
4530, 44mpbird 247 . . . . . . . 8 (𝜑 → (𝑃𝑁) ∈ (1...(#‘𝑋)))
46 1zzd 11446 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
47 fzsubel 12415 . . . . . . . . 9 (((1 ∈ ℤ ∧ (#‘𝑋) ∈ ℤ) ∧ ((𝑃𝑁) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑃𝑁) ∈ (1...(#‘𝑋)) ↔ ((𝑃𝑁) − 1) ∈ ((1 − 1)...((#‘𝑋) − 1))))
4846, 34, 7, 46, 47syl22anc 1367 . . . . . . . 8 (𝜑 → ((𝑃𝑁) ∈ (1...(#‘𝑋)) ↔ ((𝑃𝑁) − 1) ∈ ((1 − 1)...((#‘𝑋) − 1))))
4945, 48mpbid 222 . . . . . . 7 (𝜑 → ((𝑃𝑁) − 1) ∈ ((1 − 1)...((#‘𝑋) − 1)))
50 1m1e0 11127 . . . . . . . 8 (1 − 1) = 0
5150oveq1i 6700 . . . . . . 7 ((1 − 1)...((#‘𝑋) − 1)) = (0...((#‘𝑋) − 1))
5249, 51syl6eleq 2740 . . . . . 6 (𝜑 → ((𝑃𝑁) − 1) ∈ (0...((#‘𝑋) − 1)))
53 bcp1nk 13144 . . . . . 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 11391 . . . . . . 7 (𝜑 → (#‘𝑋) ∈ ℂ)
56 ax-1cn 10032 . . . . . . 7 1 ∈ ℂ
57 npcan 10328 . . . . . . 7 (((#‘𝑋) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘𝑋) − 1) + 1) = (#‘𝑋))
5855, 56, 57sylancl 695 . . . . . 6 (𝜑 → (((#‘𝑋) − 1) + 1) = (#‘𝑋))
596nncnd 11074 . . . . . . 7 (𝜑 → (𝑃𝑁) ∈ ℂ)
60 npcan 10328 . . . . . . 7 (((𝑃𝑁) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑃𝑁) − 1) + 1) = (𝑃𝑁))
6159, 56, 60sylancl 695 . . . . . 6 (𝜑 → (((𝑃𝑁) − 1) + 1) = (𝑃𝑁))
6258, 61oveq12d 6708 . . . . 5 (𝜑 → ((((#‘𝑋) − 1) + 1)C(((𝑃𝑁) − 1) + 1)) = ((#‘𝑋)C(𝑃𝑁)))
6358, 61oveq12d 6708 . . . . . 6 (𝜑 → ((((#‘𝑋) − 1) + 1) / (((𝑃𝑁) − 1) + 1)) = ((#‘𝑋) / (𝑃𝑁)))
6463oveq2d 6706 . . . . 5 (𝜑 → ((((#‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((((#‘𝑋) − 1) + 1) / (((𝑃𝑁) − 1) + 1))) = ((((#‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((#‘𝑋) / (𝑃𝑁))))
6554, 62, 643eqtr3d 2693 . . . 4 (𝜑 → ((#‘𝑋)C(𝑃𝑁)) = ((((#‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((#‘𝑋) / (𝑃𝑁))))
6665oveq2d 6706 . . 3 (𝜑 → (𝑃 pCnt ((#‘𝑋)C(𝑃𝑁))) = (𝑃 pCnt ((((#‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((#‘𝑋) / (𝑃𝑁)))))
6712oveq2d 6706 . . 3 (𝜑 → (𝑃 pCnt ((#‘𝑋)C(𝑃𝑁))) = (𝑃 pCnt (#‘𝑆)))
68 bccl2 13150 . . . . . . 7 (((𝑃𝑁) − 1) ∈ (0...((#‘𝑋) − 1)) → (((#‘𝑋) − 1)C((𝑃𝑁) − 1)) ∈ ℕ)
6952, 68syl 17 . . . . . 6 (𝜑 → (((#‘𝑋) − 1)C((𝑃𝑁) − 1)) ∈ ℕ)
7069nnzd 11519 . . . . 5 (𝜑 → (((#‘𝑋) − 1)C((𝑃𝑁) − 1)) ∈ ℤ)
7169nnne0d 11103 . . . . 5 (𝜑 → (((#‘𝑋) − 1)C((𝑃𝑁) − 1)) ≠ 0)
726nnne0d 11103 . . . . . . 7 (𝜑 → (𝑃𝑁) ≠ 0)
73 dvdsval2 15030 . . . . . . 7 (((𝑃𝑁) ∈ ℤ ∧ (𝑃𝑁) ≠ 0 ∧ (#‘𝑋) ∈ ℤ) → ((𝑃𝑁) ∥ (#‘𝑋) ↔ ((#‘𝑋) / (𝑃𝑁)) ∈ ℤ))
747, 72, 34, 73syl3anc 1366 . . . . . 6 (𝜑 → ((𝑃𝑁) ∥ (#‘𝑋) ↔ ((#‘𝑋) / (𝑃𝑁)) ∈ ℤ))
7513, 74mpbid 222 . . . . 5 (𝜑 → ((#‘𝑋) / (𝑃𝑁)) ∈ ℤ)
7627nnne0d 11103 . . . . . 6 (𝜑 → (#‘𝑋) ≠ 0)
7755, 59, 76, 72divne0d 10855 . . . . 5 (𝜑 → ((#‘𝑋) / (𝑃𝑁)) ≠ 0)
78 pcmul 15603 . . . . 5 ((𝑃 ∈ ℙ ∧ ((((#‘𝑋) − 1)C((𝑃𝑁) − 1)) ∈ ℤ ∧ (((#‘𝑋) − 1)C((𝑃𝑁) − 1)) ≠ 0) ∧ (((#‘𝑋) / (𝑃𝑁)) ∈ ℤ ∧ ((#‘𝑋) / (𝑃𝑁)) ≠ 0)) → (𝑃 pCnt ((((#‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((#‘𝑋) / (𝑃𝑁)))) = ((𝑃 pCnt (((#‘𝑋) − 1)C((𝑃𝑁) − 1))) + (𝑃 pCnt ((#‘𝑋) / (𝑃𝑁)))))
792, 70, 71, 75, 77, 78syl122anc 1375 . . . 4 (𝜑 → (𝑃 pCnt ((((#‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((#‘𝑋) / (𝑃𝑁)))) = ((𝑃 pCnt (((#‘𝑋) − 1)C((𝑃𝑁) − 1))) + (𝑃 pCnt ((#‘𝑋) / (𝑃𝑁)))))
80 1cnd 10094 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
8155, 59, 80npncand 10454 . . . . . . . 8 (𝜑 → (((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1)) = ((#‘𝑋) − 1))
8281oveq1d 6705 . . . . . . 7 (𝜑 → ((((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1)) = (((#‘𝑋) − 1)C((𝑃𝑁) − 1)))
8382oveq2d 6706 . . . . . 6 (𝜑 → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = (𝑃 pCnt (((#‘𝑋) − 1)C((𝑃𝑁) − 1))))
846nnred 11073 . . . . . . . 8 (𝜑 → (𝑃𝑁) ∈ ℝ)
8584ltm1d 10994 . . . . . . 7 (𝜑 → ((𝑃𝑁) − 1) < (𝑃𝑁))
86 nnm1nn0 11372 . . . . . . . . 9 ((𝑃𝑁) ∈ ℕ → ((𝑃𝑁) − 1) ∈ ℕ0)
876, 86syl 17 . . . . . . . 8 (𝜑 → ((𝑃𝑁) − 1) ∈ ℕ0)
88 breq1 4688 . . . . . . . . . . 11 (𝑥 = 0 → (𝑥 < (𝑃𝑁) ↔ 0 < (𝑃𝑁)))
89 bcxmaslem1 14610 . . . . . . . . . . . . 13 (𝑥 = 0 → ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥) = ((((#‘𝑋) − (𝑃𝑁)) + 0)C0))
9089oveq2d 6706 . . . . . . . . . . . 12 (𝑥 = 0 → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 0)C0)))
9190eqeq1d 2653 . . . . . . . . . . 11 (𝑥 = 0 → ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 0)C0)) = 0))
9288, 91imbi12d 333 . . . . . . . . . 10 (𝑥 = 0 → ((𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0) ↔ (0 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 0)C0)) = 0)))
9392imbi2d 329 . . . . . . . . 9 (𝑥 = 0 → ((𝜑 → (𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (0 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 0)C0)) = 0))))
94 breq1 4688 . . . . . . . . . . 11 (𝑥 = 𝑛 → (𝑥 < (𝑃𝑁) ↔ 𝑛 < (𝑃𝑁)))
95 bcxmaslem1 14610 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥) = ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛))
9695oveq2d 6706 . . . . . . . . . . . 12 (𝑥 = 𝑛 → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)))
9796eqeq1d 2653 . . . . . . . . . . 11 (𝑥 = 𝑛 → ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0))
9894, 97imbi12d 333 . . . . . . . . . 10 (𝑥 = 𝑛 → ((𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0) ↔ (𝑛 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0)))
9998imbi2d 329 . . . . . . . . 9 (𝑥 = 𝑛 → ((𝜑 → (𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (𝑛 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0))))
100 breq1 4688 . . . . . . . . . . 11 (𝑥 = (𝑛 + 1) → (𝑥 < (𝑃𝑁) ↔ (𝑛 + 1) < (𝑃𝑁)))
101 bcxmaslem1 14610 . . . . . . . . . . . . 13 (𝑥 = (𝑛 + 1) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥) = ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1)))
102101oveq2d 6706 . . . . . . . . . . . 12 (𝑥 = (𝑛 + 1) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))))
103102eqeq1d 2653 . . . . . . . . . . 11 (𝑥 = (𝑛 + 1) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))
104100, 103imbi12d 333 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → ((𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0) ↔ ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)))
105104imbi2d 329 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))))
106 breq1 4688 . . . . . . . . . . 11 (𝑥 = ((𝑃𝑁) − 1) → (𝑥 < (𝑃𝑁) ↔ ((𝑃𝑁) − 1) < (𝑃𝑁)))
107 bcxmaslem1 14610 . . . . . . . . . . . . 13 (𝑥 = ((𝑃𝑁) − 1) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥) = ((((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1)))
108107oveq2d 6706 . . . . . . . . . . . 12 (𝑥 = ((𝑃𝑁) − 1) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))))
109108eqeq1d 2653 . . . . . . . . . . 11 (𝑥 = ((𝑃𝑁) − 1) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0))
110106, 109imbi12d 333 . . . . . . . . . 10 (𝑥 = ((𝑃𝑁) − 1) → ((𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0) ↔ (((𝑃𝑁) − 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0)))
111110imbi2d 329 . . . . . . . . 9 (𝑥 = ((𝑃𝑁) − 1) → ((𝜑 → (𝑥 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (((𝑃𝑁) − 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0))))
112 znn0sub 11462 . . . . . . . . . . . . . . . 16 (((𝑃𝑁) ∈ ℤ ∧ (#‘𝑋) ∈ ℤ) → ((𝑃𝑁) ≤ (#‘𝑋) ↔ ((#‘𝑋) − (𝑃𝑁)) ∈ ℕ0))
1137, 34, 112syl2anc 694 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑃𝑁) ≤ (#‘𝑋) ↔ ((#‘𝑋) − (𝑃𝑁)) ∈ ℕ0))
11430, 113mpbid 222 . . . . . . . . . . . . . 14 (𝜑 → ((#‘𝑋) − (𝑃𝑁)) ∈ ℕ0)
115 0nn0 11345 . . . . . . . . . . . . . 14 0 ∈ ℕ0
116 nn0addcl 11366 . . . . . . . . . . . . . 14 ((((#‘𝑋) − (𝑃𝑁)) ∈ ℕ0 ∧ 0 ∈ ℕ0) → (((#‘𝑋) − (𝑃𝑁)) + 0) ∈ ℕ0)
117114, 115, 116sylancl 695 . . . . . . . . . . . . 13 (𝜑 → (((#‘𝑋) − (𝑃𝑁)) + 0) ∈ ℕ0)
118 bcn0 13137 . . . . . . . . . . . . 13 ((((#‘𝑋) − (𝑃𝑁)) + 0) ∈ ℕ0 → ((((#‘𝑋) − (𝑃𝑁)) + 0)C0) = 1)
119117, 118syl 17 . . . . . . . . . . . 12 (𝜑 → ((((#‘𝑋) − (𝑃𝑁)) + 0)C0) = 1)
120119oveq2d 6706 . . . . . . . . . . 11 (𝜑 → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 0)C0)) = (𝑃 pCnt 1))
121 pc1 15607 . . . . . . . . . . . 12 (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0)
1222, 121syl 17 . . . . . . . . . . 11 (𝜑 → (𝑃 pCnt 1) = 0)
123120, 122eqtrd 2685 . . . . . . . . . 10 (𝜑 → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 0)C0)) = 0)
124123a1d 25 . . . . . . . . 9 (𝜑 → (0 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 0)C0)) = 0))
125 nn0re 11339 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
126125ad2antrl 764 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ∈ ℝ)
127 nn0p1nn 11370 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ)
128127ad2antrl 764 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) ∈ ℕ)
129128nnred 11073 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) ∈ ℝ)
1306adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃𝑁) ∈ ℕ)
131130nnred 11073 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃𝑁) ∈ ℝ)
132126ltp1d 10992 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 < (𝑛 + 1))
133 simprr 811 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) < (𝑃𝑁))
134126, 129, 131, 132, 133lttrd 10236 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 < (𝑃𝑁))
135134expr 642 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((𝑛 + 1) < (𝑃𝑁) → 𝑛 < (𝑃𝑁)))
136135imim1d 82 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → ((𝑛 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0) → ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0)))
137 oveq1 6697 . . . . . . . . . . . . . . 15 ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0 → ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
138114adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((#‘𝑋) − (𝑃𝑁)) ∈ ℕ0)
139138nn0cnd 11391 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((#‘𝑋) − (𝑃𝑁)) ∈ ℂ)
140 nn0cn 11340 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
141140ad2antrl 764 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ∈ ℂ)
142 1cnd 10094 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 1 ∈ ℂ)
143139, 141, 142addassd 10100 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) = (((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1)))
144143oveq1d 6705 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1)))
145 nn0addge2 11378 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℝ ∧ ((#‘𝑋) − (𝑃𝑁)) ∈ ℕ0) → 𝑛 ≤ (((#‘𝑋) − (𝑃𝑁)) + 𝑛))
146126, 138, 145syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ≤ (((#‘𝑋) − (𝑃𝑁)) + 𝑛))
147 simprl 809 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ∈ ℕ0)
148147, 32syl6eleq 2740 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ∈ (ℤ‘0))
149138, 147nn0addcld 11393 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((#‘𝑋) − (𝑃𝑁)) + 𝑛) ∈ ℕ0)
150149nn0zd 11518 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((#‘𝑋) − (𝑃𝑁)) + 𝑛) ∈ ℤ)
151 elfz5 12372 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ℤ‘0) ∧ (((#‘𝑋) − (𝑃𝑁)) + 𝑛) ∈ ℤ) → (𝑛 ∈ (0...(((#‘𝑋) − (𝑃𝑁)) + 𝑛)) ↔ 𝑛 ≤ (((#‘𝑋) − (𝑃𝑁)) + 𝑛)))
152148, 150, 151syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 ∈ (0...(((#‘𝑋) − (𝑃𝑁)) + 𝑛)) ↔ 𝑛 ≤ (((#‘𝑋) − (𝑃𝑁)) + 𝑛)))
153146, 152mpbird 247 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑛 ∈ (0...(((#‘𝑋) − (𝑃𝑁)) + 𝑛)))
154 bcp1nk 13144 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (0...(((#‘𝑋) − (𝑃𝑁)) + 𝑛)) → (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = (((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))))
155153, 154syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = (((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))))
156144, 155eqtr3d 2687 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1)) = (((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))))
157156oveq2d 6706 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
1582adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑃 ∈ ℙ)
159 bccl2 13150 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (0...(((#‘𝑋) − (𝑃𝑁)) + 𝑛)) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℕ)
160153, 159syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℕ)
161 nnq 11839 . . . . . . . . . . . . . . . . . . 19 (((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℕ → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℚ)
162160, 161syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℚ)
163160nnne0d 11103 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ≠ 0)
164150peano2zd 11523 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℤ)
165 znq 11830 . . . . . . . . . . . . . . . . . . 19 ((((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) → (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℚ)
166164, 128, 165syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℚ)
167 nn0p1nn 11370 . . . . . . . . . . . . . . . . . . . . 21 ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) ∈ ℕ0 → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℕ)
168149, 167syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℕ)
169 nnrp 11880 . . . . . . . . . . . . . . . . . . . . 21 (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℕ → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℝ+)
170 nnrp 11880 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 + 1) ∈ ℕ → (𝑛 + 1) ∈ ℝ+)
171 rpdivcl 11894 . . . . . . . . . . . . . . . . . . . . 21 ((((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℝ+ ∧ (𝑛 + 1) ∈ ℝ+) → (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
172169, 170, 171syl2an 493 . . . . . . . . . . . . . . . . . . . 20 ((((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) → (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
173168, 128, 172syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
174173rpne0d 11915 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ≠ 0)
175 pcqmul 15605 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ (((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ∈ ℚ ∧ ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) ≠ 0) ∧ ((((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℚ ∧ (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ≠ 0)) → (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
176158, 162, 163, 166, 174, 175syl122anc 1375 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
177157, 176eqtrd 2685 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
178168nnne0d 11103 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ≠ 0)
179 pcdiv 15604 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℙ ∧ (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ∈ ℤ ∧ ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) ≠ 0) ∧ (𝑛 + 1) ∈ ℕ) → (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1))))
180158, 164, 178, 128, 179syl121anc 1371 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1))))
181128nncnd 11074 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) ∈ ℂ)
182139, 181addcomd 10276 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1)) = ((𝑛 + 1) + ((#‘𝑋) − (𝑃𝑁))))
183143, 182eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) = ((𝑛 + 1) + ((#‘𝑋) − (𝑃𝑁))))
184183oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((#‘𝑋) − (𝑃𝑁)))))
185 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) = 0) → ((#‘𝑋) − (𝑃𝑁)) = 0)
186185oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) = 0) → ((𝑛 + 1) + ((#‘𝑋) − (𝑃𝑁))) = ((𝑛 + 1) + 0))
187181addid1d 10274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑛 + 1) + 0) = (𝑛 + 1))
188187adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) = 0) → ((𝑛 + 1) + 0) = (𝑛 + 1))
189186, 188eqtr2d 2686 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) = 0) → (𝑛 + 1) = ((𝑛 + 1) + ((#‘𝑋) − (𝑃𝑁))))
190189oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) = 0) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((#‘𝑋) − (𝑃𝑁)))))
1912ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → 𝑃 ∈ ℙ)
192 nnq 11839 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 + 1) ∈ ℕ → (𝑛 + 1) ∈ ℚ)
193128, 192syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) ∈ ℚ)
194193adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑛 + 1) ∈ ℚ)
195138nn0zd 11518 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((#‘𝑋) − (𝑃𝑁)) ∈ ℤ)
196 zq 11832 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#‘𝑋) − (𝑃𝑁)) ∈ ℤ → ((#‘𝑋) − (𝑃𝑁)) ∈ ℚ)
197195, 196syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((#‘𝑋) − (𝑃𝑁)) ∈ ℚ)
198197adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → ((#‘𝑋) − (𝑃𝑁)) ∈ ℚ)
199158, 128pccld 15602 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℕ0)
200199nn0red 11390 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ)
201200adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ)
2025adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑁 ∈ ℕ0)
203202nn0red 11390 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 𝑁 ∈ ℝ)
204203adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → 𝑁 ∈ ℝ)
205 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → ((#‘𝑋) − (𝑃𝑁)) ≠ 0)
206205neneqd 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → ¬ ((#‘𝑋) − (𝑃𝑁)) = 0)
207114ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → ((#‘𝑋) − (𝑃𝑁)) ∈ ℕ0)
208 elnn0 11332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((#‘𝑋) − (𝑃𝑁)) ∈ ℕ0 ↔ (((#‘𝑋) − (𝑃𝑁)) ∈ ℕ ∨ ((#‘𝑋) − (𝑃𝑁)) = 0))
209207, 208sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (((#‘𝑋) − (𝑃𝑁)) ∈ ℕ ∨ ((#‘𝑋) − (𝑃𝑁)) = 0))
210209ord 391 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (¬ ((#‘𝑋) − (𝑃𝑁)) ∈ ℕ → ((#‘𝑋) − (𝑃𝑁)) = 0))
211206, 210mt3d 140 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → ((#‘𝑋) − (𝑃𝑁)) ∈ ℕ)
212191, 211pccld 15602 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt ((#‘𝑋) − (𝑃𝑁))) ∈ ℕ0)
213212nn0red 11390 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt ((#‘𝑋) − (𝑃𝑁))) ∈ ℝ)
214128nnzd 11519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑛 + 1) ∈ ℤ)
215 pcdvdsb 15620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑃 ∈ ℙ ∧ (𝑛 + 1) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃𝑁) ∥ (𝑛 + 1)))
216158, 214, 202, 215syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃𝑁) ∥ (𝑛 + 1)))
2177adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃𝑁) ∈ ℤ)
218 dvdsle 15079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑃𝑁) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) → ((𝑃𝑁) ∥ (𝑛 + 1) → (𝑃𝑁) ≤ (𝑛 + 1)))
219217, 128, 218syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑃𝑁) ∥ (𝑛 + 1) → (𝑃𝑁) ≤ (𝑛 + 1)))
220216, 219sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) → (𝑃𝑁) ≤ (𝑛 + 1)))
221203, 200lenltd 10221 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ ¬ (𝑃 pCnt (𝑛 + 1)) < 𝑁))
222131, 129lenltd 10221 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑃𝑁) ≤ (𝑛 + 1) ↔ ¬ (𝑛 + 1) < (𝑃𝑁)))
223220, 221, 2223imtr3d 282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (¬ (𝑃 pCnt (𝑛 + 1)) < 𝑁 → ¬ (𝑛 + 1) < (𝑃𝑁)))
224133, 223mt4d 152 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (𝑛 + 1)) < 𝑁)
225224adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) < 𝑁)
226 dvdssubr 15074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑃𝑁) ∈ ℤ ∧ (#‘𝑋) ∈ ℤ) → ((𝑃𝑁) ∥ (#‘𝑋) ↔ (𝑃𝑁) ∥ ((#‘𝑋) − (𝑃𝑁))))
2277, 34, 226syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((𝑃𝑁) ∥ (#‘𝑋) ↔ (𝑃𝑁) ∥ ((#‘𝑋) − (𝑃𝑁))))
22813, 227mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑃𝑁) ∥ ((#‘𝑋) − (𝑃𝑁)))
229228ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃𝑁) ∥ ((#‘𝑋) − (𝑃𝑁)))
230207nn0zd 11518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → ((#‘𝑋) − (𝑃𝑁)) ∈ ℤ)
2315ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → 𝑁 ∈ ℕ0)
232 pcdvdsb 15620 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ ℙ ∧ ((#‘𝑋) − (𝑃𝑁)) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ (𝑃 pCnt ((#‘𝑋) − (𝑃𝑁))) ↔ (𝑃𝑁) ∥ ((#‘𝑋) − (𝑃𝑁))))
233191, 230, 231, 232syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑁 ≤ (𝑃 pCnt ((#‘𝑋) − (𝑃𝑁))) ↔ (𝑃𝑁) ∥ ((#‘𝑋) − (𝑃𝑁))))
234229, 233mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → 𝑁 ≤ (𝑃 pCnt ((#‘𝑋) − (𝑃𝑁))))
235201, 204, 213, 225, 234ltletrd 10235 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) < (𝑃 pCnt ((#‘𝑋) − (𝑃𝑁))))
236191, 194, 198, 235pcadd2 15641 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) ∧ ((#‘𝑋) − (𝑃𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((#‘𝑋) − (𝑃𝑁)))))
237190, 236pm2.61dane 2910 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((#‘𝑋) − (𝑃𝑁)))))
238184, 237eqtr4d 2688 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) = (𝑃 pCnt (𝑛 + 1)))
239199nn0cnd 11391 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℂ)
240238, 239eqeltrd 2730 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) ∈ ℂ)
241240, 238subeq0bd 10494 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1))) = 0)
242180, 241eqtrd 2685 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = 0)
243242oveq2d 6706 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → (0 + (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + 0))
244 00id 10249 . . . . . . . . . . . . . . . . 17 (0 + 0) = 0
245243, 244syl6req 2702 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → 0 = (0 + (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))
246177, 245eqeq12d 2666 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0 ↔ ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + (𝑃 pCnt (((((#‘𝑋) − (𝑃𝑁)) + 𝑛) + 1) / (𝑛 + 1))))))
247137, 246syl5ibr 236 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃𝑁))) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0 → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))
248247expr 642 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((𝑛 + 1) < (𝑃𝑁) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0 → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)))
249248a2d 29 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0) → ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)))
250136, 249syld 47 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ((𝑛 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0) → ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)))
251250expcom 450 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → (𝜑 → ((𝑛 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0) → ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))))
252251a2d 29 . . . . . . . . 9 (𝑛 ∈ ℕ0 → ((𝜑 → (𝑛 < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + 𝑛)C𝑛)) = 0)) → (𝜑 → ((𝑛 + 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))))
25393, 99, 105, 111, 124, 252nn0ind 11510 . . . . . . . 8 (((𝑃𝑁) − 1) ∈ ℕ0 → (𝜑 → (((𝑃𝑁) − 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0)))
25487, 253mpcom 38 . . . . . . 7 (𝜑 → (((𝑃𝑁) − 1) < (𝑃𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0))
25585, 254mpd 15 . . . . . 6 (𝜑 → (𝑃 pCnt ((((#‘𝑋) − (𝑃𝑁)) + ((𝑃𝑁) − 1))C((𝑃𝑁) − 1))) = 0)
25683, 255eqtr3d 2687 . . . . 5 (𝜑 → (𝑃 pCnt (((#‘𝑋) − 1)C((𝑃𝑁) − 1))) = 0)
257 pcdiv 15604 . . . . . . 7 ((𝑃 ∈ ℙ ∧ ((#‘𝑋) ∈ ℤ ∧ (#‘𝑋) ≠ 0) ∧ (𝑃𝑁) ∈ ℕ) → (𝑃 pCnt ((#‘𝑋) / (𝑃𝑁))) = ((𝑃 pCnt (#‘𝑋)) − (𝑃 pCnt (𝑃𝑁))))
2582, 34, 76, 6, 257syl121anc 1371 . . . . . 6 (𝜑 → (𝑃 pCnt ((#‘𝑋) / (𝑃𝑁))) = ((𝑃 pCnt (#‘𝑋)) − (𝑃 pCnt (𝑃𝑁))))
2595nn0zd 11518 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
260 pcid 15624 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝑃𝑁)) = 𝑁)
2612, 259, 260syl2anc 694 . . . . . . 7 (𝜑 → (𝑃 pCnt (𝑃𝑁)) = 𝑁)
262261oveq2d 6706 . . . . . 6 (𝜑 → ((𝑃 pCnt (#‘𝑋)) − (𝑃 pCnt (𝑃𝑁))) = ((𝑃 pCnt (#‘𝑋)) − 𝑁))
263258, 262eqtrd 2685 . . . . 5 (𝜑 → (𝑃 pCnt ((#‘𝑋) / (𝑃𝑁))) = ((𝑃 pCnt (#‘𝑋)) − 𝑁))
264256, 263oveq12d 6708 . . . 4 (𝜑 → ((𝑃 pCnt (((#‘𝑋) − 1)C((𝑃𝑁) − 1))) + (𝑃 pCnt ((#‘𝑋) / (𝑃𝑁)))) = (0 + ((𝑃 pCnt (#‘𝑋)) − 𝑁)))
2652, 27pccld 15602 . . . . . . . 8 (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈ ℕ0)
266265nn0zd 11518 . . . . . . 7 (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈ ℤ)
267266, 259zsubcld 11525 . . . . . 6 (𝜑 → ((𝑃 pCnt (#‘𝑋)) − 𝑁) ∈ ℤ)
268267zcnd 11521 . . . . 5 (𝜑 → ((𝑃 pCnt (#‘𝑋)) − 𝑁) ∈ ℂ)
269268addid2d 10275 . . . 4 (𝜑 → (0 + ((𝑃 pCnt (#‘𝑋)) − 𝑁)) = ((𝑃 pCnt (#‘𝑋)) − 𝑁))
27079, 264, 2693eqtrd 2689 . . 3 (𝜑 → (𝑃 pCnt ((((#‘𝑋) − 1)C((𝑃𝑁) − 1)) · ((#‘𝑋) / (𝑃𝑁)))) = ((𝑃 pCnt (#‘𝑋)) − 𝑁))
27166, 67, 2703eqtr3d 2693 . 2 (𝜑 → (𝑃 pCnt (#‘𝑆)) = ((𝑃 pCnt (#‘𝑋)) − 𝑁))
27240, 271jca 553 1 (𝜑 → ((#‘𝑆) ∈ ℕ ∧ (𝑃 pCnt (#‘𝑆)) = ((𝑃 pCnt (#‘𝑋)) − 𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  wne 2823  {crab 2945  c0 3948  𝒫 cpw 4191   class class class wbr 4685  cfv 5926  (class class class)co 6690  Fincfn 7997  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  cn 11058  0cn0 11330  cz 11415  cuz 11725  cq 11826  +crp 11870  ...cfz 12364  cexp 12900  Ccbc 13129  #chash 13157  cdvds 15027  cprime 15432   pCnt cpc 15588  Basecbs 15904  +gcplusg 15988  Grpcgrp 17469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-fz 12365  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-dvds 15028  df-gcd 15264  df-prm 15433  df-pc 15589  df-0g 16149  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-grp 17472
This theorem is referenced by:  sylow1lem3  18061
  Copyright terms: Public domain W3C validator