Metamath Proof Explorer

Theorem icopnfcnv

Description: Define a bijection from [ 0 , 1 ) to [ 0 , +oo ) . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypothesis icopnfhmeo.f 
|- F = ( x e. ( 0 [,) 1 ) |-> ( x / ( 1 - x ) ) )
Assertion icopnfcnv 
|- ( F : ( 0 [,) 1 ) -1-1-onto-> ( 0 [,) +oo ) /\ `' F = ( y e. ( 0 [,) +oo ) |-> ( y / ( 1 + y ) ) ) )

Proof

Step Hyp Ref Expression
1 icopnfhmeo.f 
 |-  F = ( x e. ( 0 [,) 1 ) |-> ( x / ( 1 - x ) ) )
2 0re 
 |-  0 e. RR
3 1xr 
 |-  1 e. RR*
4 elico2 
 |-  ( ( 0 e. RR /\ 1 e. RR* ) -> ( x e. ( 0 [,) 1 ) <-> ( x e. RR /\ 0 <_ x /\ x < 1 ) ) )
5 2 3 4 mp2an 
 |-  ( x e. ( 0 [,) 1 ) <-> ( x e. RR /\ 0 <_ x /\ x < 1 ) )
6 5 simp1bi 
 |-  ( x e. ( 0 [,) 1 ) -> x e. RR )
7 5 simp3bi 
 |-  ( x e. ( 0 [,) 1 ) -> x < 1 )
8 1re 
 |-  1 e. RR
9 difrp 
 |-  ( ( x e. RR /\ 1 e. RR ) -> ( x < 1 <-> ( 1 - x ) e. RR+ ) )
10 6 8 9 sylancl 
 |-  ( x e. ( 0 [,) 1 ) -> ( x < 1 <-> ( 1 - x ) e. RR+ ) )
11 7 10 mpbid 
 |-  ( x e. ( 0 [,) 1 ) -> ( 1 - x ) e. RR+ )
12 6 11 rerpdivcld 
 |-  ( x e. ( 0 [,) 1 ) -> ( x / ( 1 - x ) ) e. RR )
13 5 simp2bi 
 |-  ( x e. ( 0 [,) 1 ) -> 0 <_ x )
14 6 11 13 divge0d 
 |-  ( x e. ( 0 [,) 1 ) -> 0 <_ ( x / ( 1 - x ) ) )
15 elrege0 
 |-  ( ( x / ( 1 - x ) ) e. ( 0 [,) +oo ) <-> ( ( x / ( 1 - x ) ) e. RR /\ 0 <_ ( x / ( 1 - x ) ) ) )
16 12 14 15 sylanbrc 
 |-  ( x e. ( 0 [,) 1 ) -> ( x / ( 1 - x ) ) e. ( 0 [,) +oo ) )
17 16 adantl 
 |-  ( ( T. /\ x e. ( 0 [,) 1 ) ) -> ( x / ( 1 - x ) ) e. ( 0 [,) +oo ) )
18 elrege0 
 |-  ( y e. ( 0 [,) +oo ) <-> ( y e. RR /\ 0 <_ y ) )
19 18 simplbi 
 |-  ( y e. ( 0 [,) +oo ) -> y e. RR )
20 readdcl 
 |-  ( ( 1 e. RR /\ y e. RR ) -> ( 1 + y ) e. RR )
21 8 19 20 sylancr 
 |-  ( y e. ( 0 [,) +oo ) -> ( 1 + y ) e. RR )
22 2 a1i 
 |-  ( y e. ( 0 [,) +oo ) -> 0 e. RR )
23 18 simprbi 
 |-  ( y e. ( 0 [,) +oo ) -> 0 <_ y )
24 19 ltp1d 
 |-  ( y e. ( 0 [,) +oo ) -> y < ( y + 1 ) )
25 ax-1cn 
 |-  1 e. CC
26 19 recnd 
 |-  ( y e. ( 0 [,) +oo ) -> y e. CC )
27 addcom 
 |-  ( ( 1 e. CC /\ y e. CC ) -> ( 1 + y ) = ( y + 1 ) )
28 25 26 27 sylancr 
 |-  ( y e. ( 0 [,) +oo ) -> ( 1 + y ) = ( y + 1 ) )
29 24 28 breqtrrd 
 |-  ( y e. ( 0 [,) +oo ) -> y < ( 1 + y ) )
30 22 19 21 23 29 lelttrd 
 |-  ( y e. ( 0 [,) +oo ) -> 0 < ( 1 + y ) )
31 21 30 elrpd 
 |-  ( y e. ( 0 [,) +oo ) -> ( 1 + y ) e. RR+ )
32 19 31 rerpdivcld 
 |-  ( y e. ( 0 [,) +oo ) -> ( y / ( 1 + y ) ) e. RR )
33 divge0 
 |-  ( ( ( y e. RR /\ 0 <_ y ) /\ ( ( 1 + y ) e. RR /\ 0 < ( 1 + y ) ) ) -> 0 <_ ( y / ( 1 + y ) ) )
34 19 23 21 30 33 syl22anc 
 |-  ( y e. ( 0 [,) +oo ) -> 0 <_ ( y / ( 1 + y ) ) )
35 21 recnd 
 |-  ( y e. ( 0 [,) +oo ) -> ( 1 + y ) e. CC )
36 35 mulid1d 
 |-  ( y e. ( 0 [,) +oo ) -> ( ( 1 + y ) x. 1 ) = ( 1 + y ) )
37 29 36 breqtrrd 
 |-  ( y e. ( 0 [,) +oo ) -> y < ( ( 1 + y ) x. 1 ) )
38 8 a1i 
 |-  ( y e. ( 0 [,) +oo ) -> 1 e. RR )
39 ltdivmul 
 |-  ( ( y e. RR /\ 1 e. RR /\ ( ( 1 + y ) e. RR /\ 0 < ( 1 + y ) ) ) -> ( ( y / ( 1 + y ) ) < 1 <-> y < ( ( 1 + y ) x. 1 ) ) )
40 19 38 21 30 39 syl112anc 
 |-  ( y e. ( 0 [,) +oo ) -> ( ( y / ( 1 + y ) ) < 1 <-> y < ( ( 1 + y ) x. 1 ) ) )
41 37 40 mpbird 
 |-  ( y e. ( 0 [,) +oo ) -> ( y / ( 1 + y ) ) < 1 )
42 elico2 
 |-  ( ( 0 e. RR /\ 1 e. RR* ) -> ( ( y / ( 1 + y ) ) e. ( 0 [,) 1 ) <-> ( ( y / ( 1 + y ) ) e. RR /\ 0 <_ ( y / ( 1 + y ) ) /\ ( y / ( 1 + y ) ) < 1 ) ) )
43 2 3 42 mp2an 
 |-  ( ( y / ( 1 + y ) ) e. ( 0 [,) 1 ) <-> ( ( y / ( 1 + y ) ) e. RR /\ 0 <_ ( y / ( 1 + y ) ) /\ ( y / ( 1 + y ) ) < 1 ) )
44 32 34 41 43 syl3anbrc 
 |-  ( y e. ( 0 [,) +oo ) -> ( y / ( 1 + y ) ) e. ( 0 [,) 1 ) )
45 44 adantl 
 |-  ( ( T. /\ y e. ( 0 [,) +oo ) ) -> ( y / ( 1 + y ) ) e. ( 0 [,) 1 ) )
46 26 adantl 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> y e. CC )
47 6 adantr 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> x e. RR )
48 47 recnd 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> x e. CC )
49 48 46 mulcld 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( x x. y ) e. CC )
50 46 49 48 subadd2d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( y - ( x x. y ) ) = x <-> ( x + ( x x. y ) ) = y ) )
51 1cnd 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> 1 e. CC )
52 51 48 46 subdird 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( 1 - x ) x. y ) = ( ( 1 x. y ) - ( x x. y ) ) )
53 46 mulid2d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( 1 x. y ) = y )
54 53 oveq1d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( 1 x. y ) - ( x x. y ) ) = ( y - ( x x. y ) ) )
55 52 54 eqtrd 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( 1 - x ) x. y ) = ( y - ( x x. y ) ) )
56 55 eqeq1d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( ( 1 - x ) x. y ) = x <-> ( y - ( x x. y ) ) = x ) )
57 48 51 46 adddid 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( x x. ( 1 + y ) ) = ( ( x x. 1 ) + ( x x. y ) ) )
58 48 mulid1d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( x x. 1 ) = x )
59 58 oveq1d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( x x. 1 ) + ( x x. y ) ) = ( x + ( x x. y ) ) )
60 57 59 eqtrd 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( x x. ( 1 + y ) ) = ( x + ( x x. y ) ) )
61 60 eqeq1d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( x x. ( 1 + y ) ) = y <-> ( x + ( x x. y ) ) = y ) )
62 50 56 61 3bitr4rd 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( x x. ( 1 + y ) ) = y <-> ( ( 1 - x ) x. y ) = x ) )
63 eqcom 
 |-  ( y = ( x x. ( 1 + y ) ) <-> ( x x. ( 1 + y ) ) = y )
64 eqcom 
 |-  ( x = ( ( 1 - x ) x. y ) <-> ( ( 1 - x ) x. y ) = x )
65 62 63 64 3bitr4g 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( y = ( x x. ( 1 + y ) ) <-> x = ( ( 1 - x ) x. y ) ) )
66 35 adantl 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( 1 + y ) e. CC )
67 31 adantl 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( 1 + y ) e. RR+ )
68 67 rpne0d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( 1 + y ) =/= 0 )
69 46 48 66 68 divmul3d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( y / ( 1 + y ) ) = x <-> y = ( x x. ( 1 + y ) ) ) )
70 11 adantr 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( 1 - x ) e. RR+ )
71 70 rpcnd 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( 1 - x ) e. CC )
72 70 rpne0d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( 1 - x ) =/= 0 )
73 48 46 71 72 divmul2d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( x / ( 1 - x ) ) = y <-> x = ( ( 1 - x ) x. y ) ) )
74 65 69 73 3bitr4d 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( ( y / ( 1 + y ) ) = x <-> ( x / ( 1 - x ) ) = y ) )
75 eqcom 
 |-  ( x = ( y / ( 1 + y ) ) <-> ( y / ( 1 + y ) ) = x )
76 eqcom 
 |-  ( y = ( x / ( 1 - x ) ) <-> ( x / ( 1 - x ) ) = y )
77 74 75 76 3bitr4g 
 |-  ( ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) -> ( x = ( y / ( 1 + y ) ) <-> y = ( x / ( 1 - x ) ) ) )
78 77 adantl 
 |-  ( ( T. /\ ( x e. ( 0 [,) 1 ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x = ( y / ( 1 + y ) ) <-> y = ( x / ( 1 - x ) ) ) )
79 1 17 45 78 f1ocnv2d 
 |-  ( T. -> ( F : ( 0 [,) 1 ) -1-1-onto-> ( 0 [,) +oo ) /\ `' F = ( y e. ( 0 [,) +oo ) |-> ( y / ( 1 + y ) ) ) ) )
80 79 mptru 
 |-  ( F : ( 0 [,) 1 ) -1-1-onto-> ( 0 [,) +oo ) /\ `' F = ( y e. ( 0 [,) +oo ) |-> ( y / ( 1 + y ) ) ) )