Step | Hyp | Ref
| Expression |
1 | | icopnfhmeo.f |
. . 3
โข ๐น = (๐ฅ โ (0[,)1) โฆ (๐ฅ / (1 โ ๐ฅ))) |
2 | | 0re 11216 |
. . . . . . . 8
โข 0 โ
โ |
3 | | 1xr 11273 |
. . . . . . . 8
โข 1 โ
โ* |
4 | | elico2 13388 |
. . . . . . . 8
โข ((0
โ โ โง 1 โ โ*) โ (๐ฅ โ (0[,)1) โ (๐ฅ โ โ โง 0 โค ๐ฅ โง ๐ฅ < 1))) |
5 | 2, 3, 4 | mp2an 691 |
. . . . . . 7
โข (๐ฅ โ (0[,)1) โ (๐ฅ โ โ โง 0 โค
๐ฅ โง ๐ฅ < 1)) |
6 | 5 | simp1bi 1146 |
. . . . . 6
โข (๐ฅ โ (0[,)1) โ ๐ฅ โ
โ) |
7 | 5 | simp3bi 1148 |
. . . . . . 7
โข (๐ฅ โ (0[,)1) โ ๐ฅ < 1) |
8 | | 1re 11214 |
. . . . . . . 8
โข 1 โ
โ |
9 | | difrp 13012 |
. . . . . . . 8
โข ((๐ฅ โ โ โง 1 โ
โ) โ (๐ฅ < 1
โ (1 โ ๐ฅ) โ
โ+)) |
10 | 6, 8, 9 | sylancl 587 |
. . . . . . 7
โข (๐ฅ โ (0[,)1) โ (๐ฅ < 1 โ (1 โ ๐ฅ) โ
โ+)) |
11 | 7, 10 | mpbid 231 |
. . . . . 6
โข (๐ฅ โ (0[,)1) โ (1
โ ๐ฅ) โ
โ+) |
12 | 6, 11 | rerpdivcld 13047 |
. . . . 5
โข (๐ฅ โ (0[,)1) โ (๐ฅ / (1 โ ๐ฅ)) โ โ) |
13 | 5 | simp2bi 1147 |
. . . . . 6
โข (๐ฅ โ (0[,)1) โ 0 โค
๐ฅ) |
14 | 6, 11, 13 | divge0d 13056 |
. . . . 5
โข (๐ฅ โ (0[,)1) โ 0 โค
(๐ฅ / (1 โ ๐ฅ))) |
15 | | elrege0 13431 |
. . . . 5
โข ((๐ฅ / (1 โ ๐ฅ)) โ (0[,)+โ) โ ((๐ฅ / (1 โ ๐ฅ)) โ โ โง 0 โค (๐ฅ / (1 โ ๐ฅ)))) |
16 | 12, 14, 15 | sylanbrc 584 |
. . . 4
โข (๐ฅ โ (0[,)1) โ (๐ฅ / (1 โ ๐ฅ)) โ (0[,)+โ)) |
17 | 16 | adantl 483 |
. . 3
โข
((โค โง ๐ฅ
โ (0[,)1)) โ (๐ฅ /
(1 โ ๐ฅ)) โ
(0[,)+โ)) |
18 | | elrege0 13431 |
. . . . . . 7
โข (๐ฆ โ (0[,)+โ) โ
(๐ฆ โ โ โง 0
โค ๐ฆ)) |
19 | 18 | simplbi 499 |
. . . . . 6
โข (๐ฆ โ (0[,)+โ) โ
๐ฆ โ
โ) |
20 | | readdcl 11193 |
. . . . . . . 8
โข ((1
โ โ โง ๐ฆ
โ โ) โ (1 + ๐ฆ) โ โ) |
21 | 8, 19, 20 | sylancr 588 |
. . . . . . 7
โข (๐ฆ โ (0[,)+โ) โ (1
+ ๐ฆ) โ
โ) |
22 | 2 | a1i 11 |
. . . . . . . 8
โข (๐ฆ โ (0[,)+โ) โ 0
โ โ) |
23 | 18 | simprbi 498 |
. . . . . . . 8
โข (๐ฆ โ (0[,)+โ) โ 0
โค ๐ฆ) |
24 | 19 | ltp1d 12144 |
. . . . . . . . 9
โข (๐ฆ โ (0[,)+โ) โ
๐ฆ < (๐ฆ + 1)) |
25 | | ax-1cn 11168 |
. . . . . . . . . 10
โข 1 โ
โ |
26 | 19 | recnd 11242 |
. . . . . . . . . 10
โข (๐ฆ โ (0[,)+โ) โ
๐ฆ โ
โ) |
27 | | addcom 11400 |
. . . . . . . . . 10
โข ((1
โ โ โง ๐ฆ
โ โ) โ (1 + ๐ฆ) = (๐ฆ + 1)) |
28 | 25, 26, 27 | sylancr 588 |
. . . . . . . . 9
โข (๐ฆ โ (0[,)+โ) โ (1
+ ๐ฆ) = (๐ฆ + 1)) |
29 | 24, 28 | breqtrrd 5177 |
. . . . . . . 8
โข (๐ฆ โ (0[,)+โ) โ
๐ฆ < (1 + ๐ฆ)) |
30 | 22, 19, 21, 23, 29 | lelttrd 11372 |
. . . . . . 7
โข (๐ฆ โ (0[,)+โ) โ 0
< (1 + ๐ฆ)) |
31 | 21, 30 | elrpd 13013 |
. . . . . 6
โข (๐ฆ โ (0[,)+โ) โ (1
+ ๐ฆ) โ
โ+) |
32 | 19, 31 | rerpdivcld 13047 |
. . . . 5
โข (๐ฆ โ (0[,)+โ) โ
(๐ฆ / (1 + ๐ฆ)) โ
โ) |
33 | | divge0 12083 |
. . . . . 6
โข (((๐ฆ โ โ โง 0 โค
๐ฆ) โง ((1 + ๐ฆ) โ โ โง 0 < (1
+ ๐ฆ))) โ 0 โค (๐ฆ / (1 + ๐ฆ))) |
34 | 19, 23, 21, 30, 33 | syl22anc 838 |
. . . . 5
โข (๐ฆ โ (0[,)+โ) โ 0
โค (๐ฆ / (1 + ๐ฆ))) |
35 | 21 | recnd 11242 |
. . . . . . . 8
โข (๐ฆ โ (0[,)+โ) โ (1
+ ๐ฆ) โ
โ) |
36 | 35 | mulridd 11231 |
. . . . . . 7
โข (๐ฆ โ (0[,)+โ) โ
((1 + ๐ฆ) ยท 1) = (1 +
๐ฆ)) |
37 | 29, 36 | breqtrrd 5177 |
. . . . . 6
โข (๐ฆ โ (0[,)+โ) โ
๐ฆ < ((1 + ๐ฆ) ยท 1)) |
38 | 8 | a1i 11 |
. . . . . . 7
โข (๐ฆ โ (0[,)+โ) โ 1
โ โ) |
39 | | ltdivmul 12089 |
. . . . . . 7
โข ((๐ฆ โ โ โง 1 โ
โ โง ((1 + ๐ฆ)
โ โ โง 0 < (1 + ๐ฆ))) โ ((๐ฆ / (1 + ๐ฆ)) < 1 โ ๐ฆ < ((1 + ๐ฆ) ยท 1))) |
40 | 19, 38, 21, 30, 39 | syl112anc 1375 |
. . . . . 6
โข (๐ฆ โ (0[,)+โ) โ
((๐ฆ / (1 + ๐ฆ)) < 1 โ ๐ฆ < ((1 + ๐ฆ) ยท 1))) |
41 | 37, 40 | mpbird 257 |
. . . . 5
โข (๐ฆ โ (0[,)+โ) โ
(๐ฆ / (1 + ๐ฆ)) < 1) |
42 | | elico2 13388 |
. . . . . 6
โข ((0
โ โ โง 1 โ โ*) โ ((๐ฆ / (1 + ๐ฆ)) โ (0[,)1) โ ((๐ฆ / (1 + ๐ฆ)) โ โ โง 0 โค (๐ฆ / (1 + ๐ฆ)) โง (๐ฆ / (1 + ๐ฆ)) < 1))) |
43 | 2, 3, 42 | mp2an 691 |
. . . . 5
โข ((๐ฆ / (1 + ๐ฆ)) โ (0[,)1) โ ((๐ฆ / (1 + ๐ฆ)) โ โ โง 0 โค (๐ฆ / (1 + ๐ฆ)) โง (๐ฆ / (1 + ๐ฆ)) < 1)) |
44 | 32, 34, 41, 43 | syl3anbrc 1344 |
. . . 4
โข (๐ฆ โ (0[,)+โ) โ
(๐ฆ / (1 + ๐ฆ)) โ
(0[,)1)) |
45 | 44 | adantl 483 |
. . 3
โข
((โค โง ๐ฆ
โ (0[,)+โ)) โ (๐ฆ / (1 + ๐ฆ)) โ (0[,)1)) |
46 | 26 | adantl 483 |
. . . . . . . . 9
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
๐ฆ โ
โ) |
47 | 6 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
๐ฅ โ
โ) |
48 | 47 | recnd 11242 |
. . . . . . . . . 10
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
๐ฅ โ
โ) |
49 | 48, 46 | mulcld 11234 |
. . . . . . . . 9
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(๐ฅ ยท ๐ฆ) โ
โ) |
50 | 46, 49, 48 | subadd2d 11590 |
. . . . . . . 8
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
((๐ฆ โ (๐ฅ ยท ๐ฆ)) = ๐ฅ โ (๐ฅ + (๐ฅ ยท ๐ฆ)) = ๐ฆ)) |
51 | | 1cnd 11209 |
. . . . . . . . . . 11
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ 1
โ โ) |
52 | 51, 48, 46 | subdird 11671 |
. . . . . . . . . 10
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
((1 โ ๐ฅ) ยท
๐ฆ) = ((1 ยท ๐ฆ) โ (๐ฅ ยท ๐ฆ))) |
53 | 46 | mullidd 11232 |
. . . . . . . . . . 11
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(1 ยท ๐ฆ) = ๐ฆ) |
54 | 53 | oveq1d 7424 |
. . . . . . . . . 10
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
((1 ยท ๐ฆ) โ
(๐ฅ ยท ๐ฆ)) = (๐ฆ โ (๐ฅ ยท ๐ฆ))) |
55 | 52, 54 | eqtrd 2773 |
. . . . . . . . 9
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
((1 โ ๐ฅ) ยท
๐ฆ) = (๐ฆ โ (๐ฅ ยท ๐ฆ))) |
56 | 55 | eqeq1d 2735 |
. . . . . . . 8
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(((1 โ ๐ฅ) ยท
๐ฆ) = ๐ฅ โ (๐ฆ โ (๐ฅ ยท ๐ฆ)) = ๐ฅ)) |
57 | 48, 51, 46 | adddid 11238 |
. . . . . . . . . 10
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(๐ฅ ยท (1 + ๐ฆ)) = ((๐ฅ ยท 1) + (๐ฅ ยท ๐ฆ))) |
58 | 48 | mulridd 11231 |
. . . . . . . . . . 11
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(๐ฅ ยท 1) = ๐ฅ) |
59 | 58 | oveq1d 7424 |
. . . . . . . . . 10
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
((๐ฅ ยท 1) + (๐ฅ ยท ๐ฆ)) = (๐ฅ + (๐ฅ ยท ๐ฆ))) |
60 | 57, 59 | eqtrd 2773 |
. . . . . . . . 9
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(๐ฅ ยท (1 + ๐ฆ)) = (๐ฅ + (๐ฅ ยท ๐ฆ))) |
61 | 60 | eqeq1d 2735 |
. . . . . . . 8
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
((๐ฅ ยท (1 + ๐ฆ)) = ๐ฆ โ (๐ฅ + (๐ฅ ยท ๐ฆ)) = ๐ฆ)) |
62 | 50, 56, 61 | 3bitr4rd 312 |
. . . . . . 7
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
((๐ฅ ยท (1 + ๐ฆ)) = ๐ฆ โ ((1 โ ๐ฅ) ยท ๐ฆ) = ๐ฅ)) |
63 | | eqcom 2740 |
. . . . . . 7
โข (๐ฆ = (๐ฅ ยท (1 + ๐ฆ)) โ (๐ฅ ยท (1 + ๐ฆ)) = ๐ฆ) |
64 | | eqcom 2740 |
. . . . . . 7
โข (๐ฅ = ((1 โ ๐ฅ) ยท ๐ฆ) โ ((1 โ ๐ฅ) ยท ๐ฆ) = ๐ฅ) |
65 | 62, 63, 64 | 3bitr4g 314 |
. . . . . 6
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(๐ฆ = (๐ฅ ยท (1 + ๐ฆ)) โ ๐ฅ = ((1 โ ๐ฅ) ยท ๐ฆ))) |
66 | 35 | adantl 483 |
. . . . . . 7
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(1 + ๐ฆ) โ
โ) |
67 | 31 | adantl 483 |
. . . . . . . 8
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(1 + ๐ฆ) โ
โ+) |
68 | 67 | rpne0d 13021 |
. . . . . . 7
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(1 + ๐ฆ) โ
0) |
69 | 46, 48, 66, 68 | divmul3d 12024 |
. . . . . 6
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
((๐ฆ / (1 + ๐ฆ)) = ๐ฅ โ ๐ฆ = (๐ฅ ยท (1 + ๐ฆ)))) |
70 | 11 | adantr 482 |
. . . . . . . 8
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(1 โ ๐ฅ) โ
โ+) |
71 | 70 | rpcnd 13018 |
. . . . . . 7
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(1 โ ๐ฅ) โ
โ) |
72 | 70 | rpne0d 13021 |
. . . . . . 7
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(1 โ ๐ฅ) โ
0) |
73 | 48, 46, 71, 72 | divmul2d 12023 |
. . . . . 6
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
((๐ฅ / (1 โ ๐ฅ)) = ๐ฆ โ ๐ฅ = ((1 โ ๐ฅ) ยท ๐ฆ))) |
74 | 65, 69, 73 | 3bitr4d 311 |
. . . . 5
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
((๐ฆ / (1 + ๐ฆ)) = ๐ฅ โ (๐ฅ / (1 โ ๐ฅ)) = ๐ฆ)) |
75 | | eqcom 2740 |
. . . . 5
โข (๐ฅ = (๐ฆ / (1 + ๐ฆ)) โ (๐ฆ / (1 + ๐ฆ)) = ๐ฅ) |
76 | | eqcom 2740 |
. . . . 5
โข (๐ฆ = (๐ฅ / (1 โ ๐ฅ)) โ (๐ฅ / (1 โ ๐ฅ)) = ๐ฆ) |
77 | 74, 75, 76 | 3bitr4g 314 |
. . . 4
โข ((๐ฅ โ (0[,)1) โง ๐ฆ โ (0[,)+โ)) โ
(๐ฅ = (๐ฆ / (1 + ๐ฆ)) โ ๐ฆ = (๐ฅ / (1 โ ๐ฅ)))) |
78 | 77 | adantl 483 |
. . 3
โข
((โค โง (๐ฅ
โ (0[,)1) โง ๐ฆ
โ (0[,)+โ))) โ (๐ฅ = (๐ฆ / (1 + ๐ฆ)) โ ๐ฆ = (๐ฅ / (1 โ ๐ฅ)))) |
79 | 1, 17, 45, 78 | f1ocnv2d 7659 |
. 2
โข (โค
โ (๐น:(0[,)1)โ1-1-ontoโ(0[,)+โ) โง โก๐น = (๐ฆ โ (0[,)+โ) โฆ (๐ฆ / (1 + ๐ฆ))))) |
80 | 79 | mptru 1549 |
1
โข (๐น:(0[,)1)โ1-1-ontoโ(0[,)+โ) โง โก๐น = (๐ฆ โ (0[,)+โ) โฆ (๐ฆ / (1 + ๐ฆ)))) |