Step | Hyp | Ref
| Expression |
1 | | sylow1.f |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | sylow1.p |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℙ) |
3 | | prmnn 16323 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
5 | | sylow1.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
6 | 4, 5 | nnexpcld 13904 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℕ) |
7 | 6 | nnzd 12370 |
. . . . 5
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℤ) |
8 | | hashbc 14109 |
. . . . 5
⊢ ((𝑋 ∈ Fin ∧ (𝑃↑𝑁) ∈ ℤ) →
((♯‘𝑋)C(𝑃↑𝑁)) = (♯‘{𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)})) |
9 | 1, 7, 8 | syl2anc 583 |
. . . 4
⊢ (𝜑 → ((♯‘𝑋)C(𝑃↑𝑁)) = (♯‘{𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)})) |
10 | | sylow1lem.s |
. . . . 5
⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)} |
11 | 10 | fveq2i 6764 |
. . . 4
⊢
(♯‘𝑆) =
(♯‘{𝑠 ∈
𝒫 𝑋 ∣
(♯‘𝑠) = (𝑃↑𝑁)}) |
12 | 9, 11 | eqtr4di 2795 |
. . 3
⊢ (𝜑 → ((♯‘𝑋)C(𝑃↑𝑁)) = (♯‘𝑆)) |
13 | | sylow1.d |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑁) ∥ (♯‘𝑋)) |
14 | | sylow1.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ Grp) |
15 | | sylow1.x |
. . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝐺) |
16 | 15 | grpbn0 18552 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≠ ∅) |
18 | | hasheq0 14022 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Fin →
((♯‘𝑋) = 0
↔ 𝑋 =
∅)) |
19 | 1, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝑋) = 0 ↔ 𝑋 = ∅)) |
20 | 19 | necon3bbid 2979 |
. . . . . . . . 9
⊢ (𝜑 → (¬
(♯‘𝑋) = 0
↔ 𝑋 ≠
∅)) |
21 | 17, 20 | mpbird 256 |
. . . . . . . 8
⊢ (𝜑 → ¬ (♯‘𝑋) = 0) |
22 | | hashcl 14015 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Fin →
(♯‘𝑋) ∈
ℕ0) |
23 | 1, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑋) ∈
ℕ0) |
24 | | elnn0 12181 |
. . . . . . . . . 10
⊢
((♯‘𝑋)
∈ ℕ0 ↔ ((♯‘𝑋) ∈ ℕ ∨ (♯‘𝑋) = 0)) |
25 | 23, 24 | sylib 217 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘𝑋) ∈ ℕ ∨
(♯‘𝑋) =
0)) |
26 | 25 | ord 860 |
. . . . . . . 8
⊢ (𝜑 → (¬
(♯‘𝑋) ∈
ℕ → (♯‘𝑋) = 0)) |
27 | 21, 26 | mt3d 148 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑋) ∈
ℕ) |
28 | | dvdsle 15963 |
. . . . . . 7
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (♯‘𝑋) ∈ ℕ) → ((𝑃↑𝑁) ∥ (♯‘𝑋) → (𝑃↑𝑁) ≤ (♯‘𝑋))) |
29 | 7, 27, 28 | syl2anc 583 |
. . . . . 6
⊢ (𝜑 → ((𝑃↑𝑁) ∥ (♯‘𝑋) → (𝑃↑𝑁) ≤ (♯‘𝑋))) |
30 | 13, 29 | mpd 15 |
. . . . 5
⊢ (𝜑 → (𝑃↑𝑁) ≤ (♯‘𝑋)) |
31 | 6 | nnnn0d 12239 |
. . . . . . 7
⊢ (𝜑 → (𝑃↑𝑁) ∈
ℕ0) |
32 | | nn0uz 12565 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
33 | 31, 32 | eleqtrdi 2847 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑁) ∈
(ℤ≥‘0)) |
34 | 23 | nn0zd 12369 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑋) ∈
ℤ) |
35 | | elfz5 13193 |
. . . . . 6
⊢ (((𝑃↑𝑁) ∈ (ℤ≥‘0)
∧ (♯‘𝑋)
∈ ℤ) → ((𝑃↑𝑁) ∈ (0...(♯‘𝑋)) ↔ (𝑃↑𝑁) ≤ (♯‘𝑋))) |
36 | 33, 34, 35 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → ((𝑃↑𝑁) ∈ (0...(♯‘𝑋)) ↔ (𝑃↑𝑁) ≤ (♯‘𝑋))) |
37 | 30, 36 | mpbird 256 |
. . . 4
⊢ (𝜑 → (𝑃↑𝑁) ∈ (0...(♯‘𝑋))) |
38 | | bccl2 13981 |
. . . 4
⊢ ((𝑃↑𝑁) ∈ (0...(♯‘𝑋)) → ((♯‘𝑋)C(𝑃↑𝑁)) ∈ ℕ) |
39 | 37, 38 | syl 17 |
. . 3
⊢ (𝜑 → ((♯‘𝑋)C(𝑃↑𝑁)) ∈ ℕ) |
40 | 12, 39 | eqeltrrd 2838 |
. 2
⊢ (𝜑 → (♯‘𝑆) ∈
ℕ) |
41 | | nnuz 12566 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
42 | 6, 41 | eleqtrdi 2847 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃↑𝑁) ∈
(ℤ≥‘1)) |
43 | | elfz5 13193 |
. . . . . . . . . 10
⊢ (((𝑃↑𝑁) ∈ (ℤ≥‘1)
∧ (♯‘𝑋)
∈ ℤ) → ((𝑃↑𝑁) ∈ (1...(♯‘𝑋)) ↔ (𝑃↑𝑁) ≤ (♯‘𝑋))) |
44 | 42, 34, 43 | syl2anc 583 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃↑𝑁) ∈ (1...(♯‘𝑋)) ↔ (𝑃↑𝑁) ≤ (♯‘𝑋))) |
45 | 30, 44 | mpbird 256 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑁) ∈ (1...(♯‘𝑋))) |
46 | | 1zzd 12297 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
47 | | fzsubel 13237 |
. . . . . . . . 9
⊢ (((1
∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) ∧ ((𝑃↑𝑁) ∈ ℤ ∧ 1 ∈ ℤ))
→ ((𝑃↑𝑁) ∈
(1...(♯‘𝑋))
↔ ((𝑃↑𝑁) − 1) ∈ ((1 −
1)...((♯‘𝑋)
− 1)))) |
48 | 46, 34, 7, 46, 47 | syl22anc 835 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃↑𝑁) ∈ (1...(♯‘𝑋)) ↔ ((𝑃↑𝑁) − 1) ∈ ((1 −
1)...((♯‘𝑋)
− 1)))) |
49 | 45, 48 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → ((𝑃↑𝑁) − 1) ∈ ((1 −
1)...((♯‘𝑋)
− 1))) |
50 | | 1m1e0 11991 |
. . . . . . . 8
⊢ (1
− 1) = 0 |
51 | 50 | oveq1i 7270 |
. . . . . . 7
⊢ ((1
− 1)...((♯‘𝑋) − 1)) = (0...((♯‘𝑋) − 1)) |
52 | 49, 51 | eleqtrdi 2847 |
. . . . . 6
⊢ (𝜑 → ((𝑃↑𝑁) − 1) ∈
(0...((♯‘𝑋)
− 1))) |
53 | | bcp1nk 13975 |
. . . . . 6
⊢ (((𝑃↑𝑁) − 1) ∈
(0...((♯‘𝑋)
− 1)) → ((((♯‘𝑋) − 1) + 1)C(((𝑃↑𝑁) − 1) + 1)) = ((((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) ·
((((♯‘𝑋)
− 1) + 1) / (((𝑃↑𝑁) − 1) + 1)))) |
54 | 52, 53 | syl 17 |
. . . . 5
⊢ (𝜑 → ((((♯‘𝑋) − 1) + 1)C(((𝑃↑𝑁) − 1) + 1)) = ((((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) ·
((((♯‘𝑋)
− 1) + 1) / (((𝑃↑𝑁) − 1) + 1)))) |
55 | 23 | nn0cnd 12241 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑋) ∈
ℂ) |
56 | | ax-1cn 10876 |
. . . . . . 7
⊢ 1 ∈
ℂ |
57 | | npcan 11176 |
. . . . . . 7
⊢
(((♯‘𝑋)
∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘𝑋) − 1) + 1) =
(♯‘𝑋)) |
58 | 55, 56, 57 | sylancl 585 |
. . . . . 6
⊢ (𝜑 → (((♯‘𝑋) − 1) + 1) =
(♯‘𝑋)) |
59 | 6 | nncnd 11935 |
. . . . . . 7
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℂ) |
60 | | npcan 11176 |
. . . . . . 7
⊢ (((𝑃↑𝑁) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝑃↑𝑁) − 1) + 1) = (𝑃↑𝑁)) |
61 | 59, 56, 60 | sylancl 585 |
. . . . . 6
⊢ (𝜑 → (((𝑃↑𝑁) − 1) + 1) = (𝑃↑𝑁)) |
62 | 58, 61 | oveq12d 7278 |
. . . . 5
⊢ (𝜑 → ((((♯‘𝑋) − 1) + 1)C(((𝑃↑𝑁) − 1) + 1)) = ((♯‘𝑋)C(𝑃↑𝑁))) |
63 | 58, 61 | oveq12d 7278 |
. . . . . 6
⊢ (𝜑 → ((((♯‘𝑋) − 1) + 1) / (((𝑃↑𝑁) − 1) + 1)) = ((♯‘𝑋) / (𝑃↑𝑁))) |
64 | 63 | oveq2d 7276 |
. . . . 5
⊢ (𝜑 → ((((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) ·
((((♯‘𝑋)
− 1) + 1) / (((𝑃↑𝑁) − 1) + 1))) =
((((♯‘𝑋)
− 1)C((𝑃↑𝑁) − 1)) ·
((♯‘𝑋) / (𝑃↑𝑁)))) |
65 | 54, 62, 64 | 3eqtr3d 2785 |
. . . 4
⊢ (𝜑 → ((♯‘𝑋)C(𝑃↑𝑁)) = ((((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((♯‘𝑋) / (𝑃↑𝑁)))) |
66 | 65 | oveq2d 7276 |
. . 3
⊢ (𝜑 → (𝑃 pCnt ((♯‘𝑋)C(𝑃↑𝑁))) = (𝑃 pCnt ((((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((♯‘𝑋) / (𝑃↑𝑁))))) |
67 | 12 | oveq2d 7276 |
. . 3
⊢ (𝜑 → (𝑃 pCnt ((♯‘𝑋)C(𝑃↑𝑁))) = (𝑃 pCnt (♯‘𝑆))) |
68 | | bccl2 13981 |
. . . . . . 7
⊢ (((𝑃↑𝑁) − 1) ∈
(0...((♯‘𝑋)
− 1)) → (((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) ∈
ℕ) |
69 | 52, 68 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) ∈
ℕ) |
70 | 69 | nnzd 12370 |
. . . . 5
⊢ (𝜑 → (((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) ∈
ℤ) |
71 | 69 | nnne0d 11969 |
. . . . 5
⊢ (𝜑 → (((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) ≠ 0) |
72 | 6 | nnne0d 11969 |
. . . . . . 7
⊢ (𝜑 → (𝑃↑𝑁) ≠ 0) |
73 | | dvdsval2 15910 |
. . . . . . 7
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (𝑃↑𝑁) ≠ 0 ∧ (♯‘𝑋) ∈ ℤ) → ((𝑃↑𝑁) ∥ (♯‘𝑋) ↔ ((♯‘𝑋) / (𝑃↑𝑁)) ∈ ℤ)) |
74 | 7, 72, 34, 73 | syl3anc 1369 |
. . . . . 6
⊢ (𝜑 → ((𝑃↑𝑁) ∥ (♯‘𝑋) ↔ ((♯‘𝑋) / (𝑃↑𝑁)) ∈ ℤ)) |
75 | 13, 74 | mpbid 231 |
. . . . 5
⊢ (𝜑 → ((♯‘𝑋) / (𝑃↑𝑁)) ∈ ℤ) |
76 | 27 | nnne0d 11969 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑋) ≠ 0) |
77 | 55, 59, 76, 72 | divne0d 11713 |
. . . . 5
⊢ (𝜑 → ((♯‘𝑋) / (𝑃↑𝑁)) ≠ 0) |
78 | | pcmul 16496 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧
((((♯‘𝑋)
− 1)C((𝑃↑𝑁) − 1)) ∈ ℤ
∧ (((♯‘𝑋)
− 1)C((𝑃↑𝑁) − 1)) ≠ 0) ∧
(((♯‘𝑋) /
(𝑃↑𝑁)) ∈ ℤ ∧
((♯‘𝑋) / (𝑃↑𝑁)) ≠ 0)) → (𝑃 pCnt ((((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((♯‘𝑋) / (𝑃↑𝑁)))) = ((𝑃 pCnt (((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1))) + (𝑃 pCnt ((♯‘𝑋) / (𝑃↑𝑁))))) |
79 | 2, 70, 71, 75, 77, 78 | syl122anc 1377 |
. . . 4
⊢ (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((♯‘𝑋) / (𝑃↑𝑁)))) = ((𝑃 pCnt (((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1))) + (𝑃 pCnt ((♯‘𝑋) / (𝑃↑𝑁))))) |
80 | | 1cnd 10917 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
81 | 55, 59, 80 | npncand 11302 |
. . . . . . . 8
⊢ (𝜑 → (((♯‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1)) = ((♯‘𝑋) − 1)) |
82 | 81 | oveq1d 7275 |
. . . . . . 7
⊢ (𝜑 → ((((♯‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1)) = (((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1))) |
83 | 82 | oveq2d 7276 |
. . . . . 6
⊢ (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = (𝑃 pCnt (((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)))) |
84 | 6 | nnred 11934 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℝ) |
85 | 84 | ltm1d 11853 |
. . . . . . 7
⊢ (𝜑 → ((𝑃↑𝑁) − 1) < (𝑃↑𝑁)) |
86 | | nnm1nn0 12220 |
. . . . . . . . 9
⊢ ((𝑃↑𝑁) ∈ ℕ → ((𝑃↑𝑁) − 1) ∈
ℕ0) |
87 | 6, 86 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃↑𝑁) − 1) ∈
ℕ0) |
88 | | breq1 5078 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝑥 < (𝑃↑𝑁) ↔ 0 < (𝑃↑𝑁))) |
89 | | bcxmaslem1 15490 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 →
((((♯‘𝑋)
− (𝑃↑𝑁)) + 𝑥)C𝑥) = ((((♯‘𝑋) − (𝑃↑𝑁)) + 0)C0)) |
90 | 89 | oveq2d 7276 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 0)C0))) |
91 | 90 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = 0)) |
92 | 88, 91 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → ((𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0) ↔ (0 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = 0))) |
93 | 92 | imbi2d 340 |
. . . . . . . . 9
⊢ (𝑥 = 0 → ((𝜑 → (𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (0 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = 0)))) |
94 | | breq1 5078 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → (𝑥 < (𝑃↑𝑁) ↔ 𝑛 < (𝑃↑𝑁))) |
95 | | bcxmaslem1 15490 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑛 → ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥) = ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) |
96 | 95 | oveq2d 7276 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑛 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛))) |
97 | 96 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0)) |
98 | 94, 97 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → ((𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0) ↔ (𝑛 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0))) |
99 | 98 | imbi2d 340 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (𝑛 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0)))) |
100 | | breq1 5078 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑛 + 1) → (𝑥 < (𝑃↑𝑁) ↔ (𝑛 + 1) < (𝑃↑𝑁))) |
101 | | bcxmaslem1 15490 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑛 + 1) → ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥) = ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) |
102 | 101 | oveq2d 7276 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑛 + 1) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1)))) |
103 | 102 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑛 + 1) → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)) |
104 | 100, 103 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0) ↔ ((𝑛 + 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))) |
105 | 104 | imbi2d 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))) |
108 | 107 | oveq2d 7276 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑃↑𝑁) − 1) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1)))) |
109 | 108 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑃↑𝑁) − 1) → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0)) |
110 | 106, 109 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑃↑𝑁) − 1) → ((𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0) ↔ (((𝑃↑𝑁) − 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0))) |
111 | 110 | imbi2d 340 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑃↑𝑁) − 1) → ((𝜑 → (𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (((𝑃↑𝑁) − 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0)))) |
112 | | znn0sub 12313 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) → ((𝑃↑𝑁) ≤ (♯‘𝑋) ↔ ((♯‘𝑋) − (𝑃↑𝑁)) ∈
ℕ0)) |
113 | 7, 34, 112 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑃↑𝑁) ≤ (♯‘𝑋) ↔ ((♯‘𝑋) − (𝑃↑𝑁)) ∈
ℕ0)) |
114 | 30, 113 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((♯‘𝑋) − (𝑃↑𝑁)) ∈
ℕ0) |
115 | | 0nn0 12194 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
116 | | nn0addcl 12214 |
. . . . . . . . . . . . . 14
⊢
((((♯‘𝑋)
− (𝑃↑𝑁)) ∈ ℕ0
∧ 0 ∈ ℕ0) → (((♯‘𝑋) − (𝑃↑𝑁)) + 0) ∈
ℕ0) |
117 | 114, 115,
116 | sylancl 585 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((♯‘𝑋) − (𝑃↑𝑁)) + 0) ∈
ℕ0) |
118 | | bcn0 13968 |
. . . . . . . . . . . . 13
⊢
((((♯‘𝑋)
− (𝑃↑𝑁)) + 0) ∈
ℕ0 → ((((♯‘𝑋) − (𝑃↑𝑁)) + 0)C0) = 1) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((♯‘𝑋) − (𝑃↑𝑁)) + 0)C0) = 1) |
120 | 119 | oveq2d 7276 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = (𝑃 pCnt 1)) |
121 | | pc1 16500 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) |
122 | 2, 121 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 pCnt 1) = 0) |
123 | 120, 122 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = 0) |
124 | 123 | a1d 25 |
. . . . . . . . 9
⊢ (𝜑 → (0 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = 0)) |
125 | | nn0re 12188 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℝ) |
126 | 125 | ad2antrl 724 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ∈ ℝ) |
127 | | nn0p1nn 12218 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) |
128 | 127 | ad2antrl 724 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) ∈ ℕ) |
129 | 128 | nnred 11934 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) ∈ ℝ) |
130 | 6 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃↑𝑁) ∈ ℕ) |
131 | 130 | nnred 11934 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃↑𝑁) ∈ ℝ) |
132 | 126 | ltp1d 11851 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 < (𝑛 + 1)) |
133 | | simprr 769 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) < (𝑃↑𝑁)) |
134 | 126, 129,
131, 132, 133 | lttrd 11082 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 < (𝑃↑𝑁)) |
135 | 134 | expr 456 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 + 1) < (𝑃↑𝑁) → 𝑛 < (𝑃↑𝑁))) |
136 | 135 | imim1d 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))))) |
138 | 114 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((♯‘𝑋) − (𝑃↑𝑁)) ∈
ℕ0) |
139 | 138 | nn0cnd 12241 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((♯‘𝑋) − (𝑃↑𝑁)) ∈ ℂ) |
140 | | nn0cn 12189 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) |
141 | 140 | ad2antrl 724 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ∈ ℂ) |
142 | | 1cnd 10917 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 1 ∈
ℂ) |
143 | 139, 141,
142 | addassd 10944 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) = (((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))) |
144 | 143 | oveq1d 7275 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) |
145 | | nn0addge2 12226 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℝ ∧
((♯‘𝑋) −
(𝑃↑𝑁)) ∈ ℕ0) → 𝑛 ≤ (((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)) |
146 | 126, 138,
145 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ≤ (((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)) |
147 | | simprl 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ∈ ℕ0) |
148 | 147, 32 | eleqtrdi 2847 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ∈
(ℤ≥‘0)) |
149 | 138, 147 | nn0addcld 12243 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) ∈
ℕ0) |
150 | 149 | nn0zd 12369 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) ∈ ℤ) |
151 | | elfz5 13193 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈
(ℤ≥‘0) ∧ (((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) ∈ ℤ) → (𝑛 ∈ (0...(((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)) ↔ 𝑛 ≤ (((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛))) |
152 | 148, 150,
151 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 ∈ (0...(((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)) ↔ 𝑛 ≤ (((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛))) |
153 | 146, 152 | mpbird 256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ∈ (0...(((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛))) |
154 | | bcp1nk 13975 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(0...(((♯‘𝑋)
− (𝑃↑𝑁)) + 𝑛)) → (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) |
156 | 144, 155 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1)) = (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) |
157 | 156 | oveq2d 7276 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))))) |
158 | 2 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑃 ∈ ℙ) |
159 | | bccl2 13981 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(0...(((♯‘𝑋)
− (𝑃↑𝑁)) + 𝑛)) → ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) ∈ ℕ) |
160 | 153, 159 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) ∈ ℕ) |
161 | | nnq 12647 |
. . . . . . . . . . . . . . 15
⊢
(((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) ∈ ℕ →
((((♯‘𝑋)
− (𝑃↑𝑁)) + 𝑛)C𝑛) ∈ ℚ) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) ∈ ℚ) |
163 | 160 | nnne0d 11969 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) ≠ 0) |
164 | 150 | peano2zd 12374 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℤ) |
165 | | znq 12637 |
. . . . . . . . . . . . . . 15
⊢
((((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) →
(((((♯‘𝑋)
− (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℚ) |
166 | 164, 128,
165 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℚ) |
167 | | nn0p1nn 12218 |
. . . . . . . . . . . . . . . . 17
⊢
((((♯‘𝑋)
− (𝑃↑𝑁)) + 𝑛) ∈ ℕ0 →
((((♯‘𝑋)
− (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℕ) |
168 | 149, 167 | syl 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)) ∈
ℝ+) |
172 | 169, 170,
171 | syl2an 595 |
. . . . . . . . . . . . . . . 16
⊢
((((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) →
(((((♯‘𝑋)
− (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈
ℝ+) |
173 | 168, 128,
172 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈
ℝ+) |
174 | 173 | rpne0d 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))))) |
176 | 158, 162,
163, 166, 174, 175 | syl122anc 1377 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) · (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))))) |
177 | 157, 176 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))))) |
178 | 168 | nnne0d 11969 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) ≠ 0) |
179 | | pcdiv 16497 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧
(((((♯‘𝑋)
− (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℤ ∧
((((♯‘𝑋)
− (𝑃↑𝑁)) + 𝑛) + 1) ≠ 0) ∧ (𝑛 + 1) ∈ ℕ) → (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1)))) |
180 | 158, 164,
178, 128, 179 | syl121anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1)))) |
181 | 128 | nncnd 11935 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) ∈ ℂ) |
182 | 139, 181,
143 | comraddd 11135 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) = ((𝑛 + 1) + ((♯‘𝑋) − (𝑃↑𝑁)))) |
183 | 182 | oveq2d 7276 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((♯‘𝑋) − (𝑃↑𝑁))))) |
184 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) = 0) → ((♯‘𝑋) − (𝑃↑𝑁)) = 0) |
185 | 184 | oveq2d 7276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) = 0) → ((𝑛 + 1) + ((♯‘𝑋) − (𝑃↑𝑁))) = ((𝑛 + 1) + 0)) |
186 | 181 | addid1d 11121 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑛 + 1) + 0) = (𝑛 + 1)) |
187 | 186 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) = 0) → ((𝑛 + 1) + 0) = (𝑛 + 1)) |
188 | 185, 187 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) = 0) → (𝑛 + 1) = ((𝑛 + 1) + ((♯‘𝑋) − (𝑃↑𝑁)))) |
189 | 188 | oveq2d 7276 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) = 0) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((♯‘𝑋) − (𝑃↑𝑁))))) |
190 | 2 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → 𝑃 ∈ ℙ) |
191 | | nnq 12647 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ∈
ℚ) |
192 | 128, 191 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) ∈ ℚ) |
193 | 192 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑛 + 1) ∈ ℚ) |
194 | 138 | nn0zd 12369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((♯‘𝑋) − (𝑃↑𝑁)) ∈ ℤ) |
195 | | zq 12639 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑋)
− (𝑃↑𝑁)) ∈ ℤ →
((♯‘𝑋) −
(𝑃↑𝑁)) ∈ ℚ) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((♯‘𝑋) − (𝑃↑𝑁)) ∈ ℚ) |
197 | 196 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ((♯‘𝑋) − (𝑃↑𝑁)) ∈ ℚ) |
198 | 158, 128 | pccld 16495 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈
ℕ0) |
199 | 198 | nn0red 12240 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ) |
200 | 199 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ) |
201 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑁 ∈
ℕ0) |
202 | 201 | nn0red 12240 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑁 ∈ ℝ) |
203 | 202 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → 𝑁 ∈ ℝ) |
204 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) |
205 | 204 | neneqd 2946 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ¬
((♯‘𝑋) −
(𝑃↑𝑁)) = 0) |
206 | 114 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ((♯‘𝑋) − (𝑃↑𝑁)) ∈
ℕ0) |
207 | | elnn0 12181 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝑋)
− (𝑃↑𝑁)) ∈ ℕ0
↔ (((♯‘𝑋)
− (𝑃↑𝑁)) ∈ ℕ ∨
((♯‘𝑋) −
(𝑃↑𝑁)) = 0)) |
208 | 206, 207 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (((♯‘𝑋) − (𝑃↑𝑁)) ∈ ℕ ∨ ((♯‘𝑋) − (𝑃↑𝑁)) = 0)) |
209 | 208 | ord 860 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (¬
((♯‘𝑋) −
(𝑃↑𝑁)) ∈ ℕ →
((♯‘𝑋) −
(𝑃↑𝑁)) = 0)) |
210 | 205, 209 | mt3d 148 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ((♯‘𝑋) − (𝑃↑𝑁)) ∈ ℕ) |
211 | 190, 210 | pccld 16495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt ((♯‘𝑋) − (𝑃↑𝑁))) ∈
ℕ0) |
212 | 211 | nn0red 12240 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt ((♯‘𝑋) − (𝑃↑𝑁))) ∈ ℝ) |
213 | 128 | nnzd 12370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) ∈ ℤ) |
214 | | pcdvdsb 16514 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℙ ∧ (𝑛 + 1) ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑𝑁) ∥ (𝑛 + 1))) |
215 | 158, 213,
201, 214 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑𝑁) ∥ (𝑛 + 1))) |
216 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃↑𝑁) ∈ ℤ) |
217 | | dvdsle 15963 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) → ((𝑃↑𝑁) ∥ (𝑛 + 1) → (𝑃↑𝑁) ≤ (𝑛 + 1))) |
218 | 216, 128,
217 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑃↑𝑁) ∥ (𝑛 + 1) → (𝑃↑𝑁) ≤ (𝑛 + 1))) |
219 | 215, 218 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) → (𝑃↑𝑁) ≤ (𝑛 + 1))) |
220 | 202, 199 | lenltd 11067 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ ¬ (𝑃 pCnt (𝑛 + 1)) < 𝑁)) |
221 | 131, 129 | lenltd 11067 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑃↑𝑁) ≤ (𝑛 + 1) ↔ ¬ (𝑛 + 1) < (𝑃↑𝑁))) |
222 | 219, 220,
221 | 3imtr3d 292 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (¬ (𝑃 pCnt (𝑛 + 1)) < 𝑁 → ¬ (𝑛 + 1) < (𝑃↑𝑁))) |
223 | 133, 222 | mt4d 117 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (𝑛 + 1)) < 𝑁) |
224 | 223 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) < 𝑁) |
225 | | dvdssubr 15958 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) → ((𝑃↑𝑁) ∥ (♯‘𝑋) ↔ (𝑃↑𝑁) ∥ ((♯‘𝑋) − (𝑃↑𝑁)))) |
226 | 7, 34, 225 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝑃↑𝑁) ∥ (♯‘𝑋) ↔ (𝑃↑𝑁) ∥ ((♯‘𝑋) − (𝑃↑𝑁)))) |
227 | 13, 226 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑃↑𝑁) ∥ ((♯‘𝑋) − (𝑃↑𝑁))) |
228 | 227 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃↑𝑁) ∥ ((♯‘𝑋) − (𝑃↑𝑁))) |
229 | 206 | nn0zd 12369 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ((♯‘𝑋) − (𝑃↑𝑁)) ∈ ℤ) |
230 | 5 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → 𝑁 ∈
ℕ0) |
231 | | pcdvdsb 16514 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℙ ∧
((♯‘𝑋) −
(𝑃↑𝑁)) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ (𝑃 pCnt ((♯‘𝑋) − (𝑃↑𝑁))) ↔ (𝑃↑𝑁) ∥ ((♯‘𝑋) − (𝑃↑𝑁)))) |
232 | 190, 229,
230, 231 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑁 ≤ (𝑃 pCnt ((♯‘𝑋) − (𝑃↑𝑁))) ↔ (𝑃↑𝑁) ∥ ((♯‘𝑋) − (𝑃↑𝑁)))) |
233 | 228, 232 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → 𝑁 ≤ (𝑃 pCnt ((♯‘𝑋) − (𝑃↑𝑁)))) |
234 | 200, 203,
212, 224, 233 | ltletrd 11081 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) < (𝑃 pCnt ((♯‘𝑋) − (𝑃↑𝑁)))) |
235 | 190, 193,
197, 234 | pcadd2 16535 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((♯‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((♯‘𝑋) − (𝑃↑𝑁))))) |
236 | 189, 235 | pm2.61dane 3030 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((♯‘𝑋) − (𝑃↑𝑁))))) |
237 | 183, 236 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) = (𝑃 pCnt (𝑛 + 1))) |
238 | 198 | nn0cnd 12241 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℂ) |
239 | 237, 238 | eqeltrd 2837 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) ∈ ℂ) |
240 | 239, 237 | subeq0bd 11347 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1))) = 0) |
241 | 180, 240 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = 0) |
242 | 241 | oveq2d 7276 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (0 + (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + 0)) |
243 | | 00id 11096 |
. . . . . . . . . . . . 13
⊢ (0 + 0) =
0 |
244 | 242, 243 | eqtr2di 2794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 0 = (0 + (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))))) |
245 | 177, 244 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0 ↔ ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + (𝑃 pCnt (((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))) |
246 | 137, 245 | syl5ibr 245 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)) |
247 | 136, 246 | animpimp2impd 842 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ ((𝜑 → (𝑛 < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0)) → (𝜑 → ((𝑛 + 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)))) |
248 | 93, 99, 105, 111, 124, 247 | nn0ind 12361 |
. . . . . . . 8
⊢ (((𝑃↑𝑁) − 1) ∈ ℕ0
→ (𝜑 → (((𝑃↑𝑁) − 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0))) |
249 | 87, 248 | mpcom 38 |
. . . . . . 7
⊢ (𝜑 → (((𝑃↑𝑁) − 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0)) |
250 | 85, 249 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0) |
251 | 83, 250 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → (𝑃 pCnt (((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1))) = 0) |
252 | | pcdiv 16497 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧
((♯‘𝑋) ∈
ℤ ∧ (♯‘𝑋) ≠ 0) ∧ (𝑃↑𝑁) ∈ ℕ) → (𝑃 pCnt ((♯‘𝑋) / (𝑃↑𝑁))) = ((𝑃 pCnt (♯‘𝑋)) − (𝑃 pCnt (𝑃↑𝑁)))) |
253 | 2, 34, 76, 6, 252 | syl121anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝑃 pCnt ((♯‘𝑋) / (𝑃↑𝑁))) = ((𝑃 pCnt (♯‘𝑋)) − (𝑃 pCnt (𝑃↑𝑁)))) |
254 | 5 | nn0zd 12369 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
255 | | pcid 16518 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝑁)) = 𝑁) |
256 | 2, 254, 255 | syl2anc 583 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt (𝑃↑𝑁)) = 𝑁) |
257 | 256 | oveq2d 7276 |
. . . . . 6
⊢ (𝜑 → ((𝑃 pCnt (♯‘𝑋)) − (𝑃 pCnt (𝑃↑𝑁))) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) |
258 | 253, 257 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (𝑃 pCnt ((♯‘𝑋) / (𝑃↑𝑁))) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) |
259 | 251, 258 | oveq12d 7278 |
. . . 4
⊢ (𝜑 → ((𝑃 pCnt (((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1))) + (𝑃 pCnt ((♯‘𝑋) / (𝑃↑𝑁)))) = (0 + ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) |
260 | 2, 27 | pccld 16495 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑋)) ∈
ℕ0) |
261 | 260 | nn0zd 12369 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑋)) ∈ ℤ) |
262 | 261, 254 | zsubcld 12376 |
. . . . . 6
⊢ (𝜑 → ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ∈ ℤ) |
263 | 262 | zcnd 12372 |
. . . . 5
⊢ (𝜑 → ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ∈ ℂ) |
264 | 263 | addid2d 11122 |
. . . 4
⊢ (𝜑 → (0 + ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) |
265 | 79, 259, 264 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (𝑃 pCnt ((((♯‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((♯‘𝑋) / (𝑃↑𝑁)))) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) |
266 | 66, 67, 265 | 3eqtr3d 2785 |
. 2
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑆)) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) |
267 | 40, 266 | jca 511 |
1
⊢ (𝜑 → ((♯‘𝑆) ∈ ℕ ∧ (𝑃 pCnt (♯‘𝑆)) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) |