Step | Hyp | Ref
| Expression |
1 | | 0re 11158 |
. . . . 5
โข 0 โ
โ |
2 | 1 | a1i 11 |
. . . 4
โข ((๐ โง (๐ดโ2) โค ๐ด) โ 0 โ โ) |
3 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ด โค 1) โ ยฌ ๐ด โค 1) |
4 | | 1red 11157 |
. . . . . . . . . 10
โข ((๐ โง ยฌ ๐ด โค 1) โ 1 โ
โ) |
5 | | sqrlearg.1 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ โ) |
6 | 5 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ยฌ ๐ด โค 1) โ ๐ด โ โ) |
7 | 4, 6 | ltnled 11303 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ด โค 1) โ (1 < ๐ด โ ยฌ ๐ด โค 1)) |
8 | 3, 7 | mpbird 257 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ด โค 1) โ 1 < ๐ด) |
9 | | 1red 11157 |
. . . . . . . . . 10
โข ((๐ โง 1 < ๐ด) โ 1 โ โ) |
10 | 5 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง 1 < ๐ด) โ ๐ด โ โ) |
11 | 1 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โง 1 < ๐ด) โ 0 โ โ) |
12 | | 0lt1 11678 |
. . . . . . . . . . . . 13
โข 0 <
1 |
13 | 12 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โง 1 < ๐ด) โ 0 < 1) |
14 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โง 1 < ๐ด) โ 1 < ๐ด) |
15 | 11, 9, 10, 13, 14 | lttrd 11317 |
. . . . . . . . . . 11
โข ((๐ โง 1 < ๐ด) โ 0 < ๐ด) |
16 | 10, 15 | elrpd 12955 |
. . . . . . . . . 10
โข ((๐ โง 1 < ๐ด) โ ๐ด โ
โ+) |
17 | 9, 10, 16, 14 | ltmul2dd 13014 |
. . . . . . . . 9
โข ((๐ โง 1 < ๐ด) โ (๐ด ยท 1) < (๐ด ยท ๐ด)) |
18 | 5 | recnd 11184 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
19 | 18 | mulid1d 11173 |
. . . . . . . . . . 11
โข (๐ โ (๐ด ยท 1) = ๐ด) |
20 | 19 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง 1 < ๐ด) โ (๐ด ยท 1) = ๐ด) |
21 | 18 | sqvald 14049 |
. . . . . . . . . . . 12
โข (๐ โ (๐ดโ2) = (๐ด ยท ๐ด)) |
22 | 21 | eqcomd 2743 |
. . . . . . . . . . 11
โข (๐ โ (๐ด ยท ๐ด) = (๐ดโ2)) |
23 | 22 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง 1 < ๐ด) โ (๐ด ยท ๐ด) = (๐ดโ2)) |
24 | 20, 23 | breq12d 5119 |
. . . . . . . . 9
โข ((๐ โง 1 < ๐ด) โ ((๐ด ยท 1) < (๐ด ยท ๐ด) โ ๐ด < (๐ดโ2))) |
25 | 17, 24 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง 1 < ๐ด) โ ๐ด < (๐ดโ2)) |
26 | 8, 25 | syldan 592 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ด โค 1) โ ๐ด < (๐ดโ2)) |
27 | 26 | adantlr 714 |
. . . . . 6
โข (((๐ โง (๐ดโ2) โค ๐ด) โง ยฌ ๐ด โค 1) โ ๐ด < (๐ดโ2)) |
28 | | simpr 486 |
. . . . . . . 8
โข ((๐ โง (๐ดโ2) โค ๐ด) โ (๐ดโ2) โค ๐ด) |
29 | 5 | resqcld 14031 |
. . . . . . . . . 10
โข (๐ โ (๐ดโ2) โ โ) |
30 | 29 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ดโ2) โค ๐ด) โ (๐ดโ2) โ โ) |
31 | 5 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ดโ2) โค ๐ด) โ ๐ด โ โ) |
32 | 30, 31 | lenltd 11302 |
. . . . . . . 8
โข ((๐ โง (๐ดโ2) โค ๐ด) โ ((๐ดโ2) โค ๐ด โ ยฌ ๐ด < (๐ดโ2))) |
33 | 28, 32 | mpbid 231 |
. . . . . . 7
โข ((๐ โง (๐ดโ2) โค ๐ด) โ ยฌ ๐ด < (๐ดโ2)) |
34 | 33 | adantr 482 |
. . . . . 6
โข (((๐ โง (๐ดโ2) โค ๐ด) โง ยฌ ๐ด โค 1) โ ยฌ ๐ด < (๐ดโ2)) |
35 | 27, 34 | condan 817 |
. . . . 5
โข ((๐ โง (๐ดโ2) โค ๐ด) โ ๐ด โค 1) |
36 | | 1red 11157 |
. . . . 5
โข ((๐ โง ๐ด โค 1) โ 1 โ
โ) |
37 | 35, 36 | syldan 592 |
. . . 4
โข ((๐ โง (๐ดโ2) โค ๐ด) โ 1 โ โ) |
38 | 31 | sqge0d 14043 |
. . . . 5
โข ((๐ โง (๐ดโ2) โค ๐ด) โ 0 โค (๐ดโ2)) |
39 | 2, 30, 31, 38, 28 | letrd 11313 |
. . . 4
โข ((๐ โง (๐ดโ2) โค ๐ด) โ 0 โค ๐ด) |
40 | 2, 37, 31, 39, 35 | eliccd 43749 |
. . 3
โข ((๐ โง (๐ดโ2) โค ๐ด) โ ๐ด โ (0[,]1)) |
41 | 40 | ex 414 |
. 2
โข (๐ โ ((๐ดโ2) โค ๐ด โ ๐ด โ (0[,]1))) |
42 | | unitssre 13417 |
. . . . . . 7
โข (0[,]1)
โ โ |
43 | 42 | sseli 3941 |
. . . . . 6
โข (๐ด โ (0[,]1) โ ๐ด โ
โ) |
44 | | 1red 11157 |
. . . . . 6
โข (๐ด โ (0[,]1) โ 1 โ
โ) |
45 | | 0xr 11203 |
. . . . . . . 8
โข 0 โ
โ* |
46 | 45 | a1i 11 |
. . . . . . 7
โข (๐ด โ (0[,]1) โ 0 โ
โ*) |
47 | 44 | rexrd 11206 |
. . . . . . 7
โข (๐ด โ (0[,]1) โ 1 โ
โ*) |
48 | | id 22 |
. . . . . . 7
โข (๐ด โ (0[,]1) โ ๐ด โ
(0[,]1)) |
49 | 46, 47, 48 | iccgelbd 43788 |
. . . . . 6
โข (๐ด โ (0[,]1) โ 0 โค
๐ด) |
50 | 46, 47, 48 | iccleubd 43793 |
. . . . . 6
โข (๐ด โ (0[,]1) โ ๐ด โค 1) |
51 | 43, 44, 43, 49, 50 | lemul2ad 12096 |
. . . . 5
โข (๐ด โ (0[,]1) โ (๐ด ยท ๐ด) โค (๐ด ยท 1)) |
52 | 51 | adantl 483 |
. . . 4
โข ((๐ โง ๐ด โ (0[,]1)) โ (๐ด ยท ๐ด) โค (๐ด ยท 1)) |
53 | 22 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ด โ (0[,]1)) โ (๐ด ยท ๐ด) = (๐ดโ2)) |
54 | 19 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ด โ (0[,]1)) โ (๐ด ยท 1) = ๐ด) |
55 | 53, 54 | breq12d 5119 |
. . . 4
โข ((๐ โง ๐ด โ (0[,]1)) โ ((๐ด ยท ๐ด) โค (๐ด ยท 1) โ (๐ดโ2) โค ๐ด)) |
56 | 52, 55 | mpbid 231 |
. . 3
โข ((๐ โง ๐ด โ (0[,]1)) โ (๐ดโ2) โค ๐ด) |
57 | 56 | ex 414 |
. 2
โข (๐ โ (๐ด โ (0[,]1) โ (๐ดโ2) โค ๐ด)) |
58 | 41, 57 | impbid 211 |
1
โข (๐ โ ((๐ดโ2) โค ๐ด โ ๐ด โ (0[,]1))) |