Step | Hyp | Ref
| Expression |
1 | | dvdsflf1o.f |
. 2
โข ๐น = (๐ โ (1...(โโ(๐ด / ๐))) โฆ (๐ ยท ๐)) |
2 | | breq2 5114 |
. . 3
โข (๐ฅ = (๐ ยท ๐) โ (๐ โฅ ๐ฅ โ ๐ โฅ (๐ ยท ๐))) |
3 | | dvdsflf1o.2 |
. . . . 5
โข (๐ โ ๐ โ โ) |
4 | | elfznn 13477 |
. . . . 5
โข (๐ โ
(1...(โโ(๐ด /
๐))) โ ๐ โ
โ) |
5 | | nnmulcl 12184 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
6 | 3, 4, 5 | syl2an 597 |
. . . 4
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ (๐ ยท ๐) โ โ) |
7 | | dvdsflf1o.1 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
8 | 7, 3 | nndivred 12214 |
. . . . . . . 8
โข (๐ โ (๐ด / ๐) โ โ) |
9 | | fznnfl 13774 |
. . . . . . . 8
โข ((๐ด / ๐) โ โ โ (๐ โ (1...(โโ(๐ด / ๐))) โ (๐ โ โ โง ๐ โค (๐ด / ๐)))) |
10 | 8, 9 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ โ (1...(โโ(๐ด / ๐))) โ (๐ โ โ โง ๐ โค (๐ด / ๐)))) |
11 | 10 | simplbda 501 |
. . . . . 6
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ๐ โค (๐ด / ๐)) |
12 | 4 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ๐ โ โ) |
13 | 12 | nnred 12175 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ๐ โ โ) |
14 | 7 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ๐ด โ โ) |
15 | 3 | nnred 12175 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
16 | 15 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ๐ โ โ) |
17 | 3 | nngt0d 12209 |
. . . . . . . 8
โข (๐ โ 0 < ๐) |
18 | 17 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ 0 < ๐) |
19 | | lemuldiv2 12043 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ โง (๐ โ โ โง 0 <
๐)) โ ((๐ ยท ๐) โค ๐ด โ ๐ โค (๐ด / ๐))) |
20 | 13, 14, 16, 18, 19 | syl112anc 1375 |
. . . . . 6
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ((๐ ยท ๐) โค ๐ด โ ๐ โค (๐ด / ๐))) |
21 | 11, 20 | mpbird 257 |
. . . . 5
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ (๐ ยท ๐) โค ๐ด) |
22 | 3 | nnzd 12533 |
. . . . . . 7
โข (๐ โ ๐ โ โค) |
23 | | elfzelz 13448 |
. . . . . . 7
โข (๐ โ
(1...(โโ(๐ด /
๐))) โ ๐ โ
โค) |
24 | | zmulcl 12559 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (๐ ยท ๐) โ โค) |
25 | 22, 23, 24 | syl2an 597 |
. . . . . 6
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ (๐ ยท ๐) โ โค) |
26 | | flge 13717 |
. . . . . 6
โข ((๐ด โ โ โง (๐ ยท ๐) โ โค) โ ((๐ ยท ๐) โค ๐ด โ (๐ ยท ๐) โค (โโ๐ด))) |
27 | 14, 25, 26 | syl2anc 585 |
. . . . 5
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ((๐ ยท ๐) โค ๐ด โ (๐ ยท ๐) โค (โโ๐ด))) |
28 | 21, 27 | mpbid 231 |
. . . 4
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ (๐ ยท ๐) โค (โโ๐ด)) |
29 | 7 | flcld 13710 |
. . . . . 6
โข (๐ โ (โโ๐ด) โ
โค) |
30 | 29 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ (โโ๐ด) โ โค) |
31 | | fznn 13516 |
. . . . 5
โข
((โโ๐ด)
โ โค โ ((๐
ยท ๐) โ
(1...(โโ๐ด))
โ ((๐ ยท ๐) โ โ โง (๐ ยท ๐) โค (โโ๐ด)))) |
32 | 30, 31 | syl 17 |
. . . 4
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ((๐ ยท ๐) โ (1...(โโ๐ด)) โ ((๐ ยท ๐) โ โ โง (๐ ยท ๐) โค (โโ๐ด)))) |
33 | 6, 28, 32 | mpbir2and 712 |
. . 3
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ (๐ ยท ๐) โ (1...(โโ๐ด))) |
34 | | dvdsmul1 16167 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ ยท ๐)) |
35 | 22, 23, 34 | syl2an 597 |
. . 3
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ๐ โฅ (๐ ยท ๐)) |
36 | 2, 33, 35 | elrabd 3652 |
. 2
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ (๐ ยท ๐) โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) |
37 | | breq2 5114 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐)) |
38 | 37 | elrab 3650 |
. . . . . 6
โข (๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} โ (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) |
39 | 38 | simprbi 498 |
. . . . 5
โข (๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} โ ๐ โฅ ๐) |
40 | 39 | adantl 483 |
. . . 4
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ๐ โฅ ๐) |
41 | | elrabi 3644 |
. . . . . . 7
โข (๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} โ ๐ โ (1...(โโ๐ด))) |
42 | 41 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ๐ โ (1...(โโ๐ด))) |
43 | | elfznn 13477 |
. . . . . 6
โข (๐ โ
(1...(โโ๐ด))
โ ๐ โ
โ) |
44 | 42, 43 | syl 17 |
. . . . 5
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ๐ โ โ) |
45 | 3 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ๐ โ โ) |
46 | | nndivdvds 16152 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โฅ ๐ โ (๐ / ๐) โ โ)) |
47 | 44, 45, 46 | syl2anc 585 |
. . . 4
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ (๐ โฅ ๐ โ (๐ / ๐) โ โ)) |
48 | 40, 47 | mpbid 231 |
. . 3
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ (๐ / ๐) โ โ) |
49 | | fznnfl 13774 |
. . . . . . 7
โข (๐ด โ โ โ (๐ โ
(1...(โโ๐ด))
โ (๐ โ โ
โง ๐ โค ๐ด))) |
50 | 7, 49 | syl 17 |
. . . . . 6
โข (๐ โ (๐ โ (1...(โโ๐ด)) โ (๐ โ โ โง ๐ โค ๐ด))) |
51 | 50 | simplbda 501 |
. . . . 5
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ๐ โค ๐ด) |
52 | 41, 51 | sylan2 594 |
. . . 4
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ๐ โค ๐ด) |
53 | 44 | nnred 12175 |
. . . . 5
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ๐ โ โ) |
54 | 7 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ๐ด โ โ) |
55 | 15 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ๐ โ โ) |
56 | 17 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ 0 < ๐) |
57 | | lediv1 12027 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ โง (๐ โ โ โง 0 <
๐)) โ (๐ โค ๐ด โ (๐ / ๐) โค (๐ด / ๐))) |
58 | 53, 54, 55, 56, 57 | syl112anc 1375 |
. . . 4
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ (๐ โค ๐ด โ (๐ / ๐) โค (๐ด / ๐))) |
59 | 52, 58 | mpbid 231 |
. . 3
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ (๐ / ๐) โค (๐ด / ๐)) |
60 | 8 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ (๐ด / ๐) โ โ) |
61 | | fznnfl 13774 |
. . . 4
โข ((๐ด / ๐) โ โ โ ((๐ / ๐) โ (1...(โโ(๐ด / ๐))) โ ((๐ / ๐) โ โ โง (๐ / ๐) โค (๐ด / ๐)))) |
62 | 60, 61 | syl 17 |
. . 3
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ((๐ / ๐) โ (1...(โโ(๐ด / ๐))) โ ((๐ / ๐) โ โ โง (๐ / ๐) โค (๐ด / ๐)))) |
63 | 48, 59, 62 | mpbir2and 712 |
. 2
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ (๐ / ๐) โ (1...(โโ(๐ด / ๐)))) |
64 | 44 | nncnd 12176 |
. . . . 5
โข ((๐ โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ๐ โ โ) |
65 | 64 | adantrl 715 |
. . . 4
โข ((๐ โง (๐ โ (1...(โโ(๐ด / ๐))) โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ})) โ ๐ โ โ) |
66 | 3 | nncnd 12176 |
. . . . 5
โข (๐ โ ๐ โ โ) |
67 | 66 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ (1...(โโ(๐ด / ๐))) โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ})) โ ๐ โ โ) |
68 | 12 | nncnd 12176 |
. . . . 5
โข ((๐ โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ๐ โ โ) |
69 | 68 | adantrr 716 |
. . . 4
โข ((๐ โง (๐ โ (1...(โโ(๐ด / ๐))) โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ})) โ ๐ โ โ) |
70 | 3 | nnne0d 12210 |
. . . . 5
โข (๐ โ ๐ โ 0) |
71 | 70 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ (1...(โโ(๐ด / ๐))) โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ})) โ ๐ โ 0) |
72 | 65, 67, 69, 71 | divmuld 11960 |
. . 3
โข ((๐ โง (๐ โ (1...(โโ(๐ด / ๐))) โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ})) โ ((๐ / ๐) = ๐ โ (๐ ยท ๐) = ๐)) |
73 | | eqcom 2744 |
. . 3
โข (๐ = (๐ / ๐) โ (๐ / ๐) = ๐) |
74 | | eqcom 2744 |
. . 3
โข (๐ = (๐ ยท ๐) โ (๐ ยท ๐) = ๐) |
75 | 72, 73, 74 | 3bitr4g 314 |
. 2
โข ((๐ โง (๐ โ (1...(โโ(๐ด / ๐))) โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ})) โ (๐ = (๐ / ๐) โ ๐ = (๐ ยท ๐))) |
76 | 1, 36, 63, 75 | f1o2d 7612 |
1
โข (๐ โ ๐น:(1...(โโ(๐ด / ๐)))โ1-1-ontoโ{๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) |