Step | Hyp | Ref
| Expression |
1 | | iccssxr 12256 |
. . 3
⊢ (0[,]1)
⊆ ℝ* |
2 | | xrltso 11974 |
. . 3
⊢ < Or
ℝ* |
3 | | soss 5053 |
. . 3
⊢ ((0[,]1)
⊆ ℝ* → ( < Or ℝ* → < Or
(0[,]1))) |
4 | 1, 2, 3 | mp2 9 |
. 2
⊢ < Or
(0[,]1) |
5 | | iccssxr 12256 |
. . 3
⊢
(0[,]+∞) ⊆ ℝ* |
6 | | cnvso 5674 |
. . . . 5
⊢ ( < Or
ℝ* ↔ ◡ < Or
ℝ*) |
7 | 2, 6 | mpbi 220 |
. . . 4
⊢ ◡ < Or
ℝ* |
8 | | sopo 5052 |
. . . 4
⊢ (◡ < Or ℝ* → ◡ < Po
ℝ*) |
9 | 7, 8 | ax-mp 5 |
. . 3
⊢ ◡ < Po
ℝ* |
10 | | poss 5037 |
. . 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 29979 |
. . . 4
⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 = +∞, 0,
(exp‘-𝑧)))) |
14 | 13 | simpli 474 |
. . 3
⊢ 𝐹:(0[,]1)–1-1-onto→(0[,]+∞) |
15 | | f1ofo 6144 |
. . 3
⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → 𝐹:(0[,]1)–onto→(0[,]+∞)) |
16 | 14, 15 | ax-mp 5 |
. 2
⊢ 𝐹:(0[,]1)–onto→(0[,]+∞) |
17 | | 0xr 10086 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
18 | | 1re 10039 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
19 | 18 | rexri 10097 |
. . . . . . . 8
⊢ 1 ∈
ℝ* |
20 | | 0le1 10551 |
. . . . . . . 8
⊢ 0 ≤
1 |
21 | | snunioc 12300 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1)
→ ({0} ∪ (0(,]1)) = (0[,]1)) |
22 | 17, 19, 20, 21 | mp3an 1424 |
. . . . . . 7
⊢ ({0}
∪ (0(,]1)) = (0[,]1) |
23 | 22 | eleq2i 2693 |
. . . . . 6
⊢ (𝑤 ∈ ({0} ∪ (0(,]1))
↔ 𝑤 ∈
(0[,]1)) |
24 | | elun 3753 |
. . . . . 6
⊢ (𝑤 ∈ ({0} ∪ (0(,]1))
↔ (𝑤 ∈ {0} ∨
𝑤 ∈
(0(,]1))) |
25 | 23, 24 | bitr3i 266 |
. . . . 5
⊢ (𝑤 ∈ (0[,]1) ↔ (𝑤 ∈ {0} ∨ 𝑤 ∈
(0(,]1))) |
26 | | velsn 4193 |
. . . . . . 7
⊢ (𝑤 ∈ {0} ↔ 𝑤 = 0) |
27 | | elunitrn 29943 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (0[,]1) → 𝑧 ∈
ℝ) |
28 | 27 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 0 <
𝑧) → 𝑧 ∈
ℝ) |
29 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 0 <
𝑧) → 0 < 𝑧) |
30 | | 0re 10040 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
31 | 30, 18 | elicc2i 12239 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (0[,]1) ↔ (𝑧 ∈ ℝ ∧ 0 ≤
𝑧 ∧ 𝑧 ≤ 1)) |
32 | 31 | simp3bi 1078 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (0[,]1) → 𝑧 ≤ 1) |
33 | 32 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (0[,]1) ∧ 0 <
𝑧) → 𝑧 ≤ 1) |
34 | | elioc2 12236 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝑧 ∈ (0(,]1) ↔ (𝑧 ∈ ℝ ∧ 0 < 𝑧 ∧ 𝑧 ≤ 1))) |
35 | 17, 18, 34 | mp2an 708 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (0(,]1) ↔ (𝑧 ∈ ℝ ∧ 0 <
𝑧 ∧ 𝑧 ≤ 1)) |
36 | 28, 29, 33, 35 | syl3anbrc 1246 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (0[,]1) ∧ 0 <
𝑧) → 𝑧 ∈
(0(,]1)) |
37 | | pnfxr 10092 |
. . . . . . . . . . . . . . 15
⊢ +∞
∈ ℝ* |
38 | | 0le0 11110 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
0 |
39 | | ltpnf 11954 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℝ → 1 < +∞) |
40 | 18, 39 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 1 <
+∞ |
41 | | iocssioo 12263 |
. . . . . . . . . . . . . . 15
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
≤ 0 ∧ 1 < +∞)) → (0(,]1) ⊆
(0(,)+∞)) |
42 | 17, 37, 38, 40, 41 | mp4an 709 |
. . . . . . . . . . . . . 14
⊢ (0(,]1)
⊆ (0(,)+∞) |
43 | | ioorp 12251 |
. . . . . . . . . . . . . 14
⊢
(0(,)+∞) = ℝ+ |
44 | 42, 43 | sseqtri 3637 |
. . . . . . . . . . . . 13
⊢ (0(,]1)
⊆ ℝ+ |
45 | 44 | sseli 3599 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (0(,]1) → 𝑧 ∈
ℝ+) |
46 | | relogcl 24322 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ+
→ (log‘𝑧) ∈
ℝ) |
47 | 46 | renegcld 10457 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ+
→ -(log‘𝑧)
∈ ℝ) |
48 | | ltpnf 11954 |
. . . . . . . . . . . . . 14
⊢
(-(log‘𝑧)
∈ ℝ → -(log‘𝑧) < +∞) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℝ+
→ -(log‘𝑧) <
+∞) |
50 | | brcnvg 5303 |
. . . . . . . . . . . . . 14
⊢
((+∞ ∈ ℝ* ∧ -(log‘𝑧) ∈ ℝ) →
(+∞◡ < -(log‘𝑧) ↔ -(log‘𝑧) <
+∞)) |
51 | 37, 47, 50 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℝ+
→ (+∞◡ <
-(log‘𝑧) ↔
-(log‘𝑧) <
+∞)) |
52 | 49, 51 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ+
→ +∞◡ < -(log‘𝑧)) |
53 | 45, 52 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (0(,]1) →
+∞◡ < -(log‘𝑧)) |
54 | 12 | xrge0iifcv 29980 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (0(,]1) → (𝐹‘𝑧) = -(log‘𝑧)) |
55 | 53, 54 | breqtrrd 4681 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0(,]1) →
+∞◡ < (𝐹‘𝑧)) |
56 | 36, 55 | syl 17 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (0[,]1) ∧ 0 <
𝑧) → +∞◡ < (𝐹‘𝑧)) |
57 | 56 | ex 450 |
. . . . . . . 8
⊢ (𝑧 ∈ (0[,]1) → (0 <
𝑧 → +∞◡ < (𝐹‘𝑧))) |
58 | | breq1 4656 |
. . . . . . . . 9
⊢ (𝑤 = 0 → (𝑤 < 𝑧 ↔ 0 < 𝑧)) |
59 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑤 = 0 → (𝐹‘𝑤) = (𝐹‘0)) |
60 | | 0elunit 12290 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]1) |
61 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → if(𝑥 = 0, +∞,
-(log‘𝑥)) =
+∞) |
62 | | pnfex 10093 |
. . . . . . . . . . . . 13
⊢ +∞
∈ V |
63 | 61, 12, 62 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0[,]1) → (𝐹‘0)
= +∞) |
64 | 60, 63 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐹‘0) =
+∞ |
65 | 59, 64 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑤 = 0 → (𝐹‘𝑤) = +∞) |
66 | 65 | breq1d 4663 |
. . . . . . . . 9
⊢ (𝑤 = 0 → ((𝐹‘𝑤)◡
< (𝐹‘𝑧) ↔ +∞◡ < (𝐹‘𝑧))) |
67 | 58, 66 | imbi12d 334 |
. . . . . . . 8
⊢ (𝑤 = 0 → ((𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)) ↔ (0 < 𝑧 → +∞◡ < (𝐹‘𝑧)))) |
68 | 57, 67 | syl5ibr 236 |
. . . . . . 7
⊢ (𝑤 = 0 → (𝑧 ∈ (0[,]1) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) |
69 | 26, 68 | sylbi 207 |
. . . . . 6
⊢ (𝑤 ∈ {0} → (𝑧 ∈ (0[,]1) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) |
70 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑤 ∈ (0(,]1)) |
71 | 27 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑧 ∈ ℝ) |
72 | 30 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 0 ∈ ℝ) |
73 | 44 | sseli 3599 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (0(,]1) → 𝑤 ∈
ℝ+) |
74 | 73 | rpred 11872 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (0(,]1) → 𝑤 ∈
ℝ) |
75 | 74 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑤 ∈ ℝ) |
76 | | elioc2 12236 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝑤 ∈ (0(,]1) ↔ (𝑤 ∈ ℝ ∧ 0 < 𝑤 ∧ 𝑤 ≤ 1))) |
77 | 17, 18, 76 | mp2an 708 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (0(,]1) ↔ (𝑤 ∈ ℝ ∧ 0 <
𝑤 ∧ 𝑤 ≤ 1)) |
78 | 77 | simp2bi 1077 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (0(,]1) → 0 <
𝑤) |
79 | 78 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 0 < 𝑤) |
80 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑤 < 𝑧) |
81 | 72, 75, 71, 79, 80 | lttrd 10198 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 0 < 𝑧) |
82 | 32 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑧 ≤ 1) |
83 | 71, 81, 82, 35 | syl3anbrc 1246 |
. . . . . . . . 9
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → 𝑧 ∈ (0(,]1)) |
84 | 70, 83 | jca 554 |
. . . . . . . 8
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → (𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1))) |
85 | 73 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → 𝑤 ∈
ℝ+) |
86 | 85 | relogcld 24369 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) →
(log‘𝑤) ∈
ℝ) |
87 | 45 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → 𝑧 ∈
ℝ+) |
88 | 87 | relogcld 24369 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) →
(log‘𝑧) ∈
ℝ) |
89 | 86, 88 | ltnegd 10605 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) →
((log‘𝑤) <
(log‘𝑧) ↔
-(log‘𝑧) <
-(log‘𝑤))) |
90 | | logltb 24346 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℝ+
∧ 𝑧 ∈
ℝ+) → (𝑤 < 𝑧 ↔ (log‘𝑤) < (log‘𝑧))) |
91 | 73, 45, 90 | syl2an 494 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → (𝑤 < 𝑧 ↔ (log‘𝑤) < (log‘𝑧))) |
92 | | negex 10279 |
. . . . . . . . . . . . 13
⊢
-(log‘𝑤)
∈ V |
93 | | negex 10279 |
. . . . . . . . . . . . 13
⊢
-(log‘𝑧)
∈ V |
94 | 92, 93 | brcnv 5305 |
. . . . . . . . . . . 12
⊢
(-(log‘𝑤)◡ < -(log‘𝑧) ↔ -(log‘𝑧) < -(log‘𝑤)) |
95 | 94 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) →
(-(log‘𝑤)◡ < -(log‘𝑧) ↔ -(log‘𝑧) < -(log‘𝑤))) |
96 | 89, 91, 95 | 3bitr4d 300 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → (𝑤 < 𝑧 ↔ -(log‘𝑤)◡
< -(log‘𝑧))) |
97 | 96 | biimpd 219 |
. . . . . . . . 9
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → (𝑤 < 𝑧 → -(log‘𝑤)◡
< -(log‘𝑧))) |
98 | 12 | xrge0iifcv 29980 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (0(,]1) → (𝐹‘𝑤) = -(log‘𝑤)) |
99 | 98, 54 | breqan12d 4669 |
. . . . . . . . 9
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → ((𝐹‘𝑤)◡
< (𝐹‘𝑧) ↔ -(log‘𝑤)◡ < -(log‘𝑧))) |
100 | 97, 99 | sylibrd 249 |
. . . . . . . 8
⊢ ((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0(,]1)) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧))) |
101 | 84, 80, 100 | sylc 65 |
. . . . . . 7
⊢ (((𝑤 ∈ (0(,]1) ∧ 𝑧 ∈ (0[,]1)) ∧ 𝑤 < 𝑧) → (𝐹‘𝑤)◡
< (𝐹‘𝑧)) |
102 | 101 | exp31 630 |
. . . . . 6
⊢ (𝑤 ∈ (0(,]1) → (𝑧 ∈ (0[,]1) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) |
103 | 69, 102 | jaoi 394 |
. . . . 5
⊢ ((𝑤 ∈ {0} ∨ 𝑤 ∈ (0(,]1)) → (𝑧 ∈ (0[,]1) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) |
104 | 25, 103 | sylbi 207 |
. . . 4
⊢ (𝑤 ∈ (0[,]1) → (𝑧 ∈ (0[,]1) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)))) |
105 | 104 | imp 445 |
. . 3
⊢ ((𝑤 ∈ (0[,]1) ∧ 𝑧 ∈ (0[,]1)) → (𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧))) |
106 | 105 | rgen2a 2977 |
. 2
⊢
∀𝑤 ∈
(0[,]1)∀𝑧 ∈
(0[,]1)(𝑤 < 𝑧 → (𝐹‘𝑤)◡
< (𝐹‘𝑧)) |
107 | | soisoi 6578 |
. 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 709 |
1
⊢ 𝐹 Isom < , ◡ < ((0[,]1),
(0[,]+∞)) |