Step | Hyp | Ref
| Expression |
1 | | iooref1o.f |
. . 3
โข ๐น = (๐ฅ โ โ โฆ (1 / (1 +
(expโ๐ฅ)))) |
2 | | 1rp 9656 |
. . . . . . . . 9
โข 1 โ
โ+ |
3 | 2 | a1i 9 |
. . . . . . . 8
โข (๐ฅ โ โ โ 1 โ
โ+) |
4 | | rpefcl 11692 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(expโ๐ฅ) โ
โ+) |
5 | 3, 4 | rpaddcld 9711 |
. . . . . . 7
โข (๐ฅ โ โ โ (1 +
(expโ๐ฅ)) โ
โ+) |
6 | 5 | rpreccld 9706 |
. . . . . 6
โข (๐ฅ โ โ โ (1 / (1 +
(expโ๐ฅ))) โ
โ+) |
7 | 6 | rpred 9695 |
. . . . 5
โข (๐ฅ โ โ โ (1 / (1 +
(expโ๐ฅ))) โ
โ) |
8 | 6 | rpgt0d 9698 |
. . . . 5
โข (๐ฅ โ โ โ 0 < (1
/ (1 + (expโ๐ฅ)))) |
9 | | 1red 7971 |
. . . . . . 7
โข (๐ฅ โ โ โ 1 โ
โ) |
10 | 9, 4 | ltaddrpd 9729 |
. . . . . 6
โข (๐ฅ โ โ โ 1 < (1
+ (expโ๐ฅ))) |
11 | 5 | recgt1d 9710 |
. . . . . 6
โข (๐ฅ โ โ โ (1 <
(1 + (expโ๐ฅ)) โ
(1 / (1 + (expโ๐ฅ)))
< 1)) |
12 | 10, 11 | mpbid 147 |
. . . . 5
โข (๐ฅ โ โ โ (1 / (1 +
(expโ๐ฅ))) <
1) |
13 | | 0xr 8003 |
. . . . . 6
โข 0 โ
โ* |
14 | | 1re 7955 |
. . . . . . 7
โข 1 โ
โ |
15 | 14 | rexri 8014 |
. . . . . 6
โข 1 โ
โ* |
16 | | elioo2 9920 |
. . . . . 6
โข ((0
โ โ* โง 1 โ โ*) โ ((1 / (1
+ (expโ๐ฅ))) โ
(0(,)1) โ ((1 / (1 + (expโ๐ฅ))) โ โ โง 0 < (1 / (1 +
(expโ๐ฅ))) โง (1 /
(1 + (expโ๐ฅ))) <
1))) |
17 | 13, 15, 16 | mp2an 426 |
. . . . 5
โข ((1 / (1
+ (expโ๐ฅ))) โ
(0(,)1) โ ((1 / (1 + (expโ๐ฅ))) โ โ โง 0 < (1 / (1 +
(expโ๐ฅ))) โง (1 /
(1 + (expโ๐ฅ))) <
1)) |
18 | 7, 8, 12, 17 | syl3anbrc 1181 |
. . . 4
โข (๐ฅ โ โ โ (1 / (1 +
(expโ๐ฅ))) โ
(0(,)1)) |
19 | 18 | adantl 277 |
. . 3
โข
((โค โง ๐ฅ
โ โ) โ (1 / (1 + (expโ๐ฅ))) โ (0(,)1)) |
20 | | elioore 9911 |
. . . . . . . . . 10
โข (๐ฆ โ (0(,)1) โ ๐ฆ โ
โ) |
21 | | eliooord 9927 |
. . . . . . . . . . 11
โข (๐ฆ โ (0(,)1) โ (0 <
๐ฆ โง ๐ฆ < 1)) |
22 | 21 | simpld 112 |
. . . . . . . . . 10
โข (๐ฆ โ (0(,)1) โ 0 <
๐ฆ) |
23 | 20, 22 | elrpd 9692 |
. . . . . . . . 9
โข (๐ฆ โ (0(,)1) โ ๐ฆ โ
โ+) |
24 | 23 | rpreccld 9706 |
. . . . . . . 8
โข (๐ฆ โ (0(,)1) โ (1 /
๐ฆ) โ
โ+) |
25 | 24 | rpred 9695 |
. . . . . . 7
โข (๐ฆ โ (0(,)1) โ (1 /
๐ฆ) โ
โ) |
26 | | 1red 7971 |
. . . . . . 7
โข (๐ฆ โ (0(,)1) โ 1 โ
โ) |
27 | 25, 26 | resubcld 8337 |
. . . . . 6
โข (๐ฆ โ (0(,)1) โ ((1 /
๐ฆ) โ 1) โ
โ) |
28 | 21 | simprd 114 |
. . . . . . . 8
โข (๐ฆ โ (0(,)1) โ ๐ฆ < 1) |
29 | 23 | reclt1d 9709 |
. . . . . . . 8
โข (๐ฆ โ (0(,)1) โ (๐ฆ < 1 โ 1 < (1 / ๐ฆ))) |
30 | 28, 29 | mpbid 147 |
. . . . . . 7
โข (๐ฆ โ (0(,)1) โ 1 < (1
/ ๐ฆ)) |
31 | 26, 25 | posdifd 8488 |
. . . . . . 7
โข (๐ฆ โ (0(,)1) โ (1 <
(1 / ๐ฆ) โ 0 < ((1 /
๐ฆ) โ
1))) |
32 | 30, 31 | mpbid 147 |
. . . . . 6
โข (๐ฆ โ (0(,)1) โ 0 <
((1 / ๐ฆ) โ
1)) |
33 | 27, 32 | elrpd 9692 |
. . . . 5
โข (๐ฆ โ (0(,)1) โ ((1 /
๐ฆ) โ 1) โ
โ+) |
34 | 33 | relogcld 14273 |
. . . 4
โข (๐ฆ โ (0(,)1) โ
(logโ((1 / ๐ฆ) โ
1)) โ โ) |
35 | 34 | adantl 277 |
. . 3
โข
((โค โง ๐ฆ
โ (0(,)1)) โ (logโ((1 / ๐ฆ) โ 1)) โ
โ) |
36 | | 1cnd 7972 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ 1 โ
โ) |
37 | 4 | adantr 276 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ
(expโ๐ฅ) โ
โ+) |
38 | 37 | rpcnd 9697 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ
(expโ๐ฅ) โ
โ) |
39 | 36, 38 | addcld 7976 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ (1 +
(expโ๐ฅ)) โ
โ) |
40 | 23 | adantl 277 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ ๐ฆ โ
โ+) |
41 | 40 | rpcnd 9697 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ ๐ฆ โ
โ) |
42 | 40 | rpap0d 9701 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ ๐ฆ # 0) |
43 | 36, 39, 41, 42 | divmulap2d 8780 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ ((1 /
๐ฆ) = (1 + (expโ๐ฅ)) โ 1 = (๐ฆ ยท (1 + (expโ๐ฅ))))) |
44 | 24 | adantl 277 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ (1 /
๐ฆ) โ
โ+) |
45 | 44 | rpcnd 9697 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ (1 /
๐ฆ) โ
โ) |
46 | 36, 38, 45 | addrsub 8327 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ ((1 +
(expโ๐ฅ)) = (1 / ๐ฆ) โ (expโ๐ฅ) = ((1 / ๐ฆ) โ 1))) |
47 | 33 | adantl 277 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ ((1 /
๐ฆ) โ 1) โ
โ+) |
48 | 47 | reeflogd 14274 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ
(expโ(logโ((1 / ๐ฆ) โ 1))) = ((1 / ๐ฆ) โ 1)) |
49 | 48 | eqeq2d 2189 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ
((expโ๐ฅ) =
(expโ(logโ((1 / ๐ฆ) โ 1))) โ (expโ๐ฅ) = ((1 / ๐ฆ) โ 1))) |
50 | | reef11 11706 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง
(logโ((1 / ๐ฆ) โ
1)) โ โ) โ ((expโ๐ฅ) = (expโ(logโ((1 / ๐ฆ) โ 1))) โ ๐ฅ = (logโ((1 / ๐ฆ) โ 1)))) |
51 | 34, 50 | sylan2 286 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ
((expโ๐ฅ) =
(expโ(logโ((1 / ๐ฆ) โ 1))) โ ๐ฅ = (logโ((1 / ๐ฆ) โ 1)))) |
52 | 46, 49, 51 | 3bitr2rd 217 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ (๐ฅ = (logโ((1 / ๐ฆ) โ 1)) โ (1 +
(expโ๐ฅ)) = (1 / ๐ฆ))) |
53 | | eqcom 2179 |
. . . . . . 7
โข ((1 +
(expโ๐ฅ)) = (1 / ๐ฆ) โ (1 / ๐ฆ) = (1 + (expโ๐ฅ))) |
54 | 52, 53 | bitrdi 196 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ (๐ฅ = (logโ((1 / ๐ฆ) โ 1)) โ (1 / ๐ฆ) = (1 + (expโ๐ฅ)))) |
55 | 5 | adantr 276 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ (1 +
(expโ๐ฅ)) โ
โ+) |
56 | 55 | rpap0d 9701 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ (1 +
(expโ๐ฅ)) #
0) |
57 | 36, 41, 39, 56 | divmulap3d 8781 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ ((1 / (1
+ (expโ๐ฅ))) = ๐ฆ โ 1 = (๐ฆ ยท (1 + (expโ๐ฅ))))) |
58 | 43, 54, 57 | 3bitr4d 220 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ (๐ฅ = (logโ((1 / ๐ฆ) โ 1)) โ (1 / (1 +
(expโ๐ฅ))) = ๐ฆ)) |
59 | | eqcom 2179 |
. . . . 5
โข ((1 / (1
+ (expโ๐ฅ))) = ๐ฆ โ ๐ฆ = (1 / (1 + (expโ๐ฅ)))) |
60 | 58, 59 | bitrdi 196 |
. . . 4
โข ((๐ฅ โ โ โง ๐ฆ โ (0(,)1)) โ (๐ฅ = (logโ((1 / ๐ฆ) โ 1)) โ ๐ฆ = (1 / (1 + (expโ๐ฅ))))) |
61 | 60 | adantl 277 |
. . 3
โข
((โค โง (๐ฅ
โ โ โง ๐ฆ
โ (0(,)1))) โ (๐ฅ
= (logโ((1 / ๐ฆ)
โ 1)) โ ๐ฆ = (1 /
(1 + (expโ๐ฅ))))) |
62 | 1, 19, 35, 61 | f1o2d 6075 |
. 2
โข (โค
โ ๐น:โโ1-1-ontoโ(0(,)1)) |
63 | 62 | mptru 1362 |
1
โข ๐น:โโ1-1-ontoโ(0(,)1) |