Step | Hyp | Ref
| Expression |
1 | | sylow1.f |
. . . . 5
โข (๐ โ ๐ โ Fin) |
2 | | sylow1.p |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
3 | | prmnn 16551 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
5 | | sylow1.n |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
6 | 4, 5 | nnexpcld 14149 |
. . . . . 6
โข (๐ โ (๐โ๐) โ โ) |
7 | 6 | nnzd 12527 |
. . . . 5
โข (๐ โ (๐โ๐) โ โค) |
8 | | hashbc 14351 |
. . . . 5
โข ((๐ โ Fin โง (๐โ๐) โ โค) โ
((โฏโ๐)C(๐โ๐)) = (โฏโ{๐ โ ๐ซ ๐ โฃ (โฏโ๐ ) = (๐โ๐)})) |
9 | 1, 7, 8 | syl2anc 585 |
. . . 4
โข (๐ โ ((โฏโ๐)C(๐โ๐)) = (โฏโ{๐ โ ๐ซ ๐ โฃ (โฏโ๐ ) = (๐โ๐)})) |
10 | | sylow1lem.s |
. . . . 5
โข ๐ = {๐ โ ๐ซ ๐ โฃ (โฏโ๐ ) = (๐โ๐)} |
11 | 10 | fveq2i 6846 |
. . . 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 18780 |
. . . . . . . . . 10
โข (๐บ โ Grp โ ๐ โ โ
) |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ
) |
18 | | hasheq0 14264 |
. . . . . . . . . . 11
โข (๐ โ Fin โ
((โฏโ๐) = 0
โ ๐ =
โ
)) |
19 | 1, 18 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ((โฏโ๐) = 0 โ ๐ = โ
)) |
20 | 19 | necon3bbid 2982 |
. . . . . . . . 9
โข (๐ โ (ยฌ
(โฏโ๐) = 0
โ ๐ โ
โ
)) |
21 | 17, 20 | mpbird 257 |
. . . . . . . 8
โข (๐ โ ยฌ (โฏโ๐) = 0) |
22 | | hashcl 14257 |
. . . . . . . . . . 11
โข (๐ โ Fin โ
(โฏโ๐) โ
โ0) |
23 | 1, 22 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (โฏโ๐) โ
โ0) |
24 | | elnn0 12416 |
. . . . . . . . . 10
โข
((โฏโ๐)
โ โ0 โ ((โฏโ๐) โ โ โจ (โฏโ๐) = 0)) |
25 | 23, 24 | sylib 217 |
. . . . . . . . 9
โข (๐ โ ((โฏโ๐) โ โ โจ
(โฏโ๐) =
0)) |
26 | 25 | ord 863 |
. . . . . . . 8
โข (๐ โ (ยฌ
(โฏโ๐) โ
โ โ (โฏโ๐) = 0)) |
27 | 21, 26 | mt3d 148 |
. . . . . . 7
โข (๐ โ (โฏโ๐) โ
โ) |
28 | | dvdsle 16193 |
. . . . . . 7
โข (((๐โ๐) โ โค โง (โฏโ๐) โ โ) โ ((๐โ๐) โฅ (โฏโ๐) โ (๐โ๐) โค (โฏโ๐))) |
29 | 7, 27, 28 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((๐โ๐) โฅ (โฏโ๐) โ (๐โ๐) โค (โฏโ๐))) |
30 | 13, 29 | mpd 15 |
. . . . 5
โข (๐ โ (๐โ๐) โค (โฏโ๐)) |
31 | 6 | nnnn0d 12474 |
. . . . . . 7
โข (๐ โ (๐โ๐) โ
โ0) |
32 | | nn0uz 12806 |
. . . . . . 7
โข
โ0 = (โคโฅโ0) |
33 | 31, 32 | eleqtrdi 2848 |
. . . . . 6
โข (๐ โ (๐โ๐) โ
(โคโฅโ0)) |
34 | 23 | nn0zd 12526 |
. . . . . 6
โข (๐ โ (โฏโ๐) โ
โค) |
35 | | elfz5 13434 |
. . . . . 6
โข (((๐โ๐) โ (โคโฅโ0)
โง (โฏโ๐)
โ โค) โ ((๐โ๐) โ (0...(โฏโ๐)) โ (๐โ๐) โค (โฏโ๐))) |
36 | 33, 34, 35 | syl2anc 585 |
. . . . 5
โข (๐ โ ((๐โ๐) โ (0...(โฏโ๐)) โ (๐โ๐) โค (โฏโ๐))) |
37 | 30, 36 | mpbird 257 |
. . . 4
โข (๐ โ (๐โ๐) โ (0...(โฏโ๐))) |
38 | | bccl2 14224 |
. . . 4
โข ((๐โ๐) โ (0...(โฏโ๐)) โ ((โฏโ๐)C(๐โ๐)) โ โ) |
39 | 37, 38 | syl 17 |
. . 3
โข (๐ โ ((โฏโ๐)C(๐โ๐)) โ โ) |
40 | 12, 39 | eqeltrrd 2839 |
. 2
โข (๐ โ (โฏโ๐) โ
โ) |
41 | | nnuz 12807 |
. . . . . . . . . . 11
โข โ =
(โคโฅโ1) |
42 | 6, 41 | eleqtrdi 2848 |
. . . . . . . . . 10
โข (๐ โ (๐โ๐) โ
(โคโฅโ1)) |
43 | | elfz5 13434 |
. . . . . . . . . 10
โข (((๐โ๐) โ (โคโฅโ1)
โง (โฏโ๐)
โ โค) โ ((๐โ๐) โ (1...(โฏโ๐)) โ (๐โ๐) โค (โฏโ๐))) |
44 | 42, 34, 43 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ ((๐โ๐) โ (1...(โฏโ๐)) โ (๐โ๐) โค (โฏโ๐))) |
45 | 30, 44 | mpbird 257 |
. . . . . . . 8
โข (๐ โ (๐โ๐) โ (1...(โฏโ๐))) |
46 | | 1zzd 12535 |
. . . . . . . . 9
โข (๐ โ 1 โ
โค) |
47 | | fzsubel 13478 |
. . . . . . . . 9
โข (((1
โ โค โง (โฏโ๐) โ โค) โง ((๐โ๐) โ โค โง 1 โ โค))
โ ((๐โ๐) โ
(1...(โฏโ๐))
โ ((๐โ๐) โ 1) โ ((1 โ
1)...((โฏโ๐)
โ 1)))) |
48 | 46, 34, 7, 46, 47 | syl22anc 838 |
. . . . . . . 8
โข (๐ โ ((๐โ๐) โ (1...(โฏโ๐)) โ ((๐โ๐) โ 1) โ ((1 โ
1)...((โฏโ๐)
โ 1)))) |
49 | 45, 48 | mpbid 231 |
. . . . . . 7
โข (๐ โ ((๐โ๐) โ 1) โ ((1 โ
1)...((โฏโ๐)
โ 1))) |
50 | | 1m1e0 12226 |
. . . . . . . 8
โข (1
โ 1) = 0 |
51 | 50 | oveq1i 7368 |
. . . . . . 7
โข ((1
โ 1)...((โฏโ๐) โ 1)) = (0...((โฏโ๐) โ 1)) |
52 | 49, 51 | eleqtrdi 2848 |
. . . . . 6
โข (๐ โ ((๐โ๐) โ 1) โ
(0...((โฏโ๐)
โ 1))) |
53 | | bcp1nk 14218 |
. . . . . 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 12476 |
. . . . . . 7
โข (๐ โ (โฏโ๐) โ
โ) |
56 | | ax-1cn 11110 |
. . . . . . 7
โข 1 โ
โ |
57 | | npcan 11411 |
. . . . . . 7
โข
(((โฏโ๐)
โ โ โง 1 โ โ) โ (((โฏโ๐) โ 1) + 1) =
(โฏโ๐)) |
58 | 55, 56, 57 | sylancl 587 |
. . . . . 6
โข (๐ โ (((โฏโ๐) โ 1) + 1) =
(โฏโ๐)) |
59 | 6 | nncnd 12170 |
. . . . . . 7
โข (๐ โ (๐โ๐) โ โ) |
60 | | npcan 11411 |
. . . . . . 7
โข (((๐โ๐) โ โ โง 1 โ โ)
โ (((๐โ๐) โ 1) + 1) = (๐โ๐)) |
61 | 59, 56, 60 | sylancl 587 |
. . . . . 6
โข (๐ โ (((๐โ๐) โ 1) + 1) = (๐โ๐)) |
62 | 58, 61 | oveq12d 7376 |
. . . . 5
โข (๐ โ ((((โฏโ๐) โ 1) + 1)C(((๐โ๐) โ 1) + 1)) = ((โฏโ๐)C(๐โ๐))) |
63 | 58, 61 | oveq12d 7376 |
. . . . . 6
โข (๐ โ ((((โฏโ๐) โ 1) + 1) / (((๐โ๐) โ 1) + 1)) = ((โฏโ๐) / (๐โ๐))) |
64 | 63 | oveq2d 7374 |
. . . . 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 7374 |
. . 3
โข (๐ โ (๐ pCnt ((โฏโ๐)C(๐โ๐))) = (๐ pCnt ((((โฏโ๐) โ 1)C((๐โ๐) โ 1)) ยท ((โฏโ๐) / (๐โ๐))))) |
67 | 12 | oveq2d 7374 |
. . 3
โข (๐ โ (๐ pCnt ((โฏโ๐)C(๐โ๐))) = (๐ pCnt (โฏโ๐))) |
68 | | bccl2 14224 |
. . . . . . 7
โข (((๐โ๐) โ 1) โ
(0...((โฏโ๐)
โ 1)) โ (((โฏโ๐) โ 1)C((๐โ๐) โ 1)) โ
โ) |
69 | 52, 68 | syl 17 |
. . . . . 6
โข (๐ โ (((โฏโ๐) โ 1)C((๐โ๐) โ 1)) โ
โ) |
70 | 69 | nnzd 12527 |
. . . . 5
โข (๐ โ (((โฏโ๐) โ 1)C((๐โ๐) โ 1)) โ
โค) |
71 | 69 | nnne0d 12204 |
. . . . 5
โข (๐ โ (((โฏโ๐) โ 1)C((๐โ๐) โ 1)) โ 0) |
72 | 6 | nnne0d 12204 |
. . . . . . 7
โข (๐ โ (๐โ๐) โ 0) |
73 | | dvdsval2 16140 |
. . . . . . 7
โข (((๐โ๐) โ โค โง (๐โ๐) โ 0 โง (โฏโ๐) โ โค) โ ((๐โ๐) โฅ (โฏโ๐) โ ((โฏโ๐) / (๐โ๐)) โ โค)) |
74 | 7, 72, 34, 73 | syl3anc 1372 |
. . . . . 6
โข (๐ โ ((๐โ๐) โฅ (โฏโ๐) โ ((โฏโ๐) / (๐โ๐)) โ โค)) |
75 | 13, 74 | mpbid 231 |
. . . . 5
โข (๐ โ ((โฏโ๐) / (๐โ๐)) โ โค) |
76 | 27 | nnne0d 12204 |
. . . . . 6
โข (๐ โ (โฏโ๐) โ 0) |
77 | 55, 59, 76, 72 | divne0d 11948 |
. . . . 5
โข (๐ โ ((โฏโ๐) / (๐โ๐)) โ 0) |
78 | | pcmul 16724 |
. . . . 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 1380 |
. . . 4
โข (๐ โ (๐ pCnt ((((โฏโ๐) โ 1)C((๐โ๐) โ 1)) ยท ((โฏโ๐) / (๐โ๐)))) = ((๐ pCnt (((โฏโ๐) โ 1)C((๐โ๐) โ 1))) + (๐ pCnt ((โฏโ๐) / (๐โ๐))))) |
80 | | 1cnd 11151 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
81 | 55, 59, 80 | npncand 11537 |
. . . . . . . 8
โข (๐ โ (((โฏโ๐) โ (๐โ๐)) + ((๐โ๐) โ 1)) = ((โฏโ๐) โ 1)) |
82 | 81 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ ((((โฏโ๐) โ (๐โ๐)) + ((๐โ๐) โ 1))C((๐โ๐) โ 1)) = (((โฏโ๐) โ 1)C((๐โ๐) โ 1))) |
83 | 82 | oveq2d 7374 |
. . . . . 6
โข (๐ โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ((๐โ๐) โ 1))C((๐โ๐) โ 1))) = (๐ pCnt (((โฏโ๐) โ 1)C((๐โ๐) โ 1)))) |
84 | 6 | nnred 12169 |
. . . . . . . 8
โข (๐ โ (๐โ๐) โ โ) |
85 | 84 | ltm1d 12088 |
. . . . . . 7
โข (๐ โ ((๐โ๐) โ 1) < (๐โ๐)) |
86 | | nnm1nn0 12455 |
. . . . . . . . 9
โข ((๐โ๐) โ โ โ ((๐โ๐) โ 1) โ
โ0) |
87 | 6, 86 | syl 17 |
. . . . . . . 8
โข (๐ โ ((๐โ๐) โ 1) โ
โ0) |
88 | | breq1 5109 |
. . . . . . . . . . 11
โข (๐ฅ = 0 โ (๐ฅ < (๐โ๐) โ 0 < (๐โ๐))) |
89 | | bcxmaslem1 15720 |
. . . . . . . . . . . . 13
โข (๐ฅ = 0 โ
((((โฏโ๐)
โ (๐โ๐)) + ๐ฅ)C๐ฅ) = ((((โฏโ๐) โ (๐โ๐)) + 0)C0)) |
90 | 89 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ฅ = 0 โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + 0)C0))) |
91 | 90 | eqeq1d 2739 |
. . . . . . . . . . 11
โข (๐ฅ = 0 โ ((๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = 0 โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + 0)C0)) = 0)) |
92 | 88, 91 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ฅ = 0 โ ((๐ฅ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = 0) โ (0 < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + 0)C0)) = 0))) |
93 | 92 | imbi2d 341 |
. . . . . . . . 9
โข (๐ฅ = 0 โ ((๐ โ (๐ฅ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = 0)) โ (๐ โ (0 < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + 0)C0)) = 0)))) |
94 | | breq1 5109 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ (๐ฅ < (๐โ๐) โ ๐ < (๐โ๐))) |
95 | | bcxmaslem1 15720 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ โ ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ) = ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐)) |
96 | 95 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐))) |
97 | 96 | eqeq1d 2739 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ ((๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = 0 โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐)) = 0)) |
98 | 94, 97 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ ((๐ฅ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = 0) โ (๐ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐)) = 0))) |
99 | 98 | imbi2d 341 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ((๐ โ (๐ฅ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = 0)) โ (๐ โ (๐ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐)) = 0)))) |
100 | | breq1 5109 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ + 1) โ (๐ฅ < (๐โ๐) โ (๐ + 1) < (๐โ๐))) |
101 | | bcxmaslem1 15720 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ + 1) โ ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ) = ((((โฏโ๐) โ (๐โ๐)) + (๐ + 1))C(๐ + 1))) |
102 | 101 | oveq2d 7374 |
. . . . . . . . . . . 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 345 |
. . . . . . . . . 10
โข (๐ฅ = (๐ + 1) โ ((๐ฅ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = 0) โ ((๐ + 1) < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + (๐ + 1))C(๐ + 1))) = 0))) |
105 | 104 | imbi2d 341 |
. . . . . . . . 9
โข (๐ฅ = (๐ + 1) โ ((๐ โ (๐ฅ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = 0)) โ (๐ โ ((๐ + 1) < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + (๐ + 1))C(๐ + 1))) = 0)))) |
106 | | breq1 5109 |
. . . . . . . . . . 11
โข (๐ฅ = ((๐โ๐) โ 1) โ (๐ฅ < (๐โ๐) โ ((๐โ๐) โ 1) < (๐โ๐))) |
107 | | bcxmaslem1 15720 |
. . . . . . . . . . . . 13
โข (๐ฅ = ((๐โ๐) โ 1) โ ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ) = ((((โฏโ๐) โ (๐โ๐)) + ((๐โ๐) โ 1))C((๐โ๐) โ 1))) |
108 | 107 | oveq2d 7374 |
. . . . . . . . . . . 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 345 |
. . . . . . . . . 10
โข (๐ฅ = ((๐โ๐) โ 1) โ ((๐ฅ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = 0) โ (((๐โ๐) โ 1) < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ((๐โ๐) โ 1))C((๐โ๐) โ 1))) = 0))) |
111 | 110 | imbi2d 341 |
. . . . . . . . 9
โข (๐ฅ = ((๐โ๐) โ 1) โ ((๐ โ (๐ฅ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐ฅ)C๐ฅ)) = 0)) โ (๐ โ (((๐โ๐) โ 1) < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ((๐โ๐) โ 1))C((๐โ๐) โ 1))) = 0)))) |
112 | | znn0sub 12551 |
. . . . . . . . . . . . . . . 16
โข (((๐โ๐) โ โค โง (โฏโ๐) โ โค) โ ((๐โ๐) โค (โฏโ๐) โ ((โฏโ๐) โ (๐โ๐)) โ
โ0)) |
113 | 7, 34, 112 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐โ๐) โค (โฏโ๐) โ ((โฏโ๐) โ (๐โ๐)) โ
โ0)) |
114 | 30, 113 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ ((โฏโ๐) โ (๐โ๐)) โ
โ0) |
115 | | 0nn0 12429 |
. . . . . . . . . . . . . 14
โข 0 โ
โ0 |
116 | | nn0addcl 12449 |
. . . . . . . . . . . . . 14
โข
((((โฏโ๐)
โ (๐โ๐)) โ โ0
โง 0 โ โ0) โ (((โฏโ๐) โ (๐โ๐)) + 0) โ
โ0) |
117 | 114, 115,
116 | sylancl 587 |
. . . . . . . . . . . . 13
โข (๐ โ (((โฏโ๐) โ (๐โ๐)) + 0) โ
โ0) |
118 | | bcn0 14211 |
. . . . . . . . . . . . 13
โข
((((โฏโ๐)
โ (๐โ๐)) + 0) โ
โ0 โ ((((โฏโ๐) โ (๐โ๐)) + 0)C0) = 1) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ((((โฏโ๐) โ (๐โ๐)) + 0)C0) = 1) |
120 | 119 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + 0)C0)) = (๐ pCnt 1)) |
121 | | pc1 16728 |
. . . . . . . . . . . 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 12423 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ ๐ โ
โ) |
126 | 125 | ad2antrl 727 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ โ โ) |
127 | | nn0p1nn 12453 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
128 | 127 | ad2antrl 727 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ + 1) โ โ) |
129 | 128 | nnred 12169 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ + 1) โ โ) |
130 | 6 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐โ๐) โ โ) |
131 | 130 | nnred 12169 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐โ๐) โ โ) |
132 | 126 | ltp1d 12086 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ < (๐ + 1)) |
133 | | simprr 772 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ + 1) < (๐โ๐)) |
134 | 126, 129,
131, 132, 133 | lttrd 11317 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ < (๐โ๐)) |
135 | 134 | expr 458 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ0) โ ((๐ + 1) < (๐โ๐) โ ๐ < (๐โ๐))) |
136 | 135 | imim1d 82 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ ((๐ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐)) = 0) โ ((๐ + 1) < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐)) = 0))) |
137 | | oveq1 7365 |
. . . . . . . . . . 11
โข ((๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐)) = 0 โ ((๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐)) + (๐ pCnt (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1)))) = (0 + (๐ pCnt (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1))))) |
138 | 114 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((โฏโ๐) โ (๐โ๐)) โ
โ0) |
139 | 138 | nn0cnd 12476 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((โฏโ๐) โ (๐โ๐)) โ โ) |
140 | | nn0cn 12424 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ ๐ โ
โ) |
141 | 140 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ โ โ) |
142 | | 1cnd 11151 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ 1 โ
โ) |
143 | 139, 141,
142 | addassd 11178 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) = (((โฏโ๐) โ (๐โ๐)) + (๐ + 1))) |
144 | 143 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1)C(๐ + 1)) = ((((โฏโ๐) โ (๐โ๐)) + (๐ + 1))C(๐ + 1))) |
145 | | nn0addge2 12461 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง
((โฏโ๐) โ
(๐โ๐)) โ โ0) โ ๐ โค (((โฏโ๐) โ (๐โ๐)) + ๐)) |
146 | 126, 138,
145 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ โค (((โฏโ๐) โ (๐โ๐)) + ๐)) |
147 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ โ โ0) |
148 | 147, 32 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ โ
(โคโฅโ0)) |
149 | 138, 147 | nn0addcld 12478 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (((โฏโ๐) โ (๐โ๐)) + ๐) โ
โ0) |
150 | 149 | nn0zd 12526 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (((โฏโ๐) โ (๐โ๐)) + ๐) โ โค) |
151 | | elfz5 13434 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ
(โคโฅโ0) โง (((โฏโ๐) โ (๐โ๐)) + ๐) โ โค) โ (๐ โ (0...(((โฏโ๐) โ (๐โ๐)) + ๐)) โ ๐ โค (((โฏโ๐) โ (๐โ๐)) + ๐))) |
152 | 148, 150,
151 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ โ (0...(((โฏโ๐) โ (๐โ๐)) + ๐)) โ ๐ โค (((โฏโ๐) โ (๐โ๐)) + ๐))) |
153 | 146, 152 | mpbird 257 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ โ (0...(((โฏโ๐) โ (๐โ๐)) + ๐))) |
154 | | bcp1nk 14218 |
. . . . . . . . . . . . . . . 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 7374 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + (๐ + 1))C(๐ + 1))) = (๐ pCnt (((((โฏโ๐) โ (๐โ๐)) + ๐)C๐) ยท (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1))))) |
158 | 2 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ โ โ) |
159 | | bccl2 14224 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(0...(((โฏโ๐)
โ (๐โ๐)) + ๐)) โ ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐) โ โ) |
160 | 153, 159 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐) โ โ) |
161 | | nnq 12888 |
. . . . . . . . . . . . . . 15
โข
(((((โฏโ๐) โ (๐โ๐)) + ๐)C๐) โ โ โ
((((โฏโ๐)
โ (๐โ๐)) + ๐)C๐) โ โ) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐) โ โ) |
163 | 160 | nnne0d 12204 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐) โ 0) |
164 | 150 | peano2zd 12611 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) โ โค) |
165 | | znq 12878 |
. . . . . . . . . . . . . . 15
โข
((((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) โ โค โง (๐ + 1) โ โ) โ
(((((โฏโ๐)
โ (๐โ๐)) + ๐) + 1) / (๐ + 1)) โ โ) |
166 | 164, 128,
165 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1)) โ โ) |
167 | | nn0p1nn 12453 |
. . . . . . . . . . . . . . . . 17
โข
((((โฏโ๐)
โ (๐โ๐)) + ๐) โ โ0 โ
((((โฏโ๐)
โ (๐โ๐)) + ๐) + 1) โ โ) |
168 | 149, 167 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) โ โ) |
169 | | nnrp 12927 |
. . . . . . . . . . . . . . . . 17
โข
(((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) โ โ โ
((((โฏโ๐)
โ (๐โ๐)) + ๐) + 1) โ
โ+) |
170 | | nnrp 12927 |
. . . . . . . . . . . . . . . . 17
โข ((๐ + 1) โ โ โ
(๐ + 1) โ
โ+) |
171 | | rpdivcl 12941 |
. . . . . . . . . . . . . . . . 17
โข
((((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) โ โ+ โง
(๐ + 1) โ
โ+) โ (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1)) โ
โ+) |
172 | 169, 170,
171 | syl2an 597 |
. . . . . . . . . . . . . . . 16
โข
((((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) โ โ โง (๐ + 1) โ โ) โ
(((((โฏโ๐)
โ (๐โ๐)) + ๐) + 1) / (๐ + 1)) โ
โ+) |
173 | 168, 128,
172 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1)) โ
โ+) |
174 | 173 | rpne0d 12963 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1)) โ 0) |
175 | | pcqmul 16726 |
. . . . . . . . . . . . . 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 1380 |
. . . . . . . . . . . . 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 12204 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) โ 0) |
179 | | pcdiv 16725 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง
(((((โฏโ๐)
โ (๐โ๐)) + ๐) + 1) โ โค โง
((((โฏโ๐)
โ (๐โ๐)) + ๐) + 1) โ 0) โง (๐ + 1) โ โ) โ (๐ pCnt (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1))) = ((๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1)) โ (๐ pCnt (๐ + 1)))) |
180 | 158, 164,
178, 128, 179 | syl121anc 1376 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1))) = ((๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1)) โ (๐ pCnt (๐ + 1)))) |
181 | 128 | nncnd 12170 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ + 1) โ โ) |
182 | 139, 181,
143 | comraddd 11370 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) = ((๐ + 1) + ((โฏโ๐) โ (๐โ๐)))) |
183 | 182 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1)) = (๐ pCnt ((๐ + 1) + ((โฏโ๐) โ (๐โ๐))))) |
184 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) = 0) โ ((โฏโ๐) โ (๐โ๐)) = 0) |
185 | 184 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) = 0) โ ((๐ + 1) + ((โฏโ๐) โ (๐โ๐))) = ((๐ + 1) + 0)) |
186 | 181 | addid1d 11356 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((๐ + 1) + 0) = (๐ + 1)) |
187 | 186 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) = 0) โ ((๐ + 1) + 0) = (๐ + 1)) |
188 | 185, 187 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) = 0) โ (๐ + 1) = ((๐ + 1) + ((โฏโ๐) โ (๐โ๐)))) |
189 | 188 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) = 0) โ (๐ pCnt (๐ + 1)) = (๐ pCnt ((๐ + 1) + ((โฏโ๐) โ (๐โ๐))))) |
190 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ ๐ โ โ) |
191 | | nnq 12888 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ + 1) โ โ โ
(๐ + 1) โ
โ) |
192 | 128, 191 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ + 1) โ โ) |
193 | 192 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (๐ + 1) โ โ) |
194 | 138 | nn0zd 12526 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((โฏโ๐) โ (๐โ๐)) โ โค) |
195 | | zq 12880 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((โฏโ๐)
โ (๐โ๐)) โ โค โ
((โฏโ๐) โ
(๐โ๐)) โ โ) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((โฏโ๐) โ (๐โ๐)) โ โ) |
197 | 196 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ ((โฏโ๐) โ (๐โ๐)) โ โ) |
198 | 158, 128 | pccld 16723 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt (๐ + 1)) โ
โ0) |
199 | 198 | nn0red 12475 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt (๐ + 1)) โ โ) |
200 | 199 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (๐ pCnt (๐ + 1)) โ โ) |
201 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ โ
โ0) |
202 | 201 | nn0red 12475 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ๐ โ โ) |
203 | 202 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ ๐ โ โ) |
204 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ ((โฏโ๐) โ (๐โ๐)) โ 0) |
205 | 204 | neneqd 2949 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ ยฌ
((โฏโ๐) โ
(๐โ๐)) = 0) |
206 | 114 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ ((โฏโ๐) โ (๐โ๐)) โ
โ0) |
207 | | elnn0 12416 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((โฏโ๐)
โ (๐โ๐)) โ โ0
โ (((โฏโ๐)
โ (๐โ๐)) โ โ โจ
((โฏโ๐) โ
(๐โ๐)) = 0)) |
208 | 206, 207 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (((โฏโ๐) โ (๐โ๐)) โ โ โจ ((โฏโ๐) โ (๐โ๐)) = 0)) |
209 | 208 | ord 863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (ยฌ
((โฏโ๐) โ
(๐โ๐)) โ โ โ
((โฏโ๐) โ
(๐โ๐)) = 0)) |
210 | 205, 209 | mt3d 148 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ ((โฏโ๐) โ (๐โ๐)) โ โ) |
211 | 190, 210 | pccld 16723 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (๐ pCnt ((โฏโ๐) โ (๐โ๐))) โ
โ0) |
212 | 211 | nn0red 12475 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (๐ pCnt ((โฏโ๐) โ (๐โ๐))) โ โ) |
213 | 128 | nnzd 12527 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ + 1) โ โค) |
214 | | pcdvdsb 16742 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โ โ โง (๐ + 1) โ โค โง ๐ โ โ0)
โ (๐ โค (๐ pCnt (๐ + 1)) โ (๐โ๐) โฅ (๐ + 1))) |
215 | 158, 213,
201, 214 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ โค (๐ pCnt (๐ + 1)) โ (๐โ๐) โฅ (๐ + 1))) |
216 | 7 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐โ๐) โ โค) |
217 | | dvdsle 16193 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐โ๐) โ โค โง (๐ + 1) โ โ) โ ((๐โ๐) โฅ (๐ + 1) โ (๐โ๐) โค (๐ + 1))) |
218 | 216, 128,
217 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((๐โ๐) โฅ (๐ + 1) โ (๐โ๐) โค (๐ + 1))) |
219 | 215, 218 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ โค (๐ pCnt (๐ + 1)) โ (๐โ๐) โค (๐ + 1))) |
220 | 202, 199 | lenltd 11302 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ โค (๐ pCnt (๐ + 1)) โ ยฌ (๐ pCnt (๐ + 1)) < ๐)) |
221 | 131, 129 | lenltd 11302 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((๐โ๐) โค (๐ + 1) โ ยฌ (๐ + 1) < (๐โ๐))) |
222 | 219, 220,
221 | 3imtr3d 293 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (ยฌ (๐ pCnt (๐ + 1)) < ๐ โ ยฌ (๐ + 1) < (๐โ๐))) |
223 | 133, 222 | mt4d 117 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt (๐ + 1)) < ๐) |
224 | 223 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (๐ pCnt (๐ + 1)) < ๐) |
225 | | dvdssubr 16188 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐โ๐) โ โค โง (โฏโ๐) โ โค) โ ((๐โ๐) โฅ (โฏโ๐) โ (๐โ๐) โฅ ((โฏโ๐) โ (๐โ๐)))) |
226 | 7, 34, 225 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ((๐โ๐) โฅ (โฏโ๐) โ (๐โ๐) โฅ ((โฏโ๐) โ (๐โ๐)))) |
227 | 13, 226 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐โ๐) โฅ ((โฏโ๐) โ (๐โ๐))) |
228 | 227 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (๐โ๐) โฅ ((โฏโ๐) โ (๐โ๐))) |
229 | 206 | nn0zd 12526 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ ((โฏโ๐) โ (๐โ๐)) โ โค) |
230 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ ๐ โ
โ0) |
231 | | pcdvdsb 16742 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โ โง
((โฏโ๐) โ
(๐โ๐)) โ โค โง ๐ โ โ0) โ (๐ โค (๐ pCnt ((โฏโ๐) โ (๐โ๐))) โ (๐โ๐) โฅ ((โฏโ๐) โ (๐โ๐)))) |
232 | 190, 229,
230, 231 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (๐ โค (๐ pCnt ((โฏโ๐) โ (๐โ๐))) โ (๐โ๐) โฅ ((โฏโ๐) โ (๐โ๐)))) |
233 | 228, 232 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ ๐ โค (๐ pCnt ((โฏโ๐) โ (๐โ๐)))) |
234 | 200, 203,
212, 224, 233 | ltletrd 11316 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (๐ pCnt (๐ + 1)) < (๐ pCnt ((โฏโ๐) โ (๐โ๐)))) |
235 | 190, 193,
197, 234 | pcadd2 16763 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โง ((โฏโ๐) โ (๐โ๐)) โ 0) โ (๐ pCnt (๐ + 1)) = (๐ pCnt ((๐ + 1) + ((โฏโ๐) โ (๐โ๐))))) |
236 | 189, 235 | pm2.61dane 3033 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt (๐ + 1)) = (๐ pCnt ((๐ + 1) + ((โฏโ๐) โ (๐โ๐))))) |
237 | 183, 236 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1)) = (๐ pCnt (๐ + 1))) |
238 | 198 | nn0cnd 12476 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt (๐ + 1)) โ โ) |
239 | 237, 238 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1)) โ โ) |
240 | 239, 237 | subeq0bd 11582 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐) + 1)) โ (๐ pCnt (๐ + 1))) = 0) |
241 | 180, 240 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (๐ pCnt (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1))) = 0) |
242 | 241 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ (0 + (๐ pCnt (((((โฏโ๐) โ (๐โ๐)) + ๐) + 1) / (๐ + 1)))) = (0 + 0)) |
243 | | 00id 11331 |
. . . . . . . . . . . . 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 246 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ0 โง (๐ + 1) < (๐โ๐))) โ ((๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐)) = 0 โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + (๐ + 1))C(๐ + 1))) = 0)) |
247 | 136, 246 | animpimp2impd 845 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((๐ โ (๐ < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + ๐)C๐)) = 0)) โ (๐ โ ((๐ + 1) < (๐โ๐) โ (๐ pCnt ((((โฏโ๐) โ (๐โ๐)) + (๐ + 1))C(๐ + 1))) = 0)))) |
248 | 93, 99, 105, 111, 124, 247 | nn0ind 12599 |
. . . . . . . 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 16725 |
. . . . . . 7
โข ((๐ โ โ โง
((โฏโ๐) โ
โค โง (โฏโ๐) โ 0) โง (๐โ๐) โ โ) โ (๐ pCnt ((โฏโ๐) / (๐โ๐))) = ((๐ pCnt (โฏโ๐)) โ (๐ pCnt (๐โ๐)))) |
253 | 2, 34, 76, 6, 252 | syl121anc 1376 |
. . . . . 6
โข (๐ โ (๐ pCnt ((โฏโ๐) / (๐โ๐))) = ((๐ pCnt (โฏโ๐)) โ (๐ pCnt (๐โ๐)))) |
254 | 5 | nn0zd 12526 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
255 | | pcid 16746 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โค) โ (๐ pCnt (๐โ๐)) = ๐) |
256 | 2, 254, 255 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐ pCnt (๐โ๐)) = ๐) |
257 | 256 | oveq2d 7374 |
. . . . . 6
โข (๐ โ ((๐ pCnt (โฏโ๐)) โ (๐ pCnt (๐โ๐))) = ((๐ pCnt (โฏโ๐)) โ ๐)) |
258 | 253, 257 | eqtrd 2777 |
. . . . 5
โข (๐ โ (๐ pCnt ((โฏโ๐) / (๐โ๐))) = ((๐ pCnt (โฏโ๐)) โ ๐)) |
259 | 251, 258 | oveq12d 7376 |
. . . 4
โข (๐ โ ((๐ pCnt (((โฏโ๐) โ 1)C((๐โ๐) โ 1))) + (๐ pCnt ((โฏโ๐) / (๐โ๐)))) = (0 + ((๐ pCnt (โฏโ๐)) โ ๐))) |
260 | 2, 27 | pccld 16723 |
. . . . . . . 8
โข (๐ โ (๐ pCnt (โฏโ๐)) โ
โ0) |
261 | 260 | nn0zd 12526 |
. . . . . . 7
โข (๐ โ (๐ pCnt (โฏโ๐)) โ โค) |
262 | 261, 254 | zsubcld 12613 |
. . . . . 6
โข (๐ โ ((๐ pCnt (โฏโ๐)) โ ๐) โ โค) |
263 | 262 | zcnd 12609 |
. . . . 5
โข (๐ โ ((๐ pCnt (โฏโ๐)) โ ๐) โ โ) |
264 | 263 | addid2d 11357 |
. . . 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 513 |
1
โข (๐ โ ((โฏโ๐) โ โ โง (๐ pCnt (โฏโ๐)) = ((๐ pCnt (โฏโ๐)) โ ๐))) |