Step | Hyp | Ref
| Expression |
1 | | 6re 12244 |
. . . . . . 7
โข 6 โ
โ |
2 | 1 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ 6 โ
โ) |
3 | | id 22 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
4 | 2, 3, 3 | leadd2d 11751 |
. . . . 5
โข (๐ โ โ โ (6 โค
๐ โ (๐ + 6) โค (๐ + ๐))) |
5 | 4 | biimpa 478 |
. . . 4
โข ((๐ โ โ โง 6 โค
๐) โ (๐ + 6) โค (๐ + ๐)) |
6 | | recn 11142 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
7 | 6 | times2d 12398 |
. . . . 5
โข (๐ โ โ โ (๐ ยท 2) = (๐ + ๐)) |
8 | 7 | adantr 482 |
. . . 4
โข ((๐ โ โ โง 6 โค
๐) โ (๐ ยท 2) = (๐ + ๐)) |
9 | 5, 8 | breqtrrd 5134 |
. . 3
โข ((๐ โ โ โง 6 โค
๐) โ (๐ + 6) โค (๐ ยท 2)) |
10 | | 4cn 12239 |
. . . . . . . 8
โข 4 โ
โ |
11 | 10 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 4 โ
โ) |
12 | | 2cn 12229 |
. . . . . . . 8
โข 2 โ
โ |
13 | 12 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 2 โ
โ) |
14 | 6, 11, 13 | addassd 11178 |
. . . . . 6
โข (๐ โ โ โ ((๐ + 4) + 2) = (๐ + (4 + 2))) |
15 | | 4p2e6 12307 |
. . . . . . 7
โข (4 + 2) =
6 |
16 | 15 | oveq2i 7369 |
. . . . . 6
โข (๐ + (4 + 2)) = (๐ + 6) |
17 | 14, 16 | eqtrdi 2793 |
. . . . 5
โข (๐ โ โ โ ((๐ + 4) + 2) = (๐ + 6)) |
18 | 17 | breq1d 5116 |
. . . 4
โข (๐ โ โ โ (((๐ + 4) + 2) โค (๐ ยท 2) โ (๐ + 6) โค (๐ ยท 2))) |
19 | 18 | adantr 482 |
. . 3
โข ((๐ โ โ โง 6 โค
๐) โ (((๐ + 4) + 2) โค (๐ ยท 2) โ (๐ + 6) โค (๐ ยท 2))) |
20 | 9, 19 | mpbird 257 |
. 2
โข ((๐ โ โ โง 6 โค
๐) โ ((๐ + 4) + 2) โค (๐ ยท 2)) |
21 | | 4re 12238 |
. . . . . . . 8
โข 4 โ
โ |
22 | 21 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 4 โ
โ) |
23 | | 4ne0 12262 |
. . . . . . . 8
โข 4 โ
0 |
24 | 23 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 4 โ
0) |
25 | 3, 22, 24 | redivcld 11984 |
. . . . . 6
โข (๐ โ โ โ (๐ / 4) โ
โ) |
26 | | peano2re 11329 |
. . . . . 6
โข ((๐ / 4) โ โ โ
((๐ / 4) + 1) โ
โ) |
27 | 25, 26 | syl 17 |
. . . . 5
โข (๐ โ โ โ ((๐ / 4) + 1) โ
โ) |
28 | | peano2rem 11469 |
. . . . . 6
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
29 | 28 | rehalfcld 12401 |
. . . . 5
โข (๐ โ โ โ ((๐ โ 1) / 2) โ
โ) |
30 | | 4pos 12261 |
. . . . . . 7
โข 0 <
4 |
31 | 21, 30 | pm3.2i 472 |
. . . . . 6
โข (4 โ
โ โง 0 < 4) |
32 | 31 | a1i 11 |
. . . . 5
โข (๐ โ โ โ (4 โ
โ โง 0 < 4)) |
33 | | lemul1 12008 |
. . . . 5
โข ((((๐ / 4) + 1) โ โ โง
((๐ โ 1) / 2) โ
โ โง (4 โ โ โง 0 < 4)) โ (((๐ / 4) + 1) โค ((๐ โ 1) / 2) โ (((๐ / 4) + 1) ยท 4) โค (((๐ โ 1) / 2) ยท
4))) |
34 | 27, 29, 32, 33 | syl3anc 1372 |
. . . 4
โข (๐ โ โ โ (((๐ / 4) + 1) โค ((๐ โ 1) / 2) โ (((๐ / 4) + 1) ยท 4) โค
(((๐ โ 1) / 2)
ยท 4))) |
35 | 25 | recnd 11184 |
. . . . . 6
โข (๐ โ โ โ (๐ / 4) โ
โ) |
36 | | 1cnd 11151 |
. . . . . 6
โข (๐ โ โ โ 1 โ
โ) |
37 | 6, 11, 24 | divcan1d 11933 |
. . . . . . 7
โข (๐ โ โ โ ((๐ / 4) ยท 4) = ๐) |
38 | 10 | mulid2i 11161 |
. . . . . . . 8
โข (1
ยท 4) = 4 |
39 | 38 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ (1
ยท 4) = 4) |
40 | 37, 39 | oveq12d 7376 |
. . . . . 6
โข (๐ โ โ โ (((๐ / 4) ยท 4) + (1 ยท
4)) = (๐ +
4)) |
41 | 35, 11, 36, 40 | joinlmuladdmuld 11183 |
. . . . 5
โข (๐ โ โ โ (((๐ / 4) + 1) ยท 4) = (๐ + 4)) |
42 | | 2t2e4 12318 |
. . . . . . . . 9
โข (2
ยท 2) = 4 |
43 | 42 | eqcomi 2746 |
. . . . . . . 8
โข 4 = (2
ยท 2) |
44 | 43 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 4 = (2
ยท 2)) |
45 | 44 | oveq2d 7374 |
. . . . . 6
โข (๐ โ โ โ (((๐ โ 1) / 2) ยท 4) =
(((๐ โ 1) / 2)
ยท (2 ยท 2))) |
46 | 29 | recnd 11184 |
. . . . . . 7
โข (๐ โ โ โ ((๐ โ 1) / 2) โ
โ) |
47 | | mulass 11140 |
. . . . . . . 8
โข ((((๐ โ 1) / 2) โ โ
โง 2 โ โ โง 2 โ โ) โ ((((๐ โ 1) / 2) ยท 2) ยท 2) =
(((๐ โ 1) / 2)
ยท (2 ยท 2))) |
48 | 47 | eqcomd 2743 |
. . . . . . 7
โข ((((๐ โ 1) / 2) โ โ
โง 2 โ โ โง 2 โ โ) โ (((๐ โ 1) / 2) ยท (2 ยท 2)) =
((((๐ โ 1) / 2)
ยท 2) ยท 2)) |
49 | 46, 13, 13, 48 | syl3anc 1372 |
. . . . . 6
โข (๐ โ โ โ (((๐ โ 1) / 2) ยท (2
ยท 2)) = ((((๐
โ 1) / 2) ยท 2) ยท 2)) |
50 | 28 | recnd 11184 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
51 | | 2ne0 12258 |
. . . . . . . . . 10
โข 2 โ
0 |
52 | 51 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ 2 โ
0) |
53 | 50, 13, 52 | divcan1d 11933 |
. . . . . . . 8
โข (๐ โ โ โ (((๐ โ 1) / 2) ยท 2) =
(๐ โ
1)) |
54 | 53 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ โ โ ((((๐ โ 1) / 2) ยท 2)
ยท 2) = ((๐ โ
1) ยท 2)) |
55 | 6, 36, 13 | subdird 11613 |
. . . . . . 7
โข (๐ โ โ โ ((๐ โ 1) ยท 2) =
((๐ ยท 2) โ (1
ยท 2))) |
56 | 12 | mulid2i 11161 |
. . . . . . . . 9
โข (1
ยท 2) = 2 |
57 | 56 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ (1
ยท 2) = 2) |
58 | 57 | oveq2d 7374 |
. . . . . . 7
โข (๐ โ โ โ ((๐ ยท 2) โ (1 ยท
2)) = ((๐ ยท 2)
โ 2)) |
59 | 54, 55, 58 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ โ โ ((((๐ โ 1) / 2) ยท 2)
ยท 2) = ((๐ ยท
2) โ 2)) |
60 | 45, 49, 59 | 3eqtrd 2781 |
. . . . 5
โข (๐ โ โ โ (((๐ โ 1) / 2) ยท 4) =
((๐ ยท 2) โ
2)) |
61 | 41, 60 | breq12d 5119 |
. . . 4
โข (๐ โ โ โ ((((๐ / 4) + 1) ยท 4) โค
(((๐ โ 1) / 2)
ยท 4) โ (๐ + 4)
โค ((๐ ยท 2)
โ 2))) |
62 | 3, 22 | readdcld 11185 |
. . . . 5
โข (๐ โ โ โ (๐ + 4) โ
โ) |
63 | | 2re 12228 |
. . . . . 6
โข 2 โ
โ |
64 | 63 | a1i 11 |
. . . . 5
โข (๐ โ โ โ 2 โ
โ) |
65 | 3, 64 | remulcld 11186 |
. . . . 5
โข (๐ โ โ โ (๐ ยท 2) โ
โ) |
66 | | leaddsub 11632 |
. . . . . 6
โข (((๐ + 4) โ โ โง 2
โ โ โง (๐
ยท 2) โ โ) โ (((๐ + 4) + 2) โค (๐ ยท 2) โ (๐ + 4) โค ((๐ ยท 2) โ 2))) |
67 | 66 | bicomd 222 |
. . . . 5
โข (((๐ + 4) โ โ โง 2
โ โ โง (๐
ยท 2) โ โ) โ ((๐ + 4) โค ((๐ ยท 2) โ 2) โ ((๐ + 4) + 2) โค (๐ ยท 2))) |
68 | 62, 64, 65, 67 | syl3anc 1372 |
. . . 4
โข (๐ โ โ โ ((๐ + 4) โค ((๐ ยท 2) โ 2) โ ((๐ + 4) + 2) โค (๐ ยท 2))) |
69 | 34, 61, 68 | 3bitrd 305 |
. . 3
โข (๐ โ โ โ (((๐ / 4) + 1) โค ((๐ โ 1) / 2) โ ((๐ + 4) + 2) โค (๐ ยท 2))) |
70 | 69 | adantr 482 |
. 2
โข ((๐ โ โ โง 6 โค
๐) โ (((๐ / 4) + 1) โค ((๐ โ 1) / 2) โ ((๐ + 4) + 2) โค (๐ ยท 2))) |
71 | 20, 70 | mpbird 257 |
1
โข ((๐ โ โ โง 6 โค
๐) โ ((๐ / 4) + 1) โค ((๐ โ 1) /
2)) |