Step | Hyp | Ref
| Expression |
1 | | oveq2 7417 |
. . . 4
โข (๐ฅ = 4 โ (4โ๐ฅ) = (4โ4)) |
2 | | id 22 |
. . . 4
โข (๐ฅ = 4 โ ๐ฅ = 4) |
3 | 1, 2 | oveq12d 7427 |
. . 3
โข (๐ฅ = 4 โ ((4โ๐ฅ) / ๐ฅ) = ((4โ4) / 4)) |
4 | | oveq2 7417 |
. . . 4
โข (๐ฅ = 4 โ (2 ยท ๐ฅ) = (2 ยท
4)) |
5 | 4, 2 | oveq12d 7427 |
. . 3
โข (๐ฅ = 4 โ ((2 ยท ๐ฅ)C๐ฅ) = ((2 ยท 4)C4)) |
6 | 3, 5 | breq12d 5162 |
. 2
โข (๐ฅ = 4 โ (((4โ๐ฅ) / ๐ฅ) < ((2 ยท ๐ฅ)C๐ฅ) โ ((4โ4) / 4) < ((2 ยท
4)C4))) |
7 | | oveq2 7417 |
. . . 4
โข (๐ฅ = ๐ โ (4โ๐ฅ) = (4โ๐)) |
8 | | id 22 |
. . . 4
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
9 | 7, 8 | oveq12d 7427 |
. . 3
โข (๐ฅ = ๐ โ ((4โ๐ฅ) / ๐ฅ) = ((4โ๐) / ๐)) |
10 | | oveq2 7417 |
. . . 4
โข (๐ฅ = ๐ โ (2 ยท ๐ฅ) = (2 ยท ๐)) |
11 | 10, 8 | oveq12d 7427 |
. . 3
โข (๐ฅ = ๐ โ ((2 ยท ๐ฅ)C๐ฅ) = ((2 ยท ๐)C๐)) |
12 | 9, 11 | breq12d 5162 |
. 2
โข (๐ฅ = ๐ โ (((4โ๐ฅ) / ๐ฅ) < ((2 ยท ๐ฅ)C๐ฅ) โ ((4โ๐) / ๐) < ((2 ยท ๐)C๐))) |
13 | | oveq2 7417 |
. . . 4
โข (๐ฅ = (๐ + 1) โ (4โ๐ฅ) = (4โ(๐ + 1))) |
14 | | id 22 |
. . . 4
โข (๐ฅ = (๐ + 1) โ ๐ฅ = (๐ + 1)) |
15 | 13, 14 | oveq12d 7427 |
. . 3
โข (๐ฅ = (๐ + 1) โ ((4โ๐ฅ) / ๐ฅ) = ((4โ(๐ + 1)) / (๐ + 1))) |
16 | | oveq2 7417 |
. . . 4
โข (๐ฅ = (๐ + 1) โ (2 ยท ๐ฅ) = (2 ยท (๐ + 1))) |
17 | 16, 14 | oveq12d 7427 |
. . 3
โข (๐ฅ = (๐ + 1) โ ((2 ยท ๐ฅ)C๐ฅ) = ((2 ยท (๐ + 1))C(๐ + 1))) |
18 | 15, 17 | breq12d 5162 |
. 2
โข (๐ฅ = (๐ + 1) โ (((4โ๐ฅ) / ๐ฅ) < ((2 ยท ๐ฅ)C๐ฅ) โ ((4โ(๐ + 1)) / (๐ + 1)) < ((2 ยท (๐ + 1))C(๐ + 1)))) |
19 | | oveq2 7417 |
. . . 4
โข (๐ฅ = ๐ โ (4โ๐ฅ) = (4โ๐)) |
20 | | id 22 |
. . . 4
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
21 | 19, 20 | oveq12d 7427 |
. . 3
โข (๐ฅ = ๐ โ ((4โ๐ฅ) / ๐ฅ) = ((4โ๐) / ๐)) |
22 | | oveq2 7417 |
. . . 4
โข (๐ฅ = ๐ โ (2 ยท ๐ฅ) = (2 ยท ๐)) |
23 | 22, 20 | oveq12d 7427 |
. . 3
โข (๐ฅ = ๐ โ ((2 ยท ๐ฅ)C๐ฅ) = ((2 ยท ๐)C๐)) |
24 | 21, 23 | breq12d 5162 |
. 2
โข (๐ฅ = ๐ โ (((4โ๐ฅ) / ๐ฅ) < ((2 ยท ๐ฅ)C๐ฅ) โ ((4โ๐) / ๐) < ((2 ยท ๐)C๐))) |
25 | | 6nn0 12493 |
. . . 4
โข 6 โ
โ0 |
26 | | 7nn0 12494 |
. . . 4
โข 7 โ
โ0 |
27 | | 4nn0 12491 |
. . . 4
โข 4 โ
โ0 |
28 | | 0nn0 12487 |
. . . 4
โข 0 โ
โ0 |
29 | | 4lt10 12813 |
. . . 4
โข 4 <
;10 |
30 | | 6lt7 12398 |
. . . 4
โข 6 <
7 |
31 | 25, 26, 27, 28, 29, 30 | decltc 12706 |
. . 3
โข ;64 < ;70 |
32 | | 2cn 12287 |
. . . . . 6
โข 2 โ
โ |
33 | | 2nn0 12489 |
. . . . . 6
โข 2 โ
โ0 |
34 | | 3nn0 12490 |
. . . . . 6
โข 3 โ
โ0 |
35 | | expmul 14073 |
. . . . . 6
โข ((2
โ โ โง 2 โ โ0 โง 3 โ
โ0) โ (2โ(2 ยท 3)) =
((2โ2)โ3)) |
36 | 32, 33, 34, 35 | mp3an 1462 |
. . . . 5
โข
(2โ(2 ยท 3)) = ((2โ2)โ3) |
37 | | sq2 14161 |
. . . . . . 7
โข
(2โ2) = 4 |
38 | 37 | eqcomi 2742 |
. . . . . 6
โข 4 =
(2โ2) |
39 | | 4m1e3 12341 |
. . . . . 6
โข (4
โ 1) = 3 |
40 | 38, 39 | oveq12i 7421 |
. . . . 5
โข
(4โ(4 โ 1)) = ((2โ2)โ3) |
41 | 36, 40 | eqtr4i 2764 |
. . . 4
โข
(2โ(2 ยท 3)) = (4โ(4 โ 1)) |
42 | | 3cn 12293 |
. . . . . . 7
โข 3 โ
โ |
43 | | 3t2e6 12378 |
. . . . . . 7
โข (3
ยท 2) = 6 |
44 | 42, 32, 43 | mulcomli 11223 |
. . . . . 6
โข (2
ยท 3) = 6 |
45 | 44 | oveq2i 7420 |
. . . . 5
โข
(2โ(2 ยท 3)) = (2โ6) |
46 | | 2exp6 17020 |
. . . . 5
โข
(2โ6) = ;64 |
47 | 45, 46 | eqtri 2761 |
. . . 4
โข
(2โ(2 ยท 3)) = ;64 |
48 | | 4cn 12297 |
. . . . 5
โข 4 โ
โ |
49 | | 4ne0 12320 |
. . . . 5
โข 4 โ
0 |
50 | | 4z 12596 |
. . . . 5
โข 4 โ
โค |
51 | | expm1 14078 |
. . . . 5
โข ((4
โ โ โง 4 โ 0 โง 4 โ โค) โ (4โ(4 โ
1)) = ((4โ4) / 4)) |
52 | 48, 49, 50, 51 | mp3an 1462 |
. . . 4
โข
(4โ(4 โ 1)) = ((4โ4) / 4) |
53 | 41, 47, 52 | 3eqtr3ri 2770 |
. . 3
โข
((4โ4) / 4) = ;64 |
54 | | df-4 12277 |
. . . . . . 7
โข 4 = (3 +
1) |
55 | 54 | oveq2i 7420 |
. . . . . 6
โข (2
ยท 4) = (2 ยท (3 + 1)) |
56 | 55, 54 | oveq12i 7421 |
. . . . 5
โข ((2
ยท 4)C4) = ((2 ยท (3 + 1))C(3 + 1)) |
57 | | bcp1ctr 26782 |
. . . . . 6
โข (3 โ
โ0 โ ((2 ยท (3 + 1))C(3 + 1)) = (((2 ยท 3)C3)
ยท (2 ยท (((2 ยท 3) + 1) / (3 + 1))))) |
58 | 34, 57 | ax-mp 5 |
. . . . 5
โข ((2
ยท (3 + 1))C(3 + 1)) = (((2 ยท 3)C3) ยท (2 ยท (((2
ยท 3) + 1) / (3 + 1)))) |
59 | | df-3 12276 |
. . . . . . . . 9
โข 3 = (2 +
1) |
60 | 59 | oveq2i 7420 |
. . . . . . . 8
โข (2
ยท 3) = (2 ยท (2 + 1)) |
61 | 60, 59 | oveq12i 7421 |
. . . . . . 7
โข ((2
ยท 3)C3) = ((2 ยท (2 + 1))C(2 + 1)) |
62 | | bcp1ctr 26782 |
. . . . . . . . 9
โข (2 โ
โ0 โ ((2 ยท (2 + 1))C(2 + 1)) = (((2 ยท 2)C2)
ยท (2 ยท (((2 ยท 2) + 1) / (2 + 1))))) |
63 | 33, 62 | ax-mp 5 |
. . . . . . . 8
โข ((2
ยท (2 + 1))C(2 + 1)) = (((2 ยท 2)C2) ยท (2 ยท (((2
ยท 2) + 1) / (2 + 1)))) |
64 | | df-2 12275 |
. . . . . . . . . . . 12
โข 2 = (1 +
1) |
65 | 64 | oveq2i 7420 |
. . . . . . . . . . 11
โข (2
ยท 2) = (2 ยท (1 + 1)) |
66 | 65, 64 | oveq12i 7421 |
. . . . . . . . . 10
โข ((2
ยท 2)C2) = ((2 ยท (1 + 1))C(1 + 1)) |
67 | | 1nn0 12488 |
. . . . . . . . . . 11
โข 1 โ
โ0 |
68 | | bcp1ctr 26782 |
. . . . . . . . . . 11
โข (1 โ
โ0 โ ((2 ยท (1 + 1))C(1 + 1)) = (((2 ยท 1)C1)
ยท (2 ยท (((2 ยท 1) + 1) / (1 + 1))))) |
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . 10
โข ((2
ยท (1 + 1))C(1 + 1)) = (((2 ยท 1)C1) ยท (2 ยท (((2
ยท 1) + 1) / (1 + 1)))) |
70 | | 1e0p1 12719 |
. . . . . . . . . . . . . . 15
โข 1 = (0 +
1) |
71 | 70 | oveq2i 7420 |
. . . . . . . . . . . . . 14
โข (2
ยท 1) = (2 ยท (0 + 1)) |
72 | 71, 70 | oveq12i 7421 |
. . . . . . . . . . . . 13
โข ((2
ยท 1)C1) = ((2 ยท (0 + 1))C(0 + 1)) |
73 | | bcp1ctr 26782 |
. . . . . . . . . . . . . 14
โข (0 โ
โ0 โ ((2 ยท (0 + 1))C(0 + 1)) = (((2 ยท 0)C0)
ยท (2 ยท (((2 ยท 0) + 1) / (0 + 1))))) |
74 | 28, 73 | ax-mp 5 |
. . . . . . . . . . . . 13
โข ((2
ยท (0 + 1))C(0 + 1)) = (((2 ยท 0)C0) ยท (2 ยท (((2
ยท 0) + 1) / (0 + 1)))) |
75 | 33, 28 | nn0mulcli 12510 |
. . . . . . . . . . . . . . . 16
โข (2
ยท 0) โ โ0 |
76 | | bcn0 14270 |
. . . . . . . . . . . . . . . 16
โข ((2
ยท 0) โ โ0 โ ((2 ยท 0)C0) =
1) |
77 | 75, 76 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข ((2
ยท 0)C0) = 1 |
78 | | 2t0e0 12381 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2
ยท 0) = 0 |
79 | 78 | oveq1i 7419 |
. . . . . . . . . . . . . . . . . . . 20
โข ((2
ยท 0) + 1) = (0 + 1) |
80 | 79, 70 | eqtr4i 2764 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
ยท 0) + 1) = 1 |
81 | 70 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . . 19
โข (0 + 1) =
1 |
82 | 80, 81 | oveq12i 7421 |
. . . . . . . . . . . . . . . . . 18
โข (((2
ยท 0) + 1) / (0 + 1)) = (1 / 1) |
83 | | 1div1e1 11904 |
. . . . . . . . . . . . . . . . . 18
โข (1 / 1) =
1 |
84 | 82, 83 | eqtri 2761 |
. . . . . . . . . . . . . . . . 17
โข (((2
ยท 0) + 1) / (0 + 1)) = 1 |
85 | 84 | oveq2i 7420 |
. . . . . . . . . . . . . . . 16
โข (2
ยท (((2 ยท 0) + 1) / (0 + 1))) = (2 ยท 1) |
86 | | 2t1e2 12375 |
. . . . . . . . . . . . . . . 16
โข (2
ยท 1) = 2 |
87 | 85, 86 | eqtri 2761 |
. . . . . . . . . . . . . . 15
โข (2
ยท (((2 ยท 0) + 1) / (0 + 1))) = 2 |
88 | 77, 87 | oveq12i 7421 |
. . . . . . . . . . . . . 14
โข (((2
ยท 0)C0) ยท (2 ยท (((2 ยท 0) + 1) / (0 + 1)))) = (1
ยท 2) |
89 | 32 | mullidi 11219 |
. . . . . . . . . . . . . 14
โข (1
ยท 2) = 2 |
90 | 88, 89 | eqtri 2761 |
. . . . . . . . . . . . 13
โข (((2
ยท 0)C0) ยท (2 ยท (((2 ยท 0) + 1) / (0 + 1)))) =
2 |
91 | 72, 74, 90 | 3eqtri 2765 |
. . . . . . . . . . . 12
โข ((2
ยท 1)C1) = 2 |
92 | 86 | oveq1i 7419 |
. . . . . . . . . . . . . . . 16
โข ((2
ยท 1) + 1) = (2 + 1) |
93 | 92, 59 | eqtr4i 2764 |
. . . . . . . . . . . . . . 15
โข ((2
ยท 1) + 1) = 3 |
94 | 64 | eqcomi 2742 |
. . . . . . . . . . . . . . 15
โข (1 + 1) =
2 |
95 | 93, 94 | oveq12i 7421 |
. . . . . . . . . . . . . 14
โข (((2
ยท 1) + 1) / (1 + 1)) = (3 / 2) |
96 | 95 | oveq2i 7420 |
. . . . . . . . . . . . 13
โข (2
ยท (((2 ยท 1) + 1) / (1 + 1))) = (2 ยท (3 /
2)) |
97 | | 2ne0 12316 |
. . . . . . . . . . . . . 14
โข 2 โ
0 |
98 | 42, 32, 97 | divcan2i 11957 |
. . . . . . . . . . . . 13
โข (2
ยท (3 / 2)) = 3 |
99 | 96, 98 | eqtri 2761 |
. . . . . . . . . . . 12
โข (2
ยท (((2 ยท 1) + 1) / (1 + 1))) = 3 |
100 | 91, 99 | oveq12i 7421 |
. . . . . . . . . . 11
โข (((2
ยท 1)C1) ยท (2 ยท (((2 ยท 1) + 1) / (1 + 1)))) = (2
ยท 3) |
101 | 100, 44 | eqtri 2761 |
. . . . . . . . . 10
โข (((2
ยท 1)C1) ยท (2 ยท (((2 ยท 1) + 1) / (1 + 1)))) =
6 |
102 | 66, 69, 101 | 3eqtri 2765 |
. . . . . . . . 9
โข ((2
ยท 2)C2) = 6 |
103 | | 2t2e4 12376 |
. . . . . . . . . . . . . 14
โข (2
ยท 2) = 4 |
104 | 103 | oveq1i 7419 |
. . . . . . . . . . . . 13
โข ((2
ยท 2) + 1) = (4 + 1) |
105 | | df-5 12278 |
. . . . . . . . . . . . 13
โข 5 = (4 +
1) |
106 | 104, 105 | eqtr4i 2764 |
. . . . . . . . . . . 12
โข ((2
ยท 2) + 1) = 5 |
107 | 59 | eqcomi 2742 |
. . . . . . . . . . . 12
โข (2 + 1) =
3 |
108 | 106, 107 | oveq12i 7421 |
. . . . . . . . . . 11
โข (((2
ยท 2) + 1) / (2 + 1)) = (5 / 3) |
109 | 108 | oveq2i 7420 |
. . . . . . . . . 10
โข (2
ยท (((2 ยท 2) + 1) / (2 + 1))) = (2 ยท (5 /
3)) |
110 | | 5cn 12300 |
. . . . . . . . . . 11
โข 5 โ
โ |
111 | | 3ne0 12318 |
. . . . . . . . . . 11
โข 3 โ
0 |
112 | 32, 110, 42, 111 | divassi 11970 |
. . . . . . . . . 10
โข ((2
ยท 5) / 3) = (2 ยท (5 / 3)) |
113 | 109, 112 | eqtr4i 2764 |
. . . . . . . . 9
โข (2
ยท (((2 ยท 2) + 1) / (2 + 1))) = ((2 ยท 5) /
3) |
114 | 102, 113 | oveq12i 7421 |
. . . . . . . 8
โข (((2
ยท 2)C2) ยท (2 ยท (((2 ยท 2) + 1) / (2 + 1)))) = (6
ยท ((2 ยท 5) / 3)) |
115 | 63, 114 | eqtri 2761 |
. . . . . . 7
โข ((2
ยท (2 + 1))C(2 + 1)) = (6 ยท ((2 ยท 5) / 3)) |
116 | | 6cn 12303 |
. . . . . . . . 9
โข 6 โ
โ |
117 | | 2nn 12285 |
. . . . . . . . . . 11
โข 2 โ
โ |
118 | | 5nn 12298 |
. . . . . . . . . . 11
โข 5 โ
โ |
119 | 117, 118 | nnmulcli 12237 |
. . . . . . . . . 10
โข (2
ยท 5) โ โ |
120 | 119 | nncni 12222 |
. . . . . . . . 9
โข (2
ยท 5) โ โ |
121 | 42, 111 | pm3.2i 472 |
. . . . . . . . 9
โข (3 โ
โ โง 3 โ 0) |
122 | | div12 11894 |
. . . . . . . . 9
โข ((6
โ โ โง (2 ยท 5) โ โ โง (3 โ โ
โง 3 โ 0)) โ (6 ยท ((2 ยท 5) / 3)) = ((2 ยท 5)
ยท (6 / 3))) |
123 | 116, 120,
121, 122 | mp3an 1462 |
. . . . . . . 8
โข (6
ยท ((2 ยท 5) / 3)) = ((2 ยท 5) ยท (6 /
3)) |
124 | | 5t2e10 12777 |
. . . . . . . . . 10
โข (5
ยท 2) = ;10 |
125 | 110, 32, 124 | mulcomli 11223 |
. . . . . . . . 9
โข (2
ยท 5) = ;10 |
126 | 116, 42, 32, 111 | divmuli 11968 |
. . . . . . . . . 10
โข ((6 / 3)
= 2 โ (3 ยท 2) = 6) |
127 | 43, 126 | mpbir 230 |
. . . . . . . . 9
โข (6 / 3) =
2 |
128 | 125, 127 | oveq12i 7421 |
. . . . . . . 8
โข ((2
ยท 5) ยท (6 / 3)) = (;10 ยท 2) |
129 | 123, 128 | eqtri 2761 |
. . . . . . 7
โข (6
ยท ((2 ยท 5) / 3)) = (;10 ยท 2) |
130 | 61, 115, 129 | 3eqtri 2765 |
. . . . . 6
โข ((2
ยท 3)C3) = (;10 ยท
2) |
131 | 44 | oveq1i 7419 |
. . . . . . . . 9
โข ((2
ยท 3) + 1) = (6 + 1) |
132 | | df-7 12280 |
. . . . . . . . 9
โข 7 = (6 +
1) |
133 | 131, 132 | eqtr4i 2764 |
. . . . . . . 8
โข ((2
ยท 3) + 1) = 7 |
134 | | 3p1e4 12357 |
. . . . . . . 8
โข (3 + 1) =
4 |
135 | 133, 134 | oveq12i 7421 |
. . . . . . 7
โข (((2
ยท 3) + 1) / (3 + 1)) = (7 / 4) |
136 | 135 | oveq2i 7420 |
. . . . . 6
โข (2
ยท (((2 ยท 3) + 1) / (3 + 1))) = (2 ยท (7 /
4)) |
137 | 130, 136 | oveq12i 7421 |
. . . . 5
โข (((2
ยท 3)C3) ยท (2 ยท (((2 ยท 3) + 1) / (3 + 1)))) =
((;10 ยท 2) ยท (2
ยท (7 / 4))) |
138 | 56, 58, 137 | 3eqtri 2765 |
. . . 4
โข ((2
ยท 4)C4) = ((;10 ยท 2)
ยท (2 ยท (7 / 4))) |
139 | | 10nn 12693 |
. . . . . . 7
โข ;10 โ โ |
140 | 139 | nncni 12222 |
. . . . . 6
โข ;10 โ โ |
141 | | 7cn 12306 |
. . . . . . . 8
โข 7 โ
โ |
142 | 141, 48, 49 | divcli 11956 |
. . . . . . 7
โข (7 / 4)
โ โ |
143 | 32, 142 | mulcli 11221 |
. . . . . 6
โข (2
ยท (7 / 4)) โ โ |
144 | 140, 32, 143 | mulassi 11225 |
. . . . 5
โข ((;10 ยท 2) ยท (2 ยท (7
/ 4))) = (;10 ยท (2 ยท
(2 ยท (7 / 4)))) |
145 | 103 | oveq1i 7419 |
. . . . . . 7
โข ((2
ยท 2) ยท (7 / 4)) = (4 ยท (7 / 4)) |
146 | 32, 32, 142 | mulassi 11225 |
. . . . . . 7
โข ((2
ยท 2) ยท (7 / 4)) = (2 ยท (2 ยท (7 /
4))) |
147 | 141, 48, 49 | divcan2i 11957 |
. . . . . . 7
โข (4
ยท (7 / 4)) = 7 |
148 | 145, 146,
147 | 3eqtr3i 2769 |
. . . . . 6
โข (2
ยท (2 ยท (7 / 4))) = 7 |
149 | 148 | oveq2i 7420 |
. . . . 5
โข (;10 ยท (2 ยท (2 ยท (7
/ 4)))) = (;10 ยท
7) |
150 | 144, 149 | eqtri 2761 |
. . . 4
โข ((;10 ยท 2) ยท (2 ยท (7
/ 4))) = (;10 ยท
7) |
151 | 26 | dec0u 12698 |
. . . 4
โข (;10 ยท 7) = ;70 |
152 | 138, 150,
151 | 3eqtri 2765 |
. . 3
โข ((2
ยท 4)C4) = ;70 |
153 | 31, 53, 152 | 3brtr4i 5179 |
. 2
โข
((4โ4) / 4) < ((2 ยท 4)C4) |
154 | | 4nn 12295 |
. . . 4
โข 4 โ
โ |
155 | | eluznn 12902 |
. . . 4
โข ((4
โ โ โง ๐
โ (โคโฅโ4)) โ ๐ โ โ) |
156 | 154, 155 | mpan 689 |
. . 3
โข (๐ โ
(โคโฅโ4) โ ๐ โ โ) |
157 | | nnnn0 12479 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ0) |
158 | | nnexpcl 14040 |
. . . . . . . . . 10
โข ((4
โ โ โง ๐
โ โ0) โ (4โ๐) โ โ) |
159 | 154, 157,
158 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ โ โ
(4โ๐) โ
โ) |
160 | 159 | nnrpd 13014 |
. . . . . . . 8
โข (๐ โ โ โ
(4โ๐) โ
โ+) |
161 | | nnrp 12985 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ+) |
162 | 160, 161 | rpdivcld 13033 |
. . . . . . 7
โข (๐ โ โ โ
((4โ๐) / ๐) โ
โ+) |
163 | 162 | rpred 13016 |
. . . . . 6
โข (๐ โ โ โ
((4โ๐) / ๐) โ
โ) |
164 | | nnmulcl 12236 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
165 | 117, 164 | mpan 689 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
166 | 165 | nnnn0d 12532 |
. . . . . . . 8
โข (๐ โ โ โ (2
ยท ๐) โ
โ0) |
167 | | nnz 12579 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
168 | | bccl 14282 |
. . . . . . . 8
โข (((2
ยท ๐) โ
โ0 โง ๐
โ โค) โ ((2 ยท ๐)C๐) โ
โ0) |
169 | 166, 167,
168 | syl2anc 585 |
. . . . . . 7
โข (๐ โ โ โ ((2
ยท ๐)C๐) โ
โ0) |
170 | 169 | nn0red 12533 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท ๐)C๐) โ
โ) |
171 | | 2rp 12979 |
. . . . . . 7
โข 2 โ
โ+ |
172 | 165 | peano2nnd 12229 |
. . . . . . . . 9
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
173 | 172 | nnrpd 13014 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ+) |
174 | | peano2nn 12224 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ + 1) โ
โ) |
175 | 174 | nnrpd 13014 |
. . . . . . . 8
โข (๐ โ โ โ (๐ + 1) โ
โ+) |
176 | 173, 175 | rpdivcld 13033 |
. . . . . . 7
โข (๐ โ โ โ (((2
ยท ๐) + 1) / (๐ + 1)) โ
โ+) |
177 | | rpmulcl 12997 |
. . . . . . 7
โข ((2
โ โ+ โง (((2 ยท ๐) + 1) / (๐ + 1)) โ โ+) โ (2
ยท (((2 ยท ๐) +
1) / (๐ + 1))) โ
โ+) |
178 | 171, 176,
177 | sylancr 588 |
. . . . . 6
โข (๐ โ โ โ (2
ยท (((2 ยท ๐) +
1) / (๐ + 1))) โ
โ+) |
179 | 163, 170,
178 | ltmul1d 13057 |
. . . . 5
โข (๐ โ โ โ
(((4โ๐) / ๐) < ((2 ยท ๐)C๐) โ (((4โ๐) / ๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))) < (((2 ยท ๐)C๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))))) |
180 | | bcp1ctr 26782 |
. . . . . . 7
โข (๐ โ โ0
โ ((2 ยท (๐ +
1))C(๐ + 1)) = (((2
ยท ๐)C๐) ยท (2 ยท (((2
ยท ๐) + 1) / (๐ + 1))))) |
181 | 157, 180 | syl 17 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท (๐ + 1))C(๐ + 1)) = (((2 ยท ๐)C๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1))))) |
182 | 181 | breq2d 5161 |
. . . . 5
โข (๐ โ โ โ
((((4โ๐) / ๐) ยท (2 ยท (((2
ยท ๐) + 1) / (๐ + 1)))) < ((2 ยท
(๐ + 1))C(๐ + 1)) โ (((4โ๐) / ๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))) < (((2 ยท ๐)C๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))))) |
183 | 179, 182 | bitr4d 282 |
. . . 4
โข (๐ โ โ โ
(((4โ๐) / ๐) < ((2 ยท ๐)C๐) โ (((4โ๐) / ๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))) < ((2 ยท (๐ + 1))C(๐ + 1)))) |
184 | | 2re 12286 |
. . . . . . . 8
โข 2 โ
โ |
185 | 184 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 2 โ
โ) |
186 | 173, 161 | rpdivcld 13033 |
. . . . . . . 8
โข (๐ โ โ โ (((2
ยท ๐) + 1) / ๐) โ
โ+) |
187 | 186 | rpred 13016 |
. . . . . . 7
โข (๐ โ โ โ (((2
ยท ๐) + 1) / ๐) โ
โ) |
188 | | nnmulcl 12236 |
. . . . . . . . . 10
โข
(((4โ๐) โ
โ โง 2 โ โ) โ ((4โ๐) ยท 2) โ
โ) |
189 | 159, 117,
188 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ โ โ
((4โ๐) ยท 2)
โ โ) |
190 | 189 | nnrpd 13014 |
. . . . . . . 8
โข (๐ โ โ โ
((4โ๐) ยท 2)
โ โ+) |
191 | 190, 175 | rpdivcld 13033 |
. . . . . . 7
โข (๐ โ โ โ
(((4โ๐) ยท 2) /
(๐ + 1)) โ
โ+) |
192 | 161 | rpreccld 13026 |
. . . . . . . . 9
โข (๐ โ โ โ (1 /
๐) โ
โ+) |
193 | | ltaddrp 13011 |
. . . . . . . . 9
โข ((2
โ โ โง (1 / ๐) โ โ+) โ 2 <
(2 + (1 / ๐))) |
194 | 184, 192,
193 | sylancr 588 |
. . . . . . . 8
โข (๐ โ โ โ 2 < (2
+ (1 / ๐))) |
195 | 165 | nncnd 12228 |
. . . . . . . . . 10
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
196 | | 1cnd 11209 |
. . . . . . . . . 10
โข (๐ โ โ โ 1 โ
โ) |
197 | | nncn 12220 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
198 | | nnne0 12246 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ 0) |
199 | 195, 196,
197, 198 | divdird 12028 |
. . . . . . . . 9
โข (๐ โ โ โ (((2
ยท ๐) + 1) / ๐) = (((2 ยท ๐) / ๐) + (1 / ๐))) |
200 | 32 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ โ 2 โ
โ) |
201 | 200, 197,
198 | divcan4d 11996 |
. . . . . . . . . 10
โข (๐ โ โ โ ((2
ยท ๐) / ๐) = 2) |
202 | 201 | oveq1d 7424 |
. . . . . . . . 9
โข (๐ โ โ โ (((2
ยท ๐) / ๐) + (1 / ๐)) = (2 + (1 / ๐))) |
203 | 199, 202 | eqtr2d 2774 |
. . . . . . . 8
โข (๐ โ โ โ (2 + (1 /
๐)) = (((2 ยท ๐) + 1) / ๐)) |
204 | 194, 203 | breqtrd 5175 |
. . . . . . 7
โข (๐ โ โ โ 2 <
(((2 ยท ๐) + 1) /
๐)) |
205 | 185, 187,
191, 204 | ltmul2dd 13072 |
. . . . . 6
โข (๐ โ โ โ
((((4โ๐) ยท 2) /
(๐ + 1)) ยท 2) <
((((4โ๐) ยท 2) /
(๐ + 1)) ยท (((2
ยท ๐) + 1) / ๐))) |
206 | | expp1 14034 |
. . . . . . . . . 10
โข ((4
โ โ โง ๐
โ โ0) โ (4โ(๐ + 1)) = ((4โ๐) ยท 4)) |
207 | 48, 157, 206 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ โ โ
(4โ(๐ + 1)) =
((4โ๐) ยท
4)) |
208 | 159 | nncnd 12228 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(4โ๐) โ
โ) |
209 | 208, 200,
200 | mulassd 11237 |
. . . . . . . . . 10
โข (๐ โ โ โ
(((4โ๐) ยท 2)
ยท 2) = ((4โ๐)
ยท (2 ยท 2))) |
210 | 103 | oveq2i 7420 |
. . . . . . . . . 10
โข
((4โ๐) ยท
(2 ยท 2)) = ((4โ๐) ยท 4) |
211 | 209, 210 | eqtrdi 2789 |
. . . . . . . . 9
โข (๐ โ โ โ
(((4โ๐) ยท 2)
ยท 2) = ((4โ๐)
ยท 4)) |
212 | 207, 211 | eqtr4d 2776 |
. . . . . . . 8
โข (๐ โ โ โ
(4โ(๐ + 1)) =
(((4โ๐) ยท 2)
ยท 2)) |
213 | 212 | oveq1d 7424 |
. . . . . . 7
โข (๐ โ โ โ
((4โ(๐ + 1)) / (๐ + 1)) = ((((4โ๐) ยท 2) ยท 2) /
(๐ + 1))) |
214 | 189 | nncnd 12228 |
. . . . . . . 8
โข (๐ โ โ โ
((4โ๐) ยท 2)
โ โ) |
215 | 174 | nncnd 12228 |
. . . . . . . 8
โข (๐ โ โ โ (๐ + 1) โ
โ) |
216 | 174 | nnne0d 12262 |
. . . . . . . 8
โข (๐ โ โ โ (๐ + 1) โ 0) |
217 | 214, 200,
215, 216 | div23d 12027 |
. . . . . . 7
โข (๐ โ โ โ
((((4โ๐) ยท 2)
ยท 2) / (๐ + 1)) =
((((4โ๐) ยท 2) /
(๐ + 1)) ยท
2)) |
218 | 213, 217 | eqtrd 2773 |
. . . . . 6
โข (๐ โ โ โ
((4โ(๐ + 1)) / (๐ + 1)) = ((((4โ๐) ยท 2) / (๐ + 1)) ยท
2)) |
219 | 208, 200,
197, 198 | div23d 12027 |
. . . . . . . 8
โข (๐ โ โ โ
(((4โ๐) ยท 2) /
๐) = (((4โ๐) / ๐) ยท 2)) |
220 | 219 | oveq1d 7424 |
. . . . . . 7
โข (๐ โ โ โ
((((4โ๐) ยท 2) /
๐) ยท (((2 ยท
๐) + 1) / (๐ + 1))) = ((((4โ๐) / ๐) ยท 2) ยท (((2 ยท ๐) + 1) / (๐ + 1)))) |
221 | 172 | nncnd 12228 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
222 | 214, 197,
221, 215, 198, 216 | divmul24d 12033 |
. . . . . . 7
โข (๐ โ โ โ
((((4โ๐) ยท 2) /
๐) ยท (((2 ยท
๐) + 1) / (๐ + 1))) = ((((4โ๐) ยท 2) / (๐ + 1)) ยท (((2 ยท
๐) + 1) / ๐))) |
223 | 162 | rpcnd 13018 |
. . . . . . . 8
โข (๐ โ โ โ
((4โ๐) / ๐) โ
โ) |
224 | 176 | rpcnd 13018 |
. . . . . . . 8
โข (๐ โ โ โ (((2
ยท ๐) + 1) / (๐ + 1)) โ
โ) |
225 | 223, 200,
224 | mulassd 11237 |
. . . . . . 7
โข (๐ โ โ โ
((((4โ๐) / ๐) ยท 2) ยท (((2
ยท ๐) + 1) / (๐ + 1))) = (((4โ๐) / ๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1))))) |
226 | 220, 222,
225 | 3eqtr3rd 2782 |
. . . . . 6
โข (๐ โ โ โ
(((4โ๐) / ๐) ยท (2 ยท (((2
ยท ๐) + 1) / (๐ + 1)))) = ((((4โ๐) ยท 2) / (๐ + 1)) ยท (((2 ยท
๐) + 1) / ๐))) |
227 | 205, 218,
226 | 3brtr4d 5181 |
. . . . 5
โข (๐ โ โ โ
((4โ(๐ + 1)) / (๐ + 1)) < (((4โ๐) / ๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1))))) |
228 | 174 | nnnn0d 12532 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ + 1) โ
โ0) |
229 | | nnexpcl 14040 |
. . . . . . . . . 10
โข ((4
โ โ โง (๐ +
1) โ โ0) โ (4โ(๐ + 1)) โ โ) |
230 | 154, 228,
229 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ โ โ
(4โ(๐ + 1)) โ
โ) |
231 | 230 | nnrpd 13014 |
. . . . . . . 8
โข (๐ โ โ โ
(4โ(๐ + 1)) โ
โ+) |
232 | 231, 175 | rpdivcld 13033 |
. . . . . . 7
โข (๐ โ โ โ
((4โ(๐ + 1)) / (๐ + 1)) โ
โ+) |
233 | 232 | rpred 13016 |
. . . . . 6
โข (๐ โ โ โ
((4โ(๐ + 1)) / (๐ + 1)) โ
โ) |
234 | 178 | rpred 13016 |
. . . . . . 7
โข (๐ โ โ โ (2
ยท (((2 ยท ๐) +
1) / (๐ + 1))) โ
โ) |
235 | 163, 234 | remulcld 11244 |
. . . . . 6
โข (๐ โ โ โ
(((4โ๐) / ๐) ยท (2 ยท (((2
ยท ๐) + 1) / (๐ + 1)))) โ
โ) |
236 | | nn0mulcl 12508 |
. . . . . . . . 9
โข ((2
โ โ0 โง (๐ + 1) โ โ0) โ (2
ยท (๐ + 1)) โ
โ0) |
237 | 33, 228, 236 | sylancr 588 |
. . . . . . . 8
โข (๐ โ โ โ (2
ยท (๐ + 1)) โ
โ0) |
238 | 174 | nnzd 12585 |
. . . . . . . 8
โข (๐ โ โ โ (๐ + 1) โ
โค) |
239 | | bccl 14282 |
. . . . . . . 8
โข (((2
ยท (๐ + 1)) โ
โ0 โง (๐ + 1) โ โค) โ ((2 ยท
(๐ + 1))C(๐ + 1)) โ
โ0) |
240 | 237, 238,
239 | syl2anc 585 |
. . . . . . 7
โข (๐ โ โ โ ((2
ยท (๐ + 1))C(๐ + 1)) โ
โ0) |
241 | 240 | nn0red 12533 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท (๐ + 1))C(๐ + 1)) โ
โ) |
242 | | lttr 11290 |
. . . . . 6
โข
((((4โ(๐ + 1))
/ (๐ + 1)) โ โ
โง (((4โ๐) / ๐) ยท (2 ยท (((2
ยท ๐) + 1) / (๐ + 1)))) โ โ โง
((2 ยท (๐ +
1))C(๐ + 1)) โ
โ) โ ((((4โ(๐ + 1)) / (๐ + 1)) < (((4โ๐) / ๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))) โง (((4โ๐) / ๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))) < ((2 ยท (๐ + 1))C(๐ + 1))) โ ((4โ(๐ + 1)) / (๐ + 1)) < ((2 ยท (๐ + 1))C(๐ + 1)))) |
243 | 233, 235,
241, 242 | syl3anc 1372 |
. . . . 5
โข (๐ โ โ โ
((((4โ(๐ + 1)) /
(๐ + 1)) <
(((4โ๐) / ๐) ยท (2 ยท (((2
ยท ๐) + 1) / (๐ + 1)))) โง (((4โ๐) / ๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))) < ((2 ยท (๐ + 1))C(๐ + 1))) โ ((4โ(๐ + 1)) / (๐ + 1)) < ((2 ยท (๐ + 1))C(๐ + 1)))) |
244 | 227, 243 | mpand 694 |
. . . 4
โข (๐ โ โ โ
((((4โ๐) / ๐) ยท (2 ยท (((2
ยท ๐) + 1) / (๐ + 1)))) < ((2 ยท
(๐ + 1))C(๐ + 1)) โ ((4โ(๐ + 1)) / (๐ + 1)) < ((2 ยท (๐ + 1))C(๐ + 1)))) |
245 | 183, 244 | sylbid 239 |
. . 3
โข (๐ โ โ โ
(((4โ๐) / ๐) < ((2 ยท ๐)C๐) โ ((4โ(๐ + 1)) / (๐ + 1)) < ((2 ยท (๐ + 1))C(๐ + 1)))) |
246 | 156, 245 | syl 17 |
. 2
โข (๐ โ
(โคโฅโ4) โ (((4โ๐) / ๐) < ((2 ยท ๐)C๐) โ ((4โ(๐ + 1)) / (๐ + 1)) < ((2 ยท (๐ + 1))C(๐ + 1)))) |
247 | 6, 12, 18, 24, 153, 246 | uzind4i 12894 |
1
โข (๐ โ
(โคโฅโ4) โ ((4โ๐) / ๐) < ((2 ยท ๐)C๐)) |