Step | Hyp | Ref
| Expression |
1 | | fzfi 13886 |
. . . . . . 7
โข
(1...๐) โ
Fin |
2 | | diffi 9129 |
. . . . . . 7
โข
((1...๐) โ Fin
โ ((1...๐) โ
{๐}) โ
Fin) |
3 | 1, 2 | mp1i 13 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ ((1...๐) โ {๐}) โ Fin) |
4 | | eldifi 4090 |
. . . . . . . . 9
โข (๐ โ ((1...๐) โ {๐}) โ ๐ โ (1...๐)) |
5 | | elfzelz 13450 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ ๐ โ โค) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
โข (๐ โ ((1...๐) โ {๐}) โ ๐ โ โค) |
7 | | 1zzd 12542 |
. . . . . . . 8
โข (๐ โ ((1...๐) โ {๐}) โ 1 โ โค) |
8 | 6, 7 | ifcld 4536 |
. . . . . . 7
โข (๐ โ ((1...๐) โ {๐}) โ if(๐ โ โ, ๐, 1) โ โค) |
9 | 8 | adantl 483 |
. . . . . 6
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โง ๐ โ ((1...๐) โ {๐})) โ if(๐ โ โ, ๐, 1) โ โค) |
10 | 3, 9 | fprodzcl 15845 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ โ๐ โ ((1...๐) โ {๐})if(๐ โ โ, ๐, 1) โ โค) |
11 | | prmz 16559 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
12 | 11 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โค) |
13 | 12 | adantr 482 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ ๐ โ โค) |
14 | | dvdsmul2 16169 |
. . . . 5
โข
((โ๐ โ
((1...๐) โ {๐})if(๐ โ โ, ๐, 1) โ โค โง ๐ โ โค) โ ๐ โฅ (โ๐ โ ((1...๐) โ {๐})if(๐ โ โ, ๐, 1) ยท ๐)) |
15 | 10, 13, 14 | syl2anc 585 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ ๐ โฅ (โ๐ โ ((1...๐) โ {๐})if(๐ โ โ, ๐, 1) ยท ๐)) |
16 | | nnnn0 12428 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ0) |
17 | | prmoval 16913 |
. . . . . . . 8
โข (๐ โ โ0
โ (#pโ๐) = โ๐ โ (1...๐)if(๐ โ โ, ๐, 1)) |
18 | 16, 17 | syl 17 |
. . . . . . 7
โข (๐ โ โ โ
(#pโ๐) =
โ๐ โ (1...๐)if(๐ โ โ, ๐, 1)) |
19 | 18 | ad2antrr 725 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ (#pโ๐) = โ๐ โ (1...๐)if(๐ โ โ, ๐, 1)) |
20 | 19 | breq2d 5121 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ (๐ โฅ (#pโ๐) โ ๐ โฅ โ๐ โ (1...๐)if(๐ โ โ, ๐, 1))) |
21 | | neldifsnd 4757 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ ยฌ ๐ โ ((1...๐) โ {๐})) |
22 | | disjsn 4676 |
. . . . . . . . 9
โข
((((1...๐) โ
{๐}) โฉ {๐}) = โ
โ ยฌ ๐ โ ((1...๐) โ {๐})) |
23 | 21, 22 | sylibr 233 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ (((1...๐) โ {๐}) โฉ {๐}) = โ
) |
24 | | prmnn 16558 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
25 | 24 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
26 | 25 | anim1i 616 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ (๐ โ โ โง ๐ โค ๐)) |
27 | | nnz 12528 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โค) |
28 | | fznn 13518 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐ โ (1...๐) โ (๐ โ โ โง ๐ โค ๐))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ (1...๐) โ (๐ โ โ โง ๐ โค ๐))) |
30 | 29 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ (๐ โ (1...๐) โ (๐ โ โ โง ๐ โค ๐))) |
31 | 26, 30 | mpbird 257 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ ๐ โ (1...๐)) |
32 | | difsnid 4774 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ (((1...๐) โ {๐}) โช {๐}) = (1...๐)) |
33 | 32 | eqcomd 2739 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ (1...๐) = (((1...๐) โ {๐}) โช {๐})) |
34 | 31, 33 | syl 17 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ (1...๐) = (((1...๐) โ {๐}) โช {๐})) |
35 | | fzfid 13887 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ (1...๐) โ Fin) |
36 | | 1zzd 12542 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ 1 โ โค) |
37 | 5, 36 | ifcld 4536 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ if(๐ โ โ, ๐, 1) โ โค) |
38 | 37 | zcnd 12616 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ if(๐ โ โ, ๐, 1) โ โ) |
39 | 38 | adantl 483 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โง ๐ โ (1...๐)) โ if(๐ โ โ, ๐, 1) โ โ) |
40 | 23, 34, 35, 39 | fprodsplit 15857 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ โ๐ โ (1...๐)if(๐ โ โ, ๐, 1) = (โ๐ โ ((1...๐) โ {๐})if(๐ โ โ, ๐, 1) ยท โ๐ โ {๐}if(๐ โ โ, ๐, 1))) |
41 | | simplr 768 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ ๐ โ โ) |
42 | 25 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ ๐ โ โ) |
43 | 42 | nncnd 12177 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ ๐ โ โ) |
44 | | 1cnd 11158 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ 1 โ โ) |
45 | 43, 44 | ifcld 4536 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ if(๐ โ โ, ๐, 1) โ โ) |
46 | | eleq1w 2817 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
47 | | id 22 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ๐ = ๐) |
48 | 46, 47 | ifbieq1d 4514 |
. . . . . . . . . . 11
โข (๐ = ๐ โ if(๐ โ โ, ๐, 1) = if(๐ โ โ, ๐, 1)) |
49 | 48 | prodsn 15853 |
. . . . . . . . . 10
โข ((๐ โ โ โง if(๐ โ โ, ๐, 1) โ โ) โ
โ๐ โ {๐}if(๐ โ โ, ๐, 1) = if(๐ โ โ, ๐, 1)) |
50 | 41, 45, 49 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ โ๐ โ {๐}if(๐ โ โ, ๐, 1) = if(๐ โ โ, ๐, 1)) |
51 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
52 | 51 | iftrued 4498 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ if(๐ โ โ, ๐, 1) = ๐) |
53 | 52 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ if(๐ โ โ, ๐, 1) = ๐) |
54 | 50, 53 | eqtrd 2773 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ โ๐ โ {๐}if(๐ โ โ, ๐, 1) = ๐) |
55 | 54 | oveq2d 7377 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ (โ๐ โ ((1...๐) โ {๐})if(๐ โ โ, ๐, 1) ยท โ๐ โ {๐}if(๐ โ โ, ๐, 1)) = (โ๐ โ ((1...๐) โ {๐})if(๐ โ โ, ๐, 1) ยท ๐)) |
56 | 40, 55 | eqtrd 2773 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ โ๐ โ (1...๐)if(๐ โ โ, ๐, 1) = (โ๐ โ ((1...๐) โ {๐})if(๐ โ โ, ๐, 1) ยท ๐)) |
57 | 56 | breq2d 5121 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ (๐ โฅ โ๐ โ (1...๐)if(๐ โ โ, ๐, 1) โ ๐ โฅ (โ๐ โ ((1...๐) โ {๐})if(๐ โ โ, ๐, 1) ยท ๐))) |
58 | 20, 57 | bitrd 279 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ (๐ โฅ (#pโ๐) โ ๐ โฅ (โ๐ โ ((1...๐) โ {๐})if(๐ โ โ, ๐, 1) ยท ๐))) |
59 | 15, 58 | mpbird 257 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โค ๐) โ ๐ โฅ (#pโ๐)) |
60 | 59 | ex 414 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โค ๐ โ ๐ โฅ (#pโ๐))) |
61 | 60 | ralrimiva 3140 |
1
โข (๐ โ โ โ
โ๐ โ โ
(๐ โค ๐ โ ๐ โฅ (#pโ๐))) |