Step | Hyp | Ref
| Expression |
1 | | sylow1.f |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | sylow1.p |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℙ) |
3 | | prmnn 15388 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
5 | | sylow1.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
6 | 4, 5 | nnexpcld 13030 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℕ) |
7 | 6 | nnzd 11481 |
. . . . 5
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℤ) |
8 | | hashbc 13237 |
. . . . 5
⊢ ((𝑋 ∈ Fin ∧ (𝑃↑𝑁) ∈ ℤ) → ((#‘𝑋)C(𝑃↑𝑁)) = (#‘{𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)})) |
9 | 1, 7, 8 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((#‘𝑋)C(𝑃↑𝑁)) = (#‘{𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)})) |
10 | | sylow1lem.s |
. . . . 5
⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} |
11 | 10 | fveq2i 6194 |
. . . 4
⊢
(#‘𝑆) =
(#‘{𝑠 ∈
𝒫 𝑋 ∣
(#‘𝑠) = (𝑃↑𝑁)}) |
12 | 9, 11 | syl6eqr 2674 |
. . 3
⊢ (𝜑 → ((#‘𝑋)C(𝑃↑𝑁)) = (#‘𝑆)) |
13 | | sylow1.d |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑁) ∥ (#‘𝑋)) |
14 | | sylow1.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ Grp) |
15 | | sylow1.x |
. . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝐺) |
16 | 15 | grpbn0 17451 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≠ ∅) |
18 | | hasheq0 13154 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Fin →
((#‘𝑋) = 0 ↔
𝑋 =
∅)) |
19 | 1, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝑋) = 0 ↔ 𝑋 = ∅)) |
20 | 19 | necon3bbid 2831 |
. . . . . . . . 9
⊢ (𝜑 → (¬ (#‘𝑋) = 0 ↔ 𝑋 ≠ ∅)) |
21 | 17, 20 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → ¬ (#‘𝑋) = 0) |
22 | | hashcl 13147 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Fin →
(#‘𝑋) ∈
ℕ0) |
23 | 1, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝑋) ∈
ℕ0) |
24 | | elnn0 11294 |
. . . . . . . . . 10
⊢
((#‘𝑋) ∈
ℕ0 ↔ ((#‘𝑋) ∈ ℕ ∨ (#‘𝑋) = 0)) |
25 | 23, 24 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝑋) ∈ ℕ ∨
(#‘𝑋) =
0)) |
26 | 25 | ord 392 |
. . . . . . . 8
⊢ (𝜑 → (¬ (#‘𝑋) ∈ ℕ →
(#‘𝑋) =
0)) |
27 | 21, 26 | mt3d 140 |
. . . . . . 7
⊢ (𝜑 → (#‘𝑋) ∈ ℕ) |
28 | | dvdsle 15032 |
. . . . . . 7
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (#‘𝑋) ∈ ℕ) → ((𝑃↑𝑁) ∥ (#‘𝑋) → (𝑃↑𝑁) ≤ (#‘𝑋))) |
29 | 7, 27, 28 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((𝑃↑𝑁) ∥ (#‘𝑋) → (𝑃↑𝑁) ≤ (#‘𝑋))) |
30 | 13, 29 | mpd 15 |
. . . . 5
⊢ (𝜑 → (𝑃↑𝑁) ≤ (#‘𝑋)) |
31 | 6 | nnnn0d 11351 |
. . . . . . 7
⊢ (𝜑 → (𝑃↑𝑁) ∈
ℕ0) |
32 | | nn0uz 11722 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
33 | 31, 32 | syl6eleq 2711 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑁) ∈
(ℤ≥‘0)) |
34 | 23 | nn0zd 11480 |
. . . . . 6
⊢ (𝜑 → (#‘𝑋) ∈ ℤ) |
35 | | elfz5 12334 |
. . . . . 6
⊢ (((𝑃↑𝑁) ∈ (ℤ≥‘0)
∧ (#‘𝑋) ∈
ℤ) → ((𝑃↑𝑁) ∈ (0...(#‘𝑋)) ↔ (𝑃↑𝑁) ≤ (#‘𝑋))) |
36 | 33, 34, 35 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((𝑃↑𝑁) ∈ (0...(#‘𝑋)) ↔ (𝑃↑𝑁) ≤ (#‘𝑋))) |
37 | 30, 36 | mpbird 247 |
. . . 4
⊢ (𝜑 → (𝑃↑𝑁) ∈ (0...(#‘𝑋))) |
38 | | bccl2 13110 |
. . . 4
⊢ ((𝑃↑𝑁) ∈ (0...(#‘𝑋)) → ((#‘𝑋)C(𝑃↑𝑁)) ∈ ℕ) |
39 | 37, 38 | syl 17 |
. . 3
⊢ (𝜑 → ((#‘𝑋)C(𝑃↑𝑁)) ∈ ℕ) |
40 | 12, 39 | eqeltrrd 2702 |
. 2
⊢ (𝜑 → (#‘𝑆) ∈ ℕ) |
41 | | nnuz 11723 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
42 | 6, 41 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃↑𝑁) ∈
(ℤ≥‘1)) |
43 | | elfz5 12334 |
. . . . . . . . . 10
⊢ (((𝑃↑𝑁) ∈ (ℤ≥‘1)
∧ (#‘𝑋) ∈
ℤ) → ((𝑃↑𝑁) ∈ (1...(#‘𝑋)) ↔ (𝑃↑𝑁) ≤ (#‘𝑋))) |
44 | 42, 34, 43 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃↑𝑁) ∈ (1...(#‘𝑋)) ↔ (𝑃↑𝑁) ≤ (#‘𝑋))) |
45 | 30, 44 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑁) ∈ (1...(#‘𝑋))) |
46 | | 1zzd 11408 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
47 | | fzsubel 12377 |
. . . . . . . . 9
⊢ (((1
∈ ℤ ∧ (#‘𝑋) ∈ ℤ) ∧ ((𝑃↑𝑁) ∈ ℤ ∧ 1 ∈ ℤ))
→ ((𝑃↑𝑁) ∈ (1...(#‘𝑋)) ↔ ((𝑃↑𝑁) − 1) ∈ ((1 −
1)...((#‘𝑋) −
1)))) |
48 | 46, 34, 7, 46, 47 | syl22anc 1327 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃↑𝑁) ∈ (1...(#‘𝑋)) ↔ ((𝑃↑𝑁) − 1) ∈ ((1 −
1)...((#‘𝑋) −
1)))) |
49 | 45, 48 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → ((𝑃↑𝑁) − 1) ∈ ((1 −
1)...((#‘𝑋) −
1))) |
50 | | 1m1e0 11089 |
. . . . . . . 8
⊢ (1
− 1) = 0 |
51 | 50 | oveq1i 6660 |
. . . . . . 7
⊢ ((1
− 1)...((#‘𝑋)
− 1)) = (0...((#‘𝑋) − 1)) |
52 | 49, 51 | syl6eleq 2711 |
. . . . . 6
⊢ (𝜑 → ((𝑃↑𝑁) − 1) ∈ (0...((#‘𝑋) − 1))) |
53 | | bcp1nk 13104 |
. . . . . 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 11353 |
. . . . . . 7
⊢ (𝜑 → (#‘𝑋) ∈ ℂ) |
56 | | ax-1cn 9994 |
. . . . . . 7
⊢ 1 ∈
ℂ |
57 | | npcan 10290 |
. . . . . . 7
⊢
(((#‘𝑋) ∈
ℂ ∧ 1 ∈ ℂ) → (((#‘𝑋) − 1) + 1) = (#‘𝑋)) |
58 | 55, 56, 57 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → (((#‘𝑋) − 1) + 1) =
(#‘𝑋)) |
59 | 6 | nncnd 11036 |
. . . . . . 7
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℂ) |
60 | | npcan 10290 |
. . . . . . 7
⊢ (((𝑃↑𝑁) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝑃↑𝑁) − 1) + 1) = (𝑃↑𝑁)) |
61 | 59, 56, 60 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → (((𝑃↑𝑁) − 1) + 1) = (𝑃↑𝑁)) |
62 | 58, 61 | oveq12d 6668 |
. . . . 5
⊢ (𝜑 → ((((#‘𝑋) − 1) + 1)C(((𝑃↑𝑁) − 1) + 1)) = ((#‘𝑋)C(𝑃↑𝑁))) |
63 | 58, 61 | oveq12d 6668 |
. . . . . 6
⊢ (𝜑 → ((((#‘𝑋) − 1) + 1) / (((𝑃↑𝑁) − 1) + 1)) = ((#‘𝑋) / (𝑃↑𝑁))) |
64 | 63 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → ((((#‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((((#‘𝑋) − 1) + 1) / (((𝑃↑𝑁) − 1) + 1))) = ((((#‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((#‘𝑋) / (𝑃↑𝑁)))) |
65 | 54, 62, 64 | 3eqtr3d 2664 |
. . . 4
⊢ (𝜑 → ((#‘𝑋)C(𝑃↑𝑁)) = ((((#‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((#‘𝑋) / (𝑃↑𝑁)))) |
66 | 65 | oveq2d 6666 |
. . 3
⊢ (𝜑 → (𝑃 pCnt ((#‘𝑋)C(𝑃↑𝑁))) = (𝑃 pCnt ((((#‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((#‘𝑋) / (𝑃↑𝑁))))) |
67 | 12 | oveq2d 6666 |
. . 3
⊢ (𝜑 → (𝑃 pCnt ((#‘𝑋)C(𝑃↑𝑁))) = (𝑃 pCnt (#‘𝑆))) |
68 | | bccl2 13110 |
. . . . . . 7
⊢ (((𝑃↑𝑁) − 1) ∈ (0...((#‘𝑋) − 1)) →
(((#‘𝑋) −
1)C((𝑃↑𝑁) − 1)) ∈
ℕ) |
69 | 52, 68 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((#‘𝑋) − 1)C((𝑃↑𝑁) − 1)) ∈
ℕ) |
70 | 69 | nnzd 11481 |
. . . . 5
⊢ (𝜑 → (((#‘𝑋) − 1)C((𝑃↑𝑁) − 1)) ∈
ℤ) |
71 | 69 | nnne0d 11065 |
. . . . 5
⊢ (𝜑 → (((#‘𝑋) − 1)C((𝑃↑𝑁) − 1)) ≠ 0) |
72 | 6 | nnne0d 11065 |
. . . . . . 7
⊢ (𝜑 → (𝑃↑𝑁) ≠ 0) |
73 | | dvdsval2 14986 |
. . . . . . 7
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (𝑃↑𝑁) ≠ 0 ∧ (#‘𝑋) ∈ ℤ) → ((𝑃↑𝑁) ∥ (#‘𝑋) ↔ ((#‘𝑋) / (𝑃↑𝑁)) ∈ ℤ)) |
74 | 7, 72, 34, 73 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → ((𝑃↑𝑁) ∥ (#‘𝑋) ↔ ((#‘𝑋) / (𝑃↑𝑁)) ∈ ℤ)) |
75 | 13, 74 | mpbid 222 |
. . . . 5
⊢ (𝜑 → ((#‘𝑋) / (𝑃↑𝑁)) ∈ ℤ) |
76 | 27 | nnne0d 11065 |
. . . . . 6
⊢ (𝜑 → (#‘𝑋) ≠ 0) |
77 | 55, 59, 76, 72 | divne0d 10817 |
. . . . 5
⊢ (𝜑 → ((#‘𝑋) / (𝑃↑𝑁)) ≠ 0) |
78 | | pcmul 15556 |
. . . . 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 1335 |
. . . 4
⊢ (𝜑 → (𝑃 pCnt ((((#‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((#‘𝑋) / (𝑃↑𝑁)))) = ((𝑃 pCnt (((#‘𝑋) − 1)C((𝑃↑𝑁) − 1))) + (𝑃 pCnt ((#‘𝑋) / (𝑃↑𝑁))))) |
80 | | 1cnd 10056 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
81 | 55, 59, 80 | npncand 10416 |
. . . . . . . 8
⊢ (𝜑 → (((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1)) = ((#‘𝑋) − 1)) |
82 | 81 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → ((((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1)) = (((#‘𝑋) − 1)C((𝑃↑𝑁) − 1))) |
83 | 82 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = (𝑃 pCnt (((#‘𝑋) − 1)C((𝑃↑𝑁) − 1)))) |
84 | 6 | nnred 11035 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℝ) |
85 | 84 | ltm1d 10956 |
. . . . . . 7
⊢ (𝜑 → ((𝑃↑𝑁) − 1) < (𝑃↑𝑁)) |
86 | | nnm1nn0 11334 |
. . . . . . . . 9
⊢ ((𝑃↑𝑁) ∈ ℕ → ((𝑃↑𝑁) − 1) ∈
ℕ0) |
87 | 6, 86 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃↑𝑁) − 1) ∈
ℕ0) |
88 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝑥 < (𝑃↑𝑁) ↔ 0 < (𝑃↑𝑁))) |
89 | | bcxmaslem1 14566 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥) = ((((#‘𝑋) − (𝑃↑𝑁)) + 0)C0)) |
90 | 89 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 0)C0))) |
91 | 90 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = 0)) |
92 | 88, 91 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → ((𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0) ↔ (0 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = 0))) |
93 | 92 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑥 = 0 → ((𝜑 → (𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (0 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = 0)))) |
94 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → (𝑥 < (𝑃↑𝑁) ↔ 𝑛 < (𝑃↑𝑁))) |
95 | | bcxmaslem1 14566 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑛 → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥) = ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) |
96 | 95 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑛 → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛))) |
97 | 96 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0)) |
98 | 94, 97 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → ((𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0) ↔ (𝑛 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0))) |
99 | 98 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (𝑛 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0)))) |
100 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑛 + 1) → (𝑥 < (𝑃↑𝑁) ↔ (𝑛 + 1) < (𝑃↑𝑁))) |
101 | | bcxmaslem1 14566 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑛 + 1) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥) = ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) |
102 | 101 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑛 + 1) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1)))) |
103 | 102 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑛 + 1) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)) |
104 | 100, 103 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0) ↔ ((𝑛 + 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))) |
105 | 104 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → ((𝑛 + 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)))) |
106 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑃↑𝑁) − 1) → (𝑥 < (𝑃↑𝑁) ↔ ((𝑃↑𝑁) − 1) < (𝑃↑𝑁))) |
107 | | bcxmaslem1 14566 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝑃↑𝑁) − 1) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥) = ((((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) |
108 | 107 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑃↑𝑁) − 1) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1)))) |
109 | 108 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑃↑𝑁) − 1) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0 ↔ (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0)) |
110 | 106, 109 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑃↑𝑁) − 1) → ((𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0) ↔ (((𝑃↑𝑁) − 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0))) |
111 | 110 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑃↑𝑁) − 1) → ((𝜑 → (𝑥 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑥)C𝑥)) = 0)) ↔ (𝜑 → (((𝑃↑𝑁) − 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0)))) |
112 | | znn0sub 11424 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (#‘𝑋) ∈ ℤ) → ((𝑃↑𝑁) ≤ (#‘𝑋) ↔ ((#‘𝑋) − (𝑃↑𝑁)) ∈
ℕ0)) |
113 | 7, 34, 112 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑃↑𝑁) ≤ (#‘𝑋) ↔ ((#‘𝑋) − (𝑃↑𝑁)) ∈
ℕ0)) |
114 | 30, 113 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((#‘𝑋) − (𝑃↑𝑁)) ∈
ℕ0) |
115 | | 0nn0 11307 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
116 | | nn0addcl 11328 |
. . . . . . . . . . . . . 14
⊢
((((#‘𝑋)
− (𝑃↑𝑁)) ∈ ℕ0
∧ 0 ∈ ℕ0) → (((#‘𝑋) − (𝑃↑𝑁)) + 0) ∈
ℕ0) |
117 | 114, 115,
116 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((#‘𝑋) − (𝑃↑𝑁)) + 0) ∈
ℕ0) |
118 | | bcn0 13097 |
. . . . . . . . . . . . 13
⊢
((((#‘𝑋)
− (𝑃↑𝑁)) + 0) ∈
ℕ0 → ((((#‘𝑋) − (𝑃↑𝑁)) + 0)C0) = 1) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((#‘𝑋) − (𝑃↑𝑁)) + 0)C0) = 1) |
120 | 119 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = (𝑃 pCnt 1)) |
121 | | pc1 15560 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) |
122 | 2, 121 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 pCnt 1) = 0) |
123 | 120, 122 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = 0) |
124 | 123 | a1d 25 |
. . . . . . . . 9
⊢ (𝜑 → (0 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 0)C0)) = 0)) |
125 | | nn0re 11301 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℝ) |
126 | 125 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ∈ ℝ) |
127 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) |
128 | 127 | ad2antrl 764 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) ∈ ℕ) |
129 | 128 | nnred 11035 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) ∈ ℝ) |
130 | 6 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃↑𝑁) ∈ ℕ) |
131 | 130 | nnred 11035 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃↑𝑁) ∈ ℝ) |
132 | 126 | ltp1d 10954 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 < (𝑛 + 1)) |
133 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) < (𝑃↑𝑁)) |
134 | 126, 129,
131, 132, 133 | lttrd 10198 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 < (𝑃↑𝑁)) |
135 | 134 | expr 643 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 + 1) < (𝑃↑𝑁) → 𝑛 < (𝑃↑𝑁))) |
136 | 135 | imim1d 82 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0) → ((𝑛 + 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0))) |
137 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0 → ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))))) |
138 | 114 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((#‘𝑋) − (𝑃↑𝑁)) ∈
ℕ0) |
139 | 138 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((#‘𝑋) − (𝑃↑𝑁)) ∈ ℂ) |
140 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) |
141 | 140 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ∈ ℂ) |
142 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 1 ∈
ℂ) |
143 | 139, 141,
142 | addassd 10062 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) = (((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))) |
144 | 143 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) |
145 | | nn0addge2 11340 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ ℝ ∧
((#‘𝑋) − (𝑃↑𝑁)) ∈ ℕ0) → 𝑛 ≤ (((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)) |
146 | 126, 138,
145 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ≤ (((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)) |
147 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ∈ ℕ0) |
148 | 147, 32 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ∈
(ℤ≥‘0)) |
149 | 138, 147 | nn0addcld 11355 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) ∈
ℕ0) |
150 | 149 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) ∈ ℤ) |
151 | | elfz5 12334 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈
(ℤ≥‘0) ∧ (((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) ∈ ℤ) → (𝑛 ∈ (0...(((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)) ↔ 𝑛 ≤ (((#‘𝑋) − (𝑃↑𝑁)) + 𝑛))) |
152 | 148, 150,
151 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 ∈ (0...(((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)) ↔ 𝑛 ≤ (((#‘𝑋) − (𝑃↑𝑁)) + 𝑛))) |
153 | 146, 152 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑛 ∈ (0...(((#‘𝑋) − (𝑃↑𝑁)) + 𝑛))) |
154 | | bcp1nk 13104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (0...(((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)) → (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)C(𝑛 + 1)) = (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) |
156 | 144, 155 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1)) = (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) |
157 | 156 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))))) |
158 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑃 ∈ ℙ) |
159 | | bccl2 13110 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (0...(((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) ∈ ℕ) |
160 | 153, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) ∈ ℕ) |
161 | | nnq 11801 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((#‘𝑋)
− (𝑃↑𝑁)) + 𝑛)C𝑛) ∈ ℕ → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) ∈ ℚ) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) ∈ ℚ) |
163 | 160 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) ≠ 0) |
164 | 150 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℤ) |
165 | | znq 11792 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((#‘𝑋)
− (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) →
(((((#‘𝑋) −
(𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℚ) |
166 | 164, 128,
165 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈ ℚ) |
167 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((#‘𝑋)
− (𝑃↑𝑁)) + 𝑛) ∈ ℕ0 →
((((#‘𝑋) −
(𝑃↑𝑁)) + 𝑛) + 1) ∈ ℕ) |
168 | 149, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℕ) |
169 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((#‘𝑋)
− (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℕ →
((((#‘𝑋) −
(𝑃↑𝑁)) + 𝑛) + 1) ∈
ℝ+) |
170 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ∈
ℝ+) |
171 | | rpdivcl 11856 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((#‘𝑋)
− (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℝ+ ∧
(𝑛 + 1) ∈
ℝ+) → (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈
ℝ+) |
172 | 169, 170,
171 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((#‘𝑋)
− (𝑃↑𝑁)) + 𝑛) + 1) ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) →
(((((#‘𝑋) −
(𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈
ℝ+) |
173 | 168, 128,
172 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ∈
ℝ+) |
174 | 173 | rpne0d 11877 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)) ≠ 0) |
175 | | pcqmul 15558 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧
(((((#‘𝑋) −
(𝑃↑𝑁)) + 𝑛)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 1335 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛) · (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))))) |
177 | 157, 176 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))))) |
178 | 168 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) ≠ 0) |
179 | | pcdiv 15557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℙ ∧
(((((#‘𝑋) −
(𝑃↑𝑁)) + 𝑛) + 1) ∈ ℤ ∧ ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) ≠ 0) ∧ (𝑛 + 1) ∈ ℕ) → (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1)))) |
180 | 158, 164,
178, 128, 179 | syl121anc 1331 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1)))) |
181 | 128 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) ∈ ℂ) |
182 | 139, 181 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1)) = ((𝑛 + 1) + ((#‘𝑋) − (𝑃↑𝑁)))) |
183 | 143, 182 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) = ((𝑛 + 1) + ((#‘𝑋) − (𝑃↑𝑁)))) |
184 | 183 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((#‘𝑋) − (𝑃↑𝑁))))) |
185 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) = 0) → ((#‘𝑋) − (𝑃↑𝑁)) = 0) |
186 | 185 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) = 0) → ((𝑛 + 1) + ((#‘𝑋) − (𝑃↑𝑁))) = ((𝑛 + 1) + 0)) |
187 | 181 | addid1d 10236 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑛 + 1) + 0) = (𝑛 + 1)) |
188 | 187 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) = 0) → ((𝑛 + 1) + 0) = (𝑛 + 1)) |
189 | 186, 188 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) = 0) → (𝑛 + 1) = ((𝑛 + 1) + ((#‘𝑋) − (𝑃↑𝑁)))) |
190 | 189 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) = 0) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((#‘𝑋) − (𝑃↑𝑁))))) |
191 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → 𝑃 ∈ ℙ) |
192 | | nnq 11801 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ∈
ℚ) |
193 | 128, 192 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) ∈ ℚ) |
194 | 193 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑛 + 1) ∈ ℚ) |
195 | 138 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((#‘𝑋) − (𝑃↑𝑁)) ∈ ℤ) |
196 | | zq 11794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝑋)
− (𝑃↑𝑁)) ∈ ℤ →
((#‘𝑋) − (𝑃↑𝑁)) ∈ ℚ) |
197 | 195, 196 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((#‘𝑋) − (𝑃↑𝑁)) ∈ ℚ) |
198 | 197 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ((#‘𝑋) − (𝑃↑𝑁)) ∈ ℚ) |
199 | 158, 128 | pccld 15555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈
ℕ0) |
200 | 199 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ) |
201 | 200 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ) |
202 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑁 ∈
ℕ0) |
203 | 202 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 𝑁 ∈ ℝ) |
204 | 203 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → 𝑁 ∈ ℝ) |
205 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) |
206 | 205 | neneqd 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ¬ ((#‘𝑋) − (𝑃↑𝑁)) = 0) |
207 | 114 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ((#‘𝑋) − (𝑃↑𝑁)) ∈
ℕ0) |
208 | | elnn0 11294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#‘𝑋)
− (𝑃↑𝑁)) ∈ ℕ0
↔ (((#‘𝑋)
− (𝑃↑𝑁)) ∈ ℕ ∨
((#‘𝑋) − (𝑃↑𝑁)) = 0)) |
209 | 207, 208 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (((#‘𝑋) − (𝑃↑𝑁)) ∈ ℕ ∨ ((#‘𝑋) − (𝑃↑𝑁)) = 0)) |
210 | 209 | ord 392 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (¬ ((#‘𝑋) − (𝑃↑𝑁)) ∈ ℕ → ((#‘𝑋) − (𝑃↑𝑁)) = 0)) |
211 | 206, 210 | mt3d 140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ((#‘𝑋) − (𝑃↑𝑁)) ∈ ℕ) |
212 | 191, 211 | pccld 15555 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt ((#‘𝑋) − (𝑃↑𝑁))) ∈
ℕ0) |
213 | 212 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt ((#‘𝑋) − (𝑃↑𝑁))) ∈ ℝ) |
214 | 128 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑛 + 1) ∈ ℤ) |
215 | | pcdvdsb 15573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑃 ∈ ℙ ∧ (𝑛 + 1) ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑𝑁) ∥ (𝑛 + 1))) |
216 | 158, 214,
202, 215 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑𝑁) ∥ (𝑛 + 1))) |
217 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃↑𝑁) ∈ ℤ) |
218 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) → ((𝑃↑𝑁) ∥ (𝑛 + 1) → (𝑃↑𝑁) ≤ (𝑛 + 1))) |
219 | 217, 128,
218 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑃↑𝑁) ∥ (𝑛 + 1) → (𝑃↑𝑁) ≤ (𝑛 + 1))) |
220 | 216, 219 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) → (𝑃↑𝑁) ≤ (𝑛 + 1))) |
221 | 203, 200 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑁 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ ¬ (𝑃 pCnt (𝑛 + 1)) < 𝑁)) |
222 | 131, 129 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑃↑𝑁) ≤ (𝑛 + 1) ↔ ¬ (𝑛 + 1) < (𝑃↑𝑁))) |
223 | 220, 221,
222 | 3imtr3d 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (¬ (𝑃 pCnt (𝑛 + 1)) < 𝑁 → ¬ (𝑛 + 1) < (𝑃↑𝑁))) |
224 | 133, 223 | mt4d 152 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (𝑛 + 1)) < 𝑁) |
225 | 224 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) < 𝑁) |
226 | | dvdssubr 15027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (#‘𝑋) ∈ ℤ) → ((𝑃↑𝑁) ∥ (#‘𝑋) ↔ (𝑃↑𝑁) ∥ ((#‘𝑋) − (𝑃↑𝑁)))) |
227 | 7, 34, 226 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ((𝑃↑𝑁) ∥ (#‘𝑋) ↔ (𝑃↑𝑁) ∥ ((#‘𝑋) − (𝑃↑𝑁)))) |
228 | 13, 227 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑃↑𝑁) ∥ ((#‘𝑋) − (𝑃↑𝑁))) |
229 | 228 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃↑𝑁) ∥ ((#‘𝑋) − (𝑃↑𝑁))) |
230 | 207 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → ((#‘𝑋) − (𝑃↑𝑁)) ∈ ℤ) |
231 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → 𝑁 ∈
ℕ0) |
232 | | pcdvdsb 15573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℙ ∧
((#‘𝑋) − (𝑃↑𝑁)) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ (𝑃 pCnt ((#‘𝑋) − (𝑃↑𝑁))) ↔ (𝑃↑𝑁) ∥ ((#‘𝑋) − (𝑃↑𝑁)))) |
233 | 191, 230,
231, 232 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑁 ≤ (𝑃 pCnt ((#‘𝑋) − (𝑃↑𝑁))) ↔ (𝑃↑𝑁) ∥ ((#‘𝑋) − (𝑃↑𝑁)))) |
234 | 229, 233 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → 𝑁 ≤ (𝑃 pCnt ((#‘𝑋) − (𝑃↑𝑁)))) |
235 | 201, 204,
213, 225, 234 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) < (𝑃 pCnt ((#‘𝑋) − (𝑃↑𝑁)))) |
236 | 191, 194,
198, 235 | pcadd2 15594 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) ∧ ((#‘𝑋) − (𝑃↑𝑁)) ≠ 0) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((#‘𝑋) − (𝑃↑𝑁))))) |
237 | 190, 236 | pm2.61dane 2881 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (𝑛 + 1)) = (𝑃 pCnt ((𝑛 + 1) + ((#‘𝑋) − (𝑃↑𝑁))))) |
238 | 184, 237 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) = (𝑃 pCnt (𝑛 + 1))) |
239 | 199 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℂ) |
240 | 238, 239 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) ∈ ℂ) |
241 | 240, 238 | subeq0bd 10456 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1)) − (𝑃 pCnt (𝑛 + 1))) = 0) |
242 | 180, 241 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))) = 0) |
243 | 242 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → (0 + (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + 0)) |
244 | | 00id 10211 |
. . . . . . . . . . . . . . . . 17
⊢ (0 + 0) =
0 |
245 | 243, 244 | syl6req 2673 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → 0 = (0 + (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1))))) |
246 | 177, 245 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0 ↔ ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) + (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))) = (0 + (𝑃 pCnt (((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛) + 1) / (𝑛 + 1)))))) |
247 | 137, 246 | syl5ibr 236 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) < (𝑃↑𝑁))) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0 → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)) |
248 | 247 | expr 643 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 + 1) < (𝑃↑𝑁) → ((𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0 → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))) |
249 | 248 | a2d 29 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 + 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0) → ((𝑛 + 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))) |
250 | 136, 249 | syld 47 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0) → ((𝑛 + 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0))) |
251 | 250 | expcom 451 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (𝜑 → ((𝑛 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0) → ((𝑛 + 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)))) |
252 | 251 | a2d 29 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ ((𝜑 → (𝑛 < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + 𝑛)C𝑛)) = 0)) → (𝜑 → ((𝑛 + 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + (𝑛 + 1))C(𝑛 + 1))) = 0)))) |
253 | 93, 99, 105, 111, 124, 252 | nn0ind 11472 |
. . . . . . . 8
⊢ (((𝑃↑𝑁) − 1) ∈ ℕ0
→ (𝜑 → (((𝑃↑𝑁) − 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0))) |
254 | 87, 253 | mpcom 38 |
. . . . . . 7
⊢ (𝜑 → (((𝑃↑𝑁) − 1) < (𝑃↑𝑁) → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0)) |
255 | 85, 254 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (𝑃 pCnt ((((#‘𝑋) − (𝑃↑𝑁)) + ((𝑃↑𝑁) − 1))C((𝑃↑𝑁) − 1))) = 0) |
256 | 83, 255 | eqtr3d 2658 |
. . . . 5
⊢ (𝜑 → (𝑃 pCnt (((#‘𝑋) − 1)C((𝑃↑𝑁) − 1))) = 0) |
257 | | pcdiv 15557 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧
((#‘𝑋) ∈ ℤ
∧ (#‘𝑋) ≠ 0)
∧ (𝑃↑𝑁) ∈ ℕ) → (𝑃 pCnt ((#‘𝑋) / (𝑃↑𝑁))) = ((𝑃 pCnt (#‘𝑋)) − (𝑃 pCnt (𝑃↑𝑁)))) |
258 | 2, 34, 76, 6, 257 | syl121anc 1331 |
. . . . . 6
⊢ (𝜑 → (𝑃 pCnt ((#‘𝑋) / (𝑃↑𝑁))) = ((𝑃 pCnt (#‘𝑋)) − (𝑃 pCnt (𝑃↑𝑁)))) |
259 | 5 | nn0zd 11480 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
260 | | pcid 15577 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝑁)) = 𝑁) |
261 | 2, 259, 260 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt (𝑃↑𝑁)) = 𝑁) |
262 | 261 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → ((𝑃 pCnt (#‘𝑋)) − (𝑃 pCnt (𝑃↑𝑁))) = ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
263 | 258, 262 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (𝑃 pCnt ((#‘𝑋) / (𝑃↑𝑁))) = ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
264 | 256, 263 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → ((𝑃 pCnt (((#‘𝑋) − 1)C((𝑃↑𝑁) − 1))) + (𝑃 pCnt ((#‘𝑋) / (𝑃↑𝑁)))) = (0 + ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
265 | 2, 27 | pccld 15555 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈
ℕ0) |
266 | 265 | nn0zd 11480 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈ ℤ) |
267 | 266, 259 | zsubcld 11487 |
. . . . . 6
⊢ (𝜑 → ((𝑃 pCnt (#‘𝑋)) − 𝑁) ∈ ℤ) |
268 | 267 | zcnd 11483 |
. . . . 5
⊢ (𝜑 → ((𝑃 pCnt (#‘𝑋)) − 𝑁) ∈ ℂ) |
269 | 268 | addid2d 10237 |
. . . 4
⊢ (𝜑 → (0 + ((𝑃 pCnt (#‘𝑋)) − 𝑁)) = ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
270 | 79, 264, 269 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → (𝑃 pCnt ((((#‘𝑋) − 1)C((𝑃↑𝑁) − 1)) · ((#‘𝑋) / (𝑃↑𝑁)))) = ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
271 | 66, 67, 270 | 3eqtr3d 2664 |
. 2
⊢ (𝜑 → (𝑃 pCnt (#‘𝑆)) = ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
272 | 40, 271 | jca 554 |
1
⊢ (𝜑 → ((#‘𝑆) ∈ ℕ ∧ (𝑃 pCnt (#‘𝑆)) = ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |