Step | Hyp | Ref
| Expression |
1 | | 1zzd 12541 |
. . . . . 6
โข (๐ โ 1 โ
โค) |
2 | | hashdvds.3 |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ (โคโฅโ(๐ด โ 1))) |
3 | | eluzelz 12780 |
. . . . . . . . . . . 12
โข (๐ต โ
(โคโฅโ(๐ด โ 1)) โ ๐ต โ โค) |
4 | 2, 3 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โค) |
5 | | hashdvds.4 |
. . . . . . . . . . 11
โข (๐ โ ๐ถ โ โค) |
6 | 4, 5 | zsubcld 12619 |
. . . . . . . . . 10
โข (๐ โ (๐ต โ ๐ถ) โ โค) |
7 | 6 | zred 12614 |
. . . . . . . . 9
โข (๐ โ (๐ต โ ๐ถ) โ โ) |
8 | | hashdvds.1 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
9 | 7, 8 | nndivred 12214 |
. . . . . . . 8
โข (๐ โ ((๐ต โ ๐ถ) / ๐) โ โ) |
10 | 9 | flcld 13710 |
. . . . . . 7
โข (๐ โ (โโ((๐ต โ ๐ถ) / ๐)) โ โค) |
11 | | hashdvds.2 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โค) |
12 | | peano2zm 12553 |
. . . . . . . . . . . 12
โข (๐ด โ โค โ (๐ด โ 1) โ
โค) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (๐ด โ 1) โ โค) |
14 | 13, 5 | zsubcld 12619 |
. . . . . . . . . 10
โข (๐ โ ((๐ด โ 1) โ ๐ถ) โ โค) |
15 | 14 | zred 12614 |
. . . . . . . . 9
โข (๐ โ ((๐ด โ 1) โ ๐ถ) โ โ) |
16 | 15, 8 | nndivred 12214 |
. . . . . . . 8
โข (๐ โ (((๐ด โ 1) โ ๐ถ) / ๐) โ โ) |
17 | 16 | flcld 13710 |
. . . . . . 7
โข (๐ โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)) โ โค) |
18 | 10, 17 | zsubcld 12619 |
. . . . . 6
โข (๐ โ ((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))) โ โค) |
19 | | fzen 13465 |
. . . . . 6
โข ((1
โ โค โง ((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))) โ โค โง
(โโ(((๐ด โ
1) โ ๐ถ) / ๐)) โ โค) โ
(1...((โโ((๐ต
โ ๐ถ) / ๐)) โ
(โโ(((๐ด โ
1) โ ๐ถ) / ๐)))) โ ((1 +
(โโ(((๐ด โ
1) โ ๐ถ) / ๐)))...(((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))) + (โโ(((๐ด โ 1) โ ๐ถ) / ๐))))) |
20 | 1, 18, 17, 19 | syl3anc 1372 |
. . . . 5
โข (๐ โ
(1...((โโ((๐ต
โ ๐ถ) / ๐)) โ
(โโ(((๐ด โ
1) โ ๐ถ) / ๐)))) โ ((1 +
(โโ(((๐ด โ
1) โ ๐ถ) / ๐)))...(((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))) + (โโ(((๐ด โ 1) โ ๐ถ) / ๐))))) |
21 | | ax-1cn 11116 |
. . . . . . 7
โข 1 โ
โ |
22 | 17 | zcnd 12615 |
. . . . . . 7
โข (๐ โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)) โ โ) |
23 | | addcom 11348 |
. . . . . . 7
โข ((1
โ โ โง (โโ(((๐ด โ 1) โ ๐ถ) / ๐)) โ โ) โ (1 +
(โโ(((๐ด โ
1) โ ๐ถ) / ๐))) = ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)) |
24 | 21, 22, 23 | sylancr 588 |
. . . . . 6
โข (๐ โ (1 +
(โโ(((๐ด โ
1) โ ๐ถ) / ๐))) = ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)) |
25 | 10 | zcnd 12615 |
. . . . . . 7
โข (๐ โ (โโ((๐ต โ ๐ถ) / ๐)) โ โ) |
26 | 25, 22 | npcand 11523 |
. . . . . 6
โข (๐ โ (((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))) + (โโ(((๐ด โ 1) โ ๐ถ) / ๐))) = (โโ((๐ต โ ๐ถ) / ๐))) |
27 | 24, 26 | oveq12d 7380 |
. . . . 5
โข (๐ โ ((1 +
(โโ(((๐ด โ
1) โ ๐ถ) / ๐)))...(((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))) + (โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) = (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) |
28 | 20, 27 | breqtrd 5136 |
. . . 4
โข (๐ โ
(1...((โโ((๐ต
โ ๐ถ) / ๐)) โ
(โโ(((๐ด โ
1) โ ๐ถ) / ๐)))) โ
(((โโ(((๐ด
โ 1) โ ๐ถ) /
๐)) +
1)...(โโ((๐ต
โ ๐ถ) / ๐)))) |
29 | | ovexd 7397 |
. . . . 5
โข (๐ โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โ V) |
30 | | fzfi 13884 |
. . . . . 6
โข (๐ด...๐ต) โ Fin |
31 | | rabexg 5293 |
. . . . . 6
โข ((๐ด...๐ต) โ Fin โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)} โ V) |
32 | 30, 31 | mp1i 13 |
. . . . 5
โข (๐ โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)} โ V) |
33 | | oveq1 7369 |
. . . . . . . 8
โข (๐ฅ = ((๐ง ยท ๐) + ๐ถ) โ (๐ฅ โ ๐ถ) = (((๐ง ยท ๐) + ๐ถ) โ ๐ถ)) |
34 | 33 | breq2d 5122 |
. . . . . . 7
โข (๐ฅ = ((๐ง ยท ๐) + ๐ถ) โ (๐ โฅ (๐ฅ โ ๐ถ) โ ๐ โฅ (((๐ง ยท ๐) + ๐ถ) โ ๐ถ))) |
35 | 11 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ด โ โค) |
36 | 4 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ต โ โค) |
37 | | elfzelz 13448 |
. . . . . . . . . . 11
โข (๐ง โ
(((โโ(((๐ด
โ 1) โ ๐ถ) /
๐)) +
1)...(โโ((๐ต
โ ๐ถ) / ๐))) โ ๐ง โ โค) |
38 | 37 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ง โ โค) |
39 | 8 | nnzd 12533 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โค) |
40 | 39 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ โ โค) |
41 | 38, 40 | zmulcld 12620 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (๐ง ยท ๐) โ โค) |
42 | 5 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ถ โ โค) |
43 | 41, 42 | zaddcld 12618 |
. . . . . . . 8
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((๐ง ยท ๐) + ๐ถ) โ โค) |
44 | | elfzle1 13451 |
. . . . . . . . . . . . . 14
โข (๐ง โ
(((โโ(((๐ด
โ 1) โ ๐ถ) /
๐)) +
1)...(โโ((๐ต
โ ๐ถ) / ๐))) โ
((โโ(((๐ด
โ 1) โ ๐ถ) /
๐)) + 1) โค ๐ง) |
45 | 44 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1) โค ๐ง) |
46 | | zltp1le 12560 |
. . . . . . . . . . . . . 14
โข
(((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) โ โค โง ๐ง โ โค) โ
((โโ(((๐ด
โ 1) โ ๐ถ) /
๐)) < ๐ง โ ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1) โค ๐ง)) |
47 | 17, 37, 46 | syl2an 597 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) < ๐ง โ ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1) โค ๐ง)) |
48 | 45, 47 | mpbird 257 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)) < ๐ง) |
49 | | fllt 13718 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ 1)
โ ๐ถ) / ๐) โ โ โง ๐ง โ โค) โ
((((๐ด โ 1) โ
๐ถ) / ๐) < ๐ง โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)) < ๐ง)) |
50 | 16, 37, 49 | syl2an 597 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((((๐ด โ 1) โ ๐ถ) / ๐) < ๐ง โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)) < ๐ง)) |
51 | 48, 50 | mpbird 257 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (((๐ด โ 1) โ ๐ถ) / ๐) < ๐ง) |
52 | 15 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((๐ด โ 1) โ ๐ถ) โ โ) |
53 | 38 | zred 12614 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ง โ โ) |
54 | 8 | nnred 12175 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โ) |
55 | 8 | nngt0d 12209 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < ๐) |
56 | 54, 55 | jca 513 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ โ โง 0 < ๐)) |
57 | 56 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (๐ โ โ โง 0 < ๐)) |
58 | | ltdivmul2 12039 |
. . . . . . . . . . . 12
โข ((((๐ด โ 1) โ ๐ถ) โ โ โง ๐ง โ โ โง (๐ โ โ โง 0 <
๐)) โ ((((๐ด โ 1) โ ๐ถ) / ๐) < ๐ง โ ((๐ด โ 1) โ ๐ถ) < (๐ง ยท ๐))) |
59 | 52, 53, 57, 58 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((((๐ด โ 1) โ ๐ถ) / ๐) < ๐ง โ ((๐ด โ 1) โ ๐ถ) < (๐ง ยท ๐))) |
60 | 51, 59 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((๐ด โ 1) โ ๐ถ) < (๐ง ยท ๐)) |
61 | 13 | zred 12614 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด โ 1) โ โ) |
62 | 61 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (๐ด โ 1) โ โ) |
63 | 5 | zred 12614 |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ โ โ) |
64 | 63 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ถ โ โ) |
65 | 41 | zred 12614 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (๐ง ยท ๐) โ โ) |
66 | 62, 64, 65 | ltsubaddd 11758 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (((๐ด โ 1) โ ๐ถ) < (๐ง ยท ๐) โ (๐ด โ 1) < ((๐ง ยท ๐) + ๐ถ))) |
67 | 60, 66 | mpbid 231 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (๐ด โ 1) < ((๐ง ยท ๐) + ๐ถ)) |
68 | | zlem1lt 12562 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ((๐ง ยท ๐) + ๐ถ) โ โค) โ (๐ด โค ((๐ง ยท ๐) + ๐ถ) โ (๐ด โ 1) < ((๐ง ยท ๐) + ๐ถ))) |
69 | 11, 43, 68 | syl2an2r 684 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (๐ด โค ((๐ง ยท ๐) + ๐ถ) โ (๐ด โ 1) < ((๐ง ยท ๐) + ๐ถ))) |
70 | 67, 69 | mpbird 257 |
. . . . . . . 8
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ด โค ((๐ง ยท ๐) + ๐ถ)) |
71 | | elfzle2 13452 |
. . . . . . . . . . . 12
โข (๐ง โ
(((โโ(((๐ด
โ 1) โ ๐ถ) /
๐)) +
1)...(โโ((๐ต
โ ๐ถ) / ๐))) โ ๐ง โค (โโ((๐ต โ ๐ถ) / ๐))) |
72 | 71 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ง โค (โโ((๐ต โ ๐ถ) / ๐))) |
73 | | flge 13717 |
. . . . . . . . . . . 12
โข ((((๐ต โ ๐ถ) / ๐) โ โ โง ๐ง โ โค) โ (๐ง โค ((๐ต โ ๐ถ) / ๐) โ ๐ง โค (โโ((๐ต โ ๐ถ) / ๐)))) |
74 | 9, 37, 73 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (๐ง โค ((๐ต โ ๐ถ) / ๐) โ ๐ง โค (โโ((๐ต โ ๐ถ) / ๐)))) |
75 | 72, 74 | mpbird 257 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ง โค ((๐ต โ ๐ถ) / ๐)) |
76 | 7 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (๐ต โ ๐ถ) โ โ) |
77 | | lemuldiv 12042 |
. . . . . . . . . . 11
โข ((๐ง โ โ โง (๐ต โ ๐ถ) โ โ โง (๐ โ โ โง 0 < ๐)) โ ((๐ง ยท ๐) โค (๐ต โ ๐ถ) โ ๐ง โค ((๐ต โ ๐ถ) / ๐))) |
78 | 53, 76, 57, 77 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((๐ง ยท ๐) โค (๐ต โ ๐ถ) โ ๐ง โค ((๐ต โ ๐ถ) / ๐))) |
79 | 75, 78 | mpbird 257 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (๐ง ยท ๐) โค (๐ต โ ๐ถ)) |
80 | 4 | zred 12614 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โ) |
81 | 80 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ต โ โ) |
82 | | leaddsub 11638 |
. . . . . . . . . 10
โข (((๐ง ยท ๐) โ โ โง ๐ถ โ โ โง ๐ต โ โ) โ (((๐ง ยท ๐) + ๐ถ) โค ๐ต โ (๐ง ยท ๐) โค (๐ต โ ๐ถ))) |
83 | 65, 64, 81, 82 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (((๐ง ยท ๐) + ๐ถ) โค ๐ต โ (๐ง ยท ๐) โค (๐ต โ ๐ถ))) |
84 | 79, 83 | mpbird 257 |
. . . . . . . 8
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((๐ง ยท ๐) + ๐ถ) โค ๐ต) |
85 | 35, 36, 43, 70, 84 | elfzd 13439 |
. . . . . . 7
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((๐ง ยท ๐) + ๐ถ) โ (๐ด...๐ต)) |
86 | | dvdsmul2 16168 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โค) โ ๐ โฅ (๐ง ยท ๐)) |
87 | 38, 40, 86 | syl2anc 585 |
. . . . . . . 8
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ โฅ (๐ง ยท ๐)) |
88 | 41 | zcnd 12615 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (๐ง ยท ๐) โ โ) |
89 | 5 | zcnd 12615 |
. . . . . . . . . 10
โข (๐ โ ๐ถ โ โ) |
90 | 89 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ถ โ โ) |
91 | 88, 90 | pncand 11520 |
. . . . . . . 8
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ (((๐ง ยท ๐) + ๐ถ) โ ๐ถ) = (๐ง ยท ๐)) |
92 | 87, 91 | breqtrrd 5138 |
. . . . . . 7
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ โฅ (((๐ง ยท ๐) + ๐ถ) โ ๐ถ)) |
93 | 34, 85, 92 | elrabd 3652 |
. . . . . 6
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ((๐ง ยท ๐) + ๐ถ) โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) |
94 | 93 | ex 414 |
. . . . 5
โข (๐ โ (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โ ((๐ง ยท ๐) + ๐ถ) โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)})) |
95 | | oveq1 7369 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ (๐ฅ โ ๐ถ) = (๐ฆ โ ๐ถ)) |
96 | 95 | breq2d 5122 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (๐ โฅ (๐ฅ โ ๐ถ) โ ๐ โฅ (๐ฆ โ ๐ถ))) |
97 | 96 | elrab 3650 |
. . . . . 6
โข (๐ฆ โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)} โ (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) |
98 | 17 | peano2zd 12617 |
. . . . . . . . 9
โข (๐ โ ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1) โ โค) |
99 | 98 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1) โ โค) |
100 | 10 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (โโ((๐ต โ ๐ถ) / ๐)) โ โค) |
101 | | simprr 772 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ โฅ (๐ฆ โ ๐ถ)) |
102 | 39 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ โ โค) |
103 | 8 | nnne0d 12210 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ 0) |
104 | 103 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ โ 0) |
105 | | elfzelz 13448 |
. . . . . . . . . . . 12
โข (๐ฆ โ (๐ด...๐ต) โ ๐ฆ โ โค) |
106 | 105 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ฆ โ โค) |
107 | 5 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ถ โ โค) |
108 | 106, 107 | zsubcld 12619 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (๐ฆ โ ๐ถ) โ โค) |
109 | | dvdsval2 16146 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ 0 โง (๐ฆ โ ๐ถ) โ โค) โ (๐ โฅ (๐ฆ โ ๐ถ) โ ((๐ฆ โ ๐ถ) / ๐) โ โค)) |
110 | 102, 104,
108, 109 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (๐ โฅ (๐ฆ โ ๐ถ) โ ((๐ฆ โ ๐ถ) / ๐) โ โค)) |
111 | 101, 110 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((๐ฆ โ ๐ถ) / ๐) โ โค) |
112 | 61 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (๐ด โ 1) โ โ) |
113 | 106 | zred 12614 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ฆ โ โ) |
114 | 63 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ถ โ โ) |
115 | | elfzle1 13451 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ (๐ด...๐ต) โ ๐ด โค ๐ฆ) |
116 | 115 | ad2antrl 727 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ด โค ๐ฆ) |
117 | | zlem1lt 12562 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โค โง ๐ฆ โ โค) โ (๐ด โค ๐ฆ โ (๐ด โ 1) < ๐ฆ)) |
118 | 11, 106, 117 | syl2an2r 684 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (๐ด โค ๐ฆ โ (๐ด โ 1) < ๐ฆ)) |
119 | 116, 118 | mpbid 231 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (๐ด โ 1) < ๐ฆ) |
120 | 112, 113,
114, 119 | ltsub1dd 11774 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((๐ด โ 1) โ ๐ถ) < (๐ฆ โ ๐ถ)) |
121 | 15 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((๐ด โ 1) โ ๐ถ) โ โ) |
122 | 108 | zred 12614 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (๐ฆ โ ๐ถ) โ โ) |
123 | 56 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (๐ โ โ โง 0 < ๐)) |
124 | | ltdiv1 12026 |
. . . . . . . . . . . 12
โข ((((๐ด โ 1) โ ๐ถ) โ โ โง (๐ฆ โ ๐ถ) โ โ โง (๐ โ โ โง 0 < ๐)) โ (((๐ด โ 1) โ ๐ถ) < (๐ฆ โ ๐ถ) โ (((๐ด โ 1) โ ๐ถ) / ๐) < ((๐ฆ โ ๐ถ) / ๐))) |
125 | 121, 122,
123, 124 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (((๐ด โ 1) โ ๐ถ) < (๐ฆ โ ๐ถ) โ (((๐ด โ 1) โ ๐ถ) / ๐) < ((๐ฆ โ ๐ถ) / ๐))) |
126 | 120, 125 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (((๐ด โ 1) โ ๐ถ) / ๐) < ((๐ฆ โ ๐ถ) / ๐)) |
127 | | fllt 13718 |
. . . . . . . . . . 11
โข
(((((๐ด โ 1)
โ ๐ถ) / ๐) โ โ โง ((๐ฆ โ ๐ถ) / ๐) โ โค) โ ((((๐ด โ 1) โ ๐ถ) / ๐) < ((๐ฆ โ ๐ถ) / ๐) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)) < ((๐ฆ โ ๐ถ) / ๐))) |
128 | 16, 111, 127 | syl2an2r 684 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((((๐ด โ 1) โ ๐ถ) / ๐) < ((๐ฆ โ ๐ถ) / ๐) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)) < ((๐ฆ โ ๐ถ) / ๐))) |
129 | 126, 128 | mpbid 231 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)) < ((๐ฆ โ ๐ถ) / ๐)) |
130 | | zltp1le 12560 |
. . . . . . . . . 10
โข
(((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) โ โค โง ((๐ฆ โ ๐ถ) / ๐) โ โค) โ
((โโ(((๐ด
โ 1) โ ๐ถ) /
๐)) < ((๐ฆ โ ๐ถ) / ๐) โ ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1) โค ((๐ฆ โ ๐ถ) / ๐))) |
131 | 17, 111, 130 | syl2an2r 684 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) < ((๐ฆ โ ๐ถ) / ๐) โ ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1) โค ((๐ฆ โ ๐ถ) / ๐))) |
132 | 129, 131 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1) โค ((๐ฆ โ ๐ถ) / ๐)) |
133 | 80 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ต โ โ) |
134 | | elfzle2 13452 |
. . . . . . . . . . . 12
โข (๐ฆ โ (๐ด...๐ต) โ ๐ฆ โค ๐ต) |
135 | 134 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ฆ โค ๐ต) |
136 | 113, 133,
114, 135 | lesub1dd 11778 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (๐ฆ โ ๐ถ) โค (๐ต โ ๐ถ)) |
137 | 7 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (๐ต โ ๐ถ) โ โ) |
138 | | lediv1 12027 |
. . . . . . . . . . 11
โข (((๐ฆ โ ๐ถ) โ โ โง (๐ต โ ๐ถ) โ โ โง (๐ โ โ โง 0 < ๐)) โ ((๐ฆ โ ๐ถ) โค (๐ต โ ๐ถ) โ ((๐ฆ โ ๐ถ) / ๐) โค ((๐ต โ ๐ถ) / ๐))) |
139 | 122, 137,
123, 138 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((๐ฆ โ ๐ถ) โค (๐ต โ ๐ถ) โ ((๐ฆ โ ๐ถ) / ๐) โค ((๐ต โ ๐ถ) / ๐))) |
140 | 136, 139 | mpbid 231 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((๐ฆ โ ๐ถ) / ๐) โค ((๐ต โ ๐ถ) / ๐)) |
141 | | flge 13717 |
. . . . . . . . . 10
โข ((((๐ต โ ๐ถ) / ๐) โ โ โง ((๐ฆ โ ๐ถ) / ๐) โ โค) โ (((๐ฆ โ ๐ถ) / ๐) โค ((๐ต โ ๐ถ) / ๐) โ ((๐ฆ โ ๐ถ) / ๐) โค (โโ((๐ต โ ๐ถ) / ๐)))) |
142 | 9, 111, 141 | syl2an2r 684 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (((๐ฆ โ ๐ถ) / ๐) โค ((๐ต โ ๐ถ) / ๐) โ ((๐ฆ โ ๐ถ) / ๐) โค (โโ((๐ต โ ๐ถ) / ๐)))) |
143 | 140, 142 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((๐ฆ โ ๐ถ) / ๐) โค (โโ((๐ต โ ๐ถ) / ๐))) |
144 | 99, 100, 111, 132, 143 | elfzd 13439 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ((๐ฆ โ ๐ถ) / ๐) โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) |
145 | 144 | ex 414 |
. . . . . 6
โข (๐ โ ((๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)) โ ((๐ฆ โ ๐ถ) / ๐) โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))))) |
146 | 97, 145 | biimtrid 241 |
. . . . 5
โข (๐ โ (๐ฆ โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)} โ ((๐ฆ โ ๐ถ) / ๐) โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))))) |
147 | 97 | anbi2i 624 |
. . . . . . 7
โข ((๐ง โ
(((โโ(((๐ด
โ 1) โ ๐ถ) /
๐)) +
1)...(โโ((๐ต
โ ๐ถ) / ๐))) โง ๐ฆ โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) โ (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) |
148 | 108 | zcnd 12615 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ (๐ฆ โ ๐ถ) โ โ) |
149 | 148 | adantrl 715 |
. . . . . . . . . 10
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ (๐ฆ โ ๐ถ) โ โ) |
150 | 38 | zcnd 12615 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐)))) โ ๐ง โ โ) |
151 | 150 | adantrr 716 |
. . . . . . . . . 10
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ ๐ง โ โ) |
152 | 8 | nncnd 12176 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
153 | 152 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ ๐ โ โ) |
154 | 103 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ ๐ โ 0) |
155 | 149, 151,
153, 154 | divmul3d 11972 |
. . . . . . . . 9
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ (((๐ฆ โ ๐ถ) / ๐) = ๐ง โ (๐ฆ โ ๐ถ) = (๐ง ยท ๐))) |
156 | 106 | zcnd 12615 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ))) โ ๐ฆ โ โ) |
157 | 156 | adantrl 715 |
. . . . . . . . . 10
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ ๐ฆ โ โ) |
158 | 89 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ ๐ถ โ โ) |
159 | 88 | adantrr 716 |
. . . . . . . . . 10
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ (๐ง ยท ๐) โ โ) |
160 | 157, 158,
159 | subadd2d 11538 |
. . . . . . . . 9
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ ((๐ฆ โ ๐ถ) = (๐ง ยท ๐) โ ((๐ง ยท ๐) + ๐ถ) = ๐ฆ)) |
161 | 155, 160 | bitrd 279 |
. . . . . . . 8
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ (((๐ฆ โ ๐ถ) / ๐) = ๐ง โ ((๐ง ยท ๐) + ๐ถ) = ๐ฆ)) |
162 | | eqcom 2744 |
. . . . . . . 8
โข (๐ง = ((๐ฆ โ ๐ถ) / ๐) โ ((๐ฆ โ ๐ถ) / ๐) = ๐ง) |
163 | | eqcom 2744 |
. . . . . . . 8
โข (๐ฆ = ((๐ง ยท ๐) + ๐ถ) โ ((๐ง ยท ๐) + ๐ถ) = ๐ฆ) |
164 | 161, 162,
163 | 3bitr4g 314 |
. . . . . . 7
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (๐ฆ โ (๐ด...๐ต) โง ๐ โฅ (๐ฆ โ ๐ถ)))) โ (๐ง = ((๐ฆ โ ๐ถ) / ๐) โ ๐ฆ = ((๐ง ยท ๐) + ๐ถ))) |
165 | 147, 164 | sylan2b 595 |
. . . . . 6
โข ((๐ โง (๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง ๐ฆ โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)})) โ (๐ง = ((๐ฆ โ ๐ถ) / ๐) โ ๐ฆ = ((๐ง ยท ๐) + ๐ถ))) |
166 | 165 | ex 414 |
. . . . 5
โข (๐ โ ((๐ง โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง ๐ฆ โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) โ (๐ง = ((๐ฆ โ ๐ถ) / ๐) โ ๐ฆ = ((๐ง ยท ๐) + ๐ถ)))) |
167 | 29, 32, 94, 146, 166 | en3d 8936 |
. . . 4
โข (๐ โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) |
168 | | entr 8953 |
. . . 4
โข
(((1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) โ (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โง (((โโ(((๐ด โ 1) โ ๐ถ) / ๐)) + 1)...(โโ((๐ต โ ๐ถ) / ๐))) โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) โ (1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) |
169 | 28, 167, 168 | syl2anc 585 |
. . 3
โข (๐ โ
(1...((โโ((๐ต
โ ๐ถ) / ๐)) โ
(โโ(((๐ด โ
1) โ ๐ถ) / ๐)))) โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) |
170 | | fzfi 13884 |
. . . 4
โข
(1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) โ Fin |
171 | | ssrab2 4042 |
. . . . 5
โข {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)} โ (๐ด...๐ต) |
172 | | ssfi 9124 |
. . . . 5
โข (((๐ด...๐ต) โ Fin โง {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)} โ (๐ด...๐ต)) โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)} โ Fin) |
173 | 30, 171, 172 | mp2an 691 |
. . . 4
โข {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)} โ Fin |
174 | | hashen 14254 |
. . . 4
โข
(((1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) โ Fin โง {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)} โ Fin) โ
((โฏโ(1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))))) = (โฏโ{๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) โ (1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)})) |
175 | 170, 173,
174 | mp2an 691 |
. . 3
โข
((โฏโ(1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))))) = (โฏโ{๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) โ (1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) โ {๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) |
176 | 169, 175 | sylibr 233 |
. 2
โข (๐ โ
(โฏโ(1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))))) = (โฏโ{๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)})) |
177 | | eluzle 12783 |
. . . . . . 7
โข (๐ต โ
(โคโฅโ(๐ด โ 1)) โ (๐ด โ 1) โค ๐ต) |
178 | 2, 177 | syl 17 |
. . . . . 6
โข (๐ โ (๐ด โ 1) โค ๐ต) |
179 | | zre 12510 |
. . . . . . . 8
โข ((๐ด โ 1) โ โค
โ (๐ด โ 1) โ
โ) |
180 | | zre 12510 |
. . . . . . . 8
โข (๐ต โ โค โ ๐ต โ
โ) |
181 | | zre 12510 |
. . . . . . . 8
โข (๐ถ โ โค โ ๐ถ โ
โ) |
182 | | lesub1 11656 |
. . . . . . . 8
โข (((๐ด โ 1) โ โ โง
๐ต โ โ โง
๐ถ โ โ) โ
((๐ด โ 1) โค ๐ต โ ((๐ด โ 1) โ ๐ถ) โค (๐ต โ ๐ถ))) |
183 | 179, 180,
181, 182 | syl3an 1161 |
. . . . . . 7
โข (((๐ด โ 1) โ โค โง
๐ต โ โค โง
๐ถ โ โค) โ
((๐ด โ 1) โค ๐ต โ ((๐ด โ 1) โ ๐ถ) โค (๐ต โ ๐ถ))) |
184 | 13, 4, 5, 183 | syl3anc 1372 |
. . . . . 6
โข (๐ โ ((๐ด โ 1) โค ๐ต โ ((๐ด โ 1) โ ๐ถ) โค (๐ต โ ๐ถ))) |
185 | 178, 184 | mpbid 231 |
. . . . 5
โข (๐ โ ((๐ด โ 1) โ ๐ถ) โค (๐ต โ ๐ถ)) |
186 | | lediv1 12027 |
. . . . . 6
โข ((((๐ด โ 1) โ ๐ถ) โ โ โง (๐ต โ ๐ถ) โ โ โง (๐ โ โ โง 0 < ๐)) โ (((๐ด โ 1) โ ๐ถ) โค (๐ต โ ๐ถ) โ (((๐ด โ 1) โ ๐ถ) / ๐) โค ((๐ต โ ๐ถ) / ๐))) |
187 | 15, 7, 56, 186 | syl3anc 1372 |
. . . . 5
โข (๐ โ (((๐ด โ 1) โ ๐ถ) โค (๐ต โ ๐ถ) โ (((๐ด โ 1) โ ๐ถ) / ๐) โค ((๐ต โ ๐ถ) / ๐))) |
188 | 185, 187 | mpbid 231 |
. . . 4
โข (๐ โ (((๐ด โ 1) โ ๐ถ) / ๐) โค ((๐ต โ ๐ถ) / ๐)) |
189 | | flword2 13725 |
. . . 4
โข
(((((๐ด โ 1)
โ ๐ถ) / ๐) โ โ โง ((๐ต โ ๐ถ) / ๐) โ โ โง (((๐ด โ 1) โ ๐ถ) / ๐) โค ((๐ต โ ๐ถ) / ๐)) โ (โโ((๐ต โ ๐ถ) / ๐)) โ
(โคโฅโ(โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) |
190 | 16, 9, 188, 189 | syl3anc 1372 |
. . 3
โข (๐ โ (โโ((๐ต โ ๐ถ) / ๐)) โ
(โคโฅโ(โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) |
191 | | uznn0sub 12809 |
. . 3
โข
((โโ((๐ต
โ ๐ถ) / ๐)) โ
(โคโฅโ(โโ(((๐ด โ 1) โ ๐ถ) / ๐))) โ ((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))) โ
โ0) |
192 | | hashfz1 14253 |
. . 3
โข
(((โโ((๐ต
โ ๐ถ) / ๐)) โ
(โโ(((๐ด โ
1) โ ๐ถ) / ๐))) โ โ0
โ (โฏโ(1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))))) = ((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) |
193 | 190, 191,
192 | 3syl 18 |
. 2
โข (๐ โ
(โฏโ(1...((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐))))) = ((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) |
194 | 176, 193 | eqtr3d 2779 |
1
โข (๐ โ (โฏโ{๐ฅ โ (๐ด...๐ต) โฃ ๐ โฅ (๐ฅ โ ๐ถ)}) = ((โโ((๐ต โ ๐ถ) / ๐)) โ (โโ(((๐ด โ 1) โ ๐ถ) / ๐)))) |