Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
โข ((๐ด โ โ โง 2 <
๐ด) โ 2 < ๐ด) |
2 | | 2re 12235 |
. . . . . . . 8
โข 2 โ
โ |
3 | 2 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง 2 <
๐ด) โ 2 โ
โ) |
4 | | simpl 484 |
. . . . . . 7
โข ((๐ด โ โ โง 2 <
๐ด) โ ๐ด โ โ) |
5 | | 1re 11163 |
. . . . . . . 8
โข 1 โ
โ |
6 | 5 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง 2 <
๐ด) โ 1 โ
โ) |
7 | | ltsub1 11659 |
. . . . . . 7
โข ((2
โ โ โง ๐ด
โ โ โง 1 โ โ) โ (2 < ๐ด โ (2 โ 1) < (๐ด โ 1))) |
8 | 3, 4, 6, 7 | syl3anc 1372 |
. . . . . 6
โข ((๐ด โ โ โง 2 <
๐ด) โ (2 < ๐ด โ (2 โ 1) <
(๐ด โ
1))) |
9 | | 2cn 12236 |
. . . . . . . . 9
โข 2 โ
โ |
10 | | ax-1cn 11117 |
. . . . . . . . 9
โข 1 โ
โ |
11 | | df-2 12224 |
. . . . . . . . . 10
โข 2 = (1 +
1) |
12 | 11 | eqcomi 2742 |
. . . . . . . . 9
โข (1 + 1) =
2 |
13 | 9, 10, 10, 12 | subaddrii 11498 |
. . . . . . . 8
โข (2
โ 1) = 1 |
14 | 13 | breq1i 5116 |
. . . . . . 7
โข ((2
โ 1) < (๐ด โ
1) โ 1 < (๐ด โ
1)) |
15 | 14 | a1i 11 |
. . . . . 6
โข ((๐ด โ โ โง 2 <
๐ด) โ ((2 โ 1)
< (๐ด โ 1) โ 1
< (๐ด โ
1))) |
16 | 8, 15 | bitrd 279 |
. . . . 5
โข ((๐ด โ โ โง 2 <
๐ด) โ (2 < ๐ด โ 1 < (๐ด โ 1))) |
17 | 1, 16 | mpbid 231 |
. . . 4
โข ((๐ด โ โ โง 2 <
๐ด) โ 1 < (๐ด โ 1)) |
18 | | simpr 486 |
. . . . 5
โข ((๐ต โ โ โง 2 <
๐ต) โ 2 < ๐ต) |
19 | 2 | a1i 11 |
. . . . . . 7
โข ((๐ต โ โ โง 2 <
๐ต) โ 2 โ
โ) |
20 | | simpl 484 |
. . . . . . 7
โข ((๐ต โ โ โง 2 <
๐ต) โ ๐ต โ โ) |
21 | 5 | a1i 11 |
. . . . . . 7
โข ((๐ต โ โ โง 2 <
๐ต) โ 1 โ
โ) |
22 | | ltsub1 11659 |
. . . . . . 7
โข ((2
โ โ โง ๐ต
โ โ โง 1 โ โ) โ (2 < ๐ต โ (2 โ 1) < (๐ต โ 1))) |
23 | 19, 20, 21, 22 | syl3anc 1372 |
. . . . . 6
โข ((๐ต โ โ โง 2 <
๐ต) โ (2 < ๐ต โ (2 โ 1) <
(๐ต โ
1))) |
24 | 13 | breq1i 5116 |
. . . . . . 7
โข ((2
โ 1) < (๐ต โ
1) โ 1 < (๐ต โ
1)) |
25 | 24 | a1i 11 |
. . . . . 6
โข ((๐ต โ โ โง 2 <
๐ต) โ ((2 โ 1)
< (๐ต โ 1) โ 1
< (๐ต โ
1))) |
26 | 23, 25 | bitrd 279 |
. . . . 5
โข ((๐ต โ โ โง 2 <
๐ต) โ (2 < ๐ต โ 1 < (๐ต โ 1))) |
27 | 18, 26 | mpbid 231 |
. . . 4
โข ((๐ต โ โ โง 2 <
๐ต) โ 1 < (๐ต โ 1)) |
28 | 17, 27 | anim12i 614 |
. . 3
โข (((๐ด โ โ โง 2 <
๐ด) โง (๐ต โ โ โง 2 < ๐ต)) โ (1 < (๐ด โ 1) โง 1 < (๐ต โ 1))) |
29 | 28 | an4s 659 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (2 <
๐ด โง 2 < ๐ต)) โ (1 < (๐ด โ 1) โง 1 < (๐ต โ 1))) |
30 | | peano2rem 11476 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ด โ 1) โ
โ) |
31 | | peano2rem 11476 |
. . . . . . . 8
โข (๐ต โ โ โ (๐ต โ 1) โ
โ) |
32 | 30, 31 | anim12i 614 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ 1) โ โ โง
(๐ต โ 1) โ
โ)) |
33 | 32 | anim1i 616 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (1 <
(๐ด โ 1) โง 1 <
(๐ต โ 1))) โ
(((๐ด โ 1) โ
โ โง (๐ต โ 1)
โ โ) โง (1 < (๐ด โ 1) โง 1 < (๐ต โ 1)))) |
34 | | mulgt1 12022 |
. . . . . 6
โข ((((๐ด โ 1) โ โ โง
(๐ต โ 1) โ
โ) โง (1 < (๐ด
โ 1) โง 1 < (๐ต
โ 1))) โ 1 < ((๐ด โ 1) ยท (๐ต โ 1))) |
35 | 33, 34 | syl 17 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (1 <
(๐ด โ 1) โง 1 <
(๐ต โ 1))) โ 1
< ((๐ด โ 1)
ยท (๐ต โ
1))) |
36 | 35 | ex 414 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 <
(๐ด โ 1) โง 1 <
(๐ต โ 1)) โ 1
< ((๐ด โ 1)
ยท (๐ต โ
1)))) |
37 | 36 | adantr 482 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (2 <
๐ด โง 2 < ๐ต)) โ ((1 < (๐ด โ 1) โง 1 < (๐ต โ 1)) โ 1 <
((๐ด โ 1) ยท
(๐ต โ
1)))) |
38 | | recn 11149 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ) |
39 | 10 | a1i 11 |
. . . . . . . . 9
โข (๐ด โ โ โ 1 โ
โ) |
40 | 38, 39 | jca 513 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ด โ โ โง 1 โ
โ)) |
41 | | recn 11149 |
. . . . . . . . 9
โข (๐ต โ โ โ ๐ต โ
โ) |
42 | 10 | a1i 11 |
. . . . . . . . 9
โข (๐ต โ โ โ 1 โ
โ) |
43 | 41, 42 | jca 513 |
. . . . . . . 8
โข (๐ต โ โ โ (๐ต โ โ โง 1 โ
โ)) |
44 | 40, 43 | anim12i 614 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ โ โง 1 โ
โ) โง (๐ต โ
โ โง 1 โ โ))) |
45 | | mulsub 11606 |
. . . . . . 7
โข (((๐ด โ โ โง 1 โ
โ) โง (๐ต โ
โ โง 1 โ โ)) โ ((๐ด โ 1) ยท (๐ต โ 1)) = (((๐ด ยท ๐ต) + (1 ยท 1)) โ ((๐ด ยท 1) + (๐ต ยท 1)))) |
46 | 44, 45 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ 1) ยท (๐ต โ 1)) = (((๐ด ยท ๐ต) + (1 ยท 1)) โ ((๐ด ยท 1) + (๐ต ยท 1)))) |
47 | 46 | breq2d 5121 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (1 <
((๐ด โ 1) ยท
(๐ต โ 1)) โ 1
< (((๐ด ยท ๐ต) + (1 ยท 1)) โ
((๐ด ยท 1) + (๐ต ยท
1))))) |
48 | 47 | biimpd 228 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (1 <
((๐ด โ 1) ยท
(๐ต โ 1)) โ 1
< (((๐ด ยท ๐ต) + (1 ยท 1)) โ
((๐ด ยท 1) + (๐ต ยท
1))))) |
49 | 48 | adantr 482 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (2 <
๐ด โง 2 < ๐ต)) โ (1 < ((๐ด โ 1) ยท (๐ต โ 1)) โ 1 <
(((๐ด ยท ๐ต) + (1 ยท 1)) โ
((๐ด ยท 1) + (๐ต ยท
1))))) |
50 | 10 | mulid2i 11168 |
. . . . . . . . 9
โข (1
ยท 1) = 1 |
51 | | eqcom 2740 |
. . . . . . . . . 10
โข ((1
ยท 1) = 1 โ 1 = (1 ยท 1)) |
52 | 51 | biimpi 215 |
. . . . . . . . 9
โข ((1
ยท 1) = 1 โ 1 = (1 ยท 1)) |
53 | 50, 52 | mp1i 13 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ 1 = (1
ยท 1)) |
54 | 53 | oveq2d 7377 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) + 1) = ((๐ด ยท ๐ต) + (1 ยท 1))) |
55 | | mulid1 11161 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (๐ด ยท 1) = ๐ด) |
56 | | eqcom 2740 |
. . . . . . . . . . . 12
โข ((๐ด ยท 1) = ๐ด โ ๐ด = (๐ด ยท 1)) |
57 | 56 | biimpi 215 |
. . . . . . . . . . 11
โข ((๐ด ยท 1) = ๐ด โ ๐ด = (๐ด ยท 1)) |
58 | 55, 57 | syl 17 |
. . . . . . . . . 10
โข (๐ด โ โ โ ๐ด = (๐ด ยท 1)) |
59 | 38, 58 | syl 17 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด = (๐ด ยท 1)) |
60 | 59 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด = (๐ด ยท 1)) |
61 | | mulid1 11161 |
. . . . . . . . . . 11
โข (๐ต โ โ โ (๐ต ยท 1) = ๐ต) |
62 | 41, 61 | syl 17 |
. . . . . . . . . 10
โข (๐ต โ โ โ (๐ต ยท 1) = ๐ต) |
63 | | eqcom 2740 |
. . . . . . . . . . 11
โข ((๐ต ยท 1) = ๐ต โ ๐ต = (๐ต ยท 1)) |
64 | 63 | biimpi 215 |
. . . . . . . . . 10
โข ((๐ต ยท 1) = ๐ต โ ๐ต = (๐ต ยท 1)) |
65 | 62, 64 | syl 17 |
. . . . . . . . 9
โข (๐ต โ โ โ ๐ต = (๐ต ยท 1)) |
66 | 65 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต = (๐ต ยท 1)) |
67 | 60, 66 | oveq12d 7379 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) = ((๐ด ยท 1) + (๐ต ยท 1))) |
68 | 54, 67 | oveq12d 7379 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด ยท ๐ต) + 1) โ (๐ด + ๐ต)) = (((๐ด ยท ๐ต) + (1 ยท 1)) โ ((๐ด ยท 1) + (๐ต ยท 1)))) |
69 | 68 | breq2d 5121 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (1 <
(((๐ด ยท ๐ต) + 1) โ (๐ด + ๐ต)) โ 1 < (((๐ด ยท ๐ต) + (1 ยท 1)) โ ((๐ด ยท 1) + (๐ต ยท
1))))) |
70 | | readdcl 11142 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
71 | 5 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ 1 โ
โ) |
72 | | remulcl 11144 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
73 | | readdcl 11142 |
. . . . . . . 8
โข (((๐ด ยท ๐ต) โ โ โง 1 โ โ)
โ ((๐ด ยท ๐ต) + 1) โ
โ) |
74 | 72, 71, 73 | syl2anc 585 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) + 1) โ โ) |
75 | | ltaddsub2 11638 |
. . . . . . 7
โข (((๐ด + ๐ต) โ โ โง 1 โ โ
โง ((๐ด ยท ๐ต) + 1) โ โ) โ
(((๐ด + ๐ต) + 1) < ((๐ด ยท ๐ต) + 1) โ 1 < (((๐ด ยท ๐ต) + 1) โ (๐ด + ๐ต)))) |
76 | 70, 71, 74, 75 | syl3anc 1372 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) + 1) < ((๐ด ยท ๐ต) + 1) โ 1 < (((๐ด ยท ๐ต) + 1) โ (๐ด + ๐ต)))) |
77 | | ltadd1 11630 |
. . . . . . . . 9
โข (((๐ด + ๐ต) โ โ โง (๐ด ยท ๐ต) โ โ โง 1 โ โ)
โ ((๐ด + ๐ต) < (๐ด ยท ๐ต) โ ((๐ด + ๐ต) + 1) < ((๐ด ยท ๐ต) + 1))) |
78 | 70, 72, 71, 77 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) < (๐ด ยท ๐ต) โ ((๐ด + ๐ต) + 1) < ((๐ด ยท ๐ต) + 1))) |
79 | 78 | bicomd 222 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) + 1) < ((๐ด ยท ๐ต) + 1) โ (๐ด + ๐ต) < (๐ด ยท ๐ต))) |
80 | 79 | biimpd 228 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) + 1) < ((๐ด ยท ๐ต) + 1) โ (๐ด + ๐ต) < (๐ด ยท ๐ต))) |
81 | 76, 80 | sylbird 260 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (1 <
(((๐ด ยท ๐ต) + 1) โ (๐ด + ๐ต)) โ (๐ด + ๐ต) < (๐ด ยท ๐ต))) |
82 | 69, 81 | sylbird 260 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (1 <
(((๐ด ยท ๐ต) + (1 ยท 1)) โ
((๐ด ยท 1) + (๐ต ยท 1))) โ (๐ด + ๐ต) < (๐ด ยท ๐ต))) |
83 | 82 | adantr 482 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (2 <
๐ด โง 2 < ๐ต)) โ (1 < (((๐ด ยท ๐ต) + (1 ยท 1)) โ ((๐ด ยท 1) + (๐ต ยท 1))) โ (๐ด + ๐ต) < (๐ด ยท ๐ต))) |
84 | 37, 49, 83 | 3syld 60 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (2 <
๐ด โง 2 < ๐ต)) โ ((1 < (๐ด โ 1) โง 1 < (๐ต โ 1)) โ (๐ด + ๐ต) < (๐ด ยท ๐ต))) |
85 | 29, 84 | mpd 15 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (2 <
๐ด โง 2 < ๐ต)) โ (๐ด + ๐ต) < (๐ด ยท ๐ต)) |