Step | Hyp | Ref
| Expression |
1 | | lcmineqlem23.1 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
2 | | 2nn 12233 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
3 | 2 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ) |
4 | 1, 3 | jca 513 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ โ โง 2 โ
โ)) |
5 | | nndivdvds 16152 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 2 โ
โ) โ (2 โฅ ๐ โ (๐ / 2) โ โ)) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (2 โฅ ๐ โ (๐ / 2) โ โ)) |
7 | 6 | biimpa 478 |
. . . . . . . . 9
โข ((๐ โง 2 โฅ ๐) โ (๐ / 2) โ โ) |
8 | 7 | nnzd 12533 |
. . . . . . . 8
โข ((๐ โง 2 โฅ ๐) โ (๐ / 2) โ โค) |
9 | | 1zzd 12541 |
. . . . . . . 8
โข ((๐ โง 2 โฅ ๐) โ 1 โ โค) |
10 | 8, 9 | zsubcld 12619 |
. . . . . . 7
โข ((๐ โง 2 โฅ ๐) โ ((๐ / 2) โ 1) โ
โค) |
11 | | 0red 11165 |
. . . . . . . 8
โข ((๐ โง 2 โฅ ๐) โ 0 โ โ) |
12 | | 4re 12244 |
. . . . . . . . 9
โข 4 โ
โ |
13 | 12 | a1i 11 |
. . . . . . . 8
โข ((๐ โง 2 โฅ ๐) โ 4 โ โ) |
14 | 7 | nnred 12175 |
. . . . . . . . 9
โข ((๐ โง 2 โฅ ๐) โ (๐ / 2) โ โ) |
15 | | 1red 11163 |
. . . . . . . . 9
โข ((๐ โง 2 โฅ ๐) โ 1 โ โ) |
16 | 14, 15 | resubcld 11590 |
. . . . . . . 8
โข ((๐ โง 2 โฅ ๐) โ ((๐ / 2) โ 1) โ
โ) |
17 | | 4pos 12267 |
. . . . . . . . 9
โข 0 <
4 |
18 | 17 | a1i 11 |
. . . . . . . 8
โข ((๐ โง 2 โฅ ๐) โ 0 < 4) |
19 | | 5m1e4 12290 |
. . . . . . . . 9
โข (5
โ 1) = 4 |
20 | | 5re 12247 |
. . . . . . . . . . 11
โข 5 โ
โ |
21 | 20 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง 2 โฅ ๐) โ 5 โ โ) |
22 | 2 | nncni 12170 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
23 | | 5cn 12248 |
. . . . . . . . . . . . . 14
โข 5 โ
โ |
24 | 22, 23 | mulcomi 11170 |
. . . . . . . . . . . . 13
โข (2
ยท 5) = (5 ยท 2) |
25 | | 5t2e10 12725 |
. . . . . . . . . . . . 13
โข (5
ยท 2) = ;10 |
26 | 24, 25 | eqtri 2765 |
. . . . . . . . . . . 12
โข (2
ยท 5) = ;10 |
27 | | 10re 12644 |
. . . . . . . . . . . . . 14
โข ;10 โ โ |
28 | 27 | recni 11176 |
. . . . . . . . . . . . 13
โข ;10 โ โ |
29 | 2 | nnne0i 12200 |
. . . . . . . . . . . . 13
โข 2 โ
0 |
30 | 28, 22, 23, 29 | divmuli 11916 |
. . . . . . . . . . . 12
โข ((;10 / 2) = 5 โ (2 ยท 5) =
;10) |
31 | 26, 30 | mpbir 230 |
. . . . . . . . . . 11
โข (;10 / 2) = 5 |
32 | 27 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โง 2 โฅ ๐) โ ;10 โ โ) |
33 | 1 | nnred 12175 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
34 | 33 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง 2 โฅ ๐) โ ๐ โ โ) |
35 | | 2rp 12927 |
. . . . . . . . . . . . 13
โข 2 โ
โ+ |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โง 2 โฅ ๐) โ 2 โ
โ+) |
37 | | 9p1e10 12627 |
. . . . . . . . . . . . 13
โข (9 + 1) =
;10 |
38 | | lcmineqlem23.2 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 9 โค ๐) |
39 | | 9re 12259 |
. . . . . . . . . . . . . . . . . . 19
โข 9 โ
โ |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 9 โ
โ) |
41 | 40, 33 | leloed 11305 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (9 โค ๐ โ (9 < ๐ โจ 9 = ๐))) |
42 | 38, 41 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (9 < ๐ โจ 9 = ๐)) |
43 | 42 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง 2 โฅ ๐) โ (9 < ๐ โจ 9 = ๐)) |
44 | | 4cn 12245 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 4 โ
โ |
45 | 22, 44 | mulcomi 11170 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (2
ยท 4) = (4 ยท 2) |
46 | | 4t2e8 12328 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (4
ยท 2) = 8 |
47 | 45, 46 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (2
ยท 4) = 8 |
48 | | 8re 12256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 8 โ
โ |
49 | 48 | recni 11176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 8 โ
โ |
50 | 49, 22, 44, 29 | divmuli 11916 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((8 / 2)
= 4 โ (2 ยท 4) = 8) |
51 | 47, 50 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (8 / 2) =
4 |
52 | | 4nn 12243 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 4 โ
โ |
53 | 51, 52 | eqeltri 2834 |
. . . . . . . . . . . . . . . . . . . . 21
โข (8 / 2)
โ โ |
54 | | 8nn 12255 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 8 โ
โ |
55 | | nndivdvds 16152 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((8
โ โ โง 2 โ โ) โ (2 โฅ 8 โ (8 / 2)
โ โ)) |
56 | 54, 2, 55 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2
โฅ 8 โ (8 / 2) โ โ) |
57 | 53, 56 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . 20
โข 2 โฅ
8 |
58 | | 9m1e8 12294 |
. . . . . . . . . . . . . . . . . . . 20
โข (9
โ 1) = 8 |
59 | 57, 58 | breqtrri 5137 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โฅ
(9 โ 1) |
60 | | 9nn 12258 |
. . . . . . . . . . . . . . . . . . . . 21
โข 9 โ
โ |
61 | 60 | nnzi 12534 |
. . . . . . . . . . . . . . . . . . . 20
โข 9 โ
โค |
62 | | oddm1even 16232 |
. . . . . . . . . . . . . . . . . . . 20
โข (9 โ
โค โ (ยฌ 2 โฅ 9 โ 2 โฅ (9 โ
1))) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
โข (ยฌ 2
โฅ 9 โ 2 โฅ (9 โ 1)) |
64 | 59, 63 | mpbir 230 |
. . . . . . . . . . . . . . . . . 18
โข ยฌ 2
โฅ 9 |
65 | | breq2 5114 |
. . . . . . . . . . . . . . . . . 18
โข (9 =
๐ โ (2 โฅ 9
โ 2 โฅ ๐)) |
66 | 64, 65 | mtbii 326 |
. . . . . . . . . . . . . . . . 17
โข (9 =
๐ โ ยฌ 2 โฅ
๐) |
67 | 66 | con2i 139 |
. . . . . . . . . . . . . . . 16
โข (2
โฅ ๐ โ ยฌ 9 =
๐) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง 2 โฅ ๐) โ ยฌ 9 = ๐) |
69 | 43, 68 | olcnd 876 |
. . . . . . . . . . . . . 14
โข ((๐ โง 2 โฅ ๐) โ 9 < ๐) |
70 | 1 | nnzd 12533 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โค) |
71 | | zltp1le 12560 |
. . . . . . . . . . . . . . . . 17
โข ((9
โ โค โง ๐
โ โค) โ (9 < ๐ โ (9 + 1) โค ๐)) |
72 | 61, 71 | mpan 689 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ (9 <
๐ โ (9 + 1) โค ๐)) |
73 | 70, 72 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (9 < ๐ โ (9 + 1) โค ๐)) |
74 | 73 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง 2 โฅ ๐) โ (9 < ๐ โ (9 + 1) โค ๐)) |
75 | 69, 74 | mpbid 231 |
. . . . . . . . . . . . 13
โข ((๐ โง 2 โฅ ๐) โ (9 + 1) โค ๐) |
76 | 37, 75 | eqbrtrrid 5146 |
. . . . . . . . . . . 12
โข ((๐ โง 2 โฅ ๐) โ ;10 โค ๐) |
77 | 32, 34, 36, 76 | lediv1dd 13022 |
. . . . . . . . . . 11
โข ((๐ โง 2 โฅ ๐) โ (;10 / 2) โค (๐ / 2)) |
78 | 31, 77 | eqbrtrrid 5146 |
. . . . . . . . . 10
โข ((๐ โง 2 โฅ ๐) โ 5 โค (๐ / 2)) |
79 | 21, 14, 15, 78 | lesub1dd 11778 |
. . . . . . . . 9
โข ((๐ โง 2 โฅ ๐) โ (5 โ 1) โค ((๐ / 2) โ
1)) |
80 | 19, 79 | eqbrtrrid 5146 |
. . . . . . . 8
โข ((๐ โง 2 โฅ ๐) โ 4 โค ((๐ / 2) โ 1)) |
81 | 11, 13, 16, 18, 80 | ltletrd 11322 |
. . . . . . 7
โข ((๐ โง 2 โฅ ๐) โ 0 < ((๐ / 2) โ 1)) |
82 | 10, 81 | jca 513 |
. . . . . 6
โข ((๐ โง 2 โฅ ๐) โ (((๐ / 2) โ 1) โ โค โง 0 <
((๐ / 2) โ
1))) |
83 | | elnnz 12516 |
. . . . . 6
โข (((๐ / 2) โ 1) โ โ
โ (((๐ / 2) โ 1)
โ โค โง 0 < ((๐ / 2) โ 1))) |
84 | 82, 83 | sylibr 233 |
. . . . 5
โข ((๐ โง 2 โฅ ๐) โ ((๐ / 2) โ 1) โ
โ) |
85 | 84, 80 | lcmineqlem22 40536 |
. . . 4
โข ((๐ โง 2 โฅ ๐) โ ((2โ((2 ยท ((๐ / 2) โ 1)) + 1)) โค
(lcmโ(1...((2 ยท ((๐ / 2) โ 1)) + 1))) โง (2โ((2
ยท ((๐ / 2) โ
1)) + 2)) โค (lcmโ(1...((2 ยท ((๐ / 2) โ 1)) + 2))))) |
86 | 85 | simprd 497 |
. . 3
โข ((๐ โง 2 โฅ ๐) โ (2โ((2 ยท ((๐ / 2) โ 1)) + 2)) โค
(lcmโ(1...((2 ยท ((๐ / 2) โ 1)) + 2)))) |
87 | 3 | nncnd 12176 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ) |
88 | 1 | nncnd 12176 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
89 | 88 | halfcld 12405 |
. . . . . . . . . 10
โข (๐ โ (๐ / 2) โ โ) |
90 | 87, 89 | muls1d 11622 |
. . . . . . . . 9
โข (๐ โ (2 ยท ((๐ / 2) โ 1)) = ((2 ยท
(๐ / 2)) โ
2)) |
91 | 90 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ ((2 ยท ((๐ / 2) โ 1)) + 2) = (((2
ยท (๐ / 2)) โ
2) + 2)) |
92 | 87, 89 | mulcld 11182 |
. . . . . . . . 9
โข (๐ โ (2 ยท (๐ / 2)) โ
โ) |
93 | 92, 87 | npcand 11523 |
. . . . . . . 8
โข (๐ โ (((2 ยท (๐ / 2)) โ 2) + 2) = (2
ยท (๐ /
2))) |
94 | 91, 93 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ ((2 ยท ((๐ / 2) โ 1)) + 2) = (2
ยท (๐ /
2))) |
95 | 3 | nnne0d 12210 |
. . . . . . . 8
โข (๐ โ 2 โ 0) |
96 | 88, 87, 95 | divcan2d 11940 |
. . . . . . 7
โข (๐ โ (2 ยท (๐ / 2)) = ๐) |
97 | 94, 96 | eqtrd 2777 |
. . . . . 6
โข (๐ โ ((2 ยท ((๐ / 2) โ 1)) + 2) = ๐) |
98 | 97 | oveq2d 7378 |
. . . . 5
โข (๐ โ (2โ((2 ยท
((๐ / 2) โ 1)) + 2))
= (2โ๐)) |
99 | 97 | oveq2d 7378 |
. . . . . 6
โข (๐ โ (1...((2 ยท ((๐ / 2) โ 1)) + 2)) =
(1...๐)) |
100 | 99 | fveq2d 6851 |
. . . . 5
โข (๐ โ (lcmโ(1...((2
ยท ((๐ / 2) โ
1)) + 2))) = (lcmโ(1...๐))) |
101 | 98, 100 | breq12d 5123 |
. . . 4
โข (๐ โ ((2โ((2 ยท
((๐ / 2) โ 1)) + 2))
โค (lcmโ(1...((2 ยท ((๐ / 2) โ 1)) + 2))) โ
(2โ๐) โค
(lcmโ(1...๐)))) |
102 | 101 | adantr 482 |
. . 3
โข ((๐ โง 2 โฅ ๐) โ ((2โ((2 ยท ((๐ / 2) โ 1)) + 2)) โค
(lcmโ(1...((2 ยท ((๐ / 2) โ 1)) + 2))) โ
(2โ๐) โค
(lcmโ(1...๐)))) |
103 | 86, 102 | mpbid 231 |
. 2
โข ((๐ โง 2 โฅ ๐) โ (2โ๐) โค (lcmโ(1...๐))) |
104 | | oddm1even 16232 |
. . . . . . . 8
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ 2 โฅ
(๐ โ
1))) |
105 | 70, 104 | syl 17 |
. . . . . . 7
โข (๐ โ (ยฌ 2 โฅ ๐ โ 2 โฅ (๐ โ 1))) |
106 | 105 | biimpa 478 |
. . . . . 6
โข ((๐ โง ยฌ 2 โฅ ๐) โ 2 โฅ (๐ โ 1)) |
107 | 2 | a1i 11 |
. . . . . . 7
โข ((๐ โง ยฌ 2 โฅ ๐) โ 2 โ
โ) |
108 | | 1zzd 12541 |
. . . . . . . . . . 11
โข (๐ โ 1 โ
โค) |
109 | 70, 108 | zsubcld 12619 |
. . . . . . . . . 10
โข (๐ โ (๐ โ 1) โ โค) |
110 | | 0red 11165 |
. . . . . . . . . . 11
โข (๐ โ 0 โ
โ) |
111 | 48 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 8 โ
โ) |
112 | | 1red 11163 |
. . . . . . . . . . . 12
โข (๐ โ 1 โ
โ) |
113 | 33, 112 | resubcld 11590 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ 1) โ โ) |
114 | | 8pos 12272 |
. . . . . . . . . . . 12
โข 0 <
8 |
115 | 114 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 0 < 8) |
116 | 40, 33, 112, 38 | lesub1dd 11778 |
. . . . . . . . . . . 12
โข (๐ โ (9 โ 1) โค (๐ โ 1)) |
117 | 58, 116 | eqbrtrrid 5146 |
. . . . . . . . . . 11
โข (๐ โ 8 โค (๐ โ 1)) |
118 | 110, 111,
113, 115, 117 | ltletrd 11322 |
. . . . . . . . . 10
โข (๐ โ 0 < (๐ โ 1)) |
119 | 109, 118 | jca 513 |
. . . . . . . . 9
โข (๐ โ ((๐ โ 1) โ โค โง 0 <
(๐ โ
1))) |
120 | | elnnz 12516 |
. . . . . . . . 9
โข ((๐ โ 1) โ โ
โ ((๐ โ 1)
โ โค โง 0 < (๐ โ 1))) |
121 | 119, 120 | sylibr 233 |
. . . . . . . 8
โข (๐ โ (๐ โ 1) โ โ) |
122 | 121 | adantr 482 |
. . . . . . 7
โข ((๐ โง ยฌ 2 โฅ ๐) โ (๐ โ 1) โ โ) |
123 | 107, 122 | nndivdvdsd 40486 |
. . . . . 6
โข ((๐ โง ยฌ 2 โฅ ๐) โ (2 โฅ (๐ โ 1) โ ((๐ โ 1) / 2) โ
โ)) |
124 | 106, 123 | mpbid 231 |
. . . . 5
โข ((๐ โง ยฌ 2 โฅ ๐) โ ((๐ โ 1) / 2) โ
โ) |
125 | 44, 22 | mulcomi 11170 |
. . . . . . . . 9
โข (4
ยท 2) = (2 ยท 4) |
126 | 125, 46 | eqtr3i 2767 |
. . . . . . . 8
โข (2
ยท 4) = 8 |
127 | 126, 50 | mpbir 230 |
. . . . . . 7
โข (8 / 2) =
4 |
128 | 3 | nnrpd 12962 |
. . . . . . . 8
โข (๐ โ 2 โ
โ+) |
129 | 111, 113,
128, 117 | lediv1dd 13022 |
. . . . . . 7
โข (๐ โ (8 / 2) โค ((๐ โ 1) /
2)) |
130 | 127, 129 | eqbrtrrid 5146 |
. . . . . 6
โข (๐ โ 4 โค ((๐ โ 1) / 2)) |
131 | 130 | adantr 482 |
. . . . 5
โข ((๐ โง ยฌ 2 โฅ ๐) โ 4 โค ((๐ โ 1) /
2)) |
132 | 124, 131 | lcmineqlem22 40536 |
. . . 4
โข ((๐ โง ยฌ 2 โฅ ๐) โ ((2โ((2 ยท
((๐ โ 1) / 2)) + 1))
โค (lcmโ(1...((2 ยท ((๐ โ 1) / 2)) + 1))) โง (2โ((2
ยท ((๐ โ 1) /
2)) + 2)) โค (lcmโ(1...((2 ยท ((๐ โ 1) / 2)) + 2))))) |
133 | 132 | simpld 496 |
. . 3
โข ((๐ โง ยฌ 2 โฅ ๐) โ (2โ((2 ยท
((๐ โ 1) / 2)) + 1))
โค (lcmโ(1...((2 ยท ((๐ โ 1) / 2)) + 1)))) |
134 | | 1cnd 11157 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
135 | 88, 134 | subcld 11519 |
. . . . . . . . 9
โข (๐ โ (๐ โ 1) โ โ) |
136 | 135, 87, 95 | divcan2d 11940 |
. . . . . . . 8
โข (๐ โ (2 ยท ((๐ โ 1) / 2)) = (๐ โ 1)) |
137 | 136 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ ((2 ยท ((๐ โ 1) / 2)) + 1) = ((๐ โ 1) +
1)) |
138 | 88, 134 | npcand 11523 |
. . . . . . 7
โข (๐ โ ((๐ โ 1) + 1) = ๐) |
139 | 137, 138 | eqtrd 2777 |
. . . . . 6
โข (๐ โ ((2 ยท ((๐ โ 1) / 2)) + 1) = ๐) |
140 | 139 | oveq2d 7378 |
. . . . 5
โข (๐ โ (2โ((2 ยท
((๐ โ 1) / 2)) + 1))
= (2โ๐)) |
141 | 139 | oveq2d 7378 |
. . . . . 6
โข (๐ โ (1...((2 ยท ((๐ โ 1) / 2)) + 1)) =
(1...๐)) |
142 | 141 | fveq2d 6851 |
. . . . 5
โข (๐ โ (lcmโ(1...((2
ยท ((๐ โ 1) /
2)) + 1))) = (lcmโ(1...๐))) |
143 | 140, 142 | breq12d 5123 |
. . . 4
โข (๐ โ ((2โ((2 ยท
((๐ โ 1) / 2)) + 1))
โค (lcmโ(1...((2 ยท ((๐ โ 1) / 2)) + 1))) โ
(2โ๐) โค
(lcmโ(1...๐)))) |
144 | 143 | adantr 482 |
. . 3
โข ((๐ โง ยฌ 2 โฅ ๐) โ ((2โ((2 ยท
((๐ โ 1) / 2)) + 1))
โค (lcmโ(1...((2 ยท ((๐ โ 1) / 2)) + 1))) โ
(2โ๐) โค
(lcmโ(1...๐)))) |
145 | 133, 144 | mpbid 231 |
. 2
โข ((๐ โง ยฌ 2 โฅ ๐) โ (2โ๐) โค
(lcmโ(1...๐))) |
146 | 103, 145 | pm2.61dan 812 |
1
โข (๐ โ (2โ๐) โค (lcmโ(1...๐))) |