Step | Hyp | Ref
| Expression |
1 | | 2xp3dxp2ge1d.1 |
. . . . . . . 8
โข (๐ โ ๐ โ (-1[,)+โ)) |
2 | | neg1rr 12273 |
. . . . . . . . 9
โข -1 โ
โ |
3 | | elicopnf 13368 |
. . . . . . . . 9
โข (-1
โ โ โ (๐
โ (-1[,)+โ) โ (๐ โ โ โง -1 โค ๐))) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . 8
โข (๐ โ (-1[,)+โ) โ
(๐ โ โ โง -1
โค ๐)) |
5 | 1, 4 | sylib 217 |
. . . . . . 7
โข (๐ โ (๐ โ โ โง -1 โค ๐)) |
6 | 5 | simpld 496 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
7 | | 2re 12232 |
. . . . . . 7
โข 2 โ
โ |
8 | | readdcl 11139 |
. . . . . . 7
โข ((๐ โ โ โง 2 โ
โ) โ (๐ + 2)
โ โ) |
9 | 7, 8 | mpan2 690 |
. . . . . 6
โข (๐ โ โ โ (๐ + 2) โ
โ) |
10 | 6, 9 | syl 17 |
. . . . 5
โข (๐ โ (๐ + 2) โ โ) |
11 | | neg1cn 12272 |
. . . . . . . . . 10
โข -1 โ
โ |
12 | | 2cn 12233 |
. . . . . . . . . 10
โข 2 โ
โ |
13 | | addcom 11346 |
. . . . . . . . . 10
โข ((-1
โ โ โง 2 โ โ) โ (-1 + 2) = (2 +
-1)) |
14 | 11, 12, 13 | mp2an 691 |
. . . . . . . . 9
โข (-1 + 2)
= (2 + -1) |
15 | | ax-1cn 11114 |
. . . . . . . . . 10
โข 1 โ
โ |
16 | | negsub 11454 |
. . . . . . . . . 10
โข ((2
โ โ โง 1 โ โ) โ (2 + -1) = (2 โ
1)) |
17 | 12, 15, 16 | mp2an 691 |
. . . . . . . . 9
โข (2 + -1)
= (2 โ 1) |
18 | | 2m1e1 12284 |
. . . . . . . . 9
โข (2
โ 1) = 1 |
19 | 14, 17, 18 | 3eqtri 2765 |
. . . . . . . 8
โข (-1 + 2)
= 1 |
20 | 5 | simprd 497 |
. . . . . . . . 9
โข (๐ โ -1 โค ๐) |
21 | | leadd1 11628 |
. . . . . . . . . . 11
โข ((-1
โ โ โง ๐
โ โ โง 2 โ โ) โ (-1 โค ๐ โ (-1 + 2) โค (๐ + 2))) |
22 | 2, 7, 21 | mp3an13 1453 |
. . . . . . . . . 10
โข (๐ โ โ โ (-1 โค
๐ โ (-1 + 2) โค
(๐ + 2))) |
23 | 6, 22 | syl 17 |
. . . . . . . . 9
โข (๐ โ (-1 โค ๐ โ (-1 + 2) โค (๐ + 2))) |
24 | 20, 23 | mpbid 231 |
. . . . . . . 8
โข (๐ โ (-1 + 2) โค (๐ + 2)) |
25 | 19, 24 | eqbrtrrid 5142 |
. . . . . . 7
โข (๐ โ 1 โค (๐ + 2)) |
26 | | 0lt1 11682 |
. . . . . . 7
โข 0 <
1 |
27 | 25, 26 | jctil 521 |
. . . . . 6
โข (๐ โ (0 < 1 โง 1 โค
(๐ + 2))) |
28 | | 0re 11162 |
. . . . . . . 8
โข 0 โ
โ |
29 | | 1re 11160 |
. . . . . . . 8
โข 1 โ
โ |
30 | | ltletr 11252 |
. . . . . . . 8
โข ((0
โ โ โง 1 โ โ โง (๐ + 2) โ โ) โ ((0 < 1
โง 1 โค (๐ + 2))
โ 0 < (๐ +
2))) |
31 | 28, 29, 30 | mp3an12 1452 |
. . . . . . 7
โข ((๐ + 2) โ โ โ ((0
< 1 โง 1 โค (๐ +
2)) โ 0 < (๐ +
2))) |
32 | 10, 31 | syl 17 |
. . . . . 6
โข (๐ โ ((0 < 1 โง 1 โค
(๐ + 2)) โ 0 <
(๐ + 2))) |
33 | 27, 32 | mpd 15 |
. . . . 5
โข (๐ โ 0 < (๐ + 2)) |
34 | 10, 33 | jca 513 |
. . . 4
โข (๐ โ ((๐ + 2) โ โ โง 0 < (๐ + 2))) |
35 | | elrp 12922 |
. . . . 5
โข ((๐ + 2) โ โ+
โ ((๐ + 2) โ
โ โง 0 < (๐ +
2))) |
36 | 35 | imbi2i 336 |
. . . 4
โข ((๐ โ (๐ + 2) โ โ+) โ
(๐ โ ((๐ + 2) โ โ โง 0 < (๐ + 2)))) |
37 | 34, 36 | mpbir 230 |
. . 3
โข (๐ โ (๐ + 2) โ
โ+) |
38 | | remulcl 11141 |
. . . . . 6
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
39 | 7, 38 | mpan 689 |
. . . . 5
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
40 | 6, 39 | syl 17 |
. . . 4
โข (๐ โ (2 ยท ๐) โ
โ) |
41 | | 3re 12238 |
. . . . 5
โข 3 โ
โ |
42 | | readdcl 11139 |
. . . . 5
โข (((2
ยท ๐) โ โ
โง 3 โ โ) โ ((2 ยท ๐) + 3) โ โ) |
43 | 41, 42 | mpan2 690 |
. . . 4
โข ((2
ยท ๐) โ โ
โ ((2 ยท ๐) + 3)
โ โ) |
44 | 40, 43 | syl 17 |
. . 3
โข (๐ โ ((2 ยท ๐) + 3) โ
โ) |
45 | 7 | a1i 11 |
. . . . 5
โข (๐ โ 2 โ
โ) |
46 | | 1red 11161 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
47 | 40, 46 | readdcld 11189 |
. . . . 5
โข (๐ โ ((2 ยท ๐) + 1) โ
โ) |
48 | | recn 11146 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
49 | | addid1 11340 |
. . . . . . . 8
โข (๐ โ โ โ (๐ + 0) = ๐) |
50 | 48, 49 | syl 17 |
. . . . . . 7
โข (๐ โ โ โ (๐ + 0) = ๐) |
51 | 6, 50 | syl 17 |
. . . . . 6
โข (๐ โ (๐ + 0) = ๐) |
52 | 11, 15 | addcomi 11351 |
. . . . . . . . . 10
โข (-1 + 1)
= (1 + -1) |
53 | 15 | negidi 11475 |
. . . . . . . . . 10
โข (1 + -1)
= 0 |
54 | 52, 53 | eqtri 2761 |
. . . . . . . . 9
โข (-1 + 1)
= 0 |
55 | | leadd1 11628 |
. . . . . . . . . . . 12
โข ((-1
โ โ โง ๐
โ โ โง 1 โ โ) โ (-1 โค ๐ โ (-1 + 1) โค (๐ + 1))) |
56 | 2, 29, 55 | mp3an13 1453 |
. . . . . . . . . . 11
โข (๐ โ โ โ (-1 โค
๐ โ (-1 + 1) โค
(๐ + 1))) |
57 | 6, 56 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (-1 โค ๐ โ (-1 + 1) โค (๐ + 1))) |
58 | 20, 57 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ (-1 + 1) โค (๐ + 1)) |
59 | 54, 58 | eqbrtrrid 5142 |
. . . . . . . 8
โข (๐ โ 0 โค (๐ + 1)) |
60 | | readdcl 11139 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 1 โ
โ) โ (๐ + 1)
โ โ) |
61 | 29, 60 | mpan2 690 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ + 1) โ
โ) |
62 | 6, 61 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ + 1) โ โ) |
63 | 62, 6 | jca 513 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) โ โ โง ๐ โ โ)) |
64 | | leadd2 11629 |
. . . . . . . . . 10
โข ((0
โ โ โง (๐ +
1) โ โ โง ๐
โ โ) โ (0 โค (๐ + 1) โ (๐ + 0) โค (๐ + (๐ + 1)))) |
65 | 28, 64 | mp3an1 1449 |
. . . . . . . . 9
โข (((๐ + 1) โ โ โง ๐ โ โ) โ (0 โค
(๐ + 1) โ (๐ + 0) โค (๐ + (๐ + 1)))) |
66 | 63, 65 | syl 17 |
. . . . . . . 8
โข (๐ โ (0 โค (๐ + 1) โ (๐ + 0) โค (๐ + (๐ + 1)))) |
67 | 59, 66 | mpbid 231 |
. . . . . . 7
โข (๐ โ (๐ + 0) โค (๐ + (๐ + 1))) |
68 | 6, 48 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
69 | 68 | 2timesd 12401 |
. . . . . . . . 9
โข (๐ โ (2 ยท ๐) = (๐ + ๐)) |
70 | 69 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐) + 1) = ((๐ + ๐) + 1)) |
71 | | addass 11143 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ โง 1 โ
โ) โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
72 | 15, 71 | mp3an3 1451 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
73 | 72 | anidms 568 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
74 | 68, 73 | syl 17 |
. . . . . . . 8
โข (๐ โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
75 | 70, 74 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ ((2 ยท ๐) + 1) = (๐ + (๐ + 1))) |
76 | 67, 75 | breqtrrd 5134 |
. . . . . 6
โข (๐ โ (๐ + 0) โค ((2 ยท ๐) + 1)) |
77 | 51, 76 | eqbrtrrd 5130 |
. . . . 5
โข (๐ โ ๐ โค ((2 ยท ๐) + 1)) |
78 | 45 | leidd 11726 |
. . . . 5
โข (๐ โ 2 โค 2) |
79 | 6, 45, 47, 45, 77, 78 | le2addd 11779 |
. . . 4
โข (๐ โ (๐ + 2) โค (((2 ยท ๐) + 1) + 2)) |
80 | 40 | recnd 11188 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โ) |
81 | 15 | a1i 11 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
82 | 12 | a1i 11 |
. . . . . 6
โข (๐ โ 2 โ
โ) |
83 | 80, 81, 82 | addassd 11182 |
. . . . 5
โข (๐ โ (((2 ยท ๐) + 1) + 2) = ((2 ยท ๐) + (1 + 2))) |
84 | | 1p2e3 12301 |
. . . . . 6
โข (1 + 2) =
3 |
85 | | oveq2 7366 |
. . . . . 6
โข ((1 + 2)
= 3 โ ((2 ยท ๐)
+ (1 + 2)) = ((2 ยท ๐) + 3)) |
86 | 84, 85 | ax-mp 5 |
. . . . 5
โข ((2
ยท ๐) + (1 + 2)) =
((2 ยท ๐) +
3) |
87 | 83, 86 | eqtrdi 2789 |
. . . 4
โข (๐ โ (((2 ยท ๐) + 1) + 2) = ((2 ยท ๐) + 3)) |
88 | 79, 87 | breqtrd 5132 |
. . 3
โข (๐ โ (๐ + 2) โค ((2 ยท ๐) + 3)) |
89 | 37, 44, 88 | 3jca 1129 |
. 2
โข (๐ โ ((๐ + 2) โ โ+ โง ((2
ยท ๐) + 3) โ
โ โง (๐ + 2) โค
((2 ยท ๐) +
3))) |
90 | | divge1 12988 |
. 2
โข (((๐ + 2) โ โ+
โง ((2 ยท ๐) + 3)
โ โ โง (๐ +
2) โค ((2 ยท ๐) +
3)) โ 1 โค (((2 ยท ๐) + 3) / (๐ + 2))) |
91 | 89, 90 | syl 17 |
1
โข (๐ โ 1 โค (((2 ยท ๐) + 3) / (๐ + 2))) |