Step |
Hyp |
Ref |
Expression |
1 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
2 |
1
|
fveq2i |
⊢ ( θ ‘ 2 ) = ( θ ‘ ( 1 + 1 ) ) |
3 |
|
1z |
⊢ 1 ∈ ℤ |
4 |
|
2prm |
⊢ 2 ∈ ℙ |
5 |
1 4
|
eqeltrri |
⊢ ( 1 + 1 ) ∈ ℙ |
6 |
|
chtprm |
⊢ ( ( 1 ∈ ℤ ∧ ( 1 + 1 ) ∈ ℙ ) → ( θ ‘ ( 1 + 1 ) ) = ( ( θ ‘ 1 ) + ( log ‘ ( 1 + 1 ) ) ) ) |
7 |
3 5 6
|
mp2an |
⊢ ( θ ‘ ( 1 + 1 ) ) = ( ( θ ‘ 1 ) + ( log ‘ ( 1 + 1 ) ) ) |
8 |
|
cht1 |
⊢ ( θ ‘ 1 ) = 0 |
9 |
8
|
eqcomi |
⊢ 0 = ( θ ‘ 1 ) |
10 |
1
|
fveq2i |
⊢ ( log ‘ 2 ) = ( log ‘ ( 1 + 1 ) ) |
11 |
9 10
|
oveq12i |
⊢ ( 0 + ( log ‘ 2 ) ) = ( ( θ ‘ 1 ) + ( log ‘ ( 1 + 1 ) ) ) |
12 |
|
2rp |
⊢ 2 ∈ ℝ+ |
13 |
|
relogcl |
⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ ) |
14 |
12 13
|
ax-mp |
⊢ ( log ‘ 2 ) ∈ ℝ |
15 |
14
|
recni |
⊢ ( log ‘ 2 ) ∈ ℂ |
16 |
15
|
addid2i |
⊢ ( 0 + ( log ‘ 2 ) ) = ( log ‘ 2 ) |
17 |
11 16
|
eqtr3i |
⊢ ( ( θ ‘ 1 ) + ( log ‘ ( 1 + 1 ) ) ) = ( log ‘ 2 ) |
18 |
2 7 17
|
3eqtri |
⊢ ( θ ‘ 2 ) = ( log ‘ 2 ) |