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