Step | Hyp | Ref
| Expression |
1 | | 3cubeslem1.a |
. . . . 5
โข (๐ โ ๐ด โ โ) |
2 | | qre 12933 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
โ) |
3 | 1, 2 | syl 17 |
. . . 4
โข (๐ โ ๐ด โ โ) |
4 | | 0red 11213 |
. . . 4
โข (๐ โ 0 โ
โ) |
5 | 3, 4 | lttri4d 11351 |
. . 3
โข (๐ โ (๐ด < 0 โจ ๐ด = 0 โจ 0 < ๐ด)) |
6 | | simpl 483 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด < 0) โ ๐ด โ
โ) |
7 | | 0red 11213 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด < 0) โ 0 โ
โ) |
8 | | peano2re 11383 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ด + 1) โ
โ) |
9 | 8 | adantr 481 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด < 0) โ (๐ด + 1) โ
โ) |
10 | 9 | resqcld 14086 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด < 0) โ ((๐ด + 1)โ2) โ
โ) |
11 | | simpr 485 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด < 0) โ ๐ด < 0) |
12 | 9 | sqge0d 14098 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด < 0) โ 0 โค ((๐ด + 1)โ2)) |
13 | 6, 7, 10, 11, 12 | ltletrd 11370 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด < 0) โ ๐ด < ((๐ด + 1)โ2)) |
14 | 13 | a1i 11 |
. . . . 5
โข (๐ โ ((๐ด โ โ โง ๐ด < 0) โ ๐ด < ((๐ด + 1)โ2))) |
15 | 3, 14 | mpand 693 |
. . . 4
โข (๐ โ (๐ด < 0 โ ๐ด < ((๐ด + 1)โ2))) |
16 | | 0lt1 11732 |
. . . . . . . 8
โข 0 <
1 |
17 | 16 | a1i 11 |
. . . . . . 7
โข (๐ด = 0 โ 0 <
1) |
18 | | id 22 |
. . . . . . 7
โข (๐ด = 0 โ ๐ด = 0) |
19 | | sq1 14155 |
. . . . . . . 8
โข
(1โ2) = 1 |
20 | 19 | a1i 11 |
. . . . . . 7
โข (๐ด = 0 โ (1โ2) =
1) |
21 | 17, 18, 20 | 3brtr4d 5179 |
. . . . . 6
โข (๐ด = 0 โ ๐ด < (1โ2)) |
22 | | 0cnd 11203 |
. . . . . . . . 9
โข (๐ด = 0 โ 0 โ
โ) |
23 | | 1cnd 11205 |
. . . . . . . . 9
โข (๐ด = 0 โ 1 โ
โ) |
24 | 18 | oveq1d 7420 |
. . . . . . . . 9
โข (๐ด = 0 โ (๐ด + 1) = (0 + 1)) |
25 | 22, 23, 24 | comraddd 11424 |
. . . . . . . 8
โข (๐ด = 0 โ (๐ด + 1) = (1 + 0)) |
26 | | 1p0e1 12332 |
. . . . . . . 8
โข (1 + 0) =
1 |
27 | 25, 26 | eqtrdi 2788 |
. . . . . . 7
โข (๐ด = 0 โ (๐ด + 1) = 1) |
28 | 27 | oveq1d 7420 |
. . . . . 6
โข (๐ด = 0 โ ((๐ด + 1)โ2) = (1โ2)) |
29 | 21, 28 | breqtrrd 5175 |
. . . . 5
โข (๐ด = 0 โ ๐ด < ((๐ด + 1)โ2)) |
30 | 29 | a1i 11 |
. . . 4
โข (๐ โ (๐ด = 0 โ ๐ด < ((๐ด + 1)โ2))) |
31 | | ax-1rid 11176 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ด ยท 1) = ๐ด) |
32 | 31 | adantr 481 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
๐ด) โ (๐ด ยท 1) = ๐ด) |
33 | | simpl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ โ) |
34 | | 1red 11211 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
๐ด) โ 1 โ
โ) |
35 | 33, 34 | readdcld 11239 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
๐ด) โ (๐ด + 1) โ
โ) |
36 | | simpr 485 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
๐ด) โ 0 < ๐ด) |
37 | | 0red 11213 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง 0 <
๐ด) โ 0 โ
โ) |
38 | | ltle 11298 |
. . . . . . . . . . . 12
โข ((0
โ โ โง ๐ด
โ โ) โ (0 < ๐ด โ 0 โค ๐ด)) |
39 | 37, 33, 38 | syl2anc 584 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
๐ด) โ (0 < ๐ด โ 0 โค ๐ด)) |
40 | 33 | ltp1d 12140 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด < (๐ด + 1)) |
41 | 39, 40 | jctird 527 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
๐ด) โ (0 < ๐ด โ (0 โค ๐ด โง ๐ด < (๐ด + 1)))) |
42 | 36, 41 | mpd 15 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
๐ด) โ (0 โค ๐ด โง ๐ด < (๐ด + 1))) |
43 | 34, 35 | jca 512 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
๐ด) โ (1 โ โ
โง (๐ด + 1) โ
โ)) |
44 | | 0le1 11733 |
. . . . . . . . . . 11
โข 0 โค
1 |
45 | 44 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
๐ด) โ 0 โค
1) |
46 | | 1e0p1 12715 |
. . . . . . . . . . 11
โข 1 = (0 +
1) |
47 | 37, 33, 34, 36 | ltadd1dd 11821 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
๐ด) โ (0 + 1) <
(๐ด + 1)) |
48 | 46, 47 | eqbrtrid 5182 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
๐ด) โ 1 < (๐ด + 1)) |
49 | 43, 45, 48 | jca32 516 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
๐ด) โ ((1 โ
โ โง (๐ด + 1)
โ โ) โง (0 โค 1 โง 1 < (๐ด + 1)))) |
50 | | ltmul12a 12066 |
. . . . . . . . 9
โข ((((๐ด โ โ โง (๐ด + 1) โ โ) โง (0
โค ๐ด โง ๐ด < (๐ด + 1))) โง ((1 โ โ โง
(๐ด + 1) โ โ)
โง (0 โค 1 โง 1 < (๐ด + 1)))) โ (๐ด ยท 1) < ((๐ด + 1) ยท (๐ด + 1))) |
51 | 33, 35, 42, 49, 50 | syl1111anc 838 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
๐ด) โ (๐ด ยท 1) < ((๐ด + 1) ยท (๐ด + 1))) |
52 | 32, 51 | eqbrtrrd 5171 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด < ((๐ด + 1) ยท (๐ด + 1))) |
53 | 35 | recnd 11238 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
๐ด) โ (๐ด + 1) โ
โ) |
54 | 53 | sqvald 14104 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
๐ด) โ ((๐ด + 1)โ2) = ((๐ด + 1) ยท (๐ด + 1))) |
55 | 52, 54 | breqtrrd 5175 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด < ((๐ด + 1)โ2)) |
56 | 55 | a1i 11 |
. . . . 5
โข (๐ โ ((๐ด โ โ โง 0 < ๐ด) โ ๐ด < ((๐ด + 1)โ2))) |
57 | 3, 56 | mpand 693 |
. . . 4
โข (๐ โ (0 < ๐ด โ ๐ด < ((๐ด + 1)โ2))) |
58 | 15, 30, 57 | 3jaod 1428 |
. . 3
โข (๐ โ ((๐ด < 0 โจ ๐ด = 0 โจ 0 < ๐ด) โ ๐ด < ((๐ด + 1)โ2))) |
59 | 5, 58 | mpd 15 |
. 2
โข (๐ โ ๐ด < ((๐ด + 1)โ2)) |
60 | 3, 8 | syl 17 |
. . . 4
โข (๐ โ (๐ด + 1) โ โ) |
61 | 60 | resqcld 14086 |
. . 3
โข (๐ โ ((๐ด + 1)โ2) โ
โ) |
62 | 3, 61 | posdifd 11797 |
. 2
โข (๐ โ (๐ด < ((๐ด + 1)โ2) โ 0 < (((๐ด + 1)โ2) โ ๐ด))) |
63 | 59, 62 | mpbid 231 |
1
โข (๐ โ 0 < (((๐ด + 1)โ2) โ ๐ด)) |