Metamath Proof Explorer

Theorem xrge0iifhom

Description: The defined function from the closed unit interval to the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 5-Apr-2017)

Ref Expression
Hypotheses xrge0iifhmeo.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
xrge0iifhmeo.k ⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
Assertion xrge0iifhom ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
2 xrge0iifhmeo.k ⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
3 0xr ⊢ 0 ∈ ℝ*
4 1xr ⊢ 1 ∈ ℝ*
5 0le1 ⊢ 0 ≤ 1
6 snunioc ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1 ) → ( { 0 } ∪ ( 0 (,] 1 ) ) = ( 0 [,] 1 ) )
7 3 4 5 6 mp3an ⊢ ( { 0 } ∪ ( 0 (,] 1 ) ) = ( 0 [,] 1 )
8 7 eleq2i ⊢ ( 𝑌 ∈ ( { 0 } ∪ ( 0 (,] 1 ) ) ↔ 𝑌 ∈ ( 0 [,] 1 ) )
9 elun ⊢ ( 𝑌 ∈ ( { 0 } ∪ ( 0 (,] 1 ) ) ↔ ( 𝑌 ∈ { 0 } ∨ 𝑌 ∈ ( 0 (,] 1 ) ) )
10 8 9 bitr3i ⊢ ( 𝑌 ∈ ( 0 [,] 1 ) ↔ ( 𝑌 ∈ { 0 } ∨ 𝑌 ∈ ( 0 (,] 1 ) ) )
11 elsni ⊢ ( 𝑌 ∈ { 0 } → 𝑌 = 0 )
12 11 orim1i ⊢ ( ( 𝑌 ∈ { 0 } ∨ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝑌 = 0 ∨ 𝑌 ∈ ( 0 (,] 1 ) ) )
13 10 12 sylbi ⊢ ( 𝑌 ∈ ( 0 [,] 1 ) → ( 𝑌 = 0 ∨ 𝑌 ∈ ( 0 (,] 1 ) ) )
14 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
15 iftrue ⊢ ( 𝑥 = 0 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = +∞ )
16 pnfex ⊢ +∞ ∈ V
17 15 1 16 fvmpt ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 0 ) = +∞ )
18 14 17 ax-mp ⊢ ( 𝐹 ‘ 0 ) = +∞
19 18 oveq2i ⊢ ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 0 ) ) = ( ( 𝐹 ‘ 𝑋 ) +𝑒 +∞ )
20 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 0 ↔ 𝑋 = 0 ) )
21 fveq2 ⊢ ( 𝑥 = 𝑋 → ( log ‘ 𝑥 ) = ( log ‘ 𝑋 ) )
22 21 negeqd ⊢ ( 𝑥 = 𝑋 → - ( log ‘ 𝑥 ) = - ( log ‘ 𝑋 ) )
23 20 22 ifbieq2d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) )
24 negex ⊢ - ( log ‘ 𝑋 ) ∈ V
25 16 24 ifex ⊢ if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) ∈ V
26 23 1 25 fvmpt ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 𝑋 ) = if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) )
27 pnfxr ⊢ +∞ ∈ ℝ*
28 27 a1i ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑋 = 0 ) → +∞ ∈ ℝ* )
29 elunitrn ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → 𝑋 ∈ ℝ )
30 29 adantr ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 = 0 ) → 𝑋 ∈ ℝ )
31 elunitge0 ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → 0 ≤ 𝑋 )
32 31 adantr ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 = 0 ) → 0 ≤ 𝑋 )
33 simpr ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 = 0 ) → ¬ 𝑋 = 0 )
34 33 neqned ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 = 0 ) → 𝑋 ≠ 0 )
35 30 32 34 ne0gt0d ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 = 0 ) → 0 < 𝑋 )
36 30 35 elrpd ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 = 0 ) → 𝑋 ∈ ℝ+ )
37 36 relogcld ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 = 0 ) → ( log ‘ 𝑋 ) ∈ ℝ )
38 37 renegcld ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 = 0 ) → - ( log ‘ 𝑋 ) ∈ ℝ )
39 38 rexrd ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 = 0 ) → - ( log ‘ 𝑋 ) ∈ ℝ* )
40 28 39 ifclda ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) ∈ ℝ* )
41 26 40 eqeltrd ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 𝑋 ) ∈ ℝ* )
42 41 adantr ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( 𝐹 ‘ 𝑋 ) ∈ ℝ* )
43 neeq1 ⊢ ( +∞ = if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) → ( +∞ ≠ -∞ ↔ if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) ≠ -∞ ) )
44 neeq1 ⊢ ( - ( log ‘ 𝑋 ) = if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) → ( - ( log ‘ 𝑋 ) ≠ -∞ ↔ if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) ≠ -∞ ) )
45 pnfnemnf ⊢ +∞ ≠ -∞
46 45 a1i ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑋 = 0 ) → +∞ ≠ -∞ )
47 38 renemnfd ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑋 = 0 ) → - ( log ‘ 𝑋 ) ≠ -∞ )
48 43 44 46 47 ifbothda ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) ≠ -∞ )
49 26 48 eqnetrd ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 𝑋 ) ≠ -∞ )
50 49 adantr ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( 𝐹 ‘ 𝑋 ) ≠ -∞ )
51 xaddpnf1 ⊢ ( ( ( 𝐹 ‘ 𝑋 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑋 ) ≠ -∞ ) → ( ( 𝐹 ‘ 𝑋 ) +𝑒 +∞ ) = +∞ )
52 42 50 51 syl2anc ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( ( 𝐹 ‘ 𝑋 ) +𝑒 +∞ ) = +∞ )
53 19 52 eqtrid ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 0 ) ) = +∞ )
54 unitsscn ⊢ ( 0 [,] 1 ) ⊆ ℂ
55 simpl ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → 𝑋 ∈ ( 0 [,] 1 ) )
56 54 55 sselid ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → 𝑋 ∈ ℂ )
57 56 mul01d ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( 𝑋 · 0 ) = 0 )
58 57 fveq2d ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( 𝐹 ‘ ( 𝑋 · 0 ) ) = ( 𝐹 ‘ 0 ) )
59 58 18 eqtrdi ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( 𝐹 ‘ ( 𝑋 · 0 ) ) = +∞ )
60 53 59 eqtr4d ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 0 ) ) = ( 𝐹 ‘ ( 𝑋 · 0 ) ) )
61 simpr ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → 𝑌 = 0 )
62 61 fveq2d ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 0 ) )
63 62 oveq2d ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 0 ) ) )
64 61 oveq2d ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 · 0 ) )
65 64 fveq2d ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 0 ) ) )
66 60 63 65 3eqtr4rd ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 = 0 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) )
67 7 eleq2i ⊢ ( 𝑋 ∈ ( { 0 } ∪ ( 0 (,] 1 ) ) ↔ 𝑋 ∈ ( 0 [,] 1 ) )
68 elun ⊢ ( 𝑋 ∈ ( { 0 } ∪ ( 0 (,] 1 ) ) ↔ ( 𝑋 ∈ { 0 } ∨ 𝑋 ∈ ( 0 (,] 1 ) ) )
69 67 68 bitr3i ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) ↔ ( 𝑋 ∈ { 0 } ∨ 𝑋 ∈ ( 0 (,] 1 ) ) )
70 elsni ⊢ ( 𝑋 ∈ { 0 } → 𝑋 = 0 )
71 70 orim1i ⊢ ( ( 𝑋 ∈ { 0 } ∨ 𝑋 ∈ ( 0 (,] 1 ) ) → ( 𝑋 = 0 ∨ 𝑋 ∈ ( 0 (,] 1 ) ) )
72 69 71 sylbi ⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → ( 𝑋 = 0 ∨ 𝑋 ∈ ( 0 (,] 1 ) ) )
73 18 oveq1i ⊢ ( ( 𝐹 ‘ 0 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) = ( +∞ +𝑒 ( 𝐹 ‘ 𝑌 ) )
74 simpr ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑌 ∈ ( 0 (,] 1 ) )
75 1 xrge0iifcv ⊢ ( 𝑌 ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ 𝑌 ) = - ( log ‘ 𝑌 ) )
76 0le0 ⊢ 0 ≤ 0
77 1re ⊢ 1 ∈ ℝ
78 ltpnf ⊢ ( 1 ∈ ℝ → 1 < +∞ )
79 77 78 ax-mp ⊢ 1 < +∞
80 iocssioo ⊢ ( ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 0 ≤ 0 ∧ 1 < +∞ ) ) → ( 0 (,] 1 ) ⊆ ( 0 (,) +∞ ) )
81 3 27 76 79 80 mp4an ⊢ ( 0 (,] 1 ) ⊆ ( 0 (,) +∞ )
82 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
83 81 82 sseqtri ⊢ ( 0 (,] 1 ) ⊆ ℝ+
84 83 sseli ⊢ ( 𝑌 ∈ ( 0 (,] 1 ) → 𝑌 ∈ ℝ+ )
85 84 relogcld ⊢ ( 𝑌 ∈ ( 0 (,] 1 ) → ( log ‘ 𝑌 ) ∈ ℝ )
86 85 renegcld ⊢ ( 𝑌 ∈ ( 0 (,] 1 ) → - ( log ‘ 𝑌 ) ∈ ℝ )
87 75 86 eqeltrd ⊢ ( 𝑌 ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ 𝑌 ) ∈ ℝ )
88 87 rexrd ⊢ ( 𝑌 ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ 𝑌 ) ∈ ℝ* )
89 74 88 syl ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ ℝ* )
90 87 renemnfd ⊢ ( 𝑌 ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ 𝑌 ) ≠ -∞ )
91 74 90 syl ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ 𝑌 ) ≠ -∞ )
92 xaddpnf2 ⊢ ( ( ( 𝐹 ‘ 𝑌 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑌 ) ≠ -∞ ) → ( +∞ +𝑒 ( 𝐹 ‘ 𝑌 ) ) = +∞ )
93 89 91 92 syl2anc ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( +∞ +𝑒 ( 𝐹 ‘ 𝑌 ) ) = +∞ )
94 73 93 eqtrid ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( ( 𝐹 ‘ 0 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) = +∞ )
95 rpssre ⊢ ℝ+ ⊆ ℝ
96 83 95 sstri ⊢ ( 0 (,] 1 ) ⊆ ℝ
97 ax-resscn ⊢ ℝ ⊆ ℂ
98 96 97 sstri ⊢ ( 0 (,] 1 ) ⊆ ℂ
99 98 74 sselid ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑌 ∈ ℂ )
100 99 mul02d ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 0 · 𝑌 ) = 0 )
101 100 fveq2d ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ ( 0 · 𝑌 ) ) = ( 𝐹 ‘ 0 ) )
102 101 18 eqtrdi ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ ( 0 · 𝑌 ) ) = +∞ )
103 94 102 eqtr4d ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( ( 𝐹 ‘ 0 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 0 · 𝑌 ) ) )
104 simpl ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑋 = 0 )
105 104 fveq2d ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 0 ) )
106 105 oveq1d ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) = ( ( 𝐹 ‘ 0 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) )
107 104 fvoveq1d ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( 𝐹 ‘ ( 0 · 𝑌 ) ) )
108 103 106 107 3eqtr4rd ⊢ ( ( 𝑋 = 0 ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) )
109 simpl ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑋 ∈ ( 0 (,] 1 ) )
110 83 109 sselid ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑋 ∈ ℝ+ )
111 110 relogcld ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( log ‘ 𝑋 ) ∈ ℝ )
112 111 renegcld ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → - ( log ‘ 𝑋 ) ∈ ℝ )
113 simpr ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑌 ∈ ( 0 (,] 1 ) )
114 83 113 sselid ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑌 ∈ ℝ+ )
115 114 relogcld ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( log ‘ 𝑌 ) ∈ ℝ )
116 115 renegcld ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → - ( log ‘ 𝑌 ) ∈ ℝ )
117 rexadd ⊢ ( ( - ( log ‘ 𝑋 ) ∈ ℝ ∧ - ( log ‘ 𝑌 ) ∈ ℝ ) → ( - ( log ‘ 𝑋 ) +𝑒 - ( log ‘ 𝑌 ) ) = ( - ( log ‘ 𝑋 ) + - ( log ‘ 𝑌 ) ) )
118 112 116 117 syl2anc ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( - ( log ‘ 𝑋 ) +𝑒 - ( log ‘ 𝑌 ) ) = ( - ( log ‘ 𝑋 ) + - ( log ‘ 𝑌 ) ) )
119 1 xrge0iifcv ⊢ ( 𝑋 ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ 𝑋 ) = - ( log ‘ 𝑋 ) )
120 119 75 oveqan12d ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) = ( - ( log ‘ 𝑋 ) +𝑒 - ( log ‘ 𝑌 ) ) )
121 110 rpred ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑋 ∈ ℝ )
122 114 rpred ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑌 ∈ ℝ )
123 121 122 remulcld ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝑋 · 𝑌 ) ∈ ℝ )
124 110 rpgt0d ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 0 < 𝑋 )
125 114 rpgt0d ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 0 < 𝑌 )
126 121 122 124 125 mulgt0d ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 0 < ( 𝑋 · 𝑌 ) )
127 iocssicc ⊢ ( 0 (,] 1 ) ⊆ ( 0 [,] 1 )
128 127 109 sselid ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑋 ∈ ( 0 [,] 1 ) )
129 127 113 sselid ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → 𝑌 ∈ ( 0 [,] 1 ) )
130 iimulcl ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 ∈ ( 0 [,] 1 ) ) → ( 𝑋 · 𝑌 ) ∈ ( 0 [,] 1 ) )
131 128 129 130 syl2anc ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝑋 · 𝑌 ) ∈ ( 0 [,] 1 ) )
132 elicc01 ⊢ ( ( 𝑋 · 𝑌 ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝑋 · 𝑌 ) ∈ ℝ ∧ 0 ≤ ( 𝑋 · 𝑌 ) ∧ ( 𝑋 · 𝑌 ) ≤ 1 ) )
133 132 simp3bi ⊢ ( ( 𝑋 · 𝑌 ) ∈ ( 0 [,] 1 ) → ( 𝑋 · 𝑌 ) ≤ 1 )
134 131 133 syl ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝑋 · 𝑌 ) ≤ 1 )
135 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( ( 𝑋 · 𝑌 ) ∈ ( 0 (,] 1 ) ↔ ( ( 𝑋 · 𝑌 ) ∈ ℝ ∧ 0 < ( 𝑋 · 𝑌 ) ∧ ( 𝑋 · 𝑌 ) ≤ 1 ) ) )
136 3 77 135 mp2an ⊢ ( ( 𝑋 · 𝑌 ) ∈ ( 0 (,] 1 ) ↔ ( ( 𝑋 · 𝑌 ) ∈ ℝ ∧ 0 < ( 𝑋 · 𝑌 ) ∧ ( 𝑋 · 𝑌 ) ≤ 1 ) )
137 123 126 134 136 syl3anbrc ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝑋 · 𝑌 ) ∈ ( 0 (,] 1 ) )
138 1 xrge0iifcv ⊢ ( ( 𝑋 · 𝑌 ) ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = - ( log ‘ ( 𝑋 · 𝑌 ) ) )
139 137 138 syl ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = - ( log ‘ ( 𝑋 · 𝑌 ) ) )
140 110 114 relogmuld ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( log ‘ ( 𝑋 · 𝑌 ) ) = ( ( log ‘ 𝑋 ) + ( log ‘ 𝑌 ) ) )
141 140 negeqd ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → - ( log ‘ ( 𝑋 · 𝑌 ) ) = - ( ( log ‘ 𝑋 ) + ( log ‘ 𝑌 ) ) )
142 111 recnd ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( log ‘ 𝑋 ) ∈ ℂ )
143 115 recnd ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( log ‘ 𝑌 ) ∈ ℂ )
144 142 143 negdid ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → - ( ( log ‘ 𝑋 ) + ( log ‘ 𝑌 ) ) = ( - ( log ‘ 𝑋 ) + - ( log ‘ 𝑌 ) ) )
145 139 141 144 3eqtrd ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( - ( log ‘ 𝑋 ) + - ( log ‘ 𝑌 ) ) )
146 118 120 145 3eqtr4rd ⊢ ( ( 𝑋 ∈ ( 0 (,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) )
147 108 146 jaoian ⊢ ( ( ( 𝑋 = 0 ∨ 𝑋 ∈ ( 0 (,] 1 ) ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) )
148 72 147 sylan ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) )
149 66 148 jaodan ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ ( 𝑌 = 0 ∨ 𝑌 ∈ ( 0 (,] 1 ) ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) )
150 13 149 sylan2 ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) +𝑒 ( 𝐹 ‘ 𝑌 ) ) )