Step | Hyp | Ref
| Expression |
1 | | breq2 5151 |
. . . 4
โข (๐ฅ = ๐ด โ (๐ < ๐ฅ โ ๐ < ๐ด)) |
2 | | breq2 5151 |
. . . . . . 7
โข (๐ฅ = ๐ด โ ((๐โ๐) โฅ ๐ฅ โ (๐โ๐) โฅ ๐ด)) |
3 | 2 | bibi2d 342 |
. . . . . 6
โข (๐ฅ = ๐ด โ (((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ด))) |
4 | 3 | notbid 317 |
. . . . 5
โข (๐ฅ = ๐ด โ (ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ด))) |
5 | 4 | 2rexbidv 3219 |
. . . 4
โข (๐ฅ = ๐ด โ (โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ด))) |
6 | 1, 5 | imbi12d 344 |
. . 3
โข (๐ฅ = ๐ด โ ((๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ)) โ (๐ < ๐ด โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ด)))) |
7 | 6 | ralbidv 3177 |
. 2
โข (๐ฅ = ๐ด โ (โ๐ โ โ (๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ)) โ โ๐ โ โ (๐ < ๐ด โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ด)))) |
8 | | breq2 5151 |
. . . . 5
โข (๐ฅ = 1 โ (๐ < ๐ฅ โ ๐ < 1)) |
9 | | breq2 5151 |
. . . . . . . 8
โข (๐ฅ = 1 โ ((๐โ๐) โฅ ๐ฅ โ (๐โ๐) โฅ 1)) |
10 | 9 | bibi2d 342 |
. . . . . . 7
โข (๐ฅ = 1 โ (((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ 1))) |
11 | 10 | notbid 317 |
. . . . . 6
โข (๐ฅ = 1 โ (ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ 1))) |
12 | 11 | 2rexbidv 3219 |
. . . . 5
โข (๐ฅ = 1 โ (โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ 1))) |
13 | 8, 12 | imbi12d 344 |
. . . 4
โข (๐ฅ = 1 โ ((๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ)) โ (๐ < 1 โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ 1)))) |
14 | 13 | ralbidv 3177 |
. . 3
โข (๐ฅ = 1 โ (โ๐ โ โ (๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ)) โ โ๐ โ โ (๐ < 1 โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ 1)))) |
15 | | breq2 5151 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ < ๐ฅ โ ๐ < ๐ฆ)) |
16 | | breq2 5151 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ ((๐โ๐) โฅ ๐ฅ โ (๐โ๐) โฅ ๐ฆ)) |
17 | 16 | bibi2d 342 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) |
18 | 17 | notbid 317 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) |
19 | 18 | 2rexbidv 3219 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) |
20 | 15, 19 | imbi12d 344 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ)) โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ)))) |
21 | 20 | ralbidv 3177 |
. . 3
โข (๐ฅ = ๐ฆ โ (โ๐ โ โ (๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ)) โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ)))) |
22 | | nnnlt1 12240 |
. . . . 5
โข (๐ โ โ โ ยฌ
๐ < 1) |
23 | 22 | pm2.21d 121 |
. . . 4
โข (๐ โ โ โ (๐ < 1 โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ 1))) |
24 | 23 | rgen 3063 |
. . 3
โข
โ๐ โ
โ (๐ < 1 โ
โ๐ โ โ
โ๐ โ โ
ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ 1)) |
25 | | exprmfct 16637 |
. . . 4
โข (๐ฅ โ
(โคโฅโ2) โ โ๐ โ โ ๐ โฅ ๐ฅ) |
26 | | prmz 16608 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โค) |
27 | 26 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ก โ โ) โ ๐ โ
โค) |
28 | | prmnn 16607 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โ) |
29 | 28 | nnne0d 12258 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ 0) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ก โ โ) โ ๐ โ 0) |
31 | | nnz 12575 |
. . . . . . . . . . . . . . . 16
โข (๐ก โ โ โ ๐ก โ
โค) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ก โ โ) โ ๐ก โ
โค) |
33 | | dvdsval2 16196 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ 0 โง ๐ก โ โค) โ (๐ โฅ ๐ก โ (๐ก / ๐) โ โค)) |
34 | 27, 30, 32, 33 | syl3anc 1371 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ก โ โ) โ (๐ โฅ ๐ก โ (๐ก / ๐) โ โค)) |
35 | 34 | biimpd 228 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ก โ โ) โ (๐ โฅ ๐ก โ (๐ก / ๐) โ โค)) |
36 | 35 | 3ad2antl2 1186 |
. . . . . . . . . . . 12
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง ๐ก โ โ) โ (๐ โฅ ๐ก โ (๐ก / ๐) โ โค)) |
37 | 36 | adantrl 714 |
. . . . . . . . . . 11
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โง ๐ก โ โ)) โ (๐ โฅ ๐ก โ (๐ก / ๐) โ โค)) |
38 | | simprr 771 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (๐ก โ โ โง (๐ก / ๐) โ โค)) โ (๐ก / ๐) โ โค) |
39 | | nnre 12215 |
. . . . . . . . . . . . . . . . . 18
โข (๐ก โ โ โ ๐ก โ
โ) |
40 | | nngt0 12239 |
. . . . . . . . . . . . . . . . . 18
โข (๐ก โ โ โ 0 <
๐ก) |
41 | 39, 40 | jca 512 |
. . . . . . . . . . . . . . . . 17
โข (๐ก โ โ โ (๐ก โ โ โง 0 <
๐ก)) |
42 | | nnre 12215 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ๐ โ
โ) |
43 | | nngt0 12239 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ 0 <
๐) |
44 | 42, 43 | jca 512 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ (๐ โ โ โง 0 <
๐)) |
45 | 28, 44 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐ โ โ โง 0 <
๐)) |
46 | | divgt0 12078 |
. . . . . . . . . . . . . . . . 17
โข (((๐ก โ โ โง 0 <
๐ก) โง (๐ โ โ โง 0 <
๐)) โ 0 < (๐ก / ๐)) |
47 | 41, 45, 46 | syl2anr 597 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ก โ โ) โ 0 <
(๐ก / ๐)) |
48 | 47 | 3ad2antl2 1186 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง ๐ก โ โ) โ 0 < (๐ก / ๐)) |
49 | 48 | adantrr 715 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (๐ก โ โ โง (๐ก / ๐) โ โค)) โ 0 < (๐ก / ๐)) |
50 | | elnnz 12564 |
. . . . . . . . . . . . . 14
โข ((๐ก / ๐) โ โ โ ((๐ก / ๐) โ โค โง 0 < (๐ก / ๐))) |
51 | 38, 49, 50 | sylanbrc 583 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (๐ก โ โ โง (๐ก / ๐) โ โค)) โ (๐ก / ๐) โ โ) |
52 | 51 | expr 457 |
. . . . . . . . . . . 12
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง ๐ก โ โ) โ ((๐ก / ๐) โ โค โ (๐ก / ๐) โ โ)) |
53 | 52 | adantrl 714 |
. . . . . . . . . . 11
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โง ๐ก โ โ)) โ ((๐ก / ๐) โ โค โ (๐ก / ๐) โ โ)) |
54 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ฅ โ
(โคโฅโ2)) โ ๐ โ โค) |
55 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ฅ โ
(โคโฅโ2)) โ ๐ โ 0) |
56 | | eluzelz 12828 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ
(โคโฅโ2) โ ๐ฅ โ โค) |
57 | 56 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ฅ โ
(โคโฅโ2)) โ ๐ฅ โ โค) |
58 | | dvdsval2 16196 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ 0 โง ๐ฅ โ โค) โ (๐ โฅ ๐ฅ โ (๐ฅ / ๐) โ โค)) |
59 | 54, 55, 57, 58 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ฅ โ
(โคโฅโ2)) โ (๐ โฅ ๐ฅ โ (๐ฅ / ๐) โ โค)) |
60 | | eluzelre 12829 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ
(โคโฅโ2) โ ๐ฅ โ โ) |
61 | | 2z 12590 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 2 โ
โค |
62 | 61 | eluz1i 12826 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ โ
(โคโฅโ2) โ (๐ฅ โ โค โง 2 โค ๐ฅ)) |
63 | | 2pos 12311 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 0 <
2 |
64 | | zre 12558 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
65 | | 0re 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข 0 โ
โ |
66 | | 2re 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข 2 โ
โ |
67 | | ltletr 11302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((0
โ โ โง 2 โ โ โง ๐ฅ โ โ) โ ((0 < 2 โง 2
โค ๐ฅ) โ 0 < ๐ฅ)) |
68 | 65, 66, 67 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฅ โ โ โ ((0 <
2 โง 2 โค ๐ฅ) โ 0
< ๐ฅ)) |
69 | 64, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฅ โ โค โ ((0 <
2 โง 2 โค ๐ฅ) โ 0
< ๐ฅ)) |
70 | 63, 69 | mpani 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ โ โค โ (2 โค
๐ฅ โ 0 < ๐ฅ)) |
71 | 70 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฅ โ โค โง 2 โค
๐ฅ) โ 0 < ๐ฅ) |
72 | 62, 71 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ
(โคโฅโ2) โ 0 < ๐ฅ) |
73 | 60, 72 | jca 512 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ
(โคโฅโ2) โ (๐ฅ โ โ โง 0 < ๐ฅ)) |
74 | | divgt0 12078 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฅ โ โ โง 0 <
๐ฅ) โง (๐ โ โ โง 0 <
๐)) โ 0 < (๐ฅ / ๐)) |
75 | 73, 45, 74 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง ๐ฅ โ
(โคโฅโ2)) โ 0 < (๐ฅ / ๐)) |
76 | 75 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ฅ โ
(โคโฅโ2)) โ ((๐ฅ / ๐) โ โค โ 0 < (๐ฅ / ๐))) |
77 | 76 | ancld 551 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ฅ โ
(โคโฅโ2)) โ ((๐ฅ / ๐) โ โค โ ((๐ฅ / ๐) โ โค โง 0 < (๐ฅ / ๐)))) |
78 | | elnnz 12564 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฅ / ๐) โ โ โ ((๐ฅ / ๐) โ โค โง 0 < (๐ฅ / ๐))) |
79 | 77, 78 | syl6ibr 251 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ฅ โ
(โคโฅโ2)) โ ((๐ฅ / ๐) โ โค โ (๐ฅ / ๐) โ โ)) |
80 | 59, 79 | sylbid 239 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ฅ โ
(โคโฅโ2)) โ (๐ โฅ ๐ฅ โ (๐ฅ / ๐) โ โ)) |
81 | 80 | ancoms 459 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โ (๐ โฅ ๐ฅ โ (๐ฅ / ๐) โ โ)) |
82 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ = (๐ฅ / ๐) โ (๐ฆ < ๐ฅ โ (๐ฅ / ๐) < ๐ฅ)) |
83 | | breq2 5151 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ = (๐ฅ / ๐) โ (๐ < ๐ฆ โ ๐ < (๐ฅ / ๐))) |
84 | | breq2 5151 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฆ = (๐ฅ / ๐) โ ((๐โ๐) โฅ ๐ฆ โ (๐โ๐) โฅ (๐ฅ / ๐))) |
85 | 84 | bibi2d 342 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ = (๐ฅ / ๐) โ (((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ) โ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)))) |
86 | 85 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฆ = (๐ฅ / ๐) โ (ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ) โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)))) |
87 | 86 | 2rexbidv 3219 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ = (๐ฅ / ๐) โ (โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)))) |
88 | 83, 87 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ = (๐ฅ / ๐) โ ((๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ)) โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐))))) |
89 | 88 | ralbidv 3177 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ = (๐ฅ / ๐) โ (โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ)) โ โ๐ โ โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐))))) |
90 | 82, 89 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ = (๐ฅ / ๐) โ ((๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ ((๐ฅ / ๐) < ๐ฅ โ โ๐ โ โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)))))) |
91 | 90 | rspcv 3608 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฅ / ๐) โ โ โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ ((๐ฅ / ๐) < ๐ฅ โ โ๐ โ โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)))))) |
92 | 91 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ) โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ ((๐ฅ / ๐) < ๐ฅ โ โ๐ โ โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)))))) |
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ ((๐ฅ / ๐) < ๐ฅ โ โ๐ โ โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)))))) |
94 | | eluzelcn 12830 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ
(โคโฅโ2) โ ๐ฅ โ โ) |
95 | 94 | mullidd 11228 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ
(โคโฅโ2) โ (1 ยท ๐ฅ) = ๐ฅ) |
96 | 95 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (1 ยท ๐ฅ) = ๐ฅ) |
97 | | prmgt1 16630 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ 1 <
๐) |
98 | 97 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ 1 < ๐) |
99 | | 1red 11211 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ 1 โ
โ) |
100 | 28 | nnred 12223 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ) |
101 | 100 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ ๐ โ โ) |
102 | 60 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ ๐ฅ โ โ) |
103 | 72 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ 0 < ๐ฅ) |
104 | | ltmul1 12060 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((1
โ โ โง ๐
โ โ โง (๐ฅ
โ โ โง 0 < ๐ฅ)) โ (1 < ๐ โ (1 ยท ๐ฅ) < (๐ ยท ๐ฅ))) |
105 | 99, 101, 102, 103, 104 | syl112anc 1374 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (1 < ๐ โ (1 ยท ๐ฅ) < (๐ ยท ๐ฅ))) |
106 | 98, 105 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (1 ยท ๐ฅ) < (๐ ยท ๐ฅ)) |
107 | 96, 106 | eqbrtrrd 5171 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ ๐ฅ < (๐ ยท ๐ฅ)) |
108 | 28, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ 0 <
๐) |
109 | 108 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ 0 < ๐) |
110 | | ltdivmul 12085 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฅ โ โ โง ๐ฅ โ โ โง (๐ โ โ โง 0 <
๐)) โ ((๐ฅ / ๐) < ๐ฅ โ ๐ฅ < (๐ ยท ๐ฅ))) |
111 | 102, 102,
101, 109, 110 | syl112anc 1374 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ ((๐ฅ / ๐) < ๐ฅ โ ๐ฅ < (๐ ยท ๐ฅ))) |
112 | 107, 111 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (๐ฅ / ๐) < ๐ฅ) |
113 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = (๐ก / ๐) โ (๐ < (๐ฅ / ๐) โ (๐ก / ๐) < (๐ฅ / ๐))) |
114 | | breq2 5151 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ = (๐ก / ๐) โ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ก / ๐))) |
115 | 114 | bibi1d 343 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = (๐ก / ๐) โ (((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)) โ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) |
116 | 115 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = (๐ก / ๐) โ (ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)) โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) |
117 | 116 | 2rexbidv 3219 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = (๐ก / ๐) โ (โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) |
118 | 113, 117 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = (๐ก / ๐) โ ((๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐))) โ ((๐ก / ๐) < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))))) |
119 | 118 | rspcv 3608 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ก / ๐) โ โ โ (โ๐ โ โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐))) โ ((๐ก / ๐) < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))))) |
120 | 119 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ) โ (โ๐ โ โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐))) โ ((๐ก / ๐) < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))))) |
121 | 120 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (โ๐ โ โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐))) โ ((๐ก / ๐) < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))))) |
122 | 39 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ) โ ๐ก โ โ) |
123 | 122 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ ๐ก โ โ) |
124 | | ltdiv1 12074 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ก โ โ โง ๐ฅ โ โ โง (๐ โ โ โง 0 <
๐)) โ (๐ก < ๐ฅ โ (๐ก / ๐) < (๐ฅ / ๐))) |
125 | 123, 102,
101, 109, 124 | syl112anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (๐ก < ๐ฅ โ (๐ก / ๐) < (๐ฅ / ๐))) |
126 | 125 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โ (๐ก / ๐) < (๐ฅ / ๐)) |
127 | | simprll 777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ ๐ โ โ) |
128 | | peano2nn 12220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ โ (๐ + 1) โ
โ) |
129 | 128 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + 1) โ
โ) |
130 | 129 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ (๐ + 1) โ โ) |
131 | 26 | ad4antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โค) |
132 | | nnnn0 12475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข (๐ โ โ โ ๐ โ
โ0) |
133 | 132 | ad2antll 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ0) |
134 | | zexpcl 14038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ โ โค โง ๐ โ โ0)
โ (๐โ๐) โ
โค) |
135 | 131, 133,
134 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (๐โ๐) โ โค) |
136 | | nnz 12575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข ((๐ก / ๐) โ โ โ (๐ก / ๐) โ โค) |
137 | 136 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข (((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ) โ (๐ก / ๐) โ โค) |
138 | 137 | ad3antlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ก / ๐) โ โค) |
139 | 29 | ad4antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ 0) |
140 | | dvdsmulcr 16225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (((๐โ๐) โ โค โง (๐ก / ๐) โ โค โง (๐ โ โค โง ๐ โ 0)) โ (((๐โ๐) ยท ๐) โฅ ((๐ก / ๐) ยท ๐) โ (๐โ๐) โฅ (๐ก / ๐))) |
141 | 135, 138,
131, 139, 140 | syl112anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (((๐โ๐) ยท ๐) โฅ ((๐ก / ๐) ยท ๐) โ (๐โ๐) โฅ (๐ก / ๐))) |
142 | 28 | nncnd 12224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข (๐ โ โ โ ๐ โ
โ) |
143 | 142 | ad4antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
144 | 143, 133 | expp1d 14108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (๐โ(๐ + 1)) = ((๐โ๐) ยท ๐)) |
145 | 144 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐โ๐) ยท ๐) = (๐โ(๐ + 1))) |
146 | | nncn 12216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข (๐ก โ โ โ ๐ก โ
โ) |
147 | 146 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข (((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ) โ ๐ก โ โ) |
148 | 147 | ad3antlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ก โ โ) |
149 | 148, 143,
139 | divcan1d 11987 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ก / ๐) ยท ๐) = ๐ก) |
150 | 145, 149 | breq12d 5160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (((๐โ๐) ยท ๐) โฅ ((๐ก / ๐) ยท ๐) โ (๐โ(๐ + 1)) โฅ ๐ก)) |
151 | 141, 150 | bitr3d 280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ(๐ + 1)) โฅ ๐ก)) |
152 | | nnz 12575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข ((๐ฅ / ๐) โ โ โ (๐ฅ / ๐) โ โค) |
153 | 152 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข (((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ) โ (๐ฅ / ๐) โ โค) |
154 | 153 | ad3antlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ฅ / ๐) โ โค) |
155 | | dvdsmulcr 16225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (((๐โ๐) โ โค โง (๐ฅ / ๐) โ โค โง (๐ โ โค โง ๐ โ 0)) โ (((๐โ๐) ยท ๐) โฅ ((๐ฅ / ๐) ยท ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))) |
156 | 135, 154,
131, 139, 155 | syl112anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (((๐โ๐) ยท ๐) โฅ ((๐ฅ / ๐) ยท ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))) |
157 | 94 | ad4antr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ฅ โ โ) |
158 | 157, 143,
139 | divcan1d 11987 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ฅ / ๐) ยท ๐) = ๐ฅ) |
159 | 145, 158 | breq12d 5160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (((๐โ๐) ยท ๐) โฅ ((๐ฅ / ๐) ยท ๐) โ (๐โ(๐ + 1)) โฅ ๐ฅ)) |
160 | 156, 159 | bitr3d 280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐โ๐) โฅ (๐ฅ / ๐) โ (๐โ(๐ + 1)) โฅ ๐ฅ)) |
161 | 151, 160 | bibi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ ((๐โ(๐ + 1)) โฅ ๐ก โ (๐โ(๐ + 1)) โฅ ๐ฅ))) |
162 | 161 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ ยฌ ((๐โ(๐ + 1)) โฅ ๐ก โ (๐โ(๐ + 1)) โฅ ๐ฅ))) |
163 | 162 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ ยฌ ((๐โ(๐ + 1)) โฅ ๐ก โ (๐โ(๐ + 1)) โฅ ๐ฅ))) |
164 | 163 | impr 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ ยฌ ((๐โ(๐ + 1)) โฅ ๐ก โ (๐โ(๐ + 1)) โฅ ๐ฅ)) |
165 | | oveq2 7413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ = (๐ + 1) โ (๐โ๐) = (๐โ(๐ + 1))) |
166 | 165 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ = (๐ + 1) โ ((๐โ๐) โฅ ๐ก โ (๐โ(๐ + 1)) โฅ ๐ก)) |
167 | 165 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ = (๐ + 1) โ ((๐โ๐) โฅ ๐ฅ โ (๐โ(๐ + 1)) โฅ ๐ฅ)) |
168 | 166, 167 | bibi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ = (๐ + 1) โ (((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ(๐ + 1)) โฅ ๐ก โ (๐โ(๐ + 1)) โฅ ๐ฅ))) |
169 | 168 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ = (๐ + 1) โ (ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ(๐ + 1)) โฅ ๐ก โ (๐โ(๐ + 1)) โฅ ๐ฅ))) |
170 | 169 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (((๐ + 1) โ โ โง ยฌ
((๐โ(๐ + 1)) โฅ ๐ก โ (๐โ(๐ + 1)) โฅ ๐ฅ)) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) |
171 | 130, 164,
170 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) |
172 | | oveq1 7412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
173 | 172 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ = ๐ โ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ก / ๐))) |
174 | 172 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ = ๐ โ ((๐โ๐) โฅ (๐ฅ / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))) |
175 | 173, 174 | bibi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ = ๐ โ (((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) |
176 | 175 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ = ๐ โ (ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) |
177 | 176 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ = ๐ โ (((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))) โ ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))))) |
178 | 177 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ = ๐ โ (((((๐ฅ โ (โคโฅโ2)
โง ๐ โ โ)
โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ ((((๐ฅ โ (โคโฅโ2)
โง ๐ โ โ)
โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))))) |
179 | | oveq1 7412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
180 | 179 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ = ๐ โ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ก)) |
181 | 179 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ = ๐ โ ((๐โ๐) โฅ ๐ฅ โ (๐โ๐) โฅ ๐ฅ)) |
182 | 180, 181 | bibi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ = ๐ โ (((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
183 | 182 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ = ๐ โ (ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
184 | 183 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ = ๐ โ (โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
185 | 178, 184 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ = ๐ โ ((((((๐ฅ โ (โคโฅโ2)
โง ๐ โ โ)
โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) โ (((((๐ฅ โ (โคโฅโ2)
โง ๐ โ โ)
โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
186 | 171, 185 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ = ๐ โ (((((๐ฅ โ (โคโฅโ2)
โง ๐ โ โ)
โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
187 | 186 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ (๐ = ๐ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
188 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (((๐ โ โ โง ๐ โ โ) โง ยฌ
๐ = ๐) โ ๐ โ โ) |
189 | 188 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข
((((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))) โ ๐ โ โ) |
190 | | prmz 16608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
โข (๐ โ โ โ ๐ โ
โค) |
191 | 190 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โค) |
192 | 191 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ๐ โ โค) |
193 | 132 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ0) |
194 | 193 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ๐ โ โ0) |
195 | | zexpcl 14038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข ((๐ โ โค โง ๐ โ โ0)
โ (๐โ๐) โ
โค) |
196 | 192, 194,
195 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (๐โ๐) โ โค) |
197 | 26 | ad4antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ๐ โ โค) |
198 | 137 | ad3antlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (๐ก / ๐) โ โค) |
199 | | dvdsmultr2 16237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข (((๐โ๐) โ โค โง ๐ โ โค โง (๐ก / ๐) โ โค) โ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ ยท (๐ก / ๐)))) |
200 | 196, 197,
198, 199 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ ยท (๐ก / ๐)))) |
201 | 196, 197 | gcdcomd 16451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) gcd ๐) = (๐ gcd (๐โ๐))) |
202 | | simp-4r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
203 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
204 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
205 | | prmdvdsexpb 16649 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ (๐ โฅ (๐โ๐) โ ๐ = ๐)) |
206 | | equcom 2021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
โข (๐ = ๐ โ ๐ = ๐) |
207 | 205, 206 | bitrdi 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ (๐ โฅ (๐โ๐) โ ๐ = ๐)) |
208 | 207 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ (๐ โฅ (๐โ๐) โ ๐ = ๐)) |
209 | 202, 203,
204, 208 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ โฅ (๐โ๐) โ ๐ = ๐)) |
210 | 209 | con3d 152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (ยฌ ๐ = ๐ โ ยฌ ๐ โฅ (๐โ๐))) |
211 | 210 | impr 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ยฌ ๐ โฅ (๐โ๐)) |
212 | | simp-4r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ๐ โ โ) |
213 | | coprm 16644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
โข ((๐ โ โ โง (๐โ๐) โ โค) โ (ยฌ ๐ โฅ (๐โ๐) โ (๐ gcd (๐โ๐)) = 1)) |
214 | 212, 196,
213 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (ยฌ ๐ โฅ (๐โ๐) โ (๐ gcd (๐โ๐)) = 1)) |
215 | 211, 214 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (๐ gcd (๐โ๐)) = 1) |
216 | 201, 215 | eqtrd 2772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) gcd ๐) = 1) |
217 | | coprmdvds 16586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข (((๐โ๐) โ โค โง ๐ โ โค โง (๐ก / ๐) โ โค) โ (((๐โ๐) โฅ (๐ ยท (๐ก / ๐)) โง ((๐โ๐) gcd ๐) = 1) โ (๐โ๐) โฅ (๐ก / ๐))) |
218 | 196, 197,
198, 217 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (((๐โ๐) โฅ (๐ ยท (๐ก / ๐)) โง ((๐โ๐) gcd ๐) = 1) โ (๐โ๐) โฅ (๐ก / ๐))) |
219 | 216, 218 | mpan2d 692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) โฅ (๐ ยท (๐ก / ๐)) โ (๐โ๐) โฅ (๐ก / ๐))) |
220 | 200, 219 | impbid 211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ ยท (๐ก / ๐)))) |
221 | 147 | ad3antlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ๐ก โ โ) |
222 | 142 | ad4antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ๐ โ โ) |
223 | 29 | ad4antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ๐ โ 0) |
224 | 221, 222,
223 | divcan2d 11988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (๐ ยท (๐ก / ๐)) = ๐ก) |
225 | 224 | breq2d 5159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) โฅ (๐ ยท (๐ก / ๐)) โ (๐โ๐) โฅ ๐ก)) |
226 | 220, 225 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ ๐ก)) |
227 | 153 | ad3antlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (๐ฅ / ๐) โ โค) |
228 | | dvdsmultr2 16237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข (((๐โ๐) โ โค โง ๐ โ โค โง (๐ฅ / ๐) โ โค) โ ((๐โ๐) โฅ (๐ฅ / ๐) โ (๐โ๐) โฅ (๐ ยท (๐ฅ / ๐)))) |
229 | 196, 197,
227, 228 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) โฅ (๐ฅ / ๐) โ (๐โ๐) โฅ (๐ ยท (๐ฅ / ๐)))) |
230 | | coprmdvds 16586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข (((๐โ๐) โ โค โง ๐ โ โค โง (๐ฅ / ๐) โ โค) โ (((๐โ๐) โฅ (๐ ยท (๐ฅ / ๐)) โง ((๐โ๐) gcd ๐) = 1) โ (๐โ๐) โฅ (๐ฅ / ๐))) |
231 | 196, 197,
227, 230 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (((๐โ๐) โฅ (๐ ยท (๐ฅ / ๐)) โง ((๐โ๐) gcd ๐) = 1) โ (๐โ๐) โฅ (๐ฅ / ๐))) |
232 | 216, 231 | mpan2d 692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) โฅ (๐ ยท (๐ฅ / ๐)) โ (๐โ๐) โฅ (๐ฅ / ๐))) |
233 | 229, 232 | impbid 211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) โฅ (๐ฅ / ๐) โ (๐โ๐) โฅ (๐ ยท (๐ฅ / ๐)))) |
234 | 94 | ad4antr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ๐ฅ โ โ) |
235 | 234, 222,
223 | divcan2d 11988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (๐ ยท (๐ฅ / ๐)) = ๐ฅ) |
236 | 235 | breq2d 5159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) โฅ (๐ ยท (๐ฅ / ๐)) โ (๐โ๐) โฅ ๐ฅ)) |
237 | 233, 236 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ ((๐โ๐) โฅ (๐ฅ / ๐) โ (๐โ๐) โฅ ๐ฅ)) |
238 | 226, 237 | bibi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
239 | 238 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
240 | 239 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข
((((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))) โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) |
241 | | oveq2 7413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
242 | 241 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ = ๐ โ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ก)) |
243 | 241 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ = ๐ โ ((๐โ๐) โฅ ๐ฅ โ (๐โ๐) โฅ ๐ฅ)) |
244 | 242, 243 | bibi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ = ๐ โ (((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
245 | 244 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ = ๐ โ (ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
246 | 245 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โ โ โง ยฌ
((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) |
247 | 189, 240,
246 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข
((((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) |
248 | 247 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ๐ = ๐)) โ (ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
249 | 248 | expr 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (ยฌ ๐ = ๐ โ (ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
250 | 249 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง (๐ โ โ โง ๐ โ โ)) โ (ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ (ยฌ ๐ = ๐ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
251 | 250 | impr 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ (ยฌ ๐ = ๐ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
252 | 187, 251 | pm2.61d 179 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) |
253 | | oveq1 7412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
254 | 253 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ = ๐ โ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ก)) |
255 | 253 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ = ๐ โ ((๐โ๐) โฅ ๐ฅ โ (๐โ๐) โฅ ๐ฅ)) |
256 | 254, 255 | bibi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ = ๐ โ (((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
257 | 256 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ = ๐ โ (ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
258 | 257 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ = ๐ โ (โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
259 | 258 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โ โ โง
โ๐ โ โ
ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) |
260 | 127, 252,
259 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โง ((๐ โ โ โง ๐ โ โ) โง ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) |
261 | 260 | exp32 421 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โ ((๐ โ โ โง ๐ โ โ) โ (ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
262 | 261 | rexlimdvv 3210 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โ (โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐)) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
263 | 126, 262 | embantd 59 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โง ๐ก < ๐ฅ) โ (((๐ก / ๐) < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
264 | 263 | ex 413 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (๐ก < ๐ฅ โ (((๐ก / ๐) < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
265 | 264 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (((๐ก / ๐) < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ (๐ก / ๐) โ (๐โ๐) โฅ (๐ฅ / ๐))) โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
266 | 121, 265 | syld 47 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (โ๐ โ โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐))) โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
267 | 112, 266 | embantd 59 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (((๐ฅ / ๐) < ๐ฅ โ โ๐ โ โ (๐ < (๐ฅ / ๐) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ (๐ฅ / ๐)))) โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
268 | 93, 267 | syld 47 |
. . . . . . . . . . . . . . . 16
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โง ((๐ฅ / ๐) โ โ โง (๐ก / ๐) โ โ โง ๐ก โ โ)) โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
269 | 268 | 3exp2 1354 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โ ((๐ฅ / ๐) โ โ โ ((๐ก / ๐) โ โ โ (๐ก โ โ โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))))))) |
270 | 81, 269 | syld 47 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ) โ (๐ โฅ ๐ฅ โ ((๐ก / ๐) โ โ โ (๐ก โ โ โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))))))) |
271 | 270 | 3impia 1117 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โ ((๐ก / ๐) โ โ โ (๐ก โ โ โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))))) |
272 | 271 | com24 95 |
. . . . . . . . . . . 12
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ (๐ก โ โ โ ((๐ก / ๐) โ โ โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))))) |
273 | 272 | imp32 419 |
. . . . . . . . . . 11
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โง ๐ก โ โ)) โ ((๐ก / ๐) โ โ โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
274 | 37, 53, 273 | 3syld 60 |
. . . . . . . . . 10
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โง ๐ก โ โ)) โ (๐ โฅ ๐ก โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
275 | | simpl2 1192 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (๐ก โ โ โง (ยฌ ๐ โฅ ๐ก โง ๐ก < ๐ฅ))) โ ๐ โ โ) |
276 | | 1nn 12219 |
. . . . . . . . . . . . . . 15
โข 1 โ
โ |
277 | 276 | a1i 11 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (๐ก โ โ โง (ยฌ ๐ โฅ ๐ก โง ๐ก < ๐ฅ))) โ 1 โ โ) |
278 | 142 | exp1d 14102 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (๐โ1) = ๐) |
279 | 278 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ((๐โ1) โฅ ๐ก โ ๐ โฅ ๐ก)) |
280 | 279 | notbid 317 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (ยฌ
(๐โ1) โฅ ๐ก โ ยฌ ๐ โฅ ๐ก)) |
281 | 280 | biimpar 478 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ยฌ
๐ โฅ ๐ก) โ ยฌ (๐โ1) โฅ ๐ก) |
282 | 281 | 3ad2antl2 1186 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง ยฌ ๐ โฅ ๐ก) โ ยฌ (๐โ1) โฅ ๐ก) |
283 | 282 | adantrr 715 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (ยฌ ๐ โฅ ๐ก โง ๐ก < ๐ฅ)) โ ยฌ (๐โ1) โฅ ๐ก) |
284 | 283 | adantrl 714 |
. . . . . . . . . . . . . . . 16
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (๐ก โ โ โง (ยฌ ๐ โฅ ๐ก โง ๐ก < ๐ฅ))) โ ยฌ (๐โ1) โฅ ๐ก) |
285 | 278 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ((๐โ1) โฅ ๐ฅ โ ๐ โฅ ๐ฅ)) |
286 | 285 | biimpar 478 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โฅ ๐ฅ) โ (๐โ1) โฅ ๐ฅ) |
287 | 286 | 3adant1 1130 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โ (๐โ1) โฅ ๐ฅ) |
288 | | idd 24 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โ (((๐โ1) โฅ ๐ฅ โ (๐โ1) โฅ ๐ก) โ ((๐โ1) โฅ ๐ฅ โ (๐โ1) โฅ ๐ก))) |
289 | 287, 288 | mpid 44 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โ (((๐โ1) โฅ ๐ฅ โ (๐โ1) โฅ ๐ก) โ (๐โ1) โฅ ๐ก)) |
290 | 289 | adantr 481 |
. . . . . . . . . . . . . . . 16
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (๐ก โ โ โง (ยฌ ๐ โฅ ๐ก โง ๐ก < ๐ฅ))) โ (((๐โ1) โฅ ๐ฅ โ (๐โ1) โฅ ๐ก) โ (๐โ1) โฅ ๐ก)) |
291 | 284, 290 | mtod 197 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (๐ก โ โ โง (ยฌ ๐ โฅ ๐ก โง ๐ก < ๐ฅ))) โ ยฌ ((๐โ1) โฅ ๐ฅ โ (๐โ1) โฅ ๐ก)) |
292 | | biimpr 219 |
. . . . . . . . . . . . . . 15
โข (((๐โ1) โฅ ๐ก โ (๐โ1) โฅ ๐ฅ) โ ((๐โ1) โฅ ๐ฅ โ (๐โ1) โฅ ๐ก)) |
293 | 291, 292 | nsyl 140 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (๐ก โ โ โง (ยฌ ๐ โฅ ๐ก โง ๐ก < ๐ฅ))) โ ยฌ ((๐โ1) โฅ ๐ก โ (๐โ1) โฅ ๐ฅ)) |
294 | | oveq1 7412 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
295 | 294 | breq1d 5157 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ก)) |
296 | 294 | breq1d 5157 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ ((๐โ๐) โฅ ๐ฅ โ (๐โ๐) โฅ ๐ฅ)) |
297 | 295, 296 | bibi12d 345 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
298 | 297 | notbid 317 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
299 | | oveq2 7413 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = 1 โ (๐โ๐) = (๐โ1)) |
300 | 299 | breq1d 5157 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 1 โ ((๐โ๐) โฅ ๐ก โ (๐โ1) โฅ ๐ก)) |
301 | 299 | breq1d 5157 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 1 โ ((๐โ๐) โฅ ๐ฅ โ (๐โ1) โฅ ๐ฅ)) |
302 | 300, 301 | bibi12d 345 |
. . . . . . . . . . . . . . . 16
โข (๐ = 1 โ (((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ1) โฅ ๐ก โ (๐โ1) โฅ ๐ฅ))) |
303 | 302 | notbid 317 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ (ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ1) โฅ ๐ก โ (๐โ1) โฅ ๐ฅ))) |
304 | 298, 303 | rspc2ev 3623 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง 1 โ
โ โง ยฌ ((๐โ1) โฅ ๐ก โ (๐โ1) โฅ ๐ฅ)) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) |
305 | 275, 277,
293, 304 | syl3anc 1371 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (๐ก โ โ โง (ยฌ ๐ โฅ ๐ก โง ๐ก < ๐ฅ))) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) |
306 | 305 | expr 457 |
. . . . . . . . . . . 12
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง ๐ก โ โ) โ ((ยฌ ๐ โฅ ๐ก โง ๐ก < ๐ฅ) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
307 | 306 | expd 416 |
. . . . . . . . . . 11
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง ๐ก โ โ) โ (ยฌ ๐ โฅ ๐ก โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
308 | 307 | adantrl 714 |
. . . . . . . . . 10
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โง ๐ก โ โ)) โ (ยฌ ๐ โฅ ๐ก โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
309 | 274, 308 | pm2.61d 179 |
. . . . . . . . 9
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โง ๐ก โ โ)) โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
310 | 309 | expr 457 |
. . . . . . . 8
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ)))) โ (๐ก โ โ โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)))) |
311 | 310 | ralrimiv 3145 |
. . . . . . 7
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ)))) โ โ๐ก โ โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ))) |
312 | | breq1 5150 |
. . . . . . . . 9
โข (๐ก = ๐ โ (๐ก < ๐ฅ โ ๐ < ๐ฅ)) |
313 | | breq2 5151 |
. . . . . . . . . . . . 13
โข (๐ก = ๐ โ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐)) |
314 | 313 | bibi1d 343 |
. . . . . . . . . . . 12
โข (๐ก = ๐ โ (((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
315 | 314 | notbid 317 |
. . . . . . . . . . 11
โข (๐ก = ๐ โ (ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
316 | 315 | 2rexbidv 3219 |
. . . . . . . . . 10
โข (๐ก = ๐ โ (โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
317 | 253 | breq1d 5157 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐)) |
318 | 317, 255 | bibi12d 345 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
319 | 318 | notbid 317 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
320 | 241 | breq1d 5157 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐)) |
321 | 320, 243 | bibi12d 345 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
322 | 321 | notbid 317 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
323 | 319, 322 | cbvrex2vw 3239 |
. . . . . . . . . 10
โข
(โ๐ โ
โ โ๐ โ
โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ)) |
324 | 316, 323 | bitrdi 286 |
. . . . . . . . 9
โข (๐ก = ๐ โ (โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ) โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
325 | 312, 324 | imbi12d 344 |
. . . . . . . 8
โข (๐ก = ๐ โ ((๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) โ (๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ)))) |
326 | 325 | cbvralvw 3234 |
. . . . . . 7
โข
(โ๐ก โ
โ (๐ก < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ก โ (๐โ๐) โฅ ๐ฅ)) โ โ๐ โ โ (๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
327 | 311, 326 | sylib 217 |
. . . . . 6
โข (((๐ฅ โ
(โคโฅโ2) โง ๐ โ โ โง ๐ โฅ ๐ฅ) โง โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ)))) โ โ๐ โ โ (๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
328 | 327 | 3exp1 1352 |
. . . . 5
โข (๐ฅ โ
(โคโฅโ2) โ (๐ โ โ โ (๐ โฅ ๐ฅ โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ โ๐ โ โ (๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ)))))) |
329 | 328 | rexlimdv 3153 |
. . . 4
โข (๐ฅ โ
(โคโฅโ2) โ (โ๐ โ โ ๐ โฅ ๐ฅ โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ โ๐ โ โ (๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))))) |
330 | 25, 329 | mpd 15 |
. . 3
โข (๐ฅ โ
(โคโฅโ2) โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ โ โ (๐ < ๐ฆ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฆ))) โ โ๐ โ โ (๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ)))) |
331 | 14, 21, 24, 330 | indstr2 12907 |
. 2
โข (๐ฅ โ โ โ
โ๐ โ โ
(๐ < ๐ฅ โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ฅ))) |
332 | 7, 331 | vtoclga 3565 |
1
โข (๐ด โ โ โ
โ๐ โ โ
(๐ < ๐ด โ โ๐ โ โ โ๐ โ โ ยฌ ((๐โ๐) โฅ ๐ โ (๐โ๐) โฅ ๐ด))) |