Step | Hyp | Ref
| Expression |
1 | | iccssxr 12906 |
. . 3
⊢ (0[,]1)
⊆ ℝ* |
2 | | xrltso 12619 |
. . 3
⊢ < Or
ℝ* |
3 | | soss 5462 |
. . 3
⊢ ((0[,]1)
⊆ ℝ* → ( < Or ℝ* → < Or
(0[,]1))) |
4 | 1, 2, 3 | mp2 9 |
. 2
⊢ < Or
(0[,]1) |
5 | | iccssxr 12906 |
. . 3
⊢
(0[,]+∞) ⊆ ℝ* |
6 | | cnvso 6120 |
. . . . 5
⊢ ( < Or
ℝ* ↔ ◡ < Or
ℝ*) |
7 | 2, 6 | mpbi 233 |
. . . 4
⊢ ◡ < Or
ℝ* |
8 | | sopo 5461 |
. . . 4
⊢ (◡ < Or ℝ* → ◡ < Po
ℝ*) |
9 | 7, 8 | ax-mp 5 |
. . 3
⊢ ◡ < Po
ℝ* |
10 | | poss 5444 |
. . 3
⊢
((0[,]+∞) ⊆ ℝ* → (◡ < Po ℝ* → ◡ < Po (0[,]+∞))) |
11 | 5, 9, 10 | mp2 9 |
. 2
⊢ ◡ < Po (0[,]+∞) |
12 | | xrge0iifhmeo.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) |
13 | 12 | xrge0iifcnv 31457 |
. . . 4
⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 = +∞, 0,
(exp‘-𝑧)))) |
14 | 13 | simpli 487 |
. . 3
⊢ 𝐹:(0[,]1)–1-1-onto→(0[,]+∞) |
15 | | f1ofo 6627 |
. . 3
⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → 𝐹:(0[,]1)–onto→(0[,]+∞)) |
16 | 14, 15 | ax-mp 5 |
. 2
⊢ 𝐹:(0[,]1)–onto→(0[,]+∞) |
17 | | 0xr 10768 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
18 | | 1xr 10780 |
. . . . . . . 8
⊢ 1 ∈
ℝ* |
19 | | 0le1 11243 |
. . . . . . . 8
⊢ 0 ≤
1 |
20 | | snunioc 12956 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1)
→ ({0} ∪ (0(,]1)) = (0[,]1)) |
21 | 17, 18, 19, 20 | mp3an 1462 |
. . . . . . 7
⊢ ({0}
∪ (0(,]1)) = (0[,]1) |
22 | 21 | eleq2i 2824 |
. . . . . 6
⊢ (𝑤 ∈ ({0} ∪ (0(,]1))
↔ 𝑤 ∈
(0[,]1)) |
23 | | elun 4039 |
. . . . . 6
⊢ (𝑤 ∈ ({0} ∪ (0(,]1))
↔ (𝑤 ∈ {0} ∨
𝑤 ∈
(0(,]1))) |
24 | 22, 23 | bitr3i 280 |
. . . . 5
⊢ (𝑤 ∈ (0[,]1) ↔ (𝑤 ∈ {0} ∨ 𝑤 ∈
(0(,]1))) |
25 | | velsn 4532 |
. . . . . . 7
⊢ (𝑤 ∈ {0} ↔ 𝑤 = 0) |
26 | | elunitrn 12943 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (0[,]1) → 𝑧 ∈
ℝ) |
27 | 26 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 0 <
𝑧) → 𝑧 ∈
ℝ) |
28 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 0 <
𝑧) → 0 < 𝑧) |
29 | | elicc01 12942 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (0[,]1) ↔ (𝑧 ∈ ℝ ∧ 0 ≤
𝑧 ∧ 𝑧 ≤ 1)) |
30 | 29 | simp3bi 1148 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (0[,]1) → 𝑧 ≤ 1) |
31 | 30 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 0 <
𝑧) → 𝑧 ≤ 1) |
32 | | 1re 10721 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
33 | | elioc2 12886 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝑧 ∈ (0(,]1) ↔ (𝑧 ∈ ℝ ∧ 0 < 𝑧 ∧ 𝑧 ≤ 1))) |
34 | 17, 32, 33 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (0(,]1) ↔ (𝑧 ∈ ℝ ∧ 0 <
𝑧 ∧ 𝑧 ≤ 1)) |
35 | 27, 28, 31, 34 | syl3anbrc 1344 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (0[,]1) ∧ 0 <
𝑧) → 𝑧 ∈
(0(,]1)) |
36 | | pnfxr 10775 |
. . . . . . . . . . . . . . 15
⊢ +∞
∈ ℝ* |
37 | | 0le0 11819 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
0 |
38 | | ltpnf 12600 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℝ → 1 < +∞) |
39 | 32, 38 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 1 <
+∞ |
40 | | iocssioo 12915 |
. . . . . . . . . . . . . . 15
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
≤ 0 ∧ 1 < +∞)) → (0(,]1) ⊆
(0(,)+∞)) |
41 | 17, 36, 37, 39, 40 | mp4an 693 |
. . . . . . . . . . . . . 14
⊢ (0(,]1)
⊆ (0(,)+∞) |
42 | | ioorp 12901 |
. . . . . . . . . . . . . 14
⊢
(0(,)+∞) = ℝ+ |
43 | 41, 42 | sseqtri 3913 |
. . . . . . . . . . . . 13
⊢ (0(,]1)
⊆ ℝ+ |
44 | 43 | sseli 3873 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (0(,]1) → 𝑧 ∈
ℝ+) |
45 | | relogcl 25321 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ+
→ (log‘𝑧) ∈
ℝ) |
46 | 45 | renegcld 11147 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ+
→ -(log‘𝑧)
∈ ℝ) |
47 | | ltpnf 12600 |
. . . . . . . . . . . . . 14
⊢
(-(log‘𝑧)
∈ ℝ → -(log‘𝑧) < +∞) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℝ+
→ -(log‘𝑧) <
+∞) |
49 | | brcnvg 5722 |
. . . . . . . . . . . . . 14
⊢
((+∞ ∈ ℝ* ∧ -(log‘𝑧) ∈ ℝ) →
(+∞◡ < -(log‘𝑧) ↔ -(log‘𝑧) <
+∞)) |
50 | 36, 46, 49 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℝ+
→ (+∞◡ <
-(log‘𝑧) ↔
-(log‘𝑧) <
+∞)) |
51 | 48, 50 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ+
→ +∞◡ < -(log‘𝑧)) |
52 | 44, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (0(,]1) →
+∞◡ < -(log‘𝑧)) |
53 | 12 | xrge0iifcv 31458 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (0(,]1) → (𝐹‘𝑧) = -(log‘𝑧)) |
54 | 52, 53 | breqtrrd 5058 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0(,]1) →
+∞◡ < (𝐹‘𝑧)) |
55 | 35, 54 | syl 17 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (0[,]1) ∧ 0 <
𝑧) → +∞◡ < (𝐹‘𝑧)) |
56 | 55 | ex 416 |
. . . . . . . 8
⊢ (𝑧 ∈ (0[,]1) → (0 <
𝑧 → +∞◡ < (𝐹‘𝑧))) |
57 | | breq1 5033 |
. . . . . . . . 9
⊢ (𝑤 = 0 → (𝑤 < 𝑧 ↔ 0 < 𝑧)) |
58 | | fveq2 6676 |
. . . . . . . . . . 11
⊢ (𝑤 = 0 → (𝐹‘𝑤) = (𝐹‘0)) |
59 | | 0elunit 12945 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]1) |
60 | | iftrue 4420 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → if(𝑥 = 0, +∞,
-(log‘𝑥)) =
+∞) |
61 | | pnfex 10774 |
. . . . . . . . . . . . 13
⊢ +∞
∈ V |
62 | 60, 12, 61 | fvmpt 6777 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0[,]1) → (𝐹‘0)
= +∞) |
63 | 59, 62 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐹‘0) =
+∞ |
64 | 58, 63 | eqtrdi 2789 |
. . . . . . . . . 10
⊢ (𝑤 = 0 → (𝐹‘𝑤) = +∞) |
65 | 64 | breq1d 5040 |
. . . . . . . . 9
⊢ (𝑤 = 0 → ((𝐹‘𝑤)◡
< (𝐹‘𝑧) ↔ +∞◡ < (𝐹‘𝑧))) |
66 | 57, 65 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑤 = 0 → ((𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)) ↔ (0 < 𝑧 → +∞◡ < (𝐹‘𝑧)))) |
67 | 56, 66 | syl5ibr 249 |
. . . . . . 7
⊢ (𝑤 = 0 → (𝑧 ∈ (0[,]1) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) |
68 | 25, 67 | sylbi 220 |
. . . . . 6
⊢ (𝑤 ∈ {0} → (𝑧 ∈ (0[,]1) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) |
69 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑤 ∈ (0(,]1)) |
70 | 26 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑧 ∈ ℝ) |
71 | | 0re 10723 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
72 | 71 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 0 ∈ ℝ) |
73 | 43 | sseli 3873 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (0(,]1) → 𝑤 ∈
ℝ+) |
74 | 73 | rpred 12516 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (0(,]1) → 𝑤 ∈
ℝ) |
75 | 74 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑤 ∈ ℝ) |
76 | | elioc2 12886 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝑤 ∈ (0(,]1) ↔ (𝑤 ∈ ℝ ∧ 0 < 𝑤 ∧ 𝑤 ≤ 1))) |
77 | 17, 32, 76 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (0(,]1) ↔ (𝑤 ∈ ℝ ∧ 0 <
𝑤 ∧ 𝑤 ≤ 1)) |
78 | 77 | simp2bi 1147 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (0(,]1) → 0 <
𝑤) |
79 | 78 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 0 < 𝑤) |
80 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑤 < 𝑧) |
81 | 72, 75, 70, 79, 80 | lttrd 10881 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 0 < 𝑧) |
82 | 30 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑧 ≤ 1) |
83 | 70, 81, 82, 34 | syl3anbrc 1344 |
. . . . . . . . 9
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑧 ∈ (0(,]1)) |
84 | 69, 83 | jca 515 |
. . . . . . . 8
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → (𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1))) |
85 | 73 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → 𝑤 ∈
ℝ+) |
86 | 85 | relogcld 25368 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) →
(log‘𝑤) ∈
ℝ) |
87 | 44 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → 𝑧 ∈
ℝ+) |
88 | 87 | relogcld 25368 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) →
(log‘𝑧) ∈
ℝ) |
89 | 86, 88 | ltnegd 11298 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) →
((log‘𝑤) <
(log‘𝑧) ↔
-(log‘𝑧) <
-(log‘𝑤))) |
90 | | logltb 25345 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℝ+
∧ 𝑧 ∈
ℝ+) → (𝑤 < 𝑧 ↔ (log‘𝑤) < (log‘𝑧))) |
91 | 73, 44, 90 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → (𝑤 < 𝑧 ↔ (log‘𝑤) < (log‘𝑧))) |
92 | | negex 10964 |
. . . . . . . . . . . . 13
⊢
-(log‘𝑤)
∈ V |
93 | | negex 10964 |
. . . . . . . . . . . . 13
⊢
-(log‘𝑧)
∈ V |
94 | 92, 93 | brcnv 5725 |
. . . . . . . . . . . 12
⊢
(-(log‘𝑤)◡ < -(log‘𝑧) ↔ -(log‘𝑧) < -(log‘𝑤)) |
95 | 94 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) →
(-(log‘𝑤)◡ < -(log‘𝑧) ↔ -(log‘𝑧) < -(log‘𝑤))) |
96 | 89, 91, 95 | 3bitr4d 314 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → (𝑤 < 𝑧 ↔ -(log‘𝑤)◡
< -(log‘𝑧))) |
97 | 96 | biimpd 232 |
. . . . . . . . 9
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → (𝑤 < 𝑧 → -(log‘𝑤)◡
< -(log‘𝑧))) |
98 | 12 | xrge0iifcv 31458 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (0(,]1) → (𝐹‘𝑤) = -(log‘𝑤)) |
99 | 98, 53 | breqan12d 5046 |
. . . . . . . . 9
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → ((𝐹‘𝑤)◡
< (𝐹‘𝑧) ↔ -(log‘𝑤)◡ < -(log‘𝑧))) |
100 | 97, 99 | sylibrd 262 |
. . . . . . . 8
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧))) |
101 | 84, 80, 100 | sylc 65 |
. . . . . . 7
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → (𝐹‘𝑤)◡
< (𝐹‘𝑧)) |
102 | 101 | exp31 423 |
. . . . . 6
⊢ (𝑤 ∈ (0(,]1) → (𝑧 ∈ (0[,]1) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) |
103 | 68, 102 | jaoi 856 |
. . . . 5
⊢ ((𝑤 ∈ {0} ∨ 𝑤 ∈ (0(,]1)) → (𝑧 ∈ (0[,]1) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) |
104 | 24, 103 | sylbi 220 |
. . . 4
⊢ (𝑤 ∈ (0[,]1) → (𝑧 ∈ (0[,]1) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) |
105 | 104 | imp 410 |
. . 3
⊢ ((𝑤 ∈ (0[,]1) ∧ 𝑧 ∈ (0[,]1)) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧))) |
106 | 105 | rgen2 3115 |
. 2
⊢
∀𝑤 ∈
(0[,]1)∀𝑧 ∈
(0[,]1)(𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)) |
107 | | soisoi 7096 |
. 2
⊢ ((( <
Or (0[,]1) ∧ ◡ < Po
(0[,]+∞)) ∧ (𝐹:(0[,]1)–onto→(0[,]+∞) ∧ ∀𝑤 ∈ (0[,]1)∀𝑧 ∈ (0[,]1)(𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) → 𝐹 Isom < , ◡ < ((0[,]1),
(0[,]+∞))) |
108 | 4, 11, 16, 106, 107 | mp4an 693 |
1
⊢ 𝐹 Isom < , ◡ < ((0[,]1),
(0[,]+∞)) |