Step | Hyp | Ref
| Expression |
1 | | bposlem7.4 |
. . . . . . . . . . . . 13
β’ (π β π΅ β β) |
2 | 1 | nnrpd 12962 |
. . . . . . . . . . . 12
β’ (π β π΅ β
β+) |
3 | 2 | rpsqrtcld 15303 |
. . . . . . . . . . 11
β’ (π β (ββπ΅) β
β+) |
4 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π₯ = (ββπ΅) β (logβπ₯) =
(logβ(ββπ΅))) |
5 | | id 22 |
. . . . . . . . . . . . 13
β’ (π₯ = (ββπ΅) β π₯ = (ββπ΅)) |
6 | 4, 5 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π₯ = (ββπ΅) β ((logβπ₯) / π₯) = ((logβ(ββπ΅)) / (ββπ΅))) |
7 | | bposlem7.2 |
. . . . . . . . . . . 12
β’ πΊ = (π₯ β β+ β¦
((logβπ₯) / π₯)) |
8 | | ovex 7395 |
. . . . . . . . . . . 12
β’
((logβ(ββπ΅)) / (ββπ΅)) β V |
9 | 6, 7, 8 | fvmpt 6953 |
. . . . . . . . . . 11
β’
((ββπ΅)
β β+ β (πΊβ(ββπ΅)) = ((logβ(ββπ΅)) / (ββπ΅))) |
10 | 3, 9 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΊβ(ββπ΅)) = ((logβ(ββπ΅)) / (ββπ΅))) |
11 | | bposlem7.3 |
. . . . . . . . . . . . 13
β’ (π β π΄ β β) |
12 | 11 | nnrpd 12962 |
. . . . . . . . . . . 12
β’ (π β π΄ β
β+) |
13 | 12 | rpsqrtcld 15303 |
. . . . . . . . . . 11
β’ (π β (ββπ΄) β
β+) |
14 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π₯ = (ββπ΄) β (logβπ₯) =
(logβ(ββπ΄))) |
15 | | id 22 |
. . . . . . . . . . . . 13
β’ (π₯ = (ββπ΄) β π₯ = (ββπ΄)) |
16 | 14, 15 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π₯ = (ββπ΄) β ((logβπ₯) / π₯) = ((logβ(ββπ΄)) / (ββπ΄))) |
17 | | ovex 7395 |
. . . . . . . . . . . 12
β’
((logβ(ββπ΄)) / (ββπ΄)) β V |
18 | 16, 7, 17 | fvmpt 6953 |
. . . . . . . . . . 11
β’
((ββπ΄)
β β+ β (πΊβ(ββπ΄)) = ((logβ(ββπ΄)) / (ββπ΄))) |
19 | 13, 18 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΊβ(ββπ΄)) = ((logβ(ββπ΄)) / (ββπ΄))) |
20 | 10, 19 | breq12d 5123 |
. . . . . . . . 9
β’ (π β ((πΊβ(ββπ΅)) < (πΊβ(ββπ΄)) β ((logβ(ββπ΅)) / (ββπ΅)) <
((logβ(ββπ΄)) / (ββπ΄)))) |
21 | 13 | rpred 12964 |
. . . . . . . . . 10
β’ (π β (ββπ΄) β
β) |
22 | | bposlem7.5 |
. . . . . . . . . . . 12
β’ (π β (eβ2) β€ π΄) |
23 | 12 | rprege0d 12971 |
. . . . . . . . . . . . 13
β’ (π β (π΄ β β β§ 0 β€ π΄)) |
24 | | resqrtth 15147 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ 0 β€
π΄) β
((ββπ΄)β2)
= π΄) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((ββπ΄)β2) = π΄) |
26 | 22, 25 | breqtrrd 5138 |
. . . . . . . . . . 11
β’ (π β (eβ2) β€
((ββπ΄)β2)) |
27 | 13 | rpge0d 12968 |
. . . . . . . . . . . 12
β’ (π β 0 β€
(ββπ΄)) |
28 | | ere 15978 |
. . . . . . . . . . . . 13
β’ e β
β |
29 | | 0re 11164 |
. . . . . . . . . . . . . 14
β’ 0 β
β |
30 | | epos 16096 |
. . . . . . . . . . . . . 14
β’ 0 <
e |
31 | 29, 28, 30 | ltleii 11285 |
. . . . . . . . . . . . 13
β’ 0 β€
e |
32 | | le2sq 14046 |
. . . . . . . . . . . . 13
β’ (((e
β β β§ 0 β€ e) β§ ((ββπ΄) β β β§ 0 β€
(ββπ΄))) β
(e β€ (ββπ΄)
β (eβ2) β€ ((ββπ΄)β2))) |
33 | 28, 31, 32 | mpanl12 701 |
. . . . . . . . . . . 12
β’
(((ββπ΄)
β β β§ 0 β€ (ββπ΄)) β (e β€ (ββπ΄) β (eβ2) β€
((ββπ΄)β2))) |
34 | 21, 27, 33 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (e β€
(ββπ΄) β
(eβ2) β€ ((ββπ΄)β2))) |
35 | 26, 34 | mpbird 257 |
. . . . . . . . . 10
β’ (π β e β€
(ββπ΄)) |
36 | 3 | rpred 12964 |
. . . . . . . . . 10
β’ (π β (ββπ΅) β
β) |
37 | | bposlem7.6 |
. . . . . . . . . . . 12
β’ (π β (eβ2) β€ π΅) |
38 | 2 | rprege0d 12971 |
. . . . . . . . . . . . 13
β’ (π β (π΅ β β β§ 0 β€ π΅)) |
39 | | resqrtth 15147 |
. . . . . . . . . . . . 13
β’ ((π΅ β β β§ 0 β€
π΅) β
((ββπ΅)β2)
= π΅) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((ββπ΅)β2) = π΅) |
41 | 37, 40 | breqtrrd 5138 |
. . . . . . . . . . 11
β’ (π β (eβ2) β€
((ββπ΅)β2)) |
42 | 3 | rpge0d 12968 |
. . . . . . . . . . . 12
β’ (π β 0 β€
(ββπ΅)) |
43 | | le2sq 14046 |
. . . . . . . . . . . . 13
β’ (((e
β β β§ 0 β€ e) β§ ((ββπ΅) β β β§ 0 β€
(ββπ΅))) β
(e β€ (ββπ΅)
β (eβ2) β€ ((ββπ΅)β2))) |
44 | 28, 31, 43 | mpanl12 701 |
. . . . . . . . . . . 12
β’
(((ββπ΅)
β β β§ 0 β€ (ββπ΅)) β (e β€ (ββπ΅) β (eβ2) β€
((ββπ΅)β2))) |
45 | 36, 42, 44 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (e β€
(ββπ΅) β
(eβ2) β€ ((ββπ΅)β2))) |
46 | 41, 45 | mpbird 257 |
. . . . . . . . . 10
β’ (π β e β€
(ββπ΅)) |
47 | | logdivlt 25992 |
. . . . . . . . . 10
β’
((((ββπ΄)
β β β§ e β€ (ββπ΄)) β§ ((ββπ΅) β β β§ e β€
(ββπ΅))) β
((ββπ΄) <
(ββπ΅) β
((logβ(ββπ΅)) / (ββπ΅)) < ((logβ(ββπ΄)) / (ββπ΄)))) |
48 | 21, 35, 36, 46, 47 | syl22anc 838 |
. . . . . . . . 9
β’ (π β ((ββπ΄) < (ββπ΅) β
((logβ(ββπ΅)) / (ββπ΅)) < ((logβ(ββπ΄)) / (ββπ΄)))) |
49 | 21, 36, 27, 42 | lt2sqd 14166 |
. . . . . . . . 9
β’ (π β ((ββπ΄) < (ββπ΅) β ((ββπ΄)β2) <
((ββπ΅)β2))) |
50 | 20, 48, 49 | 3bitr2rd 308 |
. . . . . . . 8
β’ (π β (((ββπ΄)β2) <
((ββπ΅)β2)
β (πΊβ(ββπ΅)) < (πΊβ(ββπ΄)))) |
51 | 25, 40 | breq12d 5123 |
. . . . . . . 8
β’ (π β (((ββπ΄)β2) <
((ββπ΅)β2)
β π΄ < π΅)) |
52 | | relogcl 25947 |
. . . . . . . . . . . . 13
β’ (π₯ β β+
β (logβπ₯) β
β) |
53 | | rerpdivcl 12952 |
. . . . . . . . . . . . 13
β’
(((logβπ₯)
β β β§ π₯
β β+) β ((logβπ₯) / π₯) β β) |
54 | 52, 53 | mpancom 687 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β ((logβπ₯) /
π₯) β
β) |
55 | 7, 54 | fmpti 7065 |
. . . . . . . . . . 11
β’ πΊ:β+βΆβ |
56 | 55 | ffvelcdmi 7039 |
. . . . . . . . . 10
β’
((ββπ΅)
β β+ β (πΊβ(ββπ΅)) β β) |
57 | 3, 56 | syl 17 |
. . . . . . . . 9
β’ (π β (πΊβ(ββπ΅)) β β) |
58 | 55 | ffvelcdmi 7039 |
. . . . . . . . . 10
β’
((ββπ΄)
β β+ β (πΊβ(ββπ΄)) β β) |
59 | 13, 58 | syl 17 |
. . . . . . . . 9
β’ (π β (πΊβ(ββπ΄)) β β) |
60 | | 2rp 12927 |
. . . . . . . . . 10
β’ 2 β
β+ |
61 | | rpsqrtcl 15156 |
. . . . . . . . . 10
β’ (2 β
β+ β (ββ2) β
β+) |
62 | 60, 61 | mp1i 13 |
. . . . . . . . 9
β’ (π β (ββ2) β
β+) |
63 | 57, 59, 62 | ltmul2d 13006 |
. . . . . . . 8
β’ (π β ((πΊβ(ββπ΅)) < (πΊβ(ββπ΄)) β ((ββ2) Β· (πΊβ(ββπ΅))) < ((ββ2)
Β· (πΊβ(ββπ΄))))) |
64 | 50, 51, 63 | 3bitr3d 309 |
. . . . . . 7
β’ (π β (π΄ < π΅ β ((ββ2) Β· (πΊβ(ββπ΅))) < ((ββ2)
Β· (πΊβ(ββπ΄))))) |
65 | 64 | biimpd 228 |
. . . . . 6
β’ (π β (π΄ < π΅ β ((ββ2) Β· (πΊβ(ββπ΅))) < ((ββ2)
Β· (πΊβ(ββπ΄))))) |
66 | 11 | nnred 12175 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
67 | 1 | nnred 12175 |
. . . . . . . . . 10
β’ (π β π΅ β β) |
68 | | 2re 12234 |
. . . . . . . . . . . 12
β’ 2 β
β |
69 | | 2pos 12263 |
. . . . . . . . . . . 12
β’ 0 <
2 |
70 | 68, 69 | pm3.2i 472 |
. . . . . . . . . . 11
β’ (2 β
β β§ 0 < 2) |
71 | 70 | a1i 11 |
. . . . . . . . . 10
β’ (π β (2 β β β§ 0
< 2)) |
72 | | ltdiv1 12026 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β β§ (2 β
β β§ 0 < 2)) β (π΄ < π΅ β (π΄ / 2) < (π΅ / 2))) |
73 | 66, 67, 71, 72 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π΄ < π΅ β (π΄ / 2) < (π΅ / 2))) |
74 | 12 | rphalfcld 12976 |
. . . . . . . . . . 11
β’ (π β (π΄ / 2) β
β+) |
75 | 74 | rpred 12964 |
. . . . . . . . . 10
β’ (π β (π΄ / 2) β β) |
76 | 28, 68 | remulcli 11178 |
. . . . . . . . . . . . 13
β’ (e
Β· 2) β β |
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (e Β· 2) β
β) |
78 | 28 | resqcli 14097 |
. . . . . . . . . . . . 13
β’
(eβ2) β β |
79 | 78 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (eβ2) β
β) |
80 | | egt2lt3 16095 |
. . . . . . . . . . . . . . . . 17
β’ (2 < e
β§ e < 3) |
81 | 80 | simpli 485 |
. . . . . . . . . . . . . . . 16
β’ 2 <
e |
82 | 68, 28, 81 | ltleii 11285 |
. . . . . . . . . . . . . . 15
β’ 2 β€
e |
83 | 68, 28, 28 | lemul2i 12085 |
. . . . . . . . . . . . . . . 16
β’ (0 < e
β (2 β€ e β (e Β· 2) β€ (e Β· e))) |
84 | 30, 83 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (2 β€ e
β (e Β· 2) β€ (e Β· e)) |
85 | 82, 84 | mpbi 229 |
. . . . . . . . . . . . . 14
β’ (e
Β· 2) β€ (e Β· e) |
86 | 28 | recni 11176 |
. . . . . . . . . . . . . . 15
β’ e β
β |
87 | 86 | sqvali 14091 |
. . . . . . . . . . . . . 14
β’
(eβ2) = (e Β· e) |
88 | 85, 87 | breqtrri 5137 |
. . . . . . . . . . . . 13
β’ (e
Β· 2) β€ (eβ2) |
89 | 88 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (e Β· 2) β€
(eβ2)) |
90 | 77, 79, 66, 89, 22 | letrd 11319 |
. . . . . . . . . . 11
β’ (π β (e Β· 2) β€ π΄) |
91 | | lemuldiv 12042 |
. . . . . . . . . . . . 13
β’ ((e
β β β§ π΄
β β β§ (2 β β β§ 0 < 2)) β ((e Β· 2)
β€ π΄ β e β€ (π΄ / 2))) |
92 | 28, 70, 91 | mp3an13 1453 |
. . . . . . . . . . . 12
β’ (π΄ β β β ((e
Β· 2) β€ π΄ β e
β€ (π΄ /
2))) |
93 | 66, 92 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((e Β· 2) β€ π΄ β e β€ (π΄ / 2))) |
94 | 90, 93 | mpbid 231 |
. . . . . . . . . 10
β’ (π β e β€ (π΄ / 2)) |
95 | 2 | rphalfcld 12976 |
. . . . . . . . . . 11
β’ (π β (π΅ / 2) β
β+) |
96 | 95 | rpred 12964 |
. . . . . . . . . 10
β’ (π β (π΅ / 2) β β) |
97 | 77, 79, 67, 89, 37 | letrd 11319 |
. . . . . . . . . . 11
β’ (π β (e Β· 2) β€ π΅) |
98 | | lemuldiv 12042 |
. . . . . . . . . . . . 13
β’ ((e
β β β§ π΅
β β β§ (2 β β β§ 0 < 2)) β ((e Β· 2)
β€ π΅ β e β€ (π΅ / 2))) |
99 | 28, 70, 98 | mp3an13 1453 |
. . . . . . . . . . . 12
β’ (π΅ β β β ((e
Β· 2) β€ π΅ β e
β€ (π΅ /
2))) |
100 | 67, 99 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((e Β· 2) β€ π΅ β e β€ (π΅ / 2))) |
101 | 97, 100 | mpbid 231 |
. . . . . . . . . 10
β’ (π β e β€ (π΅ / 2)) |
102 | | logdivlt 25992 |
. . . . . . . . . 10
β’ ((((π΄ / 2) β β β§ e
β€ (π΄ / 2)) β§ ((π΅ / 2) β β β§ e
β€ (π΅ / 2))) β
((π΄ / 2) < (π΅ / 2) β ((logβ(π΅ / 2)) / (π΅ / 2)) < ((logβ(π΄ / 2)) / (π΄ / 2)))) |
103 | 75, 94, 96, 101, 102 | syl22anc 838 |
. . . . . . . . 9
β’ (π β ((π΄ / 2) < (π΅ / 2) β ((logβ(π΅ / 2)) / (π΅ / 2)) < ((logβ(π΄ / 2)) / (π΄ / 2)))) |
104 | 73, 103 | bitrd 279 |
. . . . . . . 8
β’ (π β (π΄ < π΅ β ((logβ(π΅ / 2)) / (π΅ / 2)) < ((logβ(π΄ / 2)) / (π΄ / 2)))) |
105 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π₯ = (π΅ / 2) β (logβπ₯) = (logβ(π΅ / 2))) |
106 | | id 22 |
. . . . . . . . . . . 12
β’ (π₯ = (π΅ / 2) β π₯ = (π΅ / 2)) |
107 | 105, 106 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π₯ = (π΅ / 2) β ((logβπ₯) / π₯) = ((logβ(π΅ / 2)) / (π΅ / 2))) |
108 | | ovex 7395 |
. . . . . . . . . . 11
β’
((logβ(π΅ / 2))
/ (π΅ / 2)) β
V |
109 | 107, 7, 108 | fvmpt 6953 |
. . . . . . . . . 10
β’ ((π΅ / 2) β β+
β (πΊβ(π΅ / 2)) = ((logβ(π΅ / 2)) / (π΅ / 2))) |
110 | 95, 109 | syl 17 |
. . . . . . . . 9
β’ (π β (πΊβ(π΅ / 2)) = ((logβ(π΅ / 2)) / (π΅ / 2))) |
111 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π₯ = (π΄ / 2) β (logβπ₯) = (logβ(π΄ / 2))) |
112 | | id 22 |
. . . . . . . . . . . 12
β’ (π₯ = (π΄ / 2) β π₯ = (π΄ / 2)) |
113 | 111, 112 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π₯ = (π΄ / 2) β ((logβπ₯) / π₯) = ((logβ(π΄ / 2)) / (π΄ / 2))) |
114 | | ovex 7395 |
. . . . . . . . . . 11
β’
((logβ(π΄ / 2))
/ (π΄ / 2)) β
V |
115 | 113, 7, 114 | fvmpt 6953 |
. . . . . . . . . 10
β’ ((π΄ / 2) β β+
β (πΊβ(π΄ / 2)) = ((logβ(π΄ / 2)) / (π΄ / 2))) |
116 | 74, 115 | syl 17 |
. . . . . . . . 9
β’ (π β (πΊβ(π΄ / 2)) = ((logβ(π΄ / 2)) / (π΄ / 2))) |
117 | 110, 116 | breq12d 5123 |
. . . . . . . 8
β’ (π β ((πΊβ(π΅ / 2)) < (πΊβ(π΄ / 2)) β ((logβ(π΅ / 2)) / (π΅ / 2)) < ((logβ(π΄ / 2)) / (π΄ / 2)))) |
118 | 55 | ffvelcdmi 7039 |
. . . . . . . . . 10
β’ ((π΅ / 2) β β+
β (πΊβ(π΅ / 2)) β
β) |
119 | 95, 118 | syl 17 |
. . . . . . . . 9
β’ (π β (πΊβ(π΅ / 2)) β β) |
120 | 55 | ffvelcdmi 7039 |
. . . . . . . . . 10
β’ ((π΄ / 2) β β+
β (πΊβ(π΄ / 2)) β
β) |
121 | 74, 120 | syl 17 |
. . . . . . . . 9
β’ (π β (πΊβ(π΄ / 2)) β β) |
122 | | 9nn 12258 |
. . . . . . . . . . 11
β’ 9 β
β |
123 | | 4nn 12243 |
. . . . . . . . . . 11
β’ 4 β
β |
124 | | nnrp 12933 |
. . . . . . . . . . . 12
β’ (9 β
β β 9 β β+) |
125 | | nnrp 12933 |
. . . . . . . . . . . 12
β’ (4 β
β β 4 β β+) |
126 | | rpdivcl 12947 |
. . . . . . . . . . . 12
β’ ((9
β β+ β§ 4 β β+) β (9 / 4)
β β+) |
127 | 124, 125,
126 | syl2an 597 |
. . . . . . . . . . 11
β’ ((9
β β β§ 4 β β) β (9 / 4) β
β+) |
128 | 122, 123,
127 | mp2an 691 |
. . . . . . . . . 10
β’ (9 / 4)
β β+ |
129 | 128 | a1i 11 |
. . . . . . . . 9
β’ (π β (9 / 4) β
β+) |
130 | 119, 121,
129 | ltmul2d 13006 |
. . . . . . . 8
β’ (π β ((πΊβ(π΅ / 2)) < (πΊβ(π΄ / 2)) β ((9 / 4) Β· (πΊβ(π΅ / 2))) < ((9 / 4) Β· (πΊβ(π΄ / 2))))) |
131 | 104, 117,
130 | 3bitr2d 307 |
. . . . . . 7
β’ (π β (π΄ < π΅ β ((9 / 4) Β· (πΊβ(π΅ / 2))) < ((9 / 4) Β· (πΊβ(π΄ / 2))))) |
132 | 131 | biimpd 228 |
. . . . . 6
β’ (π β (π΄ < π΅ β ((9 / 4) Β· (πΊβ(π΅ / 2))) < ((9 / 4) Β· (πΊβ(π΄ / 2))))) |
133 | 65, 132 | jcad 514 |
. . . . 5
β’ (π β (π΄ < π΅ β (((ββ2) Β· (πΊβ(ββπ΅))) < ((ββ2)
Β· (πΊβ(ββπ΄))) β§ ((9 / 4) Β· (πΊβ(π΅ / 2))) < ((9 / 4) Β· (πΊβ(π΄ / 2)))))) |
134 | | sqrt2re 16139 |
. . . . . . 7
β’
(ββ2) β β |
135 | | remulcl 11143 |
. . . . . . 7
β’
(((ββ2) β β β§ (πΊβ(ββπ΅)) β β) β ((ββ2)
Β· (πΊβ(ββπ΅))) β β) |
136 | 134, 57, 135 | sylancr 588 |
. . . . . 6
β’ (π β ((ββ2)
Β· (πΊβ(ββπ΅))) β β) |
137 | | 9re 12259 |
. . . . . . . 8
β’ 9 β
β |
138 | | 4re 12244 |
. . . . . . . 8
β’ 4 β
β |
139 | | 4ne0 12268 |
. . . . . . . 8
β’ 4 β
0 |
140 | 137, 138,
139 | redivcli 11929 |
. . . . . . 7
β’ (9 / 4)
β β |
141 | | remulcl 11143 |
. . . . . . 7
β’ (((9 / 4)
β β β§ (πΊβ(π΅ / 2)) β β) β ((9 / 4)
Β· (πΊβ(π΅ / 2))) β
β) |
142 | 140, 119,
141 | sylancr 588 |
. . . . . 6
β’ (π β ((9 / 4) Β· (πΊβ(π΅ / 2))) β β) |
143 | | remulcl 11143 |
. . . . . . 7
β’
(((ββ2) β β β§ (πΊβ(ββπ΄)) β β) β ((ββ2)
Β· (πΊβ(ββπ΄))) β β) |
144 | 134, 59, 143 | sylancr 588 |
. . . . . 6
β’ (π β ((ββ2)
Β· (πΊβ(ββπ΄))) β β) |
145 | | remulcl 11143 |
. . . . . . 7
β’ (((9 / 4)
β β β§ (πΊβ(π΄ / 2)) β β) β ((9 / 4)
Β· (πΊβ(π΄ / 2))) β
β) |
146 | 140, 121,
145 | sylancr 588 |
. . . . . 6
β’ (π β ((9 / 4) Β· (πΊβ(π΄ / 2))) β β) |
147 | | lt2add 11647 |
. . . . . 6
β’
(((((ββ2) Β· (πΊβ(ββπ΅))) β β β§ ((9 / 4) Β·
(πΊβ(π΅ / 2))) β β) β§
(((ββ2) Β· (πΊβ(ββπ΄))) β β β§ ((9 / 4) Β·
(πΊβ(π΄ / 2))) β β)) β
((((ββ2) Β· (πΊβ(ββπ΅))) < ((ββ2) Β· (πΊβ(ββπ΄))) β§ ((9 / 4) Β·
(πΊβ(π΅ / 2))) < ((9 / 4) Β· (πΊβ(π΄ / 2)))) β (((ββ2) Β·
(πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) < (((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))))) |
148 | 136, 142,
144, 146, 147 | syl22anc 838 |
. . . . 5
β’ (π β ((((ββ2)
Β· (πΊβ(ββπ΅))) < ((ββ2) Β· (πΊβ(ββπ΄))) β§ ((9 / 4) Β·
(πΊβ(π΅ / 2))) < ((9 / 4) Β· (πΊβ(π΄ / 2)))) β (((ββ2) Β·
(πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) < (((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))))) |
149 | 133, 148 | syld 47 |
. . . 4
β’ (π β (π΄ < π΅ β (((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) < (((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))))) |
150 | | ltmul2 12013 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ (2 β
β β§ 0 < 2)) β (π΄ < π΅ β (2 Β· π΄) < (2 Β· π΅))) |
151 | 66, 67, 71, 150 | syl3anc 1372 |
. . . . . 6
β’ (π β (π΄ < π΅ β (2 Β· π΄) < (2 Β· π΅))) |
152 | | rpmulcl 12945 |
. . . . . . . . . 10
β’ ((2
β β+ β§ π΄ β β+) β (2
Β· π΄) β
β+) |
153 | 60, 12, 152 | sylancr 588 |
. . . . . . . . 9
β’ (π β (2 Β· π΄) β
β+) |
154 | 153 | rpsqrtcld 15303 |
. . . . . . . 8
β’ (π β (ββ(2 Β·
π΄)) β
β+) |
155 | | rpmulcl 12945 |
. . . . . . . . . 10
β’ ((2
β β+ β§ π΅ β β+) β (2
Β· π΅) β
β+) |
156 | 60, 2, 155 | sylancr 588 |
. . . . . . . . 9
β’ (π β (2 Β· π΅) β
β+) |
157 | 156 | rpsqrtcld 15303 |
. . . . . . . 8
β’ (π β (ββ(2 Β·
π΅)) β
β+) |
158 | | rprege0 12937 |
. . . . . . . . 9
β’
((ββ(2 Β· π΄)) β β+ β
((ββ(2 Β· π΄)) β β β§ 0 β€
(ββ(2 Β· π΄)))) |
159 | | rprege0 12937 |
. . . . . . . . 9
β’
((ββ(2 Β· π΅)) β β+ β
((ββ(2 Β· π΅)) β β β§ 0 β€
(ββ(2 Β· π΅)))) |
160 | | lt2sq 14045 |
. . . . . . . . 9
β’
((((ββ(2 Β· π΄)) β β β§ 0 β€
(ββ(2 Β· π΄))) β§ ((ββ(2 Β· π΅)) β β β§ 0 β€
(ββ(2 Β· π΅)))) β ((ββ(2 Β·
π΄)) < (ββ(2
Β· π΅)) β
((ββ(2 Β· π΄))β2) < ((ββ(2 Β·
π΅))β2))) |
161 | 158, 159,
160 | syl2an 597 |
. . . . . . . 8
β’
(((ββ(2 Β· π΄)) β β+ β§
(ββ(2 Β· π΅)) β β+) β
((ββ(2 Β· π΄)) < (ββ(2 Β· π΅)) β ((ββ(2
Β· π΄))β2) <
((ββ(2 Β· π΅))β2))) |
162 | 154, 157,
161 | syl2anc 585 |
. . . . . . 7
β’ (π β ((ββ(2
Β· π΄)) <
(ββ(2 Β· π΅)) β ((ββ(2 Β· π΄))β2) <
((ββ(2 Β· π΅))β2))) |
163 | 153 | rprege0d 12971 |
. . . . . . . . 9
β’ (π β ((2 Β· π΄) β β β§ 0 β€ (2
Β· π΄))) |
164 | | resqrtth 15147 |
. . . . . . . . 9
β’ (((2
Β· π΄) β β
β§ 0 β€ (2 Β· π΄)) β ((ββ(2 Β· π΄))β2) = (2 Β· π΄)) |
165 | 163, 164 | syl 17 |
. . . . . . . 8
β’ (π β ((ββ(2
Β· π΄))β2) = (2
Β· π΄)) |
166 | 156 | rprege0d 12971 |
. . . . . . . . 9
β’ (π β ((2 Β· π΅) β β β§ 0 β€ (2
Β· π΅))) |
167 | | resqrtth 15147 |
. . . . . . . . 9
β’ (((2
Β· π΅) β β
β§ 0 β€ (2 Β· π΅)) β ((ββ(2 Β· π΅))β2) = (2 Β· π΅)) |
168 | 166, 167 | syl 17 |
. . . . . . . 8
β’ (π β ((ββ(2
Β· π΅))β2) = (2
Β· π΅)) |
169 | 165, 168 | breq12d 5123 |
. . . . . . 7
β’ (π β (((ββ(2
Β· π΄))β2) <
((ββ(2 Β· π΅))β2) β (2 Β· π΄) < (2 Β· π΅))) |
170 | 162, 169 | bitr2d 280 |
. . . . . 6
β’ (π β ((2 Β· π΄) < (2 Β· π΅) β (ββ(2
Β· π΄)) <
(ββ(2 Β· π΅)))) |
171 | | 1lt2 12331 |
. . . . . . . . 9
β’ 1 <
2 |
172 | | rplogcl 25975 |
. . . . . . . . 9
β’ ((2
β β β§ 1 < 2) β (logβ2) β
β+) |
173 | 68, 171, 172 | mp2an 691 |
. . . . . . . 8
β’
(logβ2) β β+ |
174 | 173 | a1i 11 |
. . . . . . 7
β’ (π β (logβ2) β
β+) |
175 | 154, 157,
174 | ltdiv2d 12987 |
. . . . . 6
β’ (π β ((ββ(2
Β· π΄)) <
(ββ(2 Β· π΅)) β ((logβ2) / (ββ(2
Β· π΅))) <
((logβ2) / (ββ(2 Β· π΄))))) |
176 | 151, 170,
175 | 3bitrd 305 |
. . . . 5
β’ (π β (π΄ < π΅ β ((logβ2) / (ββ(2
Β· π΅))) <
((logβ2) / (ββ(2 Β· π΄))))) |
177 | 176 | biimpd 228 |
. . . 4
β’ (π β (π΄ < π΅ β ((logβ2) / (ββ(2
Β· π΅))) <
((logβ2) / (ββ(2 Β· π΄))))) |
178 | 149, 177 | jcad 514 |
. . 3
β’ (π β (π΄ < π΅ β ((((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) < (((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) β§ ((logβ2) /
(ββ(2 Β· π΅))) < ((logβ2) / (ββ(2
Β· π΄)))))) |
179 | 136, 142 | readdcld 11191 |
. . . 4
β’ (π β (((ββ2)
Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) β β) |
180 | | rpre 12930 |
. . . . . 6
β’
((logβ2) β β+ β (logβ2) β
β) |
181 | 173, 180 | ax-mp 5 |
. . . . 5
β’
(logβ2) β β |
182 | | rerpdivcl 12952 |
. . . . 5
β’
(((logβ2) β β β§ (ββ(2 Β· π΅)) β β+)
β ((logβ2) / (ββ(2 Β· π΅))) β β) |
183 | 181, 157,
182 | sylancr 588 |
. . . 4
β’ (π β ((logβ2) /
(ββ(2 Β· π΅))) β β) |
184 | 144, 146 | readdcld 11191 |
. . . 4
β’ (π β (((ββ2)
Β· (πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) β β) |
185 | | rerpdivcl 12952 |
. . . . 5
β’
(((logβ2) β β β§ (ββ(2 Β· π΄)) β β+)
β ((logβ2) / (ββ(2 Β· π΄))) β β) |
186 | 181, 154,
185 | sylancr 588 |
. . . 4
β’ (π β ((logβ2) /
(ββ(2 Β· π΄))) β β) |
187 | | lt2add 11647 |
. . . 4
β’
((((((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) β β β§ ((logβ2)
/ (ββ(2 Β· π΅))) β β) β§
((((ββ2) Β· (πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) β β β§ ((logβ2)
/ (ββ(2 Β· π΄))) β β)) β
(((((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) < (((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) β§ ((logβ2) /
(ββ(2 Β· π΅))) < ((logβ2) / (ββ(2
Β· π΄)))) β
((((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) + ((logβ2) /
(ββ(2 Β· π΅)))) < ((((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) + ((logβ2) /
(ββ(2 Β· π΄)))))) |
188 | 179, 183,
184, 186, 187 | syl22anc 838 |
. . 3
β’ (π β (((((ββ2)
Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) < (((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) β§ ((logβ2) /
(ββ(2 Β· π΅))) < ((logβ2) / (ββ(2
Β· π΄)))) β
((((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) + ((logβ2) /
(ββ(2 Β· π΅)))) < ((((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) + ((logβ2) /
(ββ(2 Β· π΄)))))) |
189 | 178, 188 | syld 47 |
. 2
β’ (π β (π΄ < π΅ β ((((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) + ((logβ2) /
(ββ(2 Β· π΅)))) < ((((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) + ((logβ2) /
(ββ(2 Β· π΄)))))) |
190 | | 2fveq3 6852 |
. . . . . . . 8
β’ (π = π΅ β (πΊβ(ββπ)) = (πΊβ(ββπ΅))) |
191 | 190 | oveq2d 7378 |
. . . . . . 7
β’ (π = π΅ β ((ββ2) Β· (πΊβ(ββπ))) = ((ββ2)
Β· (πΊβ(ββπ΅)))) |
192 | | fvoveq1 7385 |
. . . . . . . 8
β’ (π = π΅ β (πΊβ(π / 2)) = (πΊβ(π΅ / 2))) |
193 | 192 | oveq2d 7378 |
. . . . . . 7
β’ (π = π΅ β ((9 / 4) Β· (πΊβ(π / 2))) = ((9 / 4) Β· (πΊβ(π΅ / 2)))) |
194 | 191, 193 | oveq12d 7380 |
. . . . . 6
β’ (π = π΅ β (((ββ2) Β· (πΊβ(ββπ))) + ((9 / 4) Β· (πΊβ(π / 2)))) = (((ββ2) Β·
(πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2))))) |
195 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π΅ β (2 Β· π) = (2 Β· π΅)) |
196 | 195 | fveq2d 6851 |
. . . . . . 7
β’ (π = π΅ β (ββ(2 Β· π)) = (ββ(2 Β·
π΅))) |
197 | 196 | oveq2d 7378 |
. . . . . 6
β’ (π = π΅ β ((logβ2) / (ββ(2
Β· π))) =
((logβ2) / (ββ(2 Β· π΅)))) |
198 | 194, 197 | oveq12d 7380 |
. . . . 5
β’ (π = π΅ β ((((ββ2) Β· (πΊβ(ββπ))) + ((9 / 4) Β· (πΊβ(π / 2)))) + ((logβ2) / (ββ(2
Β· π)))) =
((((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) + ((logβ2) /
(ββ(2 Β· π΅))))) |
199 | | bposlem7.1 |
. . . . 5
β’ πΉ = (π β β β¦ ((((ββ2)
Β· (πΊβ(ββπ))) + ((9 / 4) Β· (πΊβ(π / 2)))) + ((logβ2) / (ββ(2
Β· π))))) |
200 | | ovex 7395 |
. . . . 5
β’
((((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) + ((logβ2) /
(ββ(2 Β· π΅)))) β V |
201 | 198, 199,
200 | fvmpt 6953 |
. . . 4
β’ (π΅ β β β (πΉβπ΅) = ((((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) + ((logβ2) /
(ββ(2 Β· π΅))))) |
202 | 1, 201 | syl 17 |
. . 3
β’ (π β (πΉβπ΅) = ((((ββ2) Β· (πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) + ((logβ2) /
(ββ(2 Β· π΅))))) |
203 | | 2fveq3 6852 |
. . . . . . . 8
β’ (π = π΄ β (πΊβ(ββπ)) = (πΊβ(ββπ΄))) |
204 | 203 | oveq2d 7378 |
. . . . . . 7
β’ (π = π΄ β ((ββ2) Β· (πΊβ(ββπ))) = ((ββ2)
Β· (πΊβ(ββπ΄)))) |
205 | | fvoveq1 7385 |
. . . . . . . 8
β’ (π = π΄ β (πΊβ(π / 2)) = (πΊβ(π΄ / 2))) |
206 | 205 | oveq2d 7378 |
. . . . . . 7
β’ (π = π΄ β ((9 / 4) Β· (πΊβ(π / 2))) = ((9 / 4) Β· (πΊβ(π΄ / 2)))) |
207 | 204, 206 | oveq12d 7380 |
. . . . . 6
β’ (π = π΄ β (((ββ2) Β· (πΊβ(ββπ))) + ((9 / 4) Β· (πΊβ(π / 2)))) = (((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2))))) |
208 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π΄ β (2 Β· π) = (2 Β· π΄)) |
209 | 208 | fveq2d 6851 |
. . . . . . 7
β’ (π = π΄ β (ββ(2 Β· π)) = (ββ(2 Β·
π΄))) |
210 | 209 | oveq2d 7378 |
. . . . . 6
β’ (π = π΄ β ((logβ2) / (ββ(2
Β· π))) =
((logβ2) / (ββ(2 Β· π΄)))) |
211 | 207, 210 | oveq12d 7380 |
. . . . 5
β’ (π = π΄ β ((((ββ2) Β· (πΊβ(ββπ))) + ((9 / 4) Β· (πΊβ(π / 2)))) + ((logβ2) / (ββ(2
Β· π)))) =
((((ββ2) Β· (πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) + ((logβ2) /
(ββ(2 Β· π΄))))) |
212 | | ovex 7395 |
. . . . 5
β’
((((ββ2) Β· (πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) + ((logβ2) /
(ββ(2 Β· π΄)))) β V |
213 | 211, 199,
212 | fvmpt 6953 |
. . . 4
β’ (π΄ β β β (πΉβπ΄) = ((((ββ2) Β· (πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) + ((logβ2) /
(ββ(2 Β· π΄))))) |
214 | 11, 213 | syl 17 |
. . 3
β’ (π β (πΉβπ΄) = ((((ββ2) Β· (πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) + ((logβ2) /
(ββ(2 Β· π΄))))) |
215 | 202, 214 | breq12d 5123 |
. 2
β’ (π β ((πΉβπ΅) < (πΉβπ΄) β ((((ββ2) Β·
(πΊβ(ββπ΅))) + ((9 / 4) Β· (πΊβ(π΅ / 2)))) + ((logβ2) /
(ββ(2 Β· π΅)))) < ((((ββ2) Β·
(πΊβ(ββπ΄))) + ((9 / 4) Β· (πΊβ(π΄ / 2)))) + ((logβ2) /
(ββ(2 Β· π΄)))))) |
216 | 189, 215 | sylibrd 259 |
1
β’ (π β (π΄ < π΅ β (πΉβπ΅) < (πΉβπ΄))) |