| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ioorp 13466 | . . . 4
⊢
(0(,)+∞) = ℝ+ | 
| 2 | 1 | eqcomi 2745 | . . 3
⊢
ℝ+ = (0(,)+∞) | 
| 3 |  | logdivsqrle.a | . . 3
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 4 |  | logdivsqrle.b | . . 3
⊢ (𝜑 → 𝐵 ∈
ℝ+) | 
| 5 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) | 
| 6 | 5 | relogcld 26666 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) | 
| 7 | 5 | rpsqrtcld 15451 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ+) | 
| 8 | 7 | rpred 13078 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ) | 
| 9 |  | rpsqrtcl 15304 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (√‘𝑥)
∈ ℝ+) | 
| 10 |  | rpne0 13052 | . . . . . . 7
⊢
((√‘𝑥)
∈ ℝ+ → (√‘𝑥) ≠ 0) | 
| 11 | 9, 10 | syl 17 | . . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (√‘𝑥)
≠ 0) | 
| 12 | 11 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ≠
0) | 
| 13 | 6, 8, 12 | redivcld 12096 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) /
(√‘𝑥)) ∈
ℝ) | 
| 14 | 13 | fmpttd 7134 | . . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((log‘𝑥) /
(√‘𝑥))):ℝ+⟶ℝ) | 
| 15 |  | rpcn 13046 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) | 
| 16 | 15 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) | 
| 17 |  | rpne0 13052 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) | 
| 18 | 17 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) | 
| 19 | 16, 18 | logcld 26613 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) | 
| 20 | 16 | sqrtcld 15477 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℂ) | 
| 21 | 19, 20, 12 | divrecd 12047 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) /
(√‘𝑥)) =
((log‘𝑥) · (1
/ (√‘𝑥)))) | 
| 22 |  | 2cnd 12345 | . . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℂ) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈
ℂ) | 
| 24 |  | 2ne0 12371 | . . . . . . . . . . . . 13
⊢ 2 ≠
0 | 
| 25 | 24 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ≠
0) | 
| 26 | 23, 25 | reccld 12037 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 / 2)
∈ ℂ) | 
| 27 | 16, 18, 26 | cxpnegd 26758 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐-(1 /
2)) = (1 / (𝑥↑𝑐(1 /
2)))) | 
| 28 |  | cxpsqrt 26746 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (𝑥↑𝑐(1 /
2)) = (√‘𝑥)) | 
| 29 | 16, 28 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐(1 /
2)) = (√‘𝑥)) | 
| 30 | 29 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥↑𝑐(1 / 2))) = (1 /
(√‘𝑥))) | 
| 31 | 27, 30 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐-(1 /
2)) = (1 / (√‘𝑥))) | 
| 32 | 31 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
(𝑥↑𝑐-(1 / 2))) =
((log‘𝑥) · (1
/ (√‘𝑥)))) | 
| 33 | 21, 32 | eqtr4d 2779 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) /
(√‘𝑥)) =
((log‘𝑥) ·
(𝑥↑𝑐-(1 /
2)))) | 
| 34 | 33 | mpteq2dva 5241 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((log‘𝑥) /
(√‘𝑥))) =
(𝑥 ∈
ℝ+ ↦ ((log‘𝑥) · (𝑥↑𝑐-(1 /
2))))) | 
| 35 | 34 | oveq2d 7448 | . . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ+
↦ ((log‘𝑥) /
(√‘𝑥)))) =
(ℝ D (𝑥 ∈
ℝ+ ↦ ((log‘𝑥) · (𝑥↑𝑐-(1 /
2)))))) | 
| 36 |  | reelprrecn 11248 | . . . . . . 7
⊢ ℝ
∈ {ℝ, ℂ} | 
| 37 | 36 | a1i 11 | . . . . . 6
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) | 
| 38 | 5 | rpreccld 13088 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ+) | 
| 39 |  | logf1o 26607 | . . . . . . . . . . 11
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log | 
| 40 |  | f1of 6847 | . . . . . . . . . . 11
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) | 
| 41 | 39, 40 | ax-mp 5 | . . . . . . . . . 10
⊢
log:(ℂ ∖ {0})⟶ran log | 
| 42 | 41 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → log:(ℂ ∖
{0})⟶ran log) | 
| 43 | 15 | ssriv 3986 | . . . . . . . . . . 11
⊢
ℝ+ ⊆ ℂ | 
| 44 |  | 0nrp 13071 | . . . . . . . . . . 11
⊢  ¬ 0
∈ ℝ+ | 
| 45 |  | ssdifsn 4787 | . . . . . . . . . . 11
⊢
(ℝ+ ⊆ (ℂ ∖ {0}) ↔
(ℝ+ ⊆ ℂ ∧ ¬ 0 ∈
ℝ+)) | 
| 46 | 43, 44, 45 | mpbir2an 711 | . . . . . . . . . 10
⊢
ℝ+ ⊆ (ℂ ∖ {0}) | 
| 47 | 46 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ℝ+
⊆ (ℂ ∖ {0})) | 
| 48 | 42, 47 | feqresmpt 6977 | . . . . . . . 8
⊢ (𝜑 → (log ↾
ℝ+) = (𝑥
∈ ℝ+ ↦ (log‘𝑥))) | 
| 49 | 48 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → (ℝ D (log ↾
ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥)))) | 
| 50 |  | dvrelog 26680 | . . . . . . 7
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) | 
| 51 | 49, 50 | eqtr3di 2791 | . . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ+
↦ (log‘𝑥))) =
(𝑥 ∈
ℝ+ ↦ (1 / 𝑥))) | 
| 52 |  | 1cnd 11257 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) | 
| 53 | 52 | halfcld 12513 | . . . . . . . . 9
⊢ (𝜑 → (1 / 2) ∈
ℂ) | 
| 54 | 53 | negcld 11608 | . . . . . . . 8
⊢ (𝜑 → -(1 / 2) ∈
ℂ) | 
| 55 | 54 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → -(1 / 2)
∈ ℂ) | 
| 56 | 16, 55 | cxpcld 26751 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐-(1 /
2)) ∈ ℂ) | 
| 57 | 52 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) | 
| 58 | 55, 57 | subcld 11621 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (-(1 / 2)
− 1) ∈ ℂ) | 
| 59 | 16, 58 | cxpcld 26751 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐(-(1 /
2) − 1)) ∈ ℂ) | 
| 60 | 55, 59 | mulcld 11282 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (-(1 / 2)
· (𝑥↑𝑐(-(1 / 2) −
1))) ∈ ℂ) | 
| 61 |  | dvcxp1 26783 | . . . . . . 7
⊢ (-(1 / 2)
∈ ℂ → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥↑𝑐-(1 /
2)))) = (𝑥 ∈
ℝ+ ↦ (-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))))) | 
| 62 | 54, 61 | syl 17 | . . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ+
↦ (𝑥↑𝑐-(1 / 2)))) =
(𝑥 ∈
ℝ+ ↦ (-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))))) | 
| 63 | 37, 19, 38, 51, 56, 60, 62 | dvmptmul 26000 | . . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ+
↦ ((log‘𝑥)
· (𝑥↑𝑐-(1 / 2))))) =
(𝑥 ∈
ℝ+ ↦ (((1 / 𝑥) · (𝑥↑𝑐-(1 / 2))) + ((-(1
/ 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))))) | 
| 64 | 35, 63 | eqtrd 2776 | . . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ+
↦ ((log‘𝑥) /
(√‘𝑥)))) =
(𝑥 ∈
ℝ+ ↦ (((1 / 𝑥) · (𝑥↑𝑐-(1 / 2))) + ((-(1
/ 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))))) | 
| 65 |  | ax-resscn 11213 | . . . . . 6
⊢ ℝ
⊆ ℂ | 
| 66 | 65 | a1i 11 | . . . . 5
⊢ (𝜑 → ℝ ⊆
ℂ) | 
| 67 |  | eqid 2736 | . . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 68 | 67 | addcn 24888 | . . . . . . 7
⊢  + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) | 
| 69 | 68 | a1i 11 | . . . . . 6
⊢ (𝜑 → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) | 
| 70 | 43 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ℝ+
⊆ ℂ) | 
| 71 |  | ssid 4005 | . . . . . . . . . 10
⊢ ℂ
⊆ ℂ | 
| 72 | 71 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 73 |  | cncfmptc 24939 | . . . . . . . . 9
⊢ ((1
∈ ℂ ∧ ℝ+ ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑥 ∈
ℝ+ ↦ 1) ∈ (ℝ+–cn→ℂ)) | 
| 74 | 52, 70, 72, 73 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 1) ∈
(ℝ+–cn→ℂ)) | 
| 75 |  | difss 4135 | . . . . . . . . 9
⊢ (ℂ
∖ {0}) ⊆ ℂ | 
| 76 |  | cncfmptid 24940 | . . . . . . . . 9
⊢
((ℝ+ ⊆ (ℂ ∖ {0}) ∧ (ℂ
∖ {0}) ⊆ ℂ) → (𝑥 ∈ ℝ+ ↦ 𝑥) ∈
(ℝ+–cn→(ℂ ∖ {0}))) | 
| 77 | 47, 75, 76 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 𝑥) ∈
(ℝ+–cn→(ℂ ∖ {0}))) | 
| 78 | 74, 77 | divcncf 25483 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) ∈
(ℝ+–cn→ℂ)) | 
| 79 |  | ax-1 6 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
→ 𝑥 ∈
ℝ+)) | 
| 80 | 15, 79 | jca 511 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ (𝑥 ∈ ℝ
→ 𝑥 ∈
ℝ+))) | 
| 81 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) | 
| 82 | 81 | ellogdm 26682 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (ℂ ∖
(-∞(,]0)) ↔ (𝑥
∈ ℂ ∧ (𝑥
∈ ℝ → 𝑥
∈ ℝ+))) | 
| 83 | 80, 82 | sylibr 234 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈ (ℂ
∖ (-∞(,]0))) | 
| 84 | 83 | ssriv 3986 | . . . . . . . . 9
⊢
ℝ+ ⊆ (ℂ ∖
(-∞(,]0)) | 
| 85 | 84 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → ℝ+
⊆ (ℂ ∖ (-∞(,]0))) | 
| 86 | 54, 85 | cxpcncf1 34611 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑥↑𝑐-(1 /
2))) ∈ (ℝ+–cn→ℂ)) | 
| 87 | 78, 86 | mulcncf 25481 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((1 /
𝑥) · (𝑥↑𝑐-(1 /
2)))) ∈ (ℝ+–cn→ℂ)) | 
| 88 |  | cncfmptc 24939 | . . . . . . . . 9
⊢ ((-(1 /
2) ∈ ℂ ∧ ℝ+ ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝑥
∈ ℝ+ ↦ -(1 / 2)) ∈
(ℝ+–cn→ℂ)) | 
| 89 | 54, 70, 72, 88 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ -(1 / 2))
∈ (ℝ+–cn→ℂ)) | 
| 90 | 54, 52 | subcld 11621 | . . . . . . . . 9
⊢ (𝜑 → (-(1 / 2) − 1)
∈ ℂ) | 
| 91 | 90, 85 | cxpcncf1 34611 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑥↑𝑐(-(1 /
2) − 1))) ∈ (ℝ+–cn→ℂ)) | 
| 92 | 89, 91 | mulcncf 25481 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (-(1 / 2)
· (𝑥↑𝑐(-(1 / 2) −
1)))) ∈ (ℝ+–cn→ℂ)) | 
| 93 |  | cncfss 24926 | . . . . . . . . 9
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) →
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ)) | 
| 94 | 65, 71, 93 | mp2an 692 | . . . . . . . 8
⊢
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ) | 
| 95 |  | relogcn 26681 | . . . . . . . . 9
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℝ) | 
| 96 | 48, 95 | eqeltrrdi 2849 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) ∈
(ℝ+–cn→ℝ)) | 
| 97 | 94, 96 | sselid 3980 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) ∈
(ℝ+–cn→ℂ)) | 
| 98 | 92, 97 | mulcncf 25481 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((-(1 /
2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))) ∈ (ℝ+–cn→ℂ)) | 
| 99 | 67, 69, 87, 98 | cncfmpt2f 24942 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)))) ∈ (ℝ+–cn→ℂ)) | 
| 100 |  | rpre 13044 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) | 
| 101 | 100, 17 | rereccld 12095 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ) | 
| 102 |  | rpge0 13049 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ 𝑥) | 
| 103 |  | halfre 12481 | . . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ | 
| 104 | 103 | renegcli 11571 | . . . . . . . . . . 11
⊢ -(1 / 2)
∈ ℝ | 
| 105 | 104 | a1i 11 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ -(1 / 2) ∈ ℝ) | 
| 106 | 100, 102,
105 | recxpcld 26766 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝑥↑𝑐-(1 / 2)) ∈
ℝ) | 
| 107 | 101, 106 | remulcld 11292 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((1 / 𝑥) ·
(𝑥↑𝑐-(1 / 2))) ∈
ℝ) | 
| 108 |  | 1re 11262 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℝ | 
| 109 | 104, 108 | resubcli 11572 | . . . . . . . . . . . 12
⊢ (-(1 / 2)
− 1) ∈ ℝ | 
| 110 | 109 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (-(1 / 2) − 1) ∈ ℝ) | 
| 111 | 100, 102,
110 | recxpcld 26766 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥↑𝑐(-(1 / 2) −
1)) ∈ ℝ) | 
| 112 | 105, 111 | remulcld 11292 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) ∈ ℝ) | 
| 113 |  | relogcl 26618 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) | 
| 114 | 112, 113 | remulcld 11292 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)) ∈ ℝ) | 
| 115 | 107, 114 | readdcld 11291 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((1 / 𝑥) ·
(𝑥↑𝑐-(1 / 2))) + ((-(1
/ 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))) ∈ ℝ) | 
| 116 | 115 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))) ∈ ℝ) | 
| 117 | 116 | fmpttd 7134 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)))):ℝ+⟶ℝ) | 
| 118 |  | cncfcdm 24925 | . . . . . 6
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ ℝ+ ↦ (((1 / 𝑥) · (𝑥↑𝑐-(1 / 2))) + ((-(1
/ 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)))) ∈ (ℝ+–cn→ℂ)) → ((𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)))) ∈ (ℝ+–cn→ℝ) ↔ (𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)))):ℝ+⟶ℝ)) | 
| 119 | 118 | biimpar 477 | . . . . 5
⊢
(((ℝ ⊆ ℂ ∧ (𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)))) ∈ (ℝ+–cn→ℂ)) ∧ (𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)))):ℝ+⟶ℝ)
→ (𝑥 ∈
ℝ+ ↦ (((1 / 𝑥) · (𝑥↑𝑐-(1 / 2))) + ((-(1
/ 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)))) ∈ (ℝ+–cn→ℝ)) | 
| 120 | 66, 99, 117, 119 | syl21anc 837 | . . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)))) ∈ (ℝ+–cn→ℝ)) | 
| 121 | 64, 120 | eqeltrd 2840 | . . 3
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ+
↦ ((log‘𝑥) /
(√‘𝑥)))) ∈
(ℝ+–cn→ℝ)) | 
| 122 |  | logdivsqrle.2 | . . 3
⊢ (𝜑 → 𝐴 ≤ 𝐵) | 
| 123 | 64 | fveq1d 6907 | . . . . 5
⊢ (𝜑 → ((ℝ D (𝑥 ∈ ℝ+
↦ ((log‘𝑥) /
(√‘𝑥))))‘𝑦) = ((𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))))‘𝑦)) | 
| 124 | 123 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑥 ∈ ℝ+ ↦
((log‘𝑥) /
(√‘𝑥))))‘𝑦) = ((𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))))‘𝑦)) | 
| 125 | 57 | negcld 11608 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → -1 ∈
ℂ) | 
| 126 |  | cxpadd 26722 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ -(1 / 2) ∈
ℂ ∧ -1 ∈ ℂ) → (𝑥↑𝑐(-(1 / 2) + -1)) =
((𝑥↑𝑐-(1 / 2)) ·
(𝑥↑𝑐-1))) | 
| 127 | 16, 18, 55, 125, 126 | syl211anc 1377 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐(-(1 /
2) + -1)) = ((𝑥↑𝑐-(1 / 2)) ·
(𝑥↑𝑐-1))) | 
| 128 | 59 | mullidd 11280 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1
· (𝑥↑𝑐(-(1 / 2) −
1))) = (𝑥↑𝑐(-(1 / 2) −
1))) | 
| 129 | 55, 57 | negsubd 11627 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (-(1 / 2)
+ -1) = (-(1 / 2) − 1)) | 
| 130 | 129 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐(-(1 /
2) + -1)) = (𝑥↑𝑐(-(1 / 2) −
1))) | 
| 131 | 128, 130 | eqtr4d 2779 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1
· (𝑥↑𝑐(-(1 / 2) −
1))) = (𝑥↑𝑐(-(1 / 2) +
-1))) | 
| 132 | 43, 38 | sselid 3980 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℂ) | 
| 133 | 132, 56 | mulcomd 11283 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) = ((𝑥↑𝑐-(1 / 2)) ·
(1 / 𝑥))) | 
| 134 |  | cxpneg 26724 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ∧ 1 ∈ ℂ)
→ (𝑥↑𝑐-1) = (1 / (𝑥↑𝑐1))) | 
| 135 | 16, 18, 57, 134 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐-1) =
(1 / (𝑥↑𝑐1))) | 
| 136 | 16 | cxp1d 26749 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐1) =
𝑥) | 
| 137 | 136 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥↑𝑐1)) = (1 / 𝑥)) | 
| 138 | 135, 137 | eqtr2d 2777 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) = (𝑥↑𝑐-1)) | 
| 139 | 138 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝑥↑𝑐-(1 /
2)) · (1 / 𝑥)) =
((𝑥↑𝑐-(1 / 2)) ·
(𝑥↑𝑐-1))) | 
| 140 | 133, 139 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) = ((𝑥↑𝑐-(1 / 2)) ·
(𝑥↑𝑐-1))) | 
| 141 | 127, 131,
140 | 3eqtr4rd 2787 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) = (1 · (𝑥↑𝑐(-(1 / 2) −
1)))) | 
| 142 | 55, 59, 19 | mul32d 11472 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((-(1 /
2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)) = ((-(1 / 2) · (log‘𝑥)) · (𝑥↑𝑐(-(1 / 2) −
1)))) | 
| 143 | 141, 142 | oveq12d 7450 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))) = ((1 · (𝑥↑𝑐(-(1 / 2) −
1))) + ((-(1 / 2) · (log‘𝑥)) · (𝑥↑𝑐(-(1 / 2) −
1))))) | 
| 144 | 55, 19 | mulcld 11282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (-(1 / 2)
· (log‘𝑥))
∈ ℂ) | 
| 145 | 57, 144, 59 | adddird 11287 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((1 +
(-(1 / 2) · (log‘𝑥))) · (𝑥↑𝑐(-(1 / 2) −
1))) = ((1 · (𝑥↑𝑐(-(1 / 2) −
1))) + ((-(1 / 2) · (log‘𝑥)) · (𝑥↑𝑐(-(1 / 2) −
1))))) | 
| 146 | 143, 145 | eqtr4d 2779 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))) = ((1 + (-(1 / 2) ·
(log‘𝑥))) ·
(𝑥↑𝑐(-(1 / 2) −
1)))) | 
| 147 | 146 | mpteq2dva 5241 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ ((1 +
(-(1 / 2) · (log‘𝑥))) · (𝑥↑𝑐(-(1 / 2) −
1))))) | 
| 148 | 147 | fveq1d 6907 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))))‘𝑦) = ((𝑥 ∈ ℝ+ ↦ ((1 +
(-(1 / 2) · (log‘𝑥))) · (𝑥↑𝑐(-(1 / 2) −
1))))‘𝑦)) | 
| 149 | 148 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))))‘𝑦) = ((𝑥 ∈ ℝ+ ↦ ((1 +
(-(1 / 2) · (log‘𝑥))) · (𝑥↑𝑐(-(1 / 2) −
1))))‘𝑦)) | 
| 150 |  | eqidd 2737 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ ℝ+ ↦ ((1 +
(-(1 / 2) · (log‘𝑥))) · (𝑥↑𝑐(-(1 / 2) −
1)))) = (𝑥 ∈
ℝ+ ↦ ((1 + (-(1 / 2) · (log‘𝑥))) · (𝑥↑𝑐(-(1 / 2) −
1))))) | 
| 151 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦) | 
| 152 | 151 | fveq2d 6909 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑦) → (log‘𝑥) = (log‘𝑦)) | 
| 153 | 152 | oveq2d 7448 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑦) → (-(1 / 2) · (log‘𝑥)) = (-(1 / 2) ·
(log‘𝑦))) | 
| 154 | 153 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑦) → (1 + (-(1 / 2) ·
(log‘𝑥))) = (1 + (-(1
/ 2) · (log‘𝑦)))) | 
| 155 | 151 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑦) → (𝑥↑𝑐(-(1 / 2) −
1)) = (𝑦↑𝑐(-(1 / 2) −
1))) | 
| 156 | 154, 155 | oveq12d 7450 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑦) → ((1 + (-(1 / 2) ·
(log‘𝑥))) ·
(𝑥↑𝑐(-(1 / 2) −
1))) = ((1 + (-(1 / 2) · (log‘𝑦))) · (𝑦↑𝑐(-(1 / 2) −
1)))) | 
| 157 |  | ioossicc 13474 | . . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) | 
| 158 | 157 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) | 
| 159 | 2, 3, 4 | fct2relem 34613 | . . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆
ℝ+) | 
| 160 | 158, 159 | sstrd 3993 | . . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ⊆
ℝ+) | 
| 161 | 160 | sselda 3982 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ+) | 
| 162 |  | ovexd 7467 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((1 + (-(1 / 2) ·
(log‘𝑦))) ·
(𝑦↑𝑐(-(1 / 2) −
1))) ∈ V) | 
| 163 | 150, 156,
161, 162 | fvmptd 7022 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ ℝ+ ↦ ((1 +
(-(1 / 2) · (log‘𝑥))) · (𝑥↑𝑐(-(1 / 2) −
1))))‘𝑦) = ((1 + (-(1
/ 2) · (log‘𝑦))) · (𝑦↑𝑐(-(1 / 2) −
1)))) | 
| 164 | 108 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ) | 
| 165 | 104 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → -(1 / 2) ∈
ℝ) | 
| 166 | 161 | relogcld 26666 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (log‘𝑦) ∈ ℝ) | 
| 167 | 165, 166 | remulcld 11292 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (-(1 / 2) ·
(log‘𝑦)) ∈
ℝ) | 
| 168 | 164, 167 | readdcld 11291 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (1 + (-(1 / 2) ·
(log‘𝑦))) ∈
ℝ) | 
| 169 |  | 0red 11265 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) | 
| 170 |  | rpcxpcl 26719 | . . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ+
∧ (-(1 / 2) − 1) ∈ ℝ) → (𝑦↑𝑐(-(1 / 2) −
1)) ∈ ℝ+) | 
| 171 | 161, 109,
170 | sylancl 586 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝑦↑𝑐(-(1 / 2) −
1)) ∈ ℝ+) | 
| 172 | 171 | rpred 13078 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝑦↑𝑐(-(1 / 2) −
1)) ∈ ℝ) | 
| 173 | 171 | rpge0d 13082 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 0 ≤ (𝑦↑𝑐(-(1 / 2) −
1))) | 
| 174 |  | 2cn 12342 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ | 
| 175 | 174 | mullidi 11267 | . . . . . . . . . . . . 13
⊢ (1
· 2) = 2 | 
| 176 |  | 2re 12341 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ | 
| 177 | 176 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ) | 
| 178 | 177 | reefcld 16125 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (exp‘2) ∈
ℝ) | 
| 179 | 3 | rpred 13078 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 180 | 179 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) | 
| 181 | 161 | rpred 13078 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ) | 
| 182 |  | logdivsqrle.1 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (exp‘2) ≤ 𝐴) | 
| 183 | 182 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (exp‘2) ≤ 𝐴) | 
| 184 |  | eliooord 13447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑦 ∧ 𝑦 < 𝐵)) | 
| 185 | 184 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (𝐴(,)𝐵) → 𝐴 < 𝑦) | 
| 186 | 185 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑦) | 
| 187 | 180, 181,
186 | ltled 11410 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐴 ≤ 𝑦) | 
| 188 | 178, 180,
181, 183, 187 | letrd 11419 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (exp‘2) ≤ 𝑦) | 
| 189 |  | reeflog 26623 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ (exp‘(log‘𝑦)) = 𝑦) | 
| 190 | 161, 189 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (exp‘(log‘𝑦)) = 𝑦) | 
| 191 | 188, 190 | breqtrrd 5170 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (exp‘2) ≤
(exp‘(log‘𝑦))) | 
| 192 |  | efle 16155 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ ℝ ∧ (log‘𝑦) ∈ ℝ) → (2 ≤
(log‘𝑦) ↔
(exp‘2) ≤ (exp‘(log‘𝑦)))) | 
| 193 | 176, 166,
192 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (2 ≤ (log‘𝑦) ↔ (exp‘2) ≤
(exp‘(log‘𝑦)))) | 
| 194 | 191, 193 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 2 ≤ (log‘𝑦)) | 
| 195 | 175, 194 | eqbrtrid 5177 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (1 · 2) ≤
(log‘𝑦)) | 
| 196 |  | 2rp 13040 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ+ | 
| 197 | 196 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 2 ∈
ℝ+) | 
| 198 | 164, 166,
197 | lemuldivd 13127 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((1 · 2) ≤
(log‘𝑦) ↔ 1 ≤
((log‘𝑦) /
2))) | 
| 199 | 195, 198 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 1 ≤ ((log‘𝑦) / 2)) | 
| 200 | 65, 166 | sselid 3980 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (log‘𝑦) ∈ ℂ) | 
| 201 | 22 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ) | 
| 202 | 24 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 2 ≠ 0) | 
| 203 | 200, 201,
202 | divrec2d 12048 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((log‘𝑦) / 2) = ((1 / 2) · (log‘𝑦))) | 
| 204 | 199, 203 | breqtrd 5168 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 1 ≤ ((1 / 2) ·
(log‘𝑦))) | 
| 205 | 53 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (1 / 2) ∈
ℂ) | 
| 206 | 205, 200 | mulneg1d 11717 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (-(1 / 2) ·
(log‘𝑦)) = -((1 / 2)
· (log‘𝑦))) | 
| 207 | 206 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (0 − (-(1 / 2) ·
(log‘𝑦))) = (0
− -((1 / 2) · (log‘𝑦)))) | 
| 208 | 65, 169 | sselid 3980 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 0 ∈ ℂ) | 
| 209 | 205, 200 | mulcld 11282 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((1 / 2) · (log‘𝑦)) ∈
ℂ) | 
| 210 | 208, 209 | subnegd 11628 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (0 − -((1 / 2) ·
(log‘𝑦))) = (0 + ((1
/ 2) · (log‘𝑦)))) | 
| 211 | 209 | addlidd 11463 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (0 + ((1 / 2) ·
(log‘𝑦))) = ((1 / 2)
· (log‘𝑦))) | 
| 212 | 207, 210,
211 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (0 − (-(1 / 2) ·
(log‘𝑦))) = ((1 / 2)
· (log‘𝑦))) | 
| 213 | 204, 212 | breqtrrd 5170 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 1 ≤ (0 − (-(1 / 2)
· (log‘𝑦)))) | 
| 214 |  | leaddsub 11740 | . . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (-(1 / 2) · (log‘𝑦)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((1 + (-(1 / 2) · (log‘𝑦))) ≤ 0 ↔ 1 ≤ (0 − (-(1 / 2)
· (log‘𝑦))))) | 
| 215 | 164, 167,
169, 214 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((1 + (-(1 / 2) ·
(log‘𝑦))) ≤ 0
↔ 1 ≤ (0 − (-(1 / 2) · (log‘𝑦))))) | 
| 216 | 213, 215 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (1 + (-(1 / 2) ·
(log‘𝑦))) ≤
0) | 
| 217 | 168, 169,
172, 173, 216 | lemul1ad 12208 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((1 + (-(1 / 2) ·
(log‘𝑦))) ·
(𝑦↑𝑐(-(1 / 2) −
1))) ≤ (0 · (𝑦↑𝑐(-(1 / 2) −
1)))) | 
| 218 | 43, 171 | sselid 3980 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝑦↑𝑐(-(1 / 2) −
1)) ∈ ℂ) | 
| 219 | 218 | mul02d 11460 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (0 · (𝑦↑𝑐(-(1 / 2) −
1))) = 0) | 
| 220 | 217, 219 | breqtrd 5168 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((1 + (-(1 / 2) ·
(log‘𝑦))) ·
(𝑦↑𝑐(-(1 / 2) −
1))) ≤ 0) | 
| 221 | 163, 220 | eqbrtrd 5164 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ ℝ+ ↦ ((1 +
(-(1 / 2) · (log‘𝑥))) · (𝑥↑𝑐(-(1 / 2) −
1))))‘𝑦) ≤
0) | 
| 222 | 149, 221 | eqbrtrd 5164 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ ℝ+ ↦ (((1 /
𝑥) · (𝑥↑𝑐-(1 /
2))) + ((-(1 / 2) · (𝑥↑𝑐(-(1 / 2) −
1))) · (log‘𝑥))))‘𝑦) ≤ 0) | 
| 223 | 124, 222 | eqbrtrd 5164 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑥 ∈ ℝ+ ↦
((log‘𝑥) /
(√‘𝑥))))‘𝑦) ≤ 0) | 
| 224 | 2, 3, 4, 14, 121, 122, 223 | fdvnegge 34618 | . 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
((log‘𝑥) /
(√‘𝑥)))‘𝐵) ≤ ((𝑥 ∈ ℝ+ ↦
((log‘𝑥) /
(√‘𝑥)))‘𝐴)) | 
| 225 |  | eqidd 2737 | . . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((log‘𝑥) /
(√‘𝑥))) =
(𝑥 ∈
ℝ+ ↦ ((log‘𝑥) / (√‘𝑥)))) | 
| 226 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵) | 
| 227 | 226 | fveq2d 6909 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (log‘𝑥) = (log‘𝐵)) | 
| 228 | 226 | fveq2d 6909 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (√‘𝑥) = (√‘𝐵)) | 
| 229 | 227, 228 | oveq12d 7450 | . . 3
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → ((log‘𝑥) / (√‘𝑥)) = ((log‘𝐵) / (√‘𝐵))) | 
| 230 |  | ovex 7465 | . . . 4
⊢
((log‘𝐵) /
(√‘𝐵)) ∈
V | 
| 231 | 230 | a1i 11 | . . 3
⊢ (𝜑 → ((log‘𝐵) / (√‘𝐵)) ∈ V) | 
| 232 | 225, 229,
4, 231 | fvmptd 7022 | . 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
((log‘𝑥) /
(√‘𝑥)))‘𝐵) = ((log‘𝐵) / (√‘𝐵))) | 
| 233 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴) | 
| 234 | 233 | fveq2d 6909 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (log‘𝑥) = (log‘𝐴)) | 
| 235 | 233 | fveq2d 6909 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (√‘𝑥) = (√‘𝐴)) | 
| 236 | 234, 235 | oveq12d 7450 | . . 3
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((log‘𝑥) / (√‘𝑥)) = ((log‘𝐴) / (√‘𝐴))) | 
| 237 |  | ovex 7465 | . . . 4
⊢
((log‘𝐴) /
(√‘𝐴)) ∈
V | 
| 238 | 237 | a1i 11 | . . 3
⊢ (𝜑 → ((log‘𝐴) / (√‘𝐴)) ∈ V) | 
| 239 | 225, 236,
3, 238 | fvmptd 7022 | . 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
((log‘𝑥) /
(√‘𝑥)))‘𝐴) = ((log‘𝐴) / (√‘𝐴))) | 
| 240 | 224, 232,
239 | 3brtr3d 5173 | 1
⊢ (𝜑 → ((log‘𝐵) / (√‘𝐵)) ≤ ((log‘𝐴) / (√‘𝐴))) |