Step | Hyp | Ref
| Expression |
1 | | breq2 5151 |
. . . . . 6
โข (๐ง = ๐ด โ (1 โค ๐ง โ 1 โค ๐ด)) |
2 | 1 | elrab 3682 |
. . . . 5
โข (๐ด โ {๐ง โ โ โฃ 1 โค ๐ง} โ (๐ด โ โ โง 1 โค ๐ด)) |
3 | | ssrab2 4076 |
. . . . . . 7
โข {๐ง โ โ โฃ 1 โค
๐ง} โ
โ |
4 | | ax-resscn 11163 |
. . . . . . 7
โข โ
โ โ |
5 | 3, 4 | sstri 3990 |
. . . . . 6
โข {๐ง โ โ โฃ 1 โค
๐ง} โ
โ |
6 | | breq2 5151 |
. . . . . . . 8
โข (๐ง = ๐ฅ โ (1 โค ๐ง โ 1 โค ๐ฅ)) |
7 | 6 | elrab 3682 |
. . . . . . 7
โข (๐ฅ โ {๐ง โ โ โฃ 1 โค ๐ง} โ (๐ฅ โ โ โง 1 โค ๐ฅ)) |
8 | | breq2 5151 |
. . . . . . . 8
โข (๐ง = ๐ฆ โ (1 โค ๐ง โ 1 โค ๐ฆ)) |
9 | 8 | elrab 3682 |
. . . . . . 7
โข (๐ฆ โ {๐ง โ โ โฃ 1 โค ๐ง} โ (๐ฆ โ โ โง 1 โค ๐ฆ)) |
10 | | breq2 5151 |
. . . . . . . 8
โข (๐ง = (๐ฅ ยท ๐ฆ) โ (1 โค ๐ง โ 1 โค (๐ฅ ยท ๐ฆ))) |
11 | | remulcl 11191 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ ยท ๐ฆ) โ โ) |
12 | 11 | ad2ant2r 745 |
. . . . . . . 8
โข (((๐ฅ โ โ โง 1 โค
๐ฅ) โง (๐ฆ โ โ โง 1 โค
๐ฆ)) โ (๐ฅ ยท ๐ฆ) โ โ) |
13 | | 1t1e1 12370 |
. . . . . . . . . 10
โข (1
ยท 1) = 1 |
14 | | 1re 11210 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
15 | | 0le1 11733 |
. . . . . . . . . . . . . 14
โข 0 โค
1 |
16 | 14, 15 | pm3.2i 471 |
. . . . . . . . . . . . 13
โข (1 โ
โ โง 0 โค 1) |
17 | 16 | jctl 524 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ ((1
โ โ โง 0 โค 1) โง ๐ฅ โ โ)) |
18 | 16 | jctl 524 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ((1
โ โ โง 0 โค 1) โง ๐ฆ โ โ)) |
19 | | lemul12a 12068 |
. . . . . . . . . . . 12
โข ((((1
โ โ โง 0 โค 1) โง ๐ฅ โ โ) โง ((1 โ โ
โง 0 โค 1) โง ๐ฆ
โ โ)) โ ((1 โค ๐ฅ โง 1 โค ๐ฆ) โ (1 ยท 1) โค (๐ฅ ยท ๐ฆ))) |
20 | 17, 18, 19 | syl2an 596 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((1 โค
๐ฅ โง 1 โค ๐ฆ) โ (1 ยท 1) โค
(๐ฅ ยท ๐ฆ))) |
21 | 20 | imp 407 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (1 โค
๐ฅ โง 1 โค ๐ฆ)) โ (1 ยท 1) โค
(๐ฅ ยท ๐ฆ)) |
22 | 13, 21 | eqbrtrrid 5183 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (1 โค
๐ฅ โง 1 โค ๐ฆ)) โ 1 โค (๐ฅ ยท ๐ฆ)) |
23 | 22 | an4s 658 |
. . . . . . . 8
โข (((๐ฅ โ โ โง 1 โค
๐ฅ) โง (๐ฆ โ โ โง 1 โค
๐ฆ)) โ 1 โค (๐ฅ ยท ๐ฆ)) |
24 | 10, 12, 23 | elrabd 3684 |
. . . . . . 7
โข (((๐ฅ โ โ โง 1 โค
๐ฅ) โง (๐ฆ โ โ โง 1 โค
๐ฆ)) โ (๐ฅ ยท ๐ฆ) โ {๐ง โ โ โฃ 1 โค ๐ง}) |
25 | 7, 9, 24 | syl2anb 598 |
. . . . . 6
โข ((๐ฅ โ {๐ง โ โ โฃ 1 โค ๐ง} โง ๐ฆ โ {๐ง โ โ โฃ 1 โค ๐ง}) โ (๐ฅ ยท ๐ฆ) โ {๐ง โ โ โฃ 1 โค ๐ง}) |
26 | | 1le1 11838 |
. . . . . . 7
โข 1 โค
1 |
27 | | breq2 5151 |
. . . . . . . 8
โข (๐ง = 1 โ (1 โค ๐ง โ 1 โค
1)) |
28 | 27 | elrab 3682 |
. . . . . . 7
โข (1 โ
{๐ง โ โ โฃ 1
โค ๐ง} โ (1 โ
โ โง 1 โค 1)) |
29 | 14, 26, 28 | mpbir2an 709 |
. . . . . 6
โข 1 โ
{๐ง โ โ โฃ 1
โค ๐ง} |
30 | 5, 25, 29 | expcllem 14034 |
. . . . 5
โข ((๐ด โ {๐ง โ โ โฃ 1 โค ๐ง} โง ๐ โ โ0) โ (๐ดโ๐) โ {๐ง โ โ โฃ 1 โค ๐ง}) |
31 | 2, 30 | sylanbr 582 |
. . . 4
โข (((๐ด โ โ โง 1 โค
๐ด) โง ๐ โ โ0) โ (๐ดโ๐) โ {๐ง โ โ โฃ 1 โค ๐ง}) |
32 | 31 | 3impa 1110 |
. . 3
โข ((๐ด โ โ โง 1 โค
๐ด โง ๐ โ โ0) โ (๐ดโ๐) โ {๐ง โ โ โฃ 1 โค ๐ง}) |
33 | 32 | 3com23 1126 |
. 2
โข ((๐ด โ โ โง ๐ โ โ0
โง 1 โค ๐ด) โ
(๐ดโ๐) โ {๐ง โ โ โฃ 1 โค ๐ง}) |
34 | | breq2 5151 |
. . . 4
โข (๐ง = (๐ดโ๐) โ (1 โค ๐ง โ 1 โค (๐ดโ๐))) |
35 | 34 | elrab 3682 |
. . 3
โข ((๐ดโ๐) โ {๐ง โ โ โฃ 1 โค ๐ง} โ ((๐ดโ๐) โ โ โง 1 โค (๐ดโ๐))) |
36 | 35 | simprbi 497 |
. 2
โข ((๐ดโ๐) โ {๐ง โ โ โฃ 1 โค ๐ง} โ 1 โค (๐ดโ๐)) |
37 | 33, 36 | syl 17 |
1
โข ((๐ด โ โ โง ๐ โ โ0
โง 1 โค ๐ด) โ 1
โค (๐ดโ๐)) |