Step | Hyp | Ref
| Expression |
1 | | 2nn 12233 |
. . . . . . . 8
โข 2 โ
โ |
2 | | 5nn 12246 |
. . . . . . . . 9
โข 5 โ
โ |
3 | | bpos.1 |
. . . . . . . . 9
โข (๐ โ ๐ โ
(โคโฅโ5)) |
4 | | eluznn 12850 |
. . . . . . . . 9
โข ((5
โ โ โง ๐
โ (โคโฅโ5)) โ ๐ โ โ) |
5 | 2, 3, 4 | sylancr 588 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
6 | | nnmulcl 12184 |
. . . . . . . 8
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
7 | 1, 5, 6 | sylancr 588 |
. . . . . . 7
โข (๐ โ (2 ยท ๐) โ
โ) |
8 | 7 | nnred 12175 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โ) |
9 | 7 | nnrpd 12962 |
. . . . . . 7
โข (๐ โ (2 ยท ๐) โ
โ+) |
10 | 9 | rpge0d 12968 |
. . . . . 6
โข (๐ โ 0 โค (2 ยท ๐)) |
11 | 8, 10 | resqrtcld 15309 |
. . . . 5
โข (๐ โ (โโ(2 ยท
๐)) โ
โ) |
12 | 11 | flcld 13710 |
. . . 4
โข (๐ โ
(โโ(โโ(2 ยท ๐))) โ โค) |
13 | | sqrt9 15165 |
. . . . . 6
โข
(โโ9) = 3 |
14 | | 9re 12259 |
. . . . . . . . 9
โข 9 โ
โ |
15 | 14 | a1i 11 |
. . . . . . . 8
โข (๐ โ 9 โ
โ) |
16 | | 10re 12644 |
. . . . . . . . 9
โข ;10 โ โ |
17 | 16 | a1i 11 |
. . . . . . . 8
โข (๐ โ ;10 โ โ) |
18 | | lep1 12003 |
. . . . . . . . . . 11
โข (9 โ
โ โ 9 โค (9 + 1)) |
19 | 14, 18 | ax-mp 5 |
. . . . . . . . . 10
โข 9 โค (9
+ 1) |
20 | | 9p1e10 12627 |
. . . . . . . . . 10
โข (9 + 1) =
;10 |
21 | 19, 20 | breqtri 5135 |
. . . . . . . . 9
โข 9 โค
;10 |
22 | 21 | a1i 11 |
. . . . . . . 8
โข (๐ โ 9 โค ;10) |
23 | | 5cn 12248 |
. . . . . . . . . 10
โข 5 โ
โ |
24 | | 2cn 12235 |
. . . . . . . . . 10
โข 2 โ
โ |
25 | | 5t2e10 12725 |
. . . . . . . . . 10
โข (5
ยท 2) = ;10 |
26 | 23, 24, 25 | mulcomli 11171 |
. . . . . . . . 9
โข (2
ยท 5) = ;10 |
27 | | eluzle 12783 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ5) โ 5 โค ๐) |
28 | 3, 27 | syl 17 |
. . . . . . . . . 10
โข (๐ โ 5 โค ๐) |
29 | 5 | nnred 12175 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
30 | | 5re 12247 |
. . . . . . . . . . . 12
โข 5 โ
โ |
31 | | 2re 12234 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
32 | | 2pos 12263 |
. . . . . . . . . . . . 13
โข 0 <
2 |
33 | 31, 32 | pm3.2i 472 |
. . . . . . . . . . . 12
โข (2 โ
โ โง 0 < 2) |
34 | | lemul2 12015 |
. . . . . . . . . . . 12
โข ((5
โ โ โง ๐
โ โ โง (2 โ โ โง 0 < 2)) โ (5 โค ๐ โ (2 ยท 5) โค (2
ยท ๐))) |
35 | 30, 33, 34 | mp3an13 1453 |
. . . . . . . . . . 11
โข (๐ โ โ โ (5 โค
๐ โ (2 ยท 5)
โค (2 ยท ๐))) |
36 | 29, 35 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (5 โค ๐ โ (2 ยท 5) โค (2 ยท
๐))) |
37 | 28, 36 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ (2 ยท 5) โค (2
ยท ๐)) |
38 | 26, 37 | eqbrtrrid 5146 |
. . . . . . . 8
โข (๐ โ ;10 โค (2 ยท ๐)) |
39 | 15, 17, 8, 22, 38 | letrd 11319 |
. . . . . . 7
โข (๐ โ 9 โค (2 ยท ๐)) |
40 | | 0re 11164 |
. . . . . . . . . 10
โข 0 โ
โ |
41 | | 9pos 12273 |
. . . . . . . . . 10
โข 0 <
9 |
42 | 40, 14, 41 | ltleii 11285 |
. . . . . . . . 9
โข 0 โค
9 |
43 | 14, 42 | pm3.2i 472 |
. . . . . . . 8
โข (9 โ
โ โง 0 โค 9) |
44 | 9 | rprege0d 12971 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐) โ โ โง 0 โค (2
ยท ๐))) |
45 | | sqrtle 15152 |
. . . . . . . 8
โข (((9
โ โ โง 0 โค 9) โง ((2 ยท ๐) โ โ โง 0 โค (2 ยท
๐))) โ (9 โค (2
ยท ๐) โ
(โโ9) โค (โโ(2 ยท ๐)))) |
46 | 43, 44, 45 | sylancr 588 |
. . . . . . 7
โข (๐ โ (9 โค (2 ยท ๐) โ (โโ9) โค
(โโ(2 ยท ๐)))) |
47 | 39, 46 | mpbid 231 |
. . . . . 6
โข (๐ โ (โโ9) โค
(โโ(2 ยท ๐))) |
48 | 13, 47 | eqbrtrrid 5146 |
. . . . 5
โข (๐ โ 3 โค (โโ(2
ยท ๐))) |
49 | | 3z 12543 |
. . . . . 6
โข 3 โ
โค |
50 | | flge 13717 |
. . . . . 6
โข
(((โโ(2 ยท ๐)) โ โ โง 3 โ โค)
โ (3 โค (โโ(2 ยท ๐)) โ 3 โค
(โโ(โโ(2 ยท ๐))))) |
51 | 11, 49, 50 | sylancl 587 |
. . . . 5
โข (๐ โ (3 โค (โโ(2
ยท ๐)) โ 3 โค
(โโ(โโ(2 ยท ๐))))) |
52 | 48, 51 | mpbid 231 |
. . . 4
โข (๐ โ 3 โค
(โโ(โโ(2 ยท ๐)))) |
53 | 49 | eluz1i 12778 |
. . . 4
โข
((โโ(โโ(2 ยท ๐))) โ (โคโฅโ3)
โ ((โโ(โโ(2 ยท ๐))) โ โค โง 3 โค
(โโ(โโ(2 ยท ๐))))) |
54 | 12, 52, 53 | sylanbrc 584 |
. . 3
โข (๐ โ
(โโ(โโ(2 ยท ๐))) โ
(โคโฅโ3)) |
55 | | 3nn 12239 |
. . . . 5
โข 3 โ
โ |
56 | | nndivre 12201 |
. . . . 5
โข (((2
ยท ๐) โ โ
โง 3 โ โ) โ ((2 ยท ๐) / 3) โ โ) |
57 | 8, 55, 56 | sylancl 587 |
. . . 4
โข (๐ โ ((2 ยท ๐) / 3) โ
โ) |
58 | | 3re 12240 |
. . . . . . . . 9
โข 3 โ
โ |
59 | 58 | a1i 11 |
. . . . . . . 8
โข (๐ โ 3 โ
โ) |
60 | 9 | sqrtgt0d 15304 |
. . . . . . . 8
โข (๐ โ 0 < (โโ(2
ยท ๐))) |
61 | | lemul2 12015 |
. . . . . . . 8
โข ((3
โ โ โง (โโ(2 ยท ๐)) โ โ โง ((โโ(2
ยท ๐)) โ โ
โง 0 < (โโ(2 ยท ๐)))) โ (3 โค (โโ(2
ยท ๐)) โ
((โโ(2 ยท ๐)) ยท 3) โค ((โโ(2
ยท ๐)) ยท
(โโ(2 ยท ๐))))) |
62 | 59, 11, 11, 60, 61 | syl112anc 1375 |
. . . . . . 7
โข (๐ โ (3 โค (โโ(2
ยท ๐)) โ
((โโ(2 ยท ๐)) ยท 3) โค ((โโ(2
ยท ๐)) ยท
(โโ(2 ยท ๐))))) |
63 | 48, 62 | mpbid 231 |
. . . . . 6
โข (๐ โ ((โโ(2
ยท ๐)) ยท 3)
โค ((โโ(2 ยท ๐)) ยท (โโ(2 ยท ๐)))) |
64 | | remsqsqrt 15148 |
. . . . . . 7
โข (((2
ยท ๐) โ โ
โง 0 โค (2 ยท ๐)) โ ((โโ(2 ยท ๐)) ยท (โโ(2
ยท ๐))) = (2 ยท
๐)) |
65 | 8, 10, 64 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((โโ(2
ยท ๐)) ยท
(โโ(2 ยท ๐))) = (2 ยท ๐)) |
66 | 63, 65 | breqtrd 5136 |
. . . . 5
โข (๐ โ ((โโ(2
ยท ๐)) ยท 3)
โค (2 ยท ๐)) |
67 | | 3pos 12265 |
. . . . . . . 8
โข 0 <
3 |
68 | 58, 67 | pm3.2i 472 |
. . . . . . 7
โข (3 โ
โ โง 0 < 3) |
69 | 68 | a1i 11 |
. . . . . 6
โข (๐ โ (3 โ โ โง 0
< 3)) |
70 | | lemuldiv 12042 |
. . . . . 6
โข
(((โโ(2 ยท ๐)) โ โ โง (2 ยท ๐) โ โ โง (3 โ
โ โง 0 < 3)) โ (((โโ(2 ยท ๐)) ยท 3) โค (2 ยท ๐) โ (โโ(2
ยท ๐)) โค ((2
ยท ๐) /
3))) |
71 | 11, 8, 69, 70 | syl3anc 1372 |
. . . . 5
โข (๐ โ (((โโ(2
ยท ๐)) ยท 3)
โค (2 ยท ๐) โ
(โโ(2 ยท ๐)) โค ((2 ยท ๐) / 3))) |
72 | 66, 71 | mpbid 231 |
. . . 4
โข (๐ โ (โโ(2 ยท
๐)) โค ((2 ยท ๐) / 3)) |
73 | | flword2 13725 |
. . . 4
โข
(((โโ(2 ยท ๐)) โ โ โง ((2 ยท ๐) / 3) โ โ โง
(โโ(2 ยท ๐)) โค ((2 ยท ๐) / 3)) โ (โโ((2 ยท
๐) / 3)) โ
(โคโฅโ(โโ(โโ(2 ยท ๐))))) |
74 | 11, 57, 72, 73 | syl3anc 1372 |
. . 3
โข (๐ โ (โโ((2
ยท ๐) / 3)) โ
(โคโฅโ(โโ(โโ(2 ยท ๐))))) |
75 | | elfzuzb 13442 |
. . 3
โข
((โโ(โโ(2 ยท ๐))) โ (3...(โโ((2 ยท
๐) / 3))) โ
((โโ(โโ(2 ยท ๐))) โ (โคโฅโ3)
โง (โโ((2 ยท ๐) / 3)) โ
(โคโฅโ(โโ(โโ(2 ยท ๐)))))) |
76 | 54, 74, 75 | sylanbrc 584 |
. 2
โข (๐ โ
(โโ(โโ(2 ยท ๐))) โ (3...(โโ((2 ยท
๐) / 3)))) |
77 | | bpos.5 |
. 2
โข ๐ =
(โโ(โโ(2 ยท ๐))) |
78 | | bpos.4 |
. . 3
โข ๐พ = (โโ((2 ยท
๐) / 3)) |
79 | 78 | oveq2i 7373 |
. 2
โข
(3...๐พ) =
(3...(โโ((2 ยท ๐) / 3))) |
80 | 76, 77, 79 | 3eltr4g 2855 |
1
โข (๐ โ ๐ โ (3...๐พ)) |