Step | Hyp | Ref
| Expression |
1 | | 2re 12234 |
. . . . . . . . . . 11
β’ 2 β
β |
2 | | elicopnf 13369 |
. . . . . . . . . . 11
β’ (2 β
β β (π₯ β
(2[,)+β) β (π₯
β β β§ 2 β€ π₯))) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β
(π₯ β β β§ 2
β€ π₯)) |
4 | | chtrpcl 26540 |
. . . . . . . . . 10
β’ ((π₯ β β β§ 2 β€
π₯) β
(ΞΈβπ₯) β
β+) |
5 | 3, 4 | sylbi 216 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
(ΞΈβπ₯) β
β+) |
6 | 5 | rpcnne0d 12973 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
((ΞΈβπ₯) β
β β§ (ΞΈβπ₯) β 0)) |
7 | 3 | simplbi 499 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β
π₯ β
β) |
8 | | 0red 11165 |
. . . . . . . . . . 11
β’ (π₯ β (2[,)+β) β 0
β β) |
9 | 1 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β (2[,)+β) β 2
β β) |
10 | | 2pos 12263 |
. . . . . . . . . . . 12
β’ 0 <
2 |
11 | 10 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β (2[,)+β) β 0
< 2) |
12 | 3 | simprbi 498 |
. . . . . . . . . . 11
β’ (π₯ β (2[,)+β) β 2
β€ π₯) |
13 | 8, 9, 7, 11, 12 | ltletrd 11322 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β 0
< π₯) |
14 | 7, 13 | elrpd 12961 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
π₯ β
β+) |
15 | 14 | rpcnne0d 12973 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
(π₯ β β β§
π₯ β 0)) |
16 | | rpre 12930 |
. . . . . . . . . . 11
β’ (π₯ β β+
β π₯ β
β) |
17 | | chpcl 26489 |
. . . . . . . . . . 11
β’ (π₯ β β β
(Οβπ₯) β
β) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
β’ (π₯ β β+
β (Οβπ₯)
β β) |
19 | 18 | recnd 11190 |
. . . . . . . . 9
β’ (π₯ β β+
β (Οβπ₯)
β β) |
20 | 14, 19 | syl 17 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
(Οβπ₯) β
β) |
21 | | dmdcan 11872 |
. . . . . . . 8
β’
((((ΞΈβπ₯)
β β β§ (ΞΈβπ₯) β 0) β§ (π₯ β β β§ π₯ β 0) β§ (Οβπ₯) β β) β
(((ΞΈβπ₯) / π₯) Β· ((Οβπ₯) / (ΞΈβπ₯))) = ((Οβπ₯) / π₯)) |
22 | 6, 15, 20, 21 | syl3anc 1372 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β
(((ΞΈβπ₯) / π₯) Β· ((Οβπ₯) / (ΞΈβπ₯))) = ((Οβπ₯) / π₯)) |
23 | 22 | adantl 483 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β (((ΞΈβπ₯) / π₯) Β· ((Οβπ₯) / (ΞΈβπ₯))) = ((Οβπ₯) / π₯)) |
24 | 23 | mpteq2dva 5210 |
. . . . 5
β’ (β€
β (π₯ β
(2[,)+β) β¦ (((ΞΈβπ₯) / π₯) Β· ((Οβπ₯) / (ΞΈβπ₯)))) = (π₯ β (2[,)+β) β¦
((Οβπ₯) / π₯))) |
25 | | ovexd 7397 |
. . . . . 6
β’ (β€
β (2[,)+β) β V) |
26 | | ovexd 7397 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) / π₯) β V) |
27 | | ovexd 7397 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β ((Οβπ₯) / (ΞΈβπ₯)) β V) |
28 | | eqidd 2738 |
. . . . . 6
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) = (π₯ β (2[,)+β) β¦
((ΞΈβπ₯) / π₯))) |
29 | | eqidd 2738 |
. . . . . 6
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((Οβπ₯) / (ΞΈβπ₯))) = (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(ΞΈβπ₯)))) |
30 | 25, 26, 27, 28, 29 | offval2 7642 |
. . . . 5
β’ (β€
β ((π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) βf Β· (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(ΞΈβπ₯)))) =
(π₯ β (2[,)+β)
β¦ (((ΞΈβπ₯)
/ π₯) Β·
((Οβπ₯) /
(ΞΈβπ₯))))) |
31 | 14 | ssriv 3953 |
. . . . . 6
β’
(2[,)+β) β β+ |
32 | | resmpt 5996 |
. . . . . 6
β’
((2[,)+β) β β+ β ((π₯ β β+ β¦
((Οβπ₯) / π₯)) βΎ (2[,)+β)) =
(π₯ β (2[,)+β)
β¦ ((Οβπ₯) /
π₯))) |
33 | 31, 32 | mp1i 13 |
. . . . 5
β’ (β€
β ((π₯ β
β+ β¦ ((Οβπ₯) / π₯)) βΎ (2[,)+β)) = (π₯ β (2[,)+β) β¦
((Οβπ₯) / π₯))) |
34 | 24, 30, 33 | 3eqtr4rd 2788 |
. . . 4
β’ (β€
β ((π₯ β
β+ β¦ ((Οβπ₯) / π₯)) βΎ (2[,)+β)) = ((π₯ β (2[,)+β) β¦
((ΞΈβπ₯) / π₯)) βf Β·
(π₯ β (2[,)+β)
β¦ ((Οβπ₯) /
(ΞΈβπ₯))))) |
35 | 31 | a1i 11 |
. . . . . 6
β’ (β€
β (2[,)+β) β β+) |
36 | | chto1ub 26840 |
. . . . . . 7
β’ (π₯ β β+
β¦ ((ΞΈβπ₯)
/ π₯)) β
π(1) |
37 | 36 | a1i 11 |
. . . . . 6
β’ (β€
β (π₯ β
β+ β¦ ((ΞΈβπ₯) / π₯)) β π(1)) |
38 | 35, 37 | o1res2 15452 |
. . . . 5
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) β π(1)) |
39 | | chpchtlim 26843 |
. . . . . 6
β’ (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(ΞΈβπ₯)))
βπ 1 |
40 | | rlimo1 15506 |
. . . . . 6
β’ ((π₯ β (2[,)+β) β¦
((Οβπ₯) /
(ΞΈβπ₯)))
βπ 1 β (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(ΞΈβπ₯))) β
π(1)) |
41 | 39, 40 | ax-mp 5 |
. . . . 5
β’ (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(ΞΈβπ₯))) β
π(1) |
42 | | o1mul 15504 |
. . . . 5
β’ (((π₯ β (2[,)+β) β¦
((ΞΈβπ₯) / π₯)) β π(1) β§
(π₯ β (2[,)+β)
β¦ ((Οβπ₯) /
(ΞΈβπ₯))) β
π(1)) β ((π₯
β (2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) βf Β· (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(ΞΈβπ₯)))) β
π(1)) |
43 | 38, 41, 42 | sylancl 587 |
. . . 4
β’ (β€
β ((π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) βf Β· (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(ΞΈβπ₯)))) β
π(1)) |
44 | 34, 43 | eqeltrd 2838 |
. . 3
β’ (β€
β ((π₯ β
β+ β¦ ((Οβπ₯) / π₯)) βΎ (2[,)+β)) β
π(1)) |
45 | | rerpdivcl 12952 |
. . . . . . . 8
β’
(((Οβπ₯)
β β β§ π₯
β β+) β ((Οβπ₯) / π₯) β β) |
46 | 18, 45 | mpancom 687 |
. . . . . . 7
β’ (π₯ β β+
β ((Οβπ₯) /
π₯) β
β) |
47 | 46 | recnd 11190 |
. . . . . 6
β’ (π₯ β β+
β ((Οβπ₯) /
π₯) β
β) |
48 | 47 | adantl 483 |
. . . . 5
β’
((β€ β§ π₯
β β+) β ((Οβπ₯) / π₯) β β) |
49 | 48 | fmpttd 7068 |
. . . 4
β’ (β€
β (π₯ β
β+ β¦ ((Οβπ₯) / π₯)):β+βΆβ) |
50 | | rpssre 12929 |
. . . . 5
β’
β+ β β |
51 | 50 | a1i 11 |
. . . 4
β’ (β€
β β+ β β) |
52 | 1 | a1i 11 |
. . . 4
β’ (β€
β 2 β β) |
53 | 49, 51, 52 | o1resb 15455 |
. . 3
β’ (β€
β ((π₯ β
β+ β¦ ((Οβπ₯) / π₯)) β π(1) β ((π₯ β β+
β¦ ((Οβπ₯) /
π₯)) βΎ (2[,)+β))
β π(1))) |
54 | 44, 53 | mpbird 257 |
. 2
β’ (β€
β (π₯ β
β+ β¦ ((Οβπ₯) / π₯)) β π(1)) |
55 | 54 | mptru 1549 |
1
β’ (π₯ β β+
β¦ ((Οβπ₯) /
π₯)) β
π(1) |