Step | Hyp | Ref
| Expression |
1 | | 2re 12228 |
. . . . . . 7
โข 2 โ
โ |
2 | | 1re 11156 |
. . . . . . 7
โข 1 โ
โ |
3 | | ltsub1 11652 |
. . . . . . 7
โข ((2
โ โ โง ๐ด
โ โ โง 1 โ โ) โ (2 < ๐ด โ (2 โ 1) < (๐ด โ 1))) |
4 | 1, 2, 3 | mp3an13 1453 |
. . . . . 6
โข (๐ด โ โ โ (2 <
๐ด โ (2 โ 1) <
(๐ด โ
1))) |
5 | | 2m1e1 12280 |
. . . . . . 7
โข (2
โ 1) = 1 |
6 | 5 | breq1i 5113 |
. . . . . 6
โข ((2
โ 1) < (๐ด โ
1) โ 1 < (๐ด โ
1)) |
7 | 4, 6 | bitrdi 287 |
. . . . 5
โข (๐ด โ โ โ (2 <
๐ด โ 1 < (๐ด โ 1))) |
8 | | ltsub1 11652 |
. . . . . . 7
โข ((2
โ โ โง ๐ต
โ โ โง 1 โ โ) โ (2 < ๐ต โ (2 โ 1) < (๐ต โ 1))) |
9 | 1, 2, 8 | mp3an13 1453 |
. . . . . 6
โข (๐ต โ โ โ (2 <
๐ต โ (2 โ 1) <
(๐ต โ
1))) |
10 | 5 | breq1i 5113 |
. . . . . 6
โข ((2
โ 1) < (๐ต โ
1) โ 1 < (๐ต โ
1)) |
11 | 9, 10 | bitrdi 287 |
. . . . 5
โข (๐ต โ โ โ (2 <
๐ต โ 1 < (๐ต โ 1))) |
12 | 7, 11 | bi2anan9 638 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2 <
๐ด โง 2 < ๐ต) โ (1 < (๐ด โ 1) โง 1 < (๐ต โ 1)))) |
13 | | peano2rem 11469 |
. . . . 5
โข (๐ด โ โ โ (๐ด โ 1) โ
โ) |
14 | | peano2rem 11469 |
. . . . 5
โข (๐ต โ โ โ (๐ต โ 1) โ
โ) |
15 | | mulgt1 12015 |
. . . . . 6
โข ((((๐ด โ 1) โ โ โง
(๐ต โ 1) โ
โ) โง (1 < (๐ด
โ 1) โง 1 < (๐ต
โ 1))) โ 1 < ((๐ด โ 1) ยท (๐ต โ 1))) |
16 | 15 | ex 414 |
. . . . 5
โข (((๐ด โ 1) โ โ โง
(๐ต โ 1) โ
โ) โ ((1 < (๐ด
โ 1) โง 1 < (๐ต
โ 1)) โ 1 < ((๐ด โ 1) ยท (๐ต โ 1)))) |
17 | 13, 14, 16 | syl2an 597 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 <
(๐ด โ 1) โง 1 <
(๐ต โ 1)) โ 1
< ((๐ด โ 1)
ยท (๐ต โ
1)))) |
18 | 12, 17 | sylbid 239 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2 <
๐ด โง 2 < ๐ต) โ 1 < ((๐ด โ 1) ยท (๐ต โ 1)))) |
19 | | recn 11142 |
. . . . . 6
โข (๐ด โ โ โ ๐ด โ
โ) |
20 | | recn 11142 |
. . . . . 6
โข (๐ต โ โ โ ๐ต โ
โ) |
21 | | ax-1cn 11110 |
. . . . . . 7
โข 1 โ
โ |
22 | | mulsub 11599 |
. . . . . . . 8
โข (((๐ด โ โ โง 1 โ
โ) โง (๐ต โ
โ โง 1 โ โ)) โ ((๐ด โ 1) ยท (๐ต โ 1)) = (((๐ด ยท ๐ต) + (1 ยท 1)) โ ((๐ด ยท 1) + (๐ต ยท 1)))) |
23 | 21, 22 | mpanl2 700 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ต โ โ โง 1 โ
โ)) โ ((๐ด
โ 1) ยท (๐ต
โ 1)) = (((๐ด ยท
๐ต) + (1 ยท 1))
โ ((๐ด ยท 1) +
(๐ต ยท
1)))) |
24 | 21, 23 | mpanr2 703 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ 1) ยท (๐ต โ 1)) = (((๐ด ยท ๐ต) + (1 ยท 1)) โ ((๐ด ยท 1) + (๐ต ยท 1)))) |
25 | 19, 20, 24 | syl2an 597 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ 1) ยท (๐ต โ 1)) = (((๐ด ยท ๐ต) + (1 ยท 1)) โ ((๐ด ยท 1) + (๐ต ยท 1)))) |
26 | 25 | breq2d 5118 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (1 <
((๐ด โ 1) ยท
(๐ต โ 1)) โ 1
< (((๐ด ยท ๐ต) + (1 ยท 1)) โ
((๐ด ยท 1) + (๐ต ยท
1))))) |
27 | | remulcl 11137 |
. . . . . . . 8
โข ((๐ด โ โ โง 1 โ
โ) โ (๐ด ยท
1) โ โ) |
28 | 2, 27 | mpan2 690 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด ยท 1) โ
โ) |
29 | | remulcl 11137 |
. . . . . . . 8
โข ((๐ต โ โ โง 1 โ
โ) โ (๐ต ยท
1) โ โ) |
30 | 2, 29 | mpan2 690 |
. . . . . . 7
โข (๐ต โ โ โ (๐ต ยท 1) โ
โ) |
31 | | readdcl 11135 |
. . . . . . 7
โข (((๐ด ยท 1) โ โ
โง (๐ต ยท 1) โ
โ) โ ((๐ด
ยท 1) + (๐ต ยท
1)) โ โ) |
32 | 28, 30, 31 | syl2an 597 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท 1) + (๐ต ยท 1)) โ
โ) |
33 | | remulcl 11137 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
34 | 2, 2 | remulcli 11172 |
. . . . . . 7
โข (1
ยท 1) โ โ |
35 | | readdcl 11135 |
. . . . . . 7
โข (((๐ด ยท ๐ต) โ โ โง (1 ยท 1) โ
โ) โ ((๐ด
ยท ๐ต) + (1 ยท
1)) โ โ) |
36 | 33, 34, 35 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) + (1 ยท 1)) โ
โ) |
37 | | ltaddsub2 11631 |
. . . . . . 7
โข ((((๐ด ยท 1) + (๐ต ยท 1)) โ โ
โง 1 โ โ โง ((๐ด ยท ๐ต) + (1 ยท 1)) โ โ) โ
((((๐ด ยท 1) + (๐ต ยท 1)) + 1) < ((๐ด ยท ๐ต) + (1 ยท 1)) โ 1 < (((๐ด ยท ๐ต) + (1 ยท 1)) โ ((๐ด ยท 1) + (๐ต ยท
1))))) |
38 | 2, 37 | mp3an2 1450 |
. . . . . 6
โข ((((๐ด ยท 1) + (๐ต ยท 1)) โ โ
โง ((๐ด ยท ๐ต) + (1 ยท 1)) โ
โ) โ ((((๐ด
ยท 1) + (๐ต ยท
1)) + 1) < ((๐ด ยท
๐ต) + (1 ยท 1)) โ
1 < (((๐ด ยท ๐ต) + (1 ยท 1)) โ
((๐ด ยท 1) + (๐ต ยท
1))))) |
39 | 32, 36, 38 | syl2anc 585 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด ยท 1) + (๐ต ยท 1)) + 1) < ((๐ด ยท ๐ต) + (1 ยท 1)) โ 1 < (((๐ด ยท ๐ต) + (1 ยท 1)) โ ((๐ด ยท 1) + (๐ต ยท
1))))) |
40 | | 1t1e1 12316 |
. . . . . . 7
โข (1
ยท 1) = 1 |
41 | 40 | oveq2i 7369 |
. . . . . 6
โข ((๐ด ยท ๐ต) + (1 ยท 1)) = ((๐ด ยท ๐ต) + 1) |
42 | 41 | breq2i 5114 |
. . . . 5
โข ((((๐ด ยท 1) + (๐ต ยท 1)) + 1) < ((๐ด ยท ๐ต) + (1 ยท 1)) โ (((๐ด ยท 1) + (๐ต ยท 1)) + 1) < ((๐ด ยท ๐ต) + 1)) |
43 | 39, 42 | bitr3di 286 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (1 <
(((๐ด ยท ๐ต) + (1 ยท 1)) โ
((๐ด ยท 1) + (๐ต ยท 1))) โ (((๐ด ยท 1) + (๐ต ยท 1)) + 1) < ((๐ด ยท ๐ต) + 1))) |
44 | | ltadd1 11623 |
. . . . . . 7
โข ((((๐ด ยท 1) + (๐ต ยท 1)) โ โ
โง (๐ด ยท ๐ต) โ โ โง 1 โ
โ) โ (((๐ด
ยท 1) + (๐ต ยท
1)) < (๐ด ยท ๐ต) โ (((๐ด ยท 1) + (๐ต ยท 1)) + 1) < ((๐ด ยท ๐ต) + 1))) |
45 | 2, 44 | mp3an3 1451 |
. . . . . 6
โข ((((๐ด ยท 1) + (๐ต ยท 1)) โ โ
โง (๐ด ยท ๐ต) โ โ) โ
(((๐ด ยท 1) + (๐ต ยท 1)) < (๐ด ยท ๐ต) โ (((๐ด ยท 1) + (๐ต ยท 1)) + 1) < ((๐ด ยท ๐ต) + 1))) |
46 | 32, 33, 45 | syl2anc 585 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด ยท 1) + (๐ต ยท 1)) < (๐ด ยท ๐ต) โ (((๐ด ยท 1) + (๐ต ยท 1)) + 1) < ((๐ด ยท ๐ต) + 1))) |
47 | | ax-1rid 11122 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด ยท 1) = ๐ด) |
48 | | ax-1rid 11122 |
. . . . . . 7
โข (๐ต โ โ โ (๐ต ยท 1) = ๐ต) |
49 | 47, 48 | oveqan12d 7377 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท 1) + (๐ต ยท 1)) = (๐ด + ๐ต)) |
50 | 49 | breq1d 5116 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด ยท 1) + (๐ต ยท 1)) < (๐ด ยท ๐ต) โ (๐ด + ๐ต) < (๐ด ยท ๐ต))) |
51 | 46, 50 | bitr3d 281 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด ยท 1) + (๐ต ยท 1)) + 1) < ((๐ด ยท ๐ต) + 1) โ (๐ด + ๐ต) < (๐ด ยท ๐ต))) |
52 | 26, 43, 51 | 3bitrd 305 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (1 <
((๐ด โ 1) ยท
(๐ต โ 1)) โ
(๐ด + ๐ต) < (๐ด ยท ๐ต))) |
53 | 18, 52 | sylibd 238 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2 <
๐ด โง 2 < ๐ต) โ (๐ด + ๐ต) < (๐ด ยท ๐ต))) |
54 | 53 | imp 408 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (2 <
๐ด โง 2 < ๐ต)) โ (๐ด + ๐ต) < (๐ด ยท ๐ต)) |