Proof of Theorem xrge0iifhom
Step | Hyp | Ref
| Expression |
1 | | 0xr 10086 |
. . . . . 6
⊢ 0 ∈
ℝ* |
2 | | 1re 10039 |
. . . . . . 7
⊢ 1 ∈
ℝ |
3 | 2 | rexri 10097 |
. . . . . 6
⊢ 1 ∈
ℝ* |
4 | | 0le1 10551 |
. . . . . 6
⊢ 0 ≤
1 |
5 | | snunioc 12300 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1)
→ ({0} ∪ (0(,]1)) = (0[,]1)) |
6 | 1, 3, 4, 5 | mp3an 1424 |
. . . . 5
⊢ ({0}
∪ (0(,]1)) = (0[,]1) |
7 | 6 | eleq2i 2693 |
. . . 4
⊢ (𝑌 ∈ ({0} ∪ (0(,]1))
↔ 𝑌 ∈
(0[,]1)) |
8 | | elun 3753 |
. . . 4
⊢ (𝑌 ∈ ({0} ∪ (0(,]1))
↔ (𝑌 ∈ {0} ∨
𝑌 ∈
(0(,]1))) |
9 | 7, 8 | bitr3i 266 |
. . 3
⊢ (𝑌 ∈ (0[,]1) ↔ (𝑌 ∈ {0} ∨ 𝑌 ∈
(0(,]1))) |
10 | | elsni 4194 |
. . . 4
⊢ (𝑌 ∈ {0} → 𝑌 = 0) |
11 | 10 | orim1i 539 |
. . 3
⊢ ((𝑌 ∈ {0} ∨ 𝑌 ∈ (0(,]1)) → (𝑌 = 0 ∨ 𝑌 ∈ (0(,]1))) |
12 | 9, 11 | sylbi 207 |
. 2
⊢ (𝑌 ∈ (0[,]1) → (𝑌 = 0 ∨ 𝑌 ∈ (0(,]1))) |
13 | | 0elunit 12290 |
. . . . . . . 8
⊢ 0 ∈
(0[,]1) |
14 | | iftrue 4092 |
. . . . . . . . 9
⊢ (𝑥 = 0 → if(𝑥 = 0, +∞,
-(log‘𝑥)) =
+∞) |
15 | | xrge0iifhmeo.1 |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) |
16 | | pnfex 10093 |
. . . . . . . . 9
⊢ +∞
∈ V |
17 | 14, 15, 16 | fvmpt 6282 |
. . . . . . . 8
⊢ (0 ∈
(0[,]1) → (𝐹‘0)
= +∞) |
18 | 13, 17 | ax-mp 5 |
. . . . . . 7
⊢ (𝐹‘0) =
+∞ |
19 | 18 | oveq2i 6661 |
. . . . . 6
⊢ ((𝐹‘𝑋) +𝑒 (𝐹‘0)) = ((𝐹‘𝑋) +𝑒
+∞) |
20 | | eqeq1 2626 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥 = 0 ↔ 𝑋 = 0)) |
21 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (log‘𝑥) = (log‘𝑋)) |
22 | 21 | negeqd 10275 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → -(log‘𝑥) = -(log‘𝑋)) |
23 | 20, 22 | ifbieq2d 4111 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → if(𝑥 = 0, +∞, -(log‘𝑥)) = if(𝑋 = 0, +∞, -(log‘𝑋))) |
24 | | negex 10279 |
. . . . . . . . . . 11
⊢
-(log‘𝑋)
∈ V |
25 | 16, 24 | ifex 4156 |
. . . . . . . . . 10
⊢ if(𝑋 = 0, +∞,
-(log‘𝑋)) ∈
V |
26 | 23, 15, 25 | fvmpt 6282 |
. . . . . . . . 9
⊢ (𝑋 ∈ (0[,]1) → (𝐹‘𝑋) = if(𝑋 = 0, +∞, -(log‘𝑋))) |
27 | | pnfxr 10092 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑋 = 0) → +∞ ∈
ℝ*) |
29 | | elunitrn 29943 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ (0[,]1) → 𝑋 ∈
ℝ) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬
𝑋 = 0) → 𝑋 ∈
ℝ) |
31 | | elunitge0 29945 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (0[,]1) → 0 ≤
𝑋) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬
𝑋 = 0) → 0 ≤ 𝑋) |
33 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬
𝑋 = 0) → ¬ 𝑋 = 0) |
34 | 33 | neqned 2801 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬
𝑋 = 0) → 𝑋 ≠ 0) |
35 | 30, 32, 34 | ne0gt0d 10174 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬
𝑋 = 0) → 0 < 𝑋) |
36 | 30, 35 | elrpd 11869 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬
𝑋 = 0) → 𝑋 ∈
ℝ+) |
37 | 36 | relogcld 24369 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬
𝑋 = 0) →
(log‘𝑋) ∈
ℝ) |
38 | 37 | renegcld 10457 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬
𝑋 = 0) →
-(log‘𝑋) ∈
ℝ) |
39 | 38 | rexrd 10089 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬
𝑋 = 0) →
-(log‘𝑋) ∈
ℝ*) |
40 | 28, 39 | ifclda 4120 |
. . . . . . . . 9
⊢ (𝑋 ∈ (0[,]1) → if(𝑋 = 0, +∞,
-(log‘𝑋)) ∈
ℝ*) |
41 | 26, 40 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝑋 ∈ (0[,]1) → (𝐹‘𝑋) ∈
ℝ*) |
42 | 41 | adantr 481 |
. . . . . . 7
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → (𝐹‘𝑋) ∈
ℝ*) |
43 | | neeq1 2856 |
. . . . . . . . . 10
⊢ (+∞
= if(𝑋 = 0, +∞,
-(log‘𝑋)) →
(+∞ ≠ -∞ ↔ if(𝑋 = 0, +∞, -(log‘𝑋)) ≠
-∞)) |
44 | | neeq1 2856 |
. . . . . . . . . 10
⊢
(-(log‘𝑋) =
if(𝑋 = 0, +∞,
-(log‘𝑋)) →
(-(log‘𝑋) ≠
-∞ ↔ if(𝑋 = 0,
+∞, -(log‘𝑋))
≠ -∞)) |
45 | | pnfnemnf 10094 |
. . . . . . . . . . 11
⊢ +∞
≠ -∞ |
46 | 45 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑋 = 0) → +∞ ≠
-∞) |
47 | 38 | renemnfd 10091 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬
𝑋 = 0) →
-(log‘𝑋) ≠
-∞) |
48 | 43, 44, 46, 47 | ifbothda 4123 |
. . . . . . . . 9
⊢ (𝑋 ∈ (0[,]1) → if(𝑋 = 0, +∞,
-(log‘𝑋)) ≠
-∞) |
49 | 26, 48 | eqnetrd 2861 |
. . . . . . . 8
⊢ (𝑋 ∈ (0[,]1) → (𝐹‘𝑋) ≠ -∞) |
50 | 49 | adantr 481 |
. . . . . . 7
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → (𝐹‘𝑋) ≠ -∞) |
51 | | xaddpnf1 12057 |
. . . . . . 7
⊢ (((𝐹‘𝑋) ∈ ℝ* ∧ (𝐹‘𝑋) ≠ -∞) → ((𝐹‘𝑋) +𝑒 +∞) =
+∞) |
52 | 42, 50, 51 | syl2anc 693 |
. . . . . 6
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → ((𝐹‘𝑋) +𝑒 +∞) =
+∞) |
53 | 19, 52 | syl5eq 2668 |
. . . . 5
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → ((𝐹‘𝑋) +𝑒 (𝐹‘0)) = +∞) |
54 | | unitsscn 29942 |
. . . . . . . . 9
⊢ (0[,]1)
⊆ ℂ |
55 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → 𝑋 ∈ (0[,]1)) |
56 | 54, 55 | sseldi 3601 |
. . . . . . . 8
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → 𝑋 ∈ ℂ) |
57 | 56 | mul01d 10235 |
. . . . . . 7
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → (𝑋 · 0) = 0) |
58 | 57 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → (𝐹‘(𝑋 · 0)) = (𝐹‘0)) |
59 | 58, 18 | syl6eq 2672 |
. . . . 5
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → (𝐹‘(𝑋 · 0)) = +∞) |
60 | 53, 59 | eqtr4d 2659 |
. . . 4
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → ((𝐹‘𝑋) +𝑒 (𝐹‘0)) = (𝐹‘(𝑋 · 0))) |
61 | | simpr 477 |
. . . . . 6
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → 𝑌 = 0) |
62 | 61 | fveq2d 6195 |
. . . . 5
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → (𝐹‘𝑌) = (𝐹‘0)) |
63 | 62 | oveq2d 6666 |
. . . 4
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘0))) |
64 | 61 | oveq2d 6666 |
. . . . 5
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → (𝑋 · 𝑌) = (𝑋 · 0)) |
65 | 64 | fveq2d 6195 |
. . . 4
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → (𝐹‘(𝑋 · 𝑌)) = (𝐹‘(𝑋 · 0))) |
66 | 60, 63, 65 | 3eqtr4rd 2667 |
. . 3
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 = 0) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌))) |
67 | 6 | eleq2i 2693 |
. . . . . 6
⊢ (𝑋 ∈ ({0} ∪ (0(,]1))
↔ 𝑋 ∈
(0[,]1)) |
68 | | elun 3753 |
. . . . . 6
⊢ (𝑋 ∈ ({0} ∪ (0(,]1))
↔ (𝑋 ∈ {0} ∨
𝑋 ∈
(0(,]1))) |
69 | 67, 68 | bitr3i 266 |
. . . . 5
⊢ (𝑋 ∈ (0[,]1) ↔ (𝑋 ∈ {0} ∨ 𝑋 ∈
(0(,]1))) |
70 | | elsni 4194 |
. . . . . 6
⊢ (𝑋 ∈ {0} → 𝑋 = 0) |
71 | 70 | orim1i 539 |
. . . . 5
⊢ ((𝑋 ∈ {0} ∨ 𝑋 ∈ (0(,]1)) → (𝑋 = 0 ∨ 𝑋 ∈ (0(,]1))) |
72 | 69, 71 | sylbi 207 |
. . . 4
⊢ (𝑋 ∈ (0[,]1) → (𝑋 = 0 ∨ 𝑋 ∈ (0(,]1))) |
73 | 18 | oveq1i 6660 |
. . . . . . . 8
⊢ ((𝐹‘0) +𝑒
(𝐹‘𝑌)) = (+∞ +𝑒 (𝐹‘𝑌)) |
74 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → 𝑌 ∈ (0(,]1)) |
75 | 15 | xrge0iifcv 29980 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ (0(,]1) → (𝐹‘𝑌) = -(log‘𝑌)) |
76 | | 0le0 11110 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
0 |
77 | | ltpnf 11954 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℝ → 1 < +∞) |
78 | 2, 77 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ 1 <
+∞ |
79 | | iocssioo 12263 |
. . . . . . . . . . . . . . . . 17
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
≤ 0 ∧ 1 < +∞)) → (0(,]1) ⊆
(0(,)+∞)) |
80 | 1, 27, 76, 78, 79 | mp4an 709 |
. . . . . . . . . . . . . . . 16
⊢ (0(,]1)
⊆ (0(,)+∞) |
81 | | ioorp 12251 |
. . . . . . . . . . . . . . . 16
⊢
(0(,)+∞) = ℝ+ |
82 | 80, 81 | sseqtri 3637 |
. . . . . . . . . . . . . . 15
⊢ (0(,]1)
⊆ ℝ+ |
83 | 82 | sseli 3599 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∈ (0(,]1) → 𝑌 ∈
ℝ+) |
84 | 83 | relogcld 24369 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ (0(,]1) →
(log‘𝑌) ∈
ℝ) |
85 | 84 | renegcld 10457 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ (0(,]1) →
-(log‘𝑌) ∈
ℝ) |
86 | 75, 85 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ (0(,]1) → (𝐹‘𝑌) ∈ ℝ) |
87 | 86 | rexrd 10089 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (0(,]1) → (𝐹‘𝑌) ∈
ℝ*) |
88 | 74, 87 | syl 17 |
. . . . . . . . 9
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘𝑌) ∈
ℝ*) |
89 | 86 | renemnfd 10091 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (0(,]1) → (𝐹‘𝑌) ≠ -∞) |
90 | 74, 89 | syl 17 |
. . . . . . . . 9
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘𝑌) ≠ -∞) |
91 | | xaddpnf2 12058 |
. . . . . . . . 9
⊢ (((𝐹‘𝑌) ∈ ℝ* ∧ (𝐹‘𝑌) ≠ -∞) → (+∞
+𝑒 (𝐹‘𝑌)) = +∞) |
92 | 88, 90, 91 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → (+∞
+𝑒 (𝐹‘𝑌)) = +∞) |
93 | 73, 92 | syl5eq 2668 |
. . . . . . 7
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → ((𝐹‘0) +𝑒 (𝐹‘𝑌)) = +∞) |
94 | | rpssre 11843 |
. . . . . . . . . . . . 13
⊢
ℝ+ ⊆ ℝ |
95 | 82, 94 | sstri 3612 |
. . . . . . . . . . . 12
⊢ (0(,]1)
⊆ ℝ |
96 | | ax-resscn 9993 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
97 | 95, 96 | sstri 3612 |
. . . . . . . . . . 11
⊢ (0(,]1)
⊆ ℂ |
98 | 97, 74 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → 𝑌 ∈ ℂ) |
99 | 98 | mul02d 10234 |
. . . . . . . . 9
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → (0 · 𝑌) = 0) |
100 | 99 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘(0 · 𝑌)) = (𝐹‘0)) |
101 | 100, 18 | syl6eq 2672 |
. . . . . . 7
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘(0 · 𝑌)) = +∞) |
102 | 93, 101 | eqtr4d 2659 |
. . . . . 6
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → ((𝐹‘0) +𝑒 (𝐹‘𝑌)) = (𝐹‘(0 · 𝑌))) |
103 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → 𝑋 = 0) |
104 | 103 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘𝑋) = (𝐹‘0)) |
105 | 104 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌)) = ((𝐹‘0) +𝑒 (𝐹‘𝑌))) |
106 | 103 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → (𝑋 · 𝑌) = (0 · 𝑌)) |
107 | 106 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘(𝑋 · 𝑌)) = (𝐹‘(0 · 𝑌))) |
108 | 102, 105,
107 | 3eqtr4rd 2667 |
. . . . 5
⊢ ((𝑋 = 0 ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌))) |
109 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 𝑋 ∈
(0(,]1)) |
110 | 82, 109 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 𝑋 ∈
ℝ+) |
111 | 110 | relogcld 24369 |
. . . . . . . 8
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) →
(log‘𝑋) ∈
ℝ) |
112 | 111 | renegcld 10457 |
. . . . . . 7
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) →
-(log‘𝑋) ∈
ℝ) |
113 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 𝑌 ∈
(0(,]1)) |
114 | 82, 113 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 𝑌 ∈
ℝ+) |
115 | 114 | relogcld 24369 |
. . . . . . . 8
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) →
(log‘𝑌) ∈
ℝ) |
116 | 115 | renegcld 10457 |
. . . . . . 7
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) →
-(log‘𝑌) ∈
ℝ) |
117 | | rexadd 12063 |
. . . . . . 7
⊢
((-(log‘𝑋)
∈ ℝ ∧ -(log‘𝑌) ∈ ℝ) → (-(log‘𝑋) +𝑒
-(log‘𝑌)) =
(-(log‘𝑋) +
-(log‘𝑌))) |
118 | 112, 116,
117 | syl2anc 693 |
. . . . . 6
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) →
(-(log‘𝑋)
+𝑒 -(log‘𝑌)) = (-(log‘𝑋) + -(log‘𝑌))) |
119 | 15 | xrge0iifcv 29980 |
. . . . . . 7
⊢ (𝑋 ∈ (0(,]1) → (𝐹‘𝑋) = -(log‘𝑋)) |
120 | 119, 75 | oveqan12d 6669 |
. . . . . 6
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌)) = (-(log‘𝑋) +𝑒 -(log‘𝑌))) |
121 | 110 | rpred 11872 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 𝑋 ∈
ℝ) |
122 | 114 | rpred 11872 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 𝑌 ∈
ℝ) |
123 | 121, 122 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → (𝑋 · 𝑌) ∈ ℝ) |
124 | 110 | rpgt0d 11875 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 0 <
𝑋) |
125 | 114 | rpgt0d 11875 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 0 <
𝑌) |
126 | 121, 122,
124, 125 | mulgt0d 10192 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 0 <
(𝑋 · 𝑌)) |
127 | | iocssicc 12261 |
. . . . . . . . . . . 12
⊢ (0(,]1)
⊆ (0[,]1) |
128 | 127, 109 | sseldi 3601 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 𝑋 ∈
(0[,]1)) |
129 | 127, 113 | sseldi 3601 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → 𝑌 ∈
(0[,]1)) |
130 | | iimulcl 22736 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → (𝑋 · 𝑌) ∈ (0[,]1)) |
131 | 128, 129,
130 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → (𝑋 · 𝑌) ∈ (0[,]1)) |
132 | | 0re 10040 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
133 | 132, 2 | elicc2i 12239 |
. . . . . . . . . . 11
⊢ ((𝑋 · 𝑌) ∈ (0[,]1) ↔ ((𝑋 · 𝑌) ∈ ℝ ∧ 0 ≤ (𝑋 · 𝑌) ∧ (𝑋 · 𝑌) ≤ 1)) |
134 | 133 | simp3bi 1078 |
. . . . . . . . . 10
⊢ ((𝑋 · 𝑌) ∈ (0[,]1) → (𝑋 · 𝑌) ≤ 1) |
135 | 131, 134 | syl 17 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → (𝑋 · 𝑌) ≤ 1) |
136 | | elioc2 12236 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → ((𝑋 · 𝑌) ∈ (0(,]1) ↔ ((𝑋 · 𝑌) ∈ ℝ ∧ 0 < (𝑋 · 𝑌) ∧ (𝑋 · 𝑌) ≤ 1))) |
137 | 1, 2, 136 | mp2an 708 |
. . . . . . . . 9
⊢ ((𝑋 · 𝑌) ∈ (0(,]1) ↔ ((𝑋 · 𝑌) ∈ ℝ ∧ 0 < (𝑋 · 𝑌) ∧ (𝑋 · 𝑌) ≤ 1)) |
138 | 123, 126,
135, 137 | syl3anbrc 1246 |
. . . . . . . 8
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → (𝑋 · 𝑌) ∈ (0(,]1)) |
139 | 15 | xrge0iifcv 29980 |
. . . . . . . 8
⊢ ((𝑋 · 𝑌) ∈ (0(,]1) → (𝐹‘(𝑋 · 𝑌)) = -(log‘(𝑋 · 𝑌))) |
140 | 138, 139 | syl 17 |
. . . . . . 7
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘(𝑋 · 𝑌)) = -(log‘(𝑋 · 𝑌))) |
141 | 110, 114 | relogmuld 24371 |
. . . . . . . 8
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) →
(log‘(𝑋 ·
𝑌)) = ((log‘𝑋) + (log‘𝑌))) |
142 | 141 | negeqd 10275 |
. . . . . . 7
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) →
-(log‘(𝑋 ·
𝑌)) = -((log‘𝑋) + (log‘𝑌))) |
143 | 111 | recnd 10068 |
. . . . . . . 8
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) →
(log‘𝑋) ∈
ℂ) |
144 | 115 | recnd 10068 |
. . . . . . . 8
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) →
(log‘𝑌) ∈
ℂ) |
145 | 143, 144 | negdid 10405 |
. . . . . . 7
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) →
-((log‘𝑋) +
(log‘𝑌)) =
(-(log‘𝑋) +
-(log‘𝑌))) |
146 | 140, 142,
145 | 3eqtrd 2660 |
. . . . . 6
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘(𝑋 · 𝑌)) = (-(log‘𝑋) + -(log‘𝑌))) |
147 | 118, 120,
146 | 3eqtr4rd 2667 |
. . . . 5
⊢ ((𝑋 ∈ (0(,]1) ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌))) |
148 | 108, 147 | jaoian 824 |
. . . 4
⊢ (((𝑋 = 0 ∨ 𝑋 ∈ (0(,]1)) ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌))) |
149 | 72, 148 | sylan 488 |
. . 3
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0(,]1)) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌))) |
150 | 66, 149 | jaodan 826 |
. 2
⊢ ((𝑋 ∈ (0[,]1) ∧ (𝑌 = 0 ∨ 𝑌 ∈ (0(,]1))) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌))) |
151 | 12, 150 | sylan2 491 |
1
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌))) |