Step | Hyp | Ref
| Expression |
1 | | stirlinglem14.1 |
. . 3
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
2 | | stirlinglem14.2 |
. . 3
⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛))) |
3 | 1, 2 | stirlinglem13 43169 |
. 2
⊢
∃𝑑 ∈
ℝ 𝐵 ⇝ 𝑑 |
4 | | simpl 486 |
. . . . 5
⊢ ((𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑) → 𝑑 ∈ ℝ) |
5 | 4 | rpefcld 15550 |
. . . 4
⊢ ((𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑) → (exp‘𝑑) ∈
ℝ+) |
6 | | nnuz 12363 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
7 | | 1zzd 12094 |
. . . . . 6
⊢ ((𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑) → 1 ∈ ℤ) |
8 | | efcn 25190 |
. . . . . . 7
⊢ exp
∈ (ℂ–cn→ℂ) |
9 | 8 | a1i 11 |
. . . . . 6
⊢ ((𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑) → exp ∈ (ℂ–cn→ℂ)) |
10 | | nnnn0 11983 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
11 | | faccl 13735 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ (!‘𝑛) ∈
ℕ) |
12 | | nncn 11724 |
. . . . . . . . . . . . 13
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
∈ ℂ) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(!‘𝑛) ∈
ℂ) |
14 | | 2cnd 11794 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 2 ∈
ℂ) |
15 | | nncn 11724 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
16 | 14, 15 | mulcld 10739 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℂ) |
17 | 16 | sqrtcld 14887 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(√‘(2 · 𝑛)) ∈ ℂ) |
18 | | epr 15653 |
. . . . . . . . . . . . . . . . 17
⊢ e ∈
ℝ+ |
19 | | rpcn 12482 |
. . . . . . . . . . . . . . . . 17
⊢ (e ∈
ℝ+ → e ∈ ℂ) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ e ∈
ℂ |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → e ∈
ℂ) |
22 | | 0re 10721 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ |
23 | | epos 15652 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
e |
24 | 22, 23 | gtneii 10830 |
. . . . . . . . . . . . . . . 16
⊢ e ≠
0 |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → e ≠
0) |
26 | 15, 21, 25 | divcld 11494 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 / e) ∈
ℂ) |
27 | 26, 10 | expcld 13602 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑𝑛) ∈ ℂ) |
28 | 17, 27 | mulcld 10739 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ∈ ℂ) |
29 | | 2rp 12477 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ+) |
31 | | nnrp 12483 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
32 | 30, 31 | rpmulcld 12530 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ+) |
33 | 32 | sqrtgt0d 14862 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 0 <
(√‘(2 · 𝑛))) |
34 | 33 | gt0ne0d 11282 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(√‘(2 · 𝑛)) ≠ 0) |
35 | | nnne0 11750 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
36 | 15, 21, 35, 25 | divne0d 11510 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 / e) ≠ 0) |
37 | | nnz 12085 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
38 | 26, 36, 37 | expne0d 13608 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑𝑛) ≠ 0) |
39 | 17, 27, 34, 38 | mulne0d 11370 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ≠ 0) |
40 | 13, 28, 39 | divcld 11494 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) ∈ ℂ) |
41 | 1 | fvmpt2 6786 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) ∈ ℂ) → (𝐴‘𝑛) = ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) |
42 | 40, 41 | mpdan 687 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) = ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) |
43 | 42, 40 | eqeltrd 2833 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) ∈ ℂ) |
44 | | nnne0 11750 |
. . . . . . . . . . . 12
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
≠ 0) |
45 | 10, 11, 44 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(!‘𝑛) ≠
0) |
46 | 13, 28, 45, 39 | divne0d 11510 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) ≠ 0) |
47 | 42, 46 | eqnetrd 3001 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) ≠ 0) |
48 | 43, 47 | logcld 25314 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(log‘(𝐴‘𝑛)) ∈
ℂ) |
49 | 2, 48 | fmpti 6886 |
. . . . . . 7
⊢ 𝐵:ℕ⟶ℂ |
50 | 49 | a1i 11 |
. . . . . 6
⊢ ((𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑) → 𝐵:ℕ⟶ℂ) |
51 | | simpr 488 |
. . . . . 6
⊢ ((𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑) → 𝐵 ⇝ 𝑑) |
52 | 4 | recnd 10747 |
. . . . . 6
⊢ ((𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑) → 𝑑 ∈ ℂ) |
53 | 6, 7, 9, 50, 51, 52 | climcncf 23652 |
. . . . 5
⊢ ((𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑) → (exp ∘ 𝐵) ⇝ (exp‘𝑑)) |
54 | 8 | elexi 3417 |
. . . . . . . . 9
⊢ exp
∈ V |
55 | | nnex 11722 |
. . . . . . . . . . 11
⊢ ℕ
∈ V |
56 | 55 | mptex 6996 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦
(log‘(𝐴‘𝑛))) ∈ V |
57 | 2, 56 | eqeltri 2829 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
58 | 54, 57 | coex 7661 |
. . . . . . . 8
⊢ (exp
∘ 𝐵) ∈
V |
59 | 58 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (exp ∘ 𝐵)
∈ V) |
60 | 55 | mptex 6996 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) ∈ V |
61 | 1, 60 | eqeltri 2829 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
62 | 61 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 𝐴 ∈
V) |
63 | | 1zzd 12094 |
. . . . . . 7
⊢ (⊤
→ 1 ∈ ℤ) |
64 | 2 | funmpt2 6378 |
. . . . . . . . . 10
⊢ Fun 𝐵 |
65 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ) |
66 | | rabid2 3284 |
. . . . . . . . . . . . 13
⊢ (ℕ
= {𝑛 ∈ ℕ ∣
(log‘(𝐴‘𝑛)) ∈ V} ↔
∀𝑛 ∈ ℕ
(log‘(𝐴‘𝑛)) ∈ V) |
67 | 1 | stirlinglem2 43158 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) ∈
ℝ+) |
68 | | relogcl 25319 |
. . . . . . . . . . . . . 14
⊢ ((𝐴‘𝑛) ∈ ℝ+ →
(log‘(𝐴‘𝑛)) ∈
ℝ) |
69 | | elex 3416 |
. . . . . . . . . . . . . 14
⊢
((log‘(𝐴‘𝑛)) ∈ ℝ → (log‘(𝐴‘𝑛)) ∈ V) |
70 | 67, 68, 69 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(log‘(𝐴‘𝑛)) ∈ V) |
71 | 66, 70 | mprgbir 3068 |
. . . . . . . . . . . 12
⊢ ℕ =
{𝑛 ∈ ℕ ∣
(log‘(𝐴‘𝑛)) ∈ V} |
72 | 2 | dmmpt 6072 |
. . . . . . . . . . . 12
⊢ dom 𝐵 = {𝑛 ∈ ℕ ∣ (log‘(𝐴‘𝑛)) ∈ V} |
73 | 71, 72 | eqtr4i 2764 |
. . . . . . . . . . 11
⊢ ℕ =
dom 𝐵 |
74 | 65, 73 | eleqtrdi 2843 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈ dom 𝐵) |
75 | | fvco 6766 |
. . . . . . . . . 10
⊢ ((Fun
𝐵 ∧ 𝑘 ∈ dom 𝐵) → ((exp ∘ 𝐵)‘𝑘) = (exp‘(𝐵‘𝑘))) |
76 | 64, 74, 75 | sylancr 590 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((exp
∘ 𝐵)‘𝑘) = (exp‘(𝐵‘𝑘))) |
77 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))))) |
78 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘) |
79 | 78 | fveq2d 6678 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (!‘𝑛) = (!‘𝑘)) |
80 | 78 | oveq2d 7186 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘)) |
81 | 80 | fveq2d 6678 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (√‘(2 · 𝑛)) = (√‘(2 ·
𝑘))) |
82 | 78 | oveq1d 7185 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (𝑛 / e) = (𝑘 / e)) |
83 | 82, 78 | oveq12d 7188 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((𝑛 / e)↑𝑛) = ((𝑘 / e)↑𝑘)) |
84 | 81, 83 | oveq12d 7188 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))) |
85 | 79, 84 | oveq12d 7188 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)))) |
86 | | nnnn0 11983 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
87 | | faccl 13735 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
88 | | nncn 11724 |
. . . . . . . . . . . . . . . 16
⊢
((!‘𝑘) ∈
ℕ → (!‘𝑘)
∈ ℂ) |
89 | 86, 87, 88 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ →
(!‘𝑘) ∈
ℂ) |
90 | | 2cnd 11794 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → 2 ∈
ℂ) |
91 | | nncn 11724 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
92 | 90, 91 | mulcld 10739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℂ) |
93 | 92 | sqrtcld 14887 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ →
(√‘(2 · 𝑘)) ∈ ℂ) |
94 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → e ∈
ℂ) |
95 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → e ≠
0) |
96 | 91, 94, 95 | divcld 11494 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (𝑘 / e) ∈
ℂ) |
97 | 96, 86 | expcld 13602 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → ((𝑘 / e)↑𝑘) ∈ ℂ) |
98 | 93, 97 | mulcld 10739 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ →
((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)) ∈ ℂ) |
99 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ → 2 ∈
ℝ+) |
100 | | nnrp 12483 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
101 | 99, 100 | rpmulcld 12530 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℝ+) |
102 | 101 | sqrtgt0d 14862 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → 0 <
(√‘(2 · 𝑘))) |
103 | 102 | gt0ne0d 11282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ →
(√‘(2 · 𝑘)) ≠ 0) |
104 | | nnne0 11750 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
105 | 91, 94, 104, 95 | divne0d 11510 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (𝑘 / e) ≠ 0) |
106 | | nnz 12085 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
107 | 96, 105, 106 | expne0d 13608 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → ((𝑘 / e)↑𝑘) ≠ 0) |
108 | 93, 97, 103, 107 | mulne0d 11370 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ →
((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)) ≠ 0) |
109 | 89, 98, 108 | divcld 11494 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ →
((!‘𝑘) /
((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))) ∈ ℂ) |
110 | 77, 85, 65, 109 | fvmptd 6782 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)))) |
111 | 110, 109 | eqeltrd 2833 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) ∈ ℂ) |
112 | | nnne0 11750 |
. . . . . . . . . . . . . . 15
⊢
((!‘𝑘) ∈
ℕ → (!‘𝑘)
≠ 0) |
113 | 86, 87, 112 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ →
(!‘𝑘) ≠
0) |
114 | 89, 98, 113, 108 | divne0d 11510 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ →
((!‘𝑘) /
((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))) ≠ 0) |
115 | 110, 114 | eqnetrd 3001 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) ≠ 0) |
116 | 111, 115 | logcld 25314 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ →
(log‘(𝐴‘𝑘)) ∈
ℂ) |
117 | | nfcv 2899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛𝑘 |
118 | | nfcv 2899 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛log |
119 | | nfmpt1 5128 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
120 | 1, 119 | nfcxfr 2897 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛𝐴 |
121 | 120, 117 | nffv 6684 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(𝐴‘𝑘) |
122 | 118, 121 | nffv 6684 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(log‘(𝐴‘𝑘)) |
123 | | 2fveq3 6679 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑘))) |
124 | 117, 122,
123, 2 | fvmptf 6796 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧
(log‘(𝐴‘𝑘)) ∈ ℂ) → (𝐵‘𝑘) = (log‘(𝐴‘𝑘))) |
125 | 116, 124 | mpdan 687 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝐵‘𝑘) = (log‘(𝐴‘𝑘))) |
126 | 125 | fveq2d 6678 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(exp‘(𝐵‘𝑘)) =
(exp‘(log‘(𝐴‘𝑘)))) |
127 | | eflog 25320 |
. . . . . . . . . 10
⊢ (((𝐴‘𝑘) ∈ ℂ ∧ (𝐴‘𝑘) ≠ 0) → (exp‘(log‘(𝐴‘𝑘))) = (𝐴‘𝑘)) |
128 | 111, 115,
127 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(exp‘(log‘(𝐴‘𝑘))) = (𝐴‘𝑘)) |
129 | 76, 126, 128 | 3eqtrd 2777 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((exp
∘ 𝐵)‘𝑘) = (𝐴‘𝑘)) |
130 | 129 | adantl 485 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((exp ∘ 𝐵)‘𝑘) = (𝐴‘𝑘)) |
131 | 6, 59, 62, 63, 130 | climeq 15014 |
. . . . . 6
⊢ (⊤
→ ((exp ∘ 𝐵)
⇝ (exp‘𝑑)
↔ 𝐴 ⇝
(exp‘𝑑))) |
132 | 131 | mptru 1549 |
. . . . 5
⊢ ((exp
∘ 𝐵) ⇝
(exp‘𝑑) ↔ 𝐴 ⇝ (exp‘𝑑)) |
133 | 53, 132 | sylib 221 |
. . . 4
⊢ ((𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑) → 𝐴 ⇝ (exp‘𝑑)) |
134 | | breq2 5034 |
. . . . 5
⊢ (𝑐 = (exp‘𝑑) → (𝐴 ⇝ 𝑐 ↔ 𝐴 ⇝ (exp‘𝑑))) |
135 | 134 | rspcev 3526 |
. . . 4
⊢
(((exp‘𝑑)
∈ ℝ+ ∧ 𝐴 ⇝ (exp‘𝑑)) → ∃𝑐 ∈ ℝ+ 𝐴 ⇝ 𝑐) |
136 | 5, 133, 135 | syl2anc 587 |
. . 3
⊢ ((𝑑 ∈ ℝ ∧ 𝐵 ⇝ 𝑑) → ∃𝑐 ∈ ℝ+ 𝐴 ⇝ 𝑐) |
137 | 136 | rexlimiva 3191 |
. 2
⊢
(∃𝑑 ∈
ℝ 𝐵 ⇝ 𝑑 → ∃𝑐 ∈ ℝ+
𝐴 ⇝ 𝑐) |
138 | 3, 137 | ax-mp 5 |
1
⊢
∃𝑐 ∈
ℝ+ 𝐴
⇝ 𝑐 |