Step | Hyp | Ref
| Expression |
1 | | ovexd 7397 |
. . . . 5
β’ (β€
β (2[,)+β) β V) |
2 | | ovexd 7397 |
. . . . 5
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) / π₯) β V) |
3 | | ovexd 7397 |
. . . . 5
β’
((β€ β§ π₯
β (2[,)+β)) β (((Οβπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)) β V) |
4 | | eqidd 2738 |
. . . . 5
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) = (π₯ β (2[,)+β) β¦
((ΞΈβπ₯) / π₯))) |
5 | | simpr 486 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (2[,)+β)) β π₯ β (2[,)+β)) |
6 | | 2re 12234 |
. . . . . . . . . . 11
β’ 2 β
β |
7 | | elicopnf 13369 |
. . . . . . . . . . 11
β’ (2 β
β β (π₯ β
(2[,)+β) β (π₯
β β β§ 2 β€ π₯))) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β
(π₯ β β β§ 2
β€ π₯)) |
9 | 5, 8 | sylib 217 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (2[,)+β)) β (π₯ β β β§ 2 β€ π₯)) |
10 | | chtrpcl 26540 |
. . . . . . . . 9
β’ ((π₯ β β β§ 2 β€
π₯) β
(ΞΈβπ₯) β
β+) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’
((β€ β§ π₯
β (2[,)+β)) β (ΞΈβπ₯) β
β+) |
12 | 11 | rpcnne0d 12973 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) β β β§ (ΞΈβπ₯) β 0)) |
13 | | ppinncl 26539 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ 2 β€
π₯) β
(Οβπ₯)
β β) |
14 | 9, 13 | syl 17 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (2[,)+β)) β (Οβπ₯) β β) |
15 | 14 | nnrpd 12962 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (2[,)+β)) β (Οβπ₯) β
β+) |
16 | 9 | simpld 496 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (2[,)+β)) β π₯ β β) |
17 | | 1red 11163 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (2[,)+β)) β 1 β β) |
18 | 6 | a1i 11 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (2[,)+β)) β 2 β β) |
19 | | 1lt2 12331 |
. . . . . . . . . . . 12
β’ 1 <
2 |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (2[,)+β)) β 1 < 2) |
21 | 9 | simprd 497 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (2[,)+β)) β 2 β€ π₯) |
22 | 17, 18, 16, 20, 21 | ltletrd 11322 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (2[,)+β)) β 1 < π₯) |
23 | 16, 22 | rplogcld 26000 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (2[,)+β)) β (logβπ₯) β
β+) |
24 | 15, 23 | rpmulcld 12980 |
. . . . . . . 8
β’
((β€ β§ π₯
β (2[,)+β)) β ((Οβπ₯) Β· (logβπ₯)) β
β+) |
25 | 24 | rpcnne0d 12973 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β (((Οβπ₯) Β· (logβπ₯)) β β β§
((Οβπ₯)
Β· (logβπ₯))
β 0)) |
26 | | recdiv 11868 |
. . . . . . 7
β’
((((ΞΈβπ₯)
β β β§ (ΞΈβπ₯) β 0) β§ (((Οβπ₯) Β· (logβπ₯)) β β β§
((Οβπ₯)
Β· (logβπ₯))
β 0)) β (1 / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) = (((Οβπ₯) Β· (logβπ₯)) / (ΞΈβπ₯))) |
27 | 12, 25, 26 | syl2anc 585 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β (1 / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) = (((Οβπ₯) Β· (logβπ₯)) / (ΞΈβπ₯))) |
28 | 27 | mpteq2dva 5210 |
. . . . 5
β’ (β€
β (π₯ β
(2[,)+β) β¦ (1 / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) = (π₯ β (2[,)+β) β¦
(((Οβπ₯)
Β· (logβπ₯)) /
(ΞΈβπ₯)))) |
29 | 1, 2, 3, 4, 28 | offval2 7642 |
. . . 4
β’ (β€
β ((π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) βf Β· (π₯ β (2[,)+β) β¦
(1 / ((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))))
= (π₯ β (2[,)+β)
β¦ (((ΞΈβπ₯)
/ π₯) Β·
(((Οβπ₯)
Β· (logβπ₯)) /
(ΞΈβπ₯))))) |
30 | | 0red 11165 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (2[,)+β)) β 0 β β) |
31 | | 2pos 12263 |
. . . . . . . . . . 11
β’ 0 <
2 |
32 | 31 | a1i 11 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (2[,)+β)) β 0 < 2) |
33 | 30, 18, 16, 32, 21 | ltletrd 11322 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (2[,)+β)) β 0 < π₯) |
34 | 16, 33 | elrpd 12961 |
. . . . . . . 8
β’
((β€ β§ π₯
β (2[,)+β)) β π₯ β β+) |
35 | 34 | rpcnne0d 12973 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β (π₯ β β β§ π₯ β 0)) |
36 | 24 | rpcnd 12966 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β ((Οβπ₯) Β· (logβπ₯)) β β) |
37 | | dmdcan 11872 |
. . . . . . 7
β’
((((ΞΈβπ₯)
β β β§ (ΞΈβπ₯) β 0) β§ (π₯ β β β§ π₯ β 0) β§ ((Οβπ₯) Β· (logβπ₯)) β β) β
(((ΞΈβπ₯) / π₯) Β·
(((Οβπ₯)
Β· (logβπ₯)) /
(ΞΈβπ₯))) =
(((Οβπ₯)
Β· (logβπ₯)) /
π₯)) |
38 | 12, 35, 36, 37 | syl3anc 1372 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β (((ΞΈβπ₯) / π₯) Β· (((Οβπ₯) Β· (logβπ₯)) / (ΞΈβπ₯))) = (((Οβπ₯) Β· (logβπ₯)) / π₯)) |
39 | 15 | rpcnd 12966 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β (Οβπ₯) β β) |
40 | 23 | rpcnne0d 12973 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β ((logβπ₯) β β β§ (logβπ₯) β 0)) |
41 | | divdiv2 11874 |
. . . . . . 7
β’
(((Οβπ₯) β β β§ (π₯ β β β§ π₯ β 0) β§ ((logβπ₯) β β β§ (logβπ₯) β 0)) β
((Οβπ₯) /
(π₯ / (logβπ₯))) = (((Οβπ₯) Β· (logβπ₯)) / π₯)) |
42 | 39, 35, 40, 41 | syl3anc 1372 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β ((Οβπ₯) / (π₯ / (logβπ₯))) = (((Οβπ₯) Β· (logβπ₯)) / π₯)) |
43 | 38, 42 | eqtr4d 2780 |
. . . . 5
β’
((β€ β§ π₯
β (2[,)+β)) β (((ΞΈβπ₯) / π₯) Β· (((Οβπ₯) Β· (logβπ₯)) / (ΞΈβπ₯))) = ((Οβπ₯) / (π₯ / (logβπ₯)))) |
44 | 43 | mpteq2dva 5210 |
. . . 4
β’ (β€
β (π₯ β
(2[,)+β) β¦ (((ΞΈβπ₯) / π₯) Β· (((Οβπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)))) = (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(π₯ / (logβπ₯))))) |
45 | 29, 44 | eqtrd 2777 |
. . 3
β’ (β€
β ((π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) βf Β· (π₯ β (2[,)+β) β¦
(1 / ((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))))
= (π₯ β (2[,)+β)
β¦ ((Οβπ₯) / (π₯ / (logβπ₯))))) |
46 | 34 | ex 414 |
. . . . . 6
β’ (β€
β (π₯ β
(2[,)+β) β π₯
β β+)) |
47 | 46 | ssrdv 3955 |
. . . . 5
β’ (β€
β (2[,)+β) β β+) |
48 | | chto1ub 26840 |
. . . . . 6
β’ (π₯ β β+
β¦ ((ΞΈβπ₯)
/ π₯)) β
π(1) |
49 | 48 | a1i 11 |
. . . . 5
β’ (β€
β (π₯ β
β+ β¦ ((ΞΈβπ₯) / π₯)) β π(1)) |
50 | 47, 49 | o1res2 15452 |
. . . 4
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) β π(1)) |
51 | | ax-1cn 11116 |
. . . . . . 7
β’ 1 β
β |
52 | 51 | a1i 11 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β 1 β β) |
53 | 11, 24 | rpdivcld 12981 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β
β+) |
54 | 53 | rpcnd 12966 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β β) |
55 | | pnfxr 11216 |
. . . . . . . . 9
β’ +β
β β* |
56 | | icossre 13352 |
. . . . . . . . 9
β’ ((2
β β β§ +β β β*) β (2[,)+β)
β β) |
57 | 6, 55, 56 | mp2an 691 |
. . . . . . . 8
β’
(2[,)+β) β β |
58 | | rlimconst 15433 |
. . . . . . . 8
β’
(((2[,)+β) β β β§ 1 β β) β (π₯ β (2[,)+β) β¦
1) βπ 1) |
59 | 57, 51, 58 | mp2an 691 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β¦
1) βπ 1 |
60 | 59 | a1i 11 |
. . . . . 6
β’ (β€
β (π₯ β
(2[,)+β) β¦ 1) βπ 1) |
61 | | chtppilim 26839 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β¦
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))
βπ 1 |
62 | 61 | a1i 11 |
. . . . . 6
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) βπ
1) |
63 | | ax-1ne0 11127 |
. . . . . . 7
β’ 1 β
0 |
64 | 63 | a1i 11 |
. . . . . 6
β’ (β€
β 1 β 0) |
65 | 53 | rpne0d 12969 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 0) |
66 | 52, 54, 60, 62, 64, 65 | rlimdiv 15537 |
. . . . 5
β’ (β€
β (π₯ β
(2[,)+β) β¦ (1 / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) βπ (1 /
1)) |
67 | | rlimo1 15506 |
. . . . 5
β’ ((π₯ β (2[,)+β) β¦
(1 / ((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯)))))
βπ (1 / 1) β (π₯ β (2[,)+β) β¦ (1 /
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯)))))
β π(1)) |
68 | 66, 67 | syl 17 |
. . . 4
β’ (β€
β (π₯ β
(2[,)+β) β¦ (1 / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) β π(1)) |
69 | | o1mul 15504 |
. . . 4
β’ (((π₯ β (2[,)+β) β¦
((ΞΈβπ₯) / π₯)) β π(1) β§
(π₯ β (2[,)+β)
β¦ (1 / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) β π(1)) β ((π₯ β (2[,)+β) β¦
((ΞΈβπ₯) / π₯)) βf Β·
(π₯ β (2[,)+β)
β¦ (1 / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))))) β π(1)) |
70 | 50, 68, 69 | syl2anc 585 |
. . 3
β’ (β€
β ((π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) βf Β· (π₯ β (2[,)+β) β¦
(1 / ((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))))
β π(1)) |
71 | 45, 70 | eqeltrrd 2839 |
. 2
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((Οβπ₯) / (π₯ / (logβπ₯)))) β π(1)) |
72 | 71 | mptru 1549 |
1
β’ (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(π₯ / (logβπ₯)))) β
π(1) |