Step | Hyp | Ref
| Expression |
1 | | 3nn 12239 |
. . . . . 6
โข 3 โ
โ |
2 | 1 | a1i 11 |
. . . . 5
โข ((๐ โง 3 < ๐) โ 3 โ โ) |
3 | | aks4d1p1.1 |
. . . . . 6
โข (๐ โ ๐ โ
(โคโฅโ3)) |
4 | 3 | adantr 482 |
. . . . 5
โข ((๐ โง 3 < ๐) โ ๐ โ
(โคโฅโ3)) |
5 | | eluznn 12850 |
. . . . 5
โข ((3
โ โ โง ๐
โ (โคโฅโ3)) โ ๐ โ โ) |
6 | 2, 4, 5 | syl2anc 585 |
. . . 4
โข ((๐ โง 3 < ๐) โ ๐ โ โ) |
7 | | aks4d1p1.2 |
. . . 4
โข ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) |
8 | | aks4d1p1.3 |
. . . 4
โข ๐ต = (โโ((2
logb ๐)โ5)) |
9 | | 3p1e4 12305 |
. . . . 5
โข (3 + 1) =
4 |
10 | | simpr 486 |
. . . . . 6
โข ((๐ โง 3 < ๐) โ 3 < ๐) |
11 | | 3z 12543 |
. . . . . . . 8
โข 3 โ
โค |
12 | 11 | a1i 11 |
. . . . . . 7
โข ((๐ โง 3 < ๐) โ 3 โ โค) |
13 | | eluzelz 12780 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ3) โ ๐ โ โค) |
14 | 3, 13 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
15 | 14 | adantr 482 |
. . . . . . 7
โข ((๐ โง 3 < ๐) โ ๐ โ โค) |
16 | 12, 15 | zltp1led 40466 |
. . . . . 6
โข ((๐ โง 3 < ๐) โ (3 < ๐ โ (3 + 1) โค ๐)) |
17 | 10, 16 | mpbid 231 |
. . . . 5
โข ((๐ โง 3 < ๐) โ (3 + 1) โค ๐) |
18 | 9, 17 | eqbrtrrid 5146 |
. . . 4
โข ((๐ โง 3 < ๐) โ 4 โค ๐) |
19 | | eqid 2737 |
. . . 4
โข (2
logb (((2 logb ๐)โ5) + 1)) = (2 logb (((2
logb ๐)โ5)
+ 1)) |
20 | | eqid 2737 |
. . . 4
โข ((2
logb ๐)โ2)
= ((2 logb ๐)โ2) |
21 | | eqid 2737 |
. . . 4
โข ((2
logb ๐)โ4)
= ((2 logb ๐)โ4) |
22 | 6, 7, 8, 18, 19, 20, 21 | aks4d1p1p5 40561 |
. . 3
โข ((๐ โง 3 < ๐) โ ๐ด < (2โ๐ต)) |
23 | 22 | ex 414 |
. 2
โข (๐ โ (3 < ๐ โ ๐ด < (2โ๐ต))) |
24 | | simp2 1138 |
. . . . . . . . . . . 12
โข ((๐ โง 3 = ๐ โง ๐ โ (1...(โโ((2
logb 3)โ2)))) โ 3 = ๐) |
25 | 24 | eqcomd 2743 |
. . . . . . . . . . 11
โข ((๐ โง 3 = ๐ โง ๐ โ (1...(โโ((2
logb 3)โ2)))) โ ๐ = 3) |
26 | 25 | oveq1d 7377 |
. . . . . . . . . 10
โข ((๐ โง 3 = ๐ โง ๐ โ (1...(โโ((2
logb 3)โ2)))) โ (๐โ๐) = (3โ๐)) |
27 | 26 | oveq1d 7377 |
. . . . . . . . 9
โข ((๐ โง 3 = ๐ โง ๐ โ (1...(โโ((2
logb 3)โ2)))) โ ((๐โ๐) โ 1) = ((3โ๐) โ 1)) |
28 | 27 | 3expa 1119 |
. . . . . . . 8
โข (((๐ โง 3 = ๐) โง ๐ โ (1...(โโ((2
logb 3)โ2)))) โ ((๐โ๐) โ 1) = ((3โ๐) โ 1)) |
29 | 28 | prodeq2dv 15813 |
. . . . . . 7
โข ((๐ โง 3 = ๐) โ โ๐ โ (1...(โโ((2
logb 3)โ2)))((๐โ๐) โ 1) = โ๐ โ (1...(โโ((2
logb 3)โ2)))((3โ๐) โ 1)) |
30 | 29 | oveq2d 7378 |
. . . . . 6
โข ((๐ โง 3 = ๐) โ ((3โ(โโ(2
logb (โโ((2 logb 3)โ5))))) ยท
โ๐ โ
(1...(โโ((2 logb 3)โ2)))((๐โ๐) โ 1)) = ((3โ(โโ(2
logb (โโ((2 logb 3)โ5))))) ยท
โ๐ โ
(1...(โโ((2 logb 3)โ2)))((3โ๐) โ 1))) |
31 | | 2rp 12927 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ+ |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 2 โ
โ+) |
33 | | 1red 11163 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 1 โ
โ) |
34 | | 1lt2 12331 |
. . . . . . . . . . . . . . . . . . 19
โข 1 <
2 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 1 < 2) |
36 | 33, 35 | ltned 11298 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 1 โ 2) |
37 | 36 | necomd 3000 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 2 โ 1) |
38 | 11 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 3 โ
โค) |
39 | 32, 37, 38 | relogbexpd 40460 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 logb
(2โ3)) = 3) |
40 | 39 | eqcomd 2743 |
. . . . . . . . . . . . . 14
โข (๐ โ 3 = (2 logb
(2โ3))) |
41 | | cu2 14111 |
. . . . . . . . . . . . . . . 16
โข
(2โ3) = 8 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2โ3) =
8) |
43 | 42 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 logb
(2โ3)) = (2 logb 8)) |
44 | 40, 43 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ 3 = (2 logb
8)) |
45 | | 2z 12542 |
. . . . . . . . . . . . . . 15
โข 2 โ
โค |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โ
โค) |
47 | 46 | zred 12614 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 โ
โ) |
48 | 47 | leidd 11728 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โค 2) |
49 | | 8re 12256 |
. . . . . . . . . . . . . . 15
โข 8 โ
โ |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 8 โ
โ) |
51 | | 8pos 12272 |
. . . . . . . . . . . . . . 15
โข 0 <
8 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < 8) |
53 | 32 | rpgt0d 12967 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 0 < 2) |
54 | | 3re 12240 |
. . . . . . . . . . . . . . . . . . 19
โข 3 โ
โ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 3 โ
โ) |
56 | 1 | nngt0i 12199 |
. . . . . . . . . . . . . . . . . . 19
โข 0 <
3 |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 0 < 3) |
58 | 47, 53, 55, 57, 37 | relogbcld 40459 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 logb 3)
โ โ) |
59 | | 5nn0 12440 |
. . . . . . . . . . . . . . . . . 18
โข 5 โ
โ0 |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 5 โ
โ0) |
61 | 58, 60 | reexpcld 14075 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((2 logb
3)โ5) โ โ) |
62 | | ceilcl 13754 |
. . . . . . . . . . . . . . . 16
โข (((2
logb 3)โ5) โ โ โ (โโ((2
logb 3)โ5)) โ โค) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โโ((2
logb 3)โ5)) โ โค) |
64 | 63 | zred 12614 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ((2
logb 3)โ5)) โ โ) |
65 | | 0red 11165 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 โ
โ) |
66 | | 9re 12259 |
. . . . . . . . . . . . . . . . 17
โข 9 โ
โ |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 9 โ
โ) |
68 | 50 | lep1d 12093 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 8 โค (8 +
1)) |
69 | | 8p1e9 12310 |
. . . . . . . . . . . . . . . . . 18
โข (8 + 1) =
9 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (8 + 1) =
9) |
71 | 68, 70 | breqtrd 5136 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 8 โค 9) |
72 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . . 20
โข 2 โ
โ |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 2 โ
โ) |
74 | | 2pos 12263 |
. . . . . . . . . . . . . . . . . . . 20
โข 0 <
2 |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 0 < 2) |
76 | | 3pos 12265 |
. . . . . . . . . . . . . . . . . . . 20
โข 0 <
3 |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 0 < 3) |
78 | 73, 75, 55, 77, 37 | relogbcld 40459 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (2 logb 3)
โ โ) |
79 | 78, 60 | reexpcld 14075 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2 logb
3)โ5) โ โ) |
80 | 79, 62 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โโ((2
logb 3)โ5)) โ โค) |
81 | 80 | zred 12614 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ((2
logb 3)โ5)) โ โ) |
82 | 55 | leidd 11728 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 3 โค 3) |
83 | 55, 82 | 3lexlogpow5ineq4 40542 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 9 < ((2 logb
3)โ5)) |
84 | 67, 79, 83 | ltled 11310 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 9 โค ((2 logb
3)โ5)) |
85 | | ceilge 13757 |
. . . . . . . . . . . . . . . . . 18
โข (((2
logb 3)โ5) โ โ โ ((2 logb 3)โ5)
โค (โโ((2 logb 3)โ5))) |
86 | 79, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2 logb
3)โ5) โค (โโ((2 logb
3)โ5))) |
87 | 67, 79, 81, 84, 86 | letrd 11319 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 9 โค (โโ((2
logb 3)โ5))) |
88 | 50, 67, 64, 71, 87 | letrd 11319 |
. . . . . . . . . . . . . . 15
โข (๐ โ 8 โค (โโ((2
logb 3)โ5))) |
89 | 65, 50, 64, 52, 88 | ltletrd 11322 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < (โโ((2
logb 3)โ5))) |
90 | 46, 48, 50, 52, 64, 89, 88 | logblebd 40462 |
. . . . . . . . . . . . 13
โข (๐ โ (2 logb 8) โค
(2 logb (โโ((2 logb
3)โ5)))) |
91 | 44, 90 | eqbrtrd 5132 |
. . . . . . . . . . . 12
โข (๐ โ 3 โค (2 logb
(โโ((2 logb 3)โ5)))) |
92 | 79, 33 | readdcld 11191 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((2 logb
3)โ5) + 1) โ โ) |
93 | | 1nn0 12436 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
โ0 |
94 | | 6nn 12249 |
. . . . . . . . . . . . . . . . . . 19
โข 6 โ
โ |
95 | 93, 94 | decnncl 12645 |
. . . . . . . . . . . . . . . . . 18
โข ;16 โ โ |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ;16 โ โ) |
97 | 96 | nnred 12175 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ;16 โ โ) |
98 | | ceilm1lt 13760 |
. . . . . . . . . . . . . . . . . 18
โข (((2
logb 3)โ5) โ โ โ ((โโ((2
logb 3)โ5)) โ 1) < ((2 logb
3)โ5)) |
99 | 79, 98 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((โโ((2
logb 3)โ5)) โ 1) < ((2 logb
3)โ5)) |
100 | 81, 33, 79 | ltsubaddd 11758 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (((โโ((2
logb 3)โ5)) โ 1) < ((2 logb 3)โ5)
โ (โโ((2 logb 3)โ5)) < (((2 logb
3)โ5) + 1))) |
101 | 99, 100 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โโ((2
logb 3)โ5)) < (((2 logb 3)โ5) +
1)) |
102 | | 3lexlogpow5ineq5 40546 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
logb 3)โ5) โค ;15 |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((2 logb
3)โ5) โค ;15) |
104 | | 5p1e6 12307 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (5 + 1) =
6 |
105 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ;15 = ;15 |
106 | 93, 59, 104, 105 | decsuc 12656 |
. . . . . . . . . . . . . . . . . . . . 21
โข (;15 + 1) = ;16 |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (;15 + 1) = ;16) |
108 | 97 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ;16 โ โ) |
109 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ 1 โ
โ) |
110 | | 5nn 12246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 5 โ
โ |
111 | 93, 110 | decnncl 12645 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ;15 โ โ |
112 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ;15 โ โ) |
113 | 112 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ;15 โ โ) |
114 | 108, 109,
113 | subadd2d 11538 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((;16 โ 1) = ;15 โ (;15 + 1) = ;16)) |
115 | 107, 114 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (;16 โ 1) = ;15) |
116 | 115 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ;15 = (;16 โ 1)) |
117 | 103, 116 | breqtrd 5136 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2 logb
3)โ5) โค (;16 โ
1)) |
118 | | leaddsub 11638 |
. . . . . . . . . . . . . . . . . 18
โข ((((2
logb 3)โ5) โ โ โง 1 โ โ โง ;16 โ โ) โ ((((2
logb 3)โ5) + 1) โค ;16 โ ((2 logb 3)โ5) โค (;16 โ 1))) |
119 | 79, 33, 97, 118 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((((2 logb
3)โ5) + 1) โค ;16 โ
((2 logb 3)โ5) โค (;16 โ 1))) |
120 | 117, 119 | mpbird 257 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((2 logb
3)โ5) + 1) โค ;16) |
121 | 81, 92, 97, 101, 120 | ltletrd 11322 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โโ((2
logb 3)โ5)) < ;16) |
122 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
โข ;16 = ;16 |
123 | | 2exp4 16964 |
. . . . . . . . . . . . . . . . 17
โข
(2โ4) = ;16 |
124 | 122, 123 | eqtr4i 2768 |
. . . . . . . . . . . . . . . 16
โข ;16 = (2โ4) |
125 | 124 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ ;16 = (2โ4)) |
126 | 121, 125 | breqtrd 5136 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ((2
logb 3)โ5)) < (2โ4)) |
127 | 46 | uzidd 12786 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 โ
(โคโฅโ2)) |
128 | 64, 89 | elrpd 12961 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โโ((2
logb 3)โ5)) โ โ+) |
129 | | 4z 12544 |
. . . . . . . . . . . . . . . . 17
โข 4 โ
โค |
130 | 129 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 4 โ
โค) |
131 | 32, 130 | rpexpcld 14157 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2โ4) โ
โ+) |
132 | | logblt 26150 |
. . . . . . . . . . . . . . 15
โข ((2
โ (โคโฅโ2) โง (โโ((2
logb 3)โ5)) โ โ+ โง (2โ4) โ
โ+) โ ((โโ((2 logb 3)โ5))
< (2โ4) โ (2 logb (โโ((2 logb
3)โ5))) < (2 logb (2โ4)))) |
133 | 127, 128,
131, 132 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข (๐ โ ((โโ((2
logb 3)โ5)) < (2โ4) โ (2 logb
(โโ((2 logb 3)โ5))) < (2 logb
(2โ4)))) |
134 | 126, 133 | mpbid 231 |
. . . . . . . . . . . . 13
โข (๐ โ (2 logb
(โโ((2 logb 3)โ5))) < (2 logb
(2โ4))) |
135 | 32, 37, 130 | relogbexpd 40460 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 logb
(2โ4)) = 4) |
136 | 9 | eqcomi 2746 |
. . . . . . . . . . . . . . 15
โข 4 = (3 +
1) |
137 | 136 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 4 = (3 +
1)) |
138 | 135, 137 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ (2 logb
(2โ4)) = (3 + 1)) |
139 | 134, 138 | breqtrd 5136 |
. . . . . . . . . . . 12
โข (๐ โ (2 logb
(โโ((2 logb 3)โ5))) < (3 + 1)) |
140 | 91, 139 | jca 513 |
. . . . . . . . . . 11
โข (๐ โ (3 โค (2 logb
(โโ((2 logb 3)โ5))) โง (2 logb
(โโ((2 logb 3)โ5))) < (3 + 1))) |
141 | 73, 75, 55, 57, 37 | relogbcld 40459 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 logb 3)
โ โ) |
142 | 141, 60 | reexpcld 14075 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 logb
3)โ5) โ โ) |
143 | 142, 62 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ((2
logb 3)โ5)) โ โค) |
144 | 143 | zred 12614 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ((2
logb 3)โ5)) โ โ) |
145 | | 9pos 12273 |
. . . . . . . . . . . . . . 15
โข 0 <
9 |
146 | 145 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < 9) |
147 | 65, 67, 144, 146, 87 | ltletrd 11322 |
. . . . . . . . . . . . 13
โข (๐ โ 0 < (โโ((2
logb 3)โ5))) |
148 | 73, 75, 144, 147, 37 | relogbcld 40459 |
. . . . . . . . . . . 12
โข (๐ โ (2 logb
(โโ((2 logb 3)โ5))) โ
โ) |
149 | | flbi 13728 |
. . . . . . . . . . . 12
โข (((2
logb (โโ((2 logb 3)โ5))) โ โ
โง 3 โ โค) โ ((โโ(2 logb
(โโ((2 logb 3)โ5)))) = 3 โ (3 โค (2
logb (โโ((2 logb 3)โ5))) โง (2
logb (โโ((2 logb 3)โ5))) < (3 +
1)))) |
150 | 148, 38, 149 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ ((โโ(2
logb (โโ((2 logb 3)โ5)))) = 3 โ (3
โค (2 logb (โโ((2 logb 3)โ5))) โง
(2 logb (โโ((2 logb 3)โ5))) < (3 +
1)))) |
151 | 140, 150 | mpbird 257 |
. . . . . . . . . 10
โข (๐ โ (โโ(2
logb (โโ((2 logb 3)โ5)))) =
3) |
152 | 151 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ (3โ(โโ(2
logb (โโ((2 logb 3)โ5))))) =
(3โ3)) |
153 | 78 | resqcld 14037 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 logb
3)โ2) โ โ) |
154 | | 3lexlogpow2ineq2 40545 |
. . . . . . . . . . . . . . . . 17
โข (2 <
((2 logb 3)โ2) โง ((2 logb 3)โ2) <
3) |
155 | 154 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 < ((2
logb 3)โ2) โง ((2 logb 3)โ2) <
3)) |
156 | 155 | simpld 496 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 < ((2 logb
3)โ2)) |
157 | 73, 153, 156 | ltled 11310 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โค ((2 logb
3)โ2)) |
158 | 155 | simprd 497 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 logb
3)โ2) < 3) |
159 | | df-3 12224 |
. . . . . . . . . . . . . . . 16
โข 3 = (2 +
1) |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 3 = (2 +
1)) |
161 | 158, 160 | breqtrd 5136 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 logb
3)โ2) < (2 + 1)) |
162 | 157, 161 | jca 513 |
. . . . . . . . . . . . 13
โข (๐ โ (2 โค ((2
logb 3)โ2) โง ((2 logb 3)โ2) < (2 +
1))) |
163 | 141 | resqcld 14037 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 logb
3)โ2) โ โ) |
164 | | flbi 13728 |
. . . . . . . . . . . . . 14
โข ((((2
logb 3)โ2) โ โ โง 2 โ โค) โ
((โโ((2 logb 3)โ2)) = 2 โ (2 โค ((2
logb 3)โ2) โง ((2 logb 3)โ2) < (2 +
1)))) |
165 | 163, 46, 164 | syl2anc 585 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ((2
logb 3)โ2)) = 2 โ (2 โค ((2 logb 3)โ2)
โง ((2 logb 3)โ2) < (2 + 1)))) |
166 | 162, 165 | mpbird 257 |
. . . . . . . . . . . 12
โข (๐ โ (โโ((2
logb 3)โ2)) = 2) |
167 | 166 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ โ (1...(โโ((2
logb 3)โ2))) = (1...2)) |
168 | 167 | prodeq1d 15811 |
. . . . . . . . . 10
โข (๐ โ โ๐ โ (1...(โโ((2
logb 3)โ2)))((3โ๐) โ 1) = โ๐ โ (1...2)((3โ๐) โ 1)) |
169 | | 1zzd 12541 |
. . . . . . . . . . . . . 14
โข (๐ โ 1 โ
โค) |
170 | 169, 46 | jca 513 |
. . . . . . . . . . . . 13
โข (๐ โ (1 โ โค โง 2
โ โค)) |
171 | | 1le2 12369 |
. . . . . . . . . . . . . . 15
โข 1 โค
2 |
172 | 171 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((1
โ โค โง 2 โ โค) โ 1 โค 2) |
173 | | eluz 12784 |
. . . . . . . . . . . . . 14
โข ((1
โ โค โง 2 โ โค) โ (2 โ
(โคโฅโ1) โ 1 โค 2)) |
174 | 172, 173 | mpbird 257 |
. . . . . . . . . . . . 13
โข ((1
โ โค โง 2 โ โค) โ 2 โ
(โคโฅโ1)) |
175 | 170, 174 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
(โคโฅโ1)) |
176 | | 3cn 12241 |
. . . . . . . . . . . . . . 15
โข 3 โ
โ |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...2)) โ 3 โ
โ) |
178 | | elfznn 13477 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...2) โ ๐ โ
โ) |
179 | 178 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...2)) โ ๐ โ โ) |
180 | 179 | nnnn0d 12480 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...2)) โ ๐ โ โ0) |
181 | 177, 180 | expcld 14058 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...2)) โ (3โ๐) โ
โ) |
182 | | 1cnd 11157 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...2)) โ 1 โ
โ) |
183 | 181, 182 | subcld 11519 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...2)) โ ((3โ๐) โ 1) โ
โ) |
184 | | oveq2 7370 |
. . . . . . . . . . . . 13
โข (๐ = 2 โ (3โ๐) = (3โ2)) |
185 | 184 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ = 2 โ ((3โ๐) โ 1) = ((3โ2)
โ 1)) |
186 | 175, 183,
185 | fprodm1 15857 |
. . . . . . . . . . 11
โข (๐ โ โ๐ โ (1...2)((3โ๐) โ 1) = (โ๐ โ (1...(2 โ 1))((3โ๐) โ 1) ยท
((3โ2) โ 1))) |
187 | | 2m1e1 12286 |
. . . . . . . . . . . . . . . 16
โข (2
โ 1) = 1 |
188 | 187 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 โ 1) =
1) |
189 | 188 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...(2 โ 1)) =
(1...1)) |
190 | 189 | prodeq1d 15811 |
. . . . . . . . . . . . 13
โข (๐ โ โ๐ โ (1...(2 โ 1))((3โ๐) โ 1) = โ๐ โ (1...1)((3โ๐) โ 1)) |
191 | 55 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 3 โ
โ) |
192 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 1 โ
โ0) |
193 | 191, 192 | expcld 14058 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (3โ1) โ
โ) |
194 | 193, 109 | subcld 11519 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((3โ1) โ 1)
โ โ) |
195 | 169, 194 | jca 513 |
. . . . . . . . . . . . . 14
โข (๐ โ (1 โ โค โง
((3โ1) โ 1) โ โ)) |
196 | | oveq2 7370 |
. . . . . . . . . . . . . . . 16
โข (๐ = 1 โ (3โ๐) = (3โ1)) |
197 | 196 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ ((3โ๐) โ 1) = ((3โ1)
โ 1)) |
198 | 197 | fprod1 15853 |
. . . . . . . . . . . . . 14
โข ((1
โ โค โง ((3โ1) โ 1) โ โ) โ โ๐ โ (1...1)((3โ๐) โ 1) = ((3โ1)
โ 1)) |
199 | 195, 198 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ โ๐ โ (1...1)((3โ๐) โ 1) = ((3โ1) โ
1)) |
200 | 190, 199 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ (1...(2 โ 1))((3โ๐) โ 1) = ((3โ1)
โ 1)) |
201 | 200 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ โ (โ๐ โ (1...(2 โ 1))((3โ๐) โ 1) ยท
((3โ2) โ 1)) = (((3โ1) โ 1) ยท ((3โ2) โ
1))) |
202 | 186, 201 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ โ๐ โ (1...2)((3โ๐) โ 1) = (((3โ1) โ 1)
ยท ((3โ2) โ 1))) |
203 | 168, 202 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ โ๐ โ (1...(โโ((2
logb 3)โ2)))((3โ๐) โ 1) = (((3โ1) โ 1)
ยท ((3โ2) โ 1))) |
204 | 152, 203 | oveq12d 7380 |
. . . . . . . 8
โข (๐ โ ((3โ(โโ(2
logb (โโ((2 logb 3)โ5))))) ยท
โ๐ โ
(1...(โโ((2 logb 3)โ2)))((3โ๐) โ 1)) = ((3โ3) ยท
(((3โ1) โ 1) ยท ((3โ2) โ 1)))) |
205 | | 3nn0 12438 |
. . . . . . . . . . . 12
โข 3 โ
โ0 |
206 | 205 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 3 โ
โ0) |
207 | 55, 206 | reexpcld 14075 |
. . . . . . . . . 10
โข (๐ โ (3โ3) โ
โ) |
208 | 55, 192 | reexpcld 14075 |
. . . . . . . . . . . 12
โข (๐ โ (3โ1) โ
โ) |
209 | 208, 33 | resubcld 11590 |
. . . . . . . . . . 11
โข (๐ โ ((3โ1) โ 1)
โ โ) |
210 | 55 | resqcld 14037 |
. . . . . . . . . . . 12
โข (๐ โ (3โ2) โ
โ) |
211 | 210, 33 | resubcld 11590 |
. . . . . . . . . . 11
โข (๐ โ ((3โ2) โ 1)
โ โ) |
212 | 209, 211 | remulcld 11192 |
. . . . . . . . . 10
โข (๐ โ (((3โ1) โ 1)
ยท ((3โ2) โ 1)) โ โ) |
213 | 207, 212 | remulcld 11192 |
. . . . . . . . 9
โข (๐ โ ((3โ3) ยท
(((3โ1) โ 1) ยท ((3โ2) โ 1))) โ
โ) |
214 | | 9nn0 12444 |
. . . . . . . . . . . 12
โข 9 โ
โ0 |
215 | 214 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 9 โ
โ0) |
216 | 73, 215 | reexpcld 14075 |
. . . . . . . . . 10
โข (๐ โ (2โ9) โ
โ) |
217 | 216, 33 | resubcld 11590 |
. . . . . . . . 9
โข (๐ โ ((2โ9) โ 1)
โ โ) |
218 | | elnnz 12516 |
. . . . . . . . . . . . 13
โข
((โโ((2 logb 3)โ5)) โ โ โ
((โโ((2 logb 3)โ5)) โ โค โง 0 <
(โโ((2 logb 3)โ5)))) |
219 | 143, 147,
218 | sylanbrc 584 |
. . . . . . . . . . . 12
โข (๐ โ (โโ((2
logb 3)โ5)) โ โ) |
220 | 219 | orcd 872 |
. . . . . . . . . . 11
โข (๐ โ ((โโ((2
logb 3)โ5)) โ โ โจ (โโ((2
logb 3)โ5)) = 0)) |
221 | | elnn0 12422 |
. . . . . . . . . . . 12
โข
((โโ((2 logb 3)โ5)) โ
โ0 โ ((โโ((2 logb 3)โ5))
โ โ โจ (โโ((2 logb 3)โ5)) =
0)) |
222 | 221 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ ((โโ((2
logb 3)โ5)) โ โ0 โ
((โโ((2 logb 3)โ5)) โ โ โจ
(โโ((2 logb 3)โ5)) = 0))) |
223 | 220, 222 | mpbird 257 |
. . . . . . . . . 10
โข (๐ โ (โโ((2
logb 3)โ5)) โ โ0) |
224 | 73, 223 | reexpcld 14075 |
. . . . . . . . 9
โข (๐ โ (2โ(โโ((2
logb 3)โ5))) โ โ) |
225 | | 8cn 12257 |
. . . . . . . . . . . . . . 15
โข 8 โ
โ |
226 | | 2cn 12235 |
. . . . . . . . . . . . . . 15
โข 2 โ
โ |
227 | | 8t2e16 12740 |
. . . . . . . . . . . . . . 15
โข (8
ยท 2) = ;16 |
228 | 225, 226,
227 | mulcomli 11171 |
. . . . . . . . . . . . . 14
โข (2
ยท 8) = ;16 |
229 | 228 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ (2 ยท 8) = ;16) |
230 | 229 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ โ (;27 ยท (2 ยท 8)) = (;27 ยท ;16)) |
231 | | 6nn0 12441 |
. . . . . . . . . . . . . . 15
โข 6 โ
โ0 |
232 | 93, 231 | deccl 12640 |
. . . . . . . . . . . . . 14
โข ;16 โ
โ0 |
233 | | 2nn0 12437 |
. . . . . . . . . . . . . 14
โข 2 โ
โ0 |
234 | | 7nn0 12442 |
. . . . . . . . . . . . . 14
โข 7 โ
โ0 |
235 | | eqid 2737 |
. . . . . . . . . . . . . 14
โข ;27 = ;27 |
236 | 93, 93 | deccl 12640 |
. . . . . . . . . . . . . 14
โข ;11 โ
โ0 |
237 | | 0nn0 12435 |
. . . . . . . . . . . . . . 15
โข 0 โ
โ0 |
238 | 233 | dec0h 12647 |
. . . . . . . . . . . . . . 15
โข 2 = ;02 |
239 | | eqid 2737 |
. . . . . . . . . . . . . . 15
โข ;11 = ;11 |
240 | 232 | nn0cni 12432 |
. . . . . . . . . . . . . . . . . 18
โข ;16 โ โ |
241 | 240 | mul02i 11351 |
. . . . . . . . . . . . . . . . 17
โข (0
ยท ;16) = 0 |
242 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . . . 18
โข 1 โ
โ |
243 | 176, 242,
9 | addcomli 11354 |
. . . . . . . . . . . . . . . . 17
โข (1 + 3) =
4 |
244 | 241, 243 | oveq12i 7374 |
. . . . . . . . . . . . . . . 16
โข ((0
ยท ;16) + (1 + 3)) = (0 +
4) |
245 | | 4cn 12245 |
. . . . . . . . . . . . . . . . 17
โข 4 โ
โ |
246 | 245 | addid2i 11350 |
. . . . . . . . . . . . . . . 16
โข (0 + 4) =
4 |
247 | 244, 246 | eqtri 2765 |
. . . . . . . . . . . . . . 15
โข ((0
ยท ;16) + (1 + 3)) =
4 |
248 | 93 | dec0h 12647 |
. . . . . . . . . . . . . . . 16
โข 1 = ;01 |
249 | | 2t1e2 12323 |
. . . . . . . . . . . . . . . . . 18
โข (2
ยท 1) = 2 |
250 | | 0p1e1 12282 |
. . . . . . . . . . . . . . . . . 18
โข (0 + 1) =
1 |
251 | 249, 250 | oveq12i 7374 |
. . . . . . . . . . . . . . . . 17
โข ((2
ยท 1) + (0 + 1)) = (2 + 1) |
252 | | 2p1e3 12302 |
. . . . . . . . . . . . . . . . 17
โข (2 + 1) =
3 |
253 | 251, 252 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
โข ((2
ยท 1) + (0 + 1)) = 3 |
254 | | 6cn 12251 |
. . . . . . . . . . . . . . . . . 18
โข 6 โ
โ |
255 | | 6t2e12 12729 |
. . . . . . . . . . . . . . . . . 18
โข (6
ยท 2) = ;12 |
256 | 254, 226,
255 | mulcomli 11171 |
. . . . . . . . . . . . . . . . 17
โข (2
ยท 6) = ;12 |
257 | 93, 233, 252, 256 | decsuc 12656 |
. . . . . . . . . . . . . . . 16
โข ((2
ยท 6) + 1) = ;13 |
258 | 93, 231, 237, 93, 122, 248, 233, 205, 93, 253, 257 | decma2c 12678 |
. . . . . . . . . . . . . . 15
โข ((2
ยท ;16) + 1) = ;33 |
259 | 237, 233,
93, 93, 238, 239, 232, 205, 205, 247, 258 | decmac 12677 |
. . . . . . . . . . . . . 14
โข ((2
ยท ;16) + ;11) = ;43 |
260 | | 4nn0 12439 |
. . . . . . . . . . . . . . 15
โข 4 โ
โ0 |
261 | | 7cn 12254 |
. . . . . . . . . . . . . . . . . 18
โข 7 โ
โ |
262 | 261 | mulid1i 11166 |
. . . . . . . . . . . . . . . . 17
โข (7
ยท 1) = 7 |
263 | 262 | oveq1i 7372 |
. . . . . . . . . . . . . . . 16
โข ((7
ยท 1) + 4) = (7 + 4) |
264 | | 7p4e11 12701 |
. . . . . . . . . . . . . . . 16
โข (7 + 4) =
;11 |
265 | 263, 264 | eqtri 2765 |
. . . . . . . . . . . . . . 15
โข ((7
ยท 1) + 4) = ;11 |
266 | | 7t6e42 12738 |
. . . . . . . . . . . . . . 15
โข (7
ยท 6) = ;42 |
267 | 234, 93, 231, 122, 233, 260, 265, 266 | decmul2c 12691 |
. . . . . . . . . . . . . 14
โข (7
ยท ;16) = ;;112 |
268 | 232, 233,
234, 235, 233, 236, 259, 267 | decmul1c 12690 |
. . . . . . . . . . . . 13
โข (;27 ยท ;16) = ;;432 |
269 | 268 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ (;27 ยท ;16) = ;;432) |
270 | 230, 269 | eqtrd 2777 |
. . . . . . . . . . 11
โข (๐ โ (;27 ยท (2 ยท 8)) = ;;432) |
271 | 260, 205 | deccl 12640 |
. . . . . . . . . . . . 13
โข ;43 โ
โ0 |
272 | 59, 93 | deccl 12640 |
. . . . . . . . . . . . 13
โข ;51 โ
โ0 |
273 | | 2lt10 12763 |
. . . . . . . . . . . . 13
โข 2 <
;10 |
274 | | 3lt10 12762 |
. . . . . . . . . . . . . 14
โข 3 <
;10 |
275 | | 4lt5 12337 |
. . . . . . . . . . . . . 14
โข 4 <
5 |
276 | 260, 59, 205, 93, 274, 275 | decltc 12654 |
. . . . . . . . . . . . 13
โข ;43 < ;51 |
277 | 271, 272,
233, 93, 273, 276 | decltc 12654 |
. . . . . . . . . . . 12
โข ;;432 < ;;511 |
278 | 277 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ ;;432
< ;;511) |
279 | 270, 278 | eqbrtrd 5132 |
. . . . . . . . . 10
โข (๐ โ (;27 ยท (2 ยท 8)) < ;;511) |
280 | | 3exp3 16971 |
. . . . . . . . . . . . 13
โข
(3โ3) = ;27 |
281 | 280 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ (3โ3) = ;27) |
282 | 281 | eqcomd 2743 |
. . . . . . . . . . 11
โข (๐ โ ;27 = (3โ3)) |
283 | 191 | exp1d 14053 |
. . . . . . . . . . . . . 14
โข (๐ โ (3โ1) =
3) |
284 | 283 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ ((3โ1) โ 1) =
(3 โ 1)) |
285 | | 3m1e2 12288 |
. . . . . . . . . . . . . 14
โข (3
โ 1) = 2 |
286 | 285 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ (3 โ 1) =
2) |
287 | 284, 286 | eqtr2d 2778 |
. . . . . . . . . . . 12
โข (๐ โ 2 = ((3โ1) โ
1)) |
288 | | sq3 14109 |
. . . . . . . . . . . . . . 15
โข
(3โ2) = 9 |
289 | 288 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ (3โ2) =
9) |
290 | 289 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ ((3โ2) โ 1) =
(9 โ 1)) |
291 | | 9m1e8 12294 |
. . . . . . . . . . . . . 14
โข (9
โ 1) = 8 |
292 | 291 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ (9 โ 1) =
8) |
293 | 290, 292 | eqtr2d 2778 |
. . . . . . . . . . . 12
โข (๐ โ 8 = ((3โ2) โ
1)) |
294 | 287, 293 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท 8) =
(((3โ1) โ 1) ยท ((3โ2) โ 1))) |
295 | 282, 294 | oveq12d 7380 |
. . . . . . . . . 10
โข (๐ โ (;27 ยท (2 ยท 8)) = ((3โ3) ยท
(((3โ1) โ 1) ยท ((3โ2) โ 1)))) |
296 | | df-9 12230 |
. . . . . . . . . . . . . . . 16
โข 9 = (8 +
1) |
297 | 296 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 9 = (8 +
1)) |
298 | 297 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ โ (2โ9) = (2โ(8 +
1))) |
299 | 287, 194 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 โ
โ) |
300 | | 8nn0 12443 |
. . . . . . . . . . . . . . . 16
โข 8 โ
โ0 |
301 | 300 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 8 โ
โ0) |
302 | 299, 192,
301 | expaddd 14060 |
. . . . . . . . . . . . . 14
โข (๐ โ (2โ(8 + 1)) =
((2โ8) ยท (2โ1))) |
303 | 298, 302 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ (2โ9) = ((2โ8)
ยท (2โ1))) |
304 | | 2exp8 16968 |
. . . . . . . . . . . . . . . . 17
โข
(2โ8) = ;;256 |
305 | 304 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2โ8) = ;;256) |
306 | 305 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2โ8) ยท
(2โ1)) = (;;256 ยท (2โ1))) |
307 | 299 | exp1d 14053 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2โ1) =
2) |
308 | 307 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข (๐ โ (;;256
ยท (2โ1)) = (;;256 ยท 2)) |
309 | 306, 308 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2โ8) ยท
(2โ1)) = (;;256 ยท 2)) |
310 | 233, 59 | deccl 12640 |
. . . . . . . . . . . . . . . 16
โข ;25 โ
โ0 |
311 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
โข ;;256 = ;;256 |
312 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
โข ;25 = ;25 |
313 | | 2t2e4 12324 |
. . . . . . . . . . . . . . . . . . 19
โข (2
ยท 2) = 4 |
314 | 313, 250 | oveq12i 7374 |
. . . . . . . . . . . . . . . . . 18
โข ((2
ยท 2) + (0 + 1)) = (4 + 1) |
315 | | 4p1e5 12306 |
. . . . . . . . . . . . . . . . . 18
โข (4 + 1) =
5 |
316 | 314, 315 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
โข ((2
ยท 2) + (0 + 1)) = 5 |
317 | | 5t2e10 12725 |
. . . . . . . . . . . . . . . . . 18
โข (5
ยท 2) = ;10 |
318 | 93, 237, 250, 317 | decsuc 12656 |
. . . . . . . . . . . . . . . . 17
โข ((5
ยท 2) + 1) = ;11 |
319 | 233, 59, 237, 93, 312, 248, 233, 93, 93, 316, 318 | decmac 12677 |
. . . . . . . . . . . . . . . 16
โข ((;25 ยท 2) + 1) = ;51 |
320 | 233, 310,
231, 311, 233, 93, 319, 255 | decmul1c 12690 |
. . . . . . . . . . . . . . 15
โข (;;256 ยท 2) = ;;512 |
321 | 320 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ (;;256
ยท 2) = ;;512) |
322 | 309, 321 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ ((2โ8) ยท
(2โ1)) = ;;512) |
323 | 303, 322 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ (2โ9) = ;;512) |
324 | 323 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ โ ((2โ9) โ 1) =
(;;512 โ 1)) |
325 | | 1p1e2 12285 |
. . . . . . . . . . . . . 14
โข (1 + 1) =
2 |
326 | | eqid 2737 |
. . . . . . . . . . . . . 14
โข ;;511 = ;;511 |
327 | 272, 93, 325, 326 | decsuc 12656 |
. . . . . . . . . . . . 13
โข (;;511 + 1) = ;;512 |
328 | 272, 233 | deccl 12640 |
. . . . . . . . . . . . . . 15
โข ;;512 โ โ0 |
329 | 328 | nn0cni 12432 |
. . . . . . . . . . . . . 14
โข ;;512 โ โ |
330 | 272, 93 | deccl 12640 |
. . . . . . . . . . . . . . 15
โข ;;511 โ โ0 |
331 | 330 | nn0cni 12432 |
. . . . . . . . . . . . . 14
โข ;;511 โ โ |
332 | 329, 242,
331 | subadd2i 11496 |
. . . . . . . . . . . . 13
โข ((;;512 โ 1) = ;;511
โ (;;511 + 1) = ;;512) |
333 | 327, 332 | mpbir 230 |
. . . . . . . . . . . 12
โข (;;512 โ 1) = ;;511 |
334 | 333 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ (;;512
โ 1) = ;;511) |
335 | 324, 334 | eqtr2d 2778 |
. . . . . . . . . 10
โข (๐ โ ;;511 =
((2โ9) โ 1)) |
336 | 279, 295,
335 | 3brtr3d 5141 |
. . . . . . . . 9
โข (๐ โ ((3โ3) ยท
(((3โ1) โ 1) ยท ((3โ2) โ 1))) < ((2โ9)
โ 1)) |
337 | 216 | ltm1d 12094 |
. . . . . . . . . 10
โข (๐ โ ((2โ9) โ 1)
< (2โ9)) |
338 | 215 | nn0zd 12532 |
. . . . . . . . . . . 12
โข (๐ โ 9 โ
โค) |
339 | 73, 338, 143, 35 | leexp2d 14162 |
. . . . . . . . . . 11
โข (๐ โ (9 โค (โโ((2
logb 3)โ5)) โ (2โ9) โค (2โ(โโ((2
logb 3)โ5))))) |
340 | 87, 339 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ (2โ9) โค
(2โ(โโ((2 logb 3)โ5)))) |
341 | 217, 216,
224, 337, 340 | ltletrd 11322 |
. . . . . . . . 9
โข (๐ โ ((2โ9) โ 1)
< (2โ(โโ((2 logb 3)โ5)))) |
342 | 213, 217,
224, 336, 341 | lttrd 11323 |
. . . . . . . 8
โข (๐ โ ((3โ3) ยท
(((3โ1) โ 1) ยท ((3โ2) โ 1))) <
(2โ(โโ((2 logb 3)โ5)))) |
343 | 204, 342 | eqbrtrd 5132 |
. . . . . . 7
โข (๐ โ ((3โ(โโ(2
logb (โโ((2 logb 3)โ5))))) ยท
โ๐ โ
(1...(โโ((2 logb 3)โ2)))((3โ๐) โ 1)) < (2โ(โโ((2
logb 3)โ5)))) |
344 | 343 | adantr 482 |
. . . . . 6
โข ((๐ โง 3 = ๐) โ ((3โ(โโ(2
logb (โโ((2 logb 3)โ5))))) ยท
โ๐ โ
(1...(โโ((2 logb 3)โ2)))((3โ๐) โ 1)) < (2โ(โโ((2
logb 3)โ5)))) |
345 | 30, 344 | eqbrtrd 5132 |
. . . . 5
โข ((๐ โง 3 = ๐) โ ((3โ(โโ(2
logb (โโ((2 logb 3)โ5))))) ยท
โ๐ โ
(1...(โโ((2 logb 3)โ2)))((๐โ๐) โ 1)) < (2โ(โโ((2
logb 3)โ5)))) |
346 | | simpr 486 |
. . . . . . 7
โข ((๐ โง 3 = ๐) โ 3 = ๐) |
347 | | oveq2 7370 |
. . . . . . . . . . . . 13
โข (3 =
๐ โ (2 logb
3) = (2 logb ๐)) |
348 | 347 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง 3 = ๐) โ (2 logb 3) = (2
logb ๐)) |
349 | 348 | oveq1d 7377 |
. . . . . . . . . . 11
โข ((๐ โง 3 = ๐) โ ((2 logb 3)โ5) =
((2 logb ๐)โ5)) |
350 | 349 | fveq2d 6851 |
. . . . . . . . . 10
โข ((๐ โง 3 = ๐) โ (โโ((2 logb
3)โ5)) = (โโ((2 logb ๐)โ5))) |
351 | 8 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โง 3 = ๐) โ ๐ต = (โโ((2 logb ๐)โ5))) |
352 | 351 | eqcomd 2743 |
. . . . . . . . . 10
โข ((๐ โง 3 = ๐) โ (โโ((2 logb
๐)โ5)) = ๐ต) |
353 | 350, 352 | eqtrd 2777 |
. . . . . . . . 9
โข ((๐ โง 3 = ๐) โ (โโ((2 logb
3)โ5)) = ๐ต) |
354 | 353 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โง 3 = ๐) โ (2 logb
(โโ((2 logb 3)โ5))) = (2 logb ๐ต)) |
355 | 354 | fveq2d 6851 |
. . . . . . 7
โข ((๐ โง 3 = ๐) โ (โโ(2 logb
(โโ((2 logb 3)โ5)))) = (โโ(2
logb ๐ต))) |
356 | 346, 355 | oveq12d 7380 |
. . . . . 6
โข ((๐ โง 3 = ๐) โ (3โ(โโ(2
logb (โโ((2 logb 3)โ5))))) = (๐โ(โโ(2
logb ๐ต)))) |
357 | 346 | oveq2d 7378 |
. . . . . . . . . 10
โข ((๐ โง 3 = ๐) โ (2 logb 3) = (2
logb ๐)) |
358 | 357 | oveq1d 7377 |
. . . . . . . . 9
โข ((๐ โง 3 = ๐) โ ((2 logb 3)โ2) =
((2 logb ๐)โ2)) |
359 | 358 | fveq2d 6851 |
. . . . . . . 8
โข ((๐ โง 3 = ๐) โ (โโ((2 logb
3)โ2)) = (โโ((2 logb ๐)โ2))) |
360 | 359 | oveq2d 7378 |
. . . . . . 7
โข ((๐ โง 3 = ๐) โ (1...(โโ((2
logb 3)โ2))) = (1...(โโ((2 logb ๐)โ2)))) |
361 | 360 | prodeq1d 15811 |
. . . . . 6
โข ((๐ โง 3 = ๐) โ โ๐ โ (1...(โโ((2
logb 3)โ2)))((๐โ๐) โ 1) = โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) |
362 | 356, 361 | oveq12d 7380 |
. . . . 5
โข ((๐ โง 3 = ๐) โ ((3โ(โโ(2
logb (โโ((2 logb 3)โ5))))) ยท
โ๐ โ
(1...(โโ((2 logb 3)โ2)))((๐โ๐) โ 1)) = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1))) |
363 | 350 | oveq2d 7378 |
. . . . 5
โข ((๐ โง 3 = ๐) โ (2โ(โโ((2
logb 3)โ5))) = (2โ(โโ((2 logb ๐)โ5)))) |
364 | 345, 362,
363 | 3brtr3d 5141 |
. . . 4
โข ((๐ โง 3 = ๐) โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) < (2โ(โโ((2
logb ๐)โ5)))) |
365 | 7 | a1i 11 |
. . . . 5
โข ((๐ โง 3 = ๐) โ ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1))) |
366 | 365 | eqcomd 2743 |
. . . 4
โข ((๐ โง 3 = ๐) โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) = ๐ด) |
367 | 8 | oveq2i 7373 |
. . . . . 6
โข
(2โ๐ต) =
(2โ(โโ((2 logb ๐)โ5))) |
368 | 367 | a1i 11 |
. . . . 5
โข ((๐ โง 3 = ๐) โ (2โ๐ต) = (2โ(โโ((2
logb ๐)โ5)))) |
369 | 368 | eqcomd 2743 |
. . . 4
โข ((๐ โง 3 = ๐) โ (2โ(โโ((2
logb ๐)โ5))) = (2โ๐ต)) |
370 | 364, 366,
369 | 3brtr3d 5141 |
. . 3
โข ((๐ โง 3 = ๐) โ ๐ด < (2โ๐ต)) |
371 | 370 | ex 414 |
. 2
โข (๐ โ (3 = ๐ โ ๐ด < (2โ๐ต))) |
372 | | eluzle 12783 |
. . . 4
โข (๐ โ
(โคโฅโ3) โ 3 โค ๐) |
373 | 3, 372 | syl 17 |
. . 3
โข (๐ โ 3 โค ๐) |
374 | 14 | zred 12614 |
. . . 4
โข (๐ โ ๐ โ โ) |
375 | 55, 374 | leloed 11305 |
. . 3
โข (๐ โ (3 โค ๐ โ (3 < ๐ โจ 3 = ๐))) |
376 | 373, 375 | mpbid 231 |
. 2
โข (๐ โ (3 < ๐ โจ 3 = ๐)) |
377 | 23, 371, 376 | mpjaod 859 |
1
โข (๐ โ ๐ด < (2โ๐ต)) |