Theorem stirlinglem13 47238

Description: 𝐵 is decreasing and has a lower bound, then it converges. Since 𝐵 is log𝐴, in another theorem it is proven that 𝐴 converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Hypotheses

Ref	Expression
stirlinglem13.1	⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
stirlinglem13.2	⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))

Assertion

Ref	Expression
stirlinglem13	⊢ ∃𝑑 ∈ ℝ 𝐵 ⇝ 𝑑

Distinct variable group:   𝐵,𝑑

Allowed substitution hints:   𝐴(𝑛, 𝑑)   𝐵(𝑛)

Proof of Theorem stirlinglem13

Dummy variables 𝑗 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3458	. . . . . 6 ⊢ 𝑦 ∈ V
2		stirlinglem13.2	. . . . . . 7 ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))
3	2	elrnmpt 5945	. . . . . 6 ⊢ (𝑦 ∈ V → (𝑦 ∈ ran 𝐵 ↔ ∃𝑛 ∈ ℕ 𝑦 = (log‘(𝐴‘𝑛))))
4	1, 3	ax-mp 5	. . . . 5 ⊢ (𝑦 ∈ ran 𝐵 ↔ ∃𝑛 ∈ ℕ 𝑦 = (log‘(𝐴‘𝑛)))
5		simpr 490	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 = (log‘(𝐴‘𝑛))) → 𝑦 = (log‘(𝐴‘𝑛)))
6		stirlinglem13.1	. . . . . . . . . 10 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
7	6	stirlinglem2 47227	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) ∈ ℝ+)
8	7	relogcld 26966	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (log‘(𝐴‘𝑛)) ∈ ℝ)
9	8	adantr 486	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 = (log‘(𝐴‘𝑛))) → (log‘(𝐴‘𝑛)) ∈ ℝ)
10	5, 9	eqeltrd 2864	. . . . . 6 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 = (log‘(𝐴‘𝑛))) → 𝑦 ∈ ℝ)
11	10	rexlimiva 3159	. . . . 5 ⊢ (∃𝑛 ∈ ℕ 𝑦 = (log‘(𝐴‘𝑛)) → 𝑦 ∈ ℝ)
12	4, 11	sylbi 220	. . . 4 ⊢ (𝑦 ∈ ran 𝐵 → 𝑦 ∈ ℝ)
13	12	ssriv 3917	. . 3 ⊢ ran 𝐵 ⊆ ℝ
14		1nn 12359	. . . . . 6 ⊢ 1 ∈ ℕ
15	6	stirlinglem2 47227	. . . . . . . 8 ⊢ (1 ∈ ℕ → (𝐴‘1) ∈ ℝ+)
16		relogcl 26918	. . . . . . . 8 ⊢ ((𝐴‘1) ∈ ℝ+ → (log‘(𝐴‘1)) ∈ ℝ)
17	14, 15, 16	mp2b 10	. . . . . . 7 ⊢ (log‘(𝐴‘1)) ∈ ℝ
18		nfcv 2926	. . . . . . . 8 ⊢ Ⅎ𝑛1
19		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑛log
20		nfmpt1 5207	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
21	6, 20	nfcxfr 2924	. . . . . . . . . 10 ⊢ Ⅎ𝑛𝐴
22	21, 18	nffv 6906	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝐴‘1)
23	19, 22	nffv 6906	. . . . . . . 8 ⊢ Ⅎ𝑛(log‘(𝐴‘1))
24		2fveq3 6901	. . . . . . . 8 ⊢ (𝑛 = 1 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘1)))
25	18, 23, 24, 2	fvmptf 7026	. . . . . . 7 ⊢ ((1 ∈ ℕ ∧ (log‘(𝐴‘1)) ∈ ℝ) → (𝐵‘1) = (log‘(𝐴‘1)))
26	14, 17, 25	mp2an 705	. . . . . 6 ⊢ (𝐵‘1) = (log‘(𝐴‘1))
27		2fveq3 6901	. . . . . . 7 ⊢ (𝑗 = 1 → (log‘(𝐴‘𝑗)) = (log‘(𝐴‘1)))
28	27	rspceeqv 3602	. . . . . 6 ⊢ ((1 ∈ ℕ ∧ (𝐵‘1) = (log‘(𝐴‘1))) → ∃𝑗 ∈ ℕ (𝐵‘1) = (log‘(𝐴‘𝑗)))
29	14, 26, 28	mp2an 705	. . . . 5 ⊢ ∃𝑗 ∈ ℕ (𝐵‘1) = (log‘(𝐴‘𝑗))
30	26, 17	eqeltri 2860	. . . . . 6 ⊢ (𝐵‘1) ∈ ℝ
31		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑗(log‘(𝐴‘𝑛))
32		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝑗
33	21, 32	nffv 6906	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝐴‘𝑗)
34	19, 33	nffv 6906	. . . . . . . . 9 ⊢ Ⅎ𝑛(log‘(𝐴‘𝑗))
35		2fveq3 6901	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑗)))
36	31, 34, 35	cbvmpt 5210	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛))) = (𝑗 ∈ ℕ ↦ (log‘(𝐴‘𝑗)))
37	2, 36	eqtri 2786	. . . . . . 7 ⊢ 𝐵 = (𝑗 ∈ ℕ ↦ (log‘(𝐴‘𝑗)))
38	37	elrnmpt 5945	. . . . . 6 ⊢ ((𝐵‘1) ∈ ℝ → ((𝐵‘1) ∈ ran 𝐵 ↔ ∃𝑗 ∈ ℕ (𝐵‘1) = (log‘(𝐴‘𝑗))))
39	30, 38	ax-mp 5	. . . . 5 ⊢ ((𝐵‘1) ∈ ran 𝐵 ↔ ∃𝑗 ∈ ℕ (𝐵‘1) = (log‘(𝐴‘𝑗)))
40	29, 39	mpbir 234	. . . 4 ⊢ (𝐵‘1) ∈ ran 𝐵
41	40	ne0ii 4293	. . 3 ⊢ ran 𝐵 ≠ ∅
42		4re 12440	. . . . . . 7 ⊢ 4 ∈ ℝ
43		4ne0 12467	. . . . . . 7 ⊢ 4 ≠ 0
44	42, 43	rereccli 12095	. . . . . 6 ⊢ (1 / 4) ∈ ℝ
45	30, 44	resubcli 11633	. . . . 5 ⊢ ((𝐵‘1) − (1 / 4)) ∈ ℝ
46		eqid 2763	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1)))) = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1))))
47	6, 2, 46	stirlinglem12 47237	. . . . . 6 ⊢ (𝑗 ∈ ℕ → ((𝐵‘1) − (1 / 4)) ≤ (𝐵‘𝑗))
48	47	rgen 3082	. . . . 5 ⊢ ∀𝑗 ∈ ℕ ((𝐵‘1) − (1 / 4)) ≤ (𝐵‘𝑗)
49		breq1 5109	. . . . . . 7 ⊢ (𝑥 = ((𝐵‘1) − (1 / 4)) → (𝑥 ≤ (𝐵‘𝑗) ↔ ((𝐵‘1) − (1 / 4)) ≤ (𝐵‘𝑗)))
50	49	ralbidv 3189	. . . . . 6 ⊢ (𝑥 = ((𝐵‘1) − (1 / 4)) → (∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ↔ ∀𝑗 ∈ ℕ ((𝐵‘1) − (1 / 4)) ≤ (𝐵‘𝑗)))
51	50	rspcev 3580	. . . . 5 ⊢ ((((𝐵‘1) − (1 / 4)) ∈ ℝ ∧ ∀𝑗 ∈ ℕ ((𝐵‘1) − (1 / 4)) ≤ (𝐵‘𝑗)) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗))
52	45, 48, 51	mp2an 705	. . . 4 ⊢ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗)
53	8	rgen 3082	. . . . . . . . 9 ⊢ ∀𝑛 ∈ ℕ (log‘(𝐴‘𝑛)) ∈ ℝ
54	2	fnmpt 6690	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ℕ (log‘(𝐴‘𝑛)) ∈ ℝ → 𝐵 Fn ℕ)
55		fvelrnb 6956	. . . . . . . . 9 ⊢ (𝐵 Fn ℕ → (𝑦 ∈ ran 𝐵 ↔ ∃𝑗 ∈ ℕ (𝐵‘𝑗) = 𝑦))
56	53, 54, 55	mp2b 10	. . . . . . . 8 ⊢ (𝑦 ∈ ran 𝐵 ↔ ∃𝑗 ∈ ℕ (𝐵‘𝑗) = 𝑦)
57	56	bilani 510	. . . . . . 7 ⊢ ((∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ∧ 𝑦 ∈ ran 𝐵) → ∃𝑗 ∈ ℕ (𝐵‘𝑗) = 𝑦)
58		nfra1 3290	. . . . . . . . 9 ⊢ Ⅎ𝑗∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗)
59		nfv 1948	. . . . . . . . 9 ⊢ Ⅎ𝑗 𝑦 ∈ ran 𝐵
60	58, 59	nfan 1933	. . . . . . . 8 ⊢ Ⅎ𝑗(∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ∧ 𝑦 ∈ ran 𝐵)
61		nfv 1948	. . . . . . . 8 ⊢ Ⅎ𝑗 𝑥 ≤ 𝑦
62		simp1l 1216	. . . . . . . . . . 11 ⊢ (((∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ∧ 𝑦 ∈ ran 𝐵) ∧ 𝑗 ∈ ℕ ∧ (𝐵‘𝑗) = 𝑦) → ∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗))
63		simp2 1155	. . . . . . . . . . 11 ⊢ (((∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ∧ 𝑦 ∈ ran 𝐵) ∧ 𝑗 ∈ ℕ ∧ (𝐵‘𝑗) = 𝑦) → 𝑗 ∈ ℕ)
64		rsp 3254	. . . . . . . . . . 11 ⊢ (∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) → (𝑗 ∈ ℕ → 𝑥 ≤ (𝐵‘𝑗)))
65	62, 63, 64	sylc 66	. . . . . . . . . 10 ⊢ (((∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ∧ 𝑦 ∈ ran 𝐵) ∧ 𝑗 ∈ ℕ ∧ (𝐵‘𝑗) = 𝑦) → 𝑥 ≤ (𝐵‘𝑗))
66		simp3 1156	. . . . . . . . . 10 ⊢ (((∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ∧ 𝑦 ∈ ran 𝐵) ∧ 𝑗 ∈ ℕ ∧ (𝐵‘𝑗) = 𝑦) → (𝐵‘𝑗) = 𝑦)
67	65, 66	breqtrd 5134	. . . . . . . . 9 ⊢ (((∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ∧ 𝑦 ∈ ran 𝐵) ∧ 𝑗 ∈ ℕ ∧ (𝐵‘𝑗) = 𝑦) → 𝑥 ≤ 𝑦)
68	67	3exp 1137	. . . . . . . 8 ⊢ ((∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ∧ 𝑦 ∈ ran 𝐵) → (𝑗 ∈ ℕ → ((𝐵‘𝑗) = 𝑦 → 𝑥 ≤ 𝑦)))
69	60, 61, 68	rexlimd 3273	. . . . . . 7 ⊢ ((∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ∧ 𝑦 ∈ ran 𝐵) → (∃𝑗 ∈ ℕ (𝐵‘𝑗) = 𝑦 → 𝑥 ≤ 𝑦))
70	57, 69	mpd 16	. . . . . 6 ⊢ ((∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) ∧ 𝑦 ∈ ran 𝐵) → 𝑥 ≤ 𝑦)
71	70	ralrimiva 3158	. . . . 5 ⊢ (∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) → ∀𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦)
72	71	reximi 3104	. . . 4 ⊢ (∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦)
73	52, 72	ax-mp 5	. . 3 ⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦
74		infrecl 12312	. . 3 ⊢ ((ran 𝐵 ⊆ ℝ ∧ ran 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐵 𝑥 ≤ 𝑦) → inf(ran 𝐵, ℝ, < ) ∈ ℝ)
75	13, 41, 73, 74	mp3an 1490	. 2 ⊢ inf(ran 𝐵, ℝ, < ) ∈ ℝ
76		nnuz 13017	. . . 4 ⊢ ℕ = (ℤ≥‘1)
77		1zzd 12740	. . . 4 ⊢ (⊤ → 1 ∈ ℤ)
78	2, 8	fmpti 7123	. . . . 5 ⊢ 𝐵:ℕ⟶ℝ
79	78	a1i 11	. . . 4 ⊢ (⊤ → 𝐵:ℕ⟶ℝ)
80		peano2nn 12360	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
81	6	a1i 11	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))))
82		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = (𝑗 + 1)) → 𝑛 = (𝑗 + 1))
83	82	fveq2d 6900	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = (𝑗 + 1)) → (!‘𝑛) = (!‘(𝑗 + 1)))
84	82	oveq2d 7446	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = (𝑗 + 1)) → (2 · 𝑛) = (2 · (𝑗 + 1)))
85	84	fveq2d 6900	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = (𝑗 + 1)) → (√‘(2 · 𝑛)) = (√‘(2 · (𝑗 + 1))))
86	82	oveq1d 7445	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = (𝑗 + 1)) → (𝑛 / e) = ((𝑗 + 1) / e))
87	86, 82	oveq12d 7448	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = (𝑗 + 1)) → ((𝑛 / e)↑𝑛) = (((𝑗 + 1) / e)↑(𝑗 + 1)))
88	85, 87	oveq12d 7448	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = (𝑗 + 1)) → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · (𝑗 + 1))) · (((𝑗 + 1) / e)↑(𝑗 + 1))))
89	83, 88	oveq12d 7448	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = (𝑗 + 1)) → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘(𝑗 + 1)) / ((√‘(2 · (𝑗 + 1))) · (((𝑗 + 1) / e)↑(𝑗 + 1)))))
90	80	nnnn0d 12680	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ0)
91		faccl 14440	. . . . . . . . . . . . 13 ⊢ ((𝑗 + 1) ∈ ℕ0 → (!‘(𝑗 + 1)) ∈ ℕ)
92		nncn 12356	. . . . . . . . . . . . 13 ⊢ ((!‘(𝑗 + 1)) ∈ ℕ → (!‘(𝑗 + 1)) ∈ ℂ)
93	90, 91, 92	3syl 19	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (!‘(𝑗 + 1)) ∈ ℂ)
94		2cnd 12434	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℂ)
95		nncn 12356	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
96		1cnd 11315	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℂ)
97	95, 96	addcld 11341	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℂ)
98	94, 97	mulcld 11342	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (2 · (𝑗 + 1)) ∈ ℂ)
99	98	sqrtcld 15622	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → (√‘(2 · (𝑗 + 1))) ∈ ℂ)
100		ere 16270	. . . . . . . . . . . . . . . . 17 ⊢ e ∈ ℝ
101	100	recni 11336	. . . . . . . . . . . . . . . 16 ⊢ e ∈ ℂ
102	101	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → e ∈ ℂ)
103		0re 11323	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
104		epos 16390	. . . . . . . . . . . . . . . . 17 ⊢ 0 < e
105	103, 104	gtneii 11435	. . . . . . . . . . . . . . . 16 ⊢ e ≠ 0
106	105	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → e ≠ 0)
107	97, 102, 106	divcld 12106	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → ((𝑗 + 1) / e) ∈ ℂ)
108	107, 90	expcld 14302	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → (((𝑗 + 1) / e)↑(𝑗 + 1)) ∈ ℂ)
109	99, 108	mulcld 11342	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((√‘(2 · (𝑗 + 1))) · (((𝑗 + 1) / e)↑(𝑗 + 1))) ∈ ℂ)
110		2rp 13138	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ+
111	110	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℝ+)
112		nnre 12355	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
113	103	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → 0 ∈ ℝ)
114		1red 11322	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℝ)
115		0le1 11852	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 1
116	115	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → 0 ≤ 1)
117		nnge1 12379	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → 1 ≤ 𝑗)
118	113, 114, 112, 116, 117	letrd 11480	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℕ → 0 ≤ 𝑗)
119	112, 118	ge0p1rpd 13207	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℝ+)
120	111, 119	rpmulcld 13193	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → (2 · (𝑗 + 1)) ∈ ℝ+)
121	120	sqrtgt0d 15595	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → 0 < (√‘(2 · (𝑗 + 1))))
122	121	gt0ne0d 11893	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → (√‘(2 · (𝑗 + 1))) ≠ 0)
123	80	nnne0d 12401	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ≠ 0)
124	97, 102, 123, 106	divne0d 12122	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → ((𝑗 + 1) / e) ≠ 0)
125		nnz 12727	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
126	125	peano2zd 12819	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℤ)
127	107, 124, 126	expne0d 14308	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → (((𝑗 + 1) / e)↑(𝑗 + 1)) ≠ 0)
128	99, 108, 122, 127	mulne0d 11981	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((√‘(2 · (𝑗 + 1))) · (((𝑗 + 1) / e)↑(𝑗 + 1))) ≠ 0)
129	93, 109, 128	divcld 12106	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((!‘(𝑗 + 1)) / ((√‘(2 · (𝑗 + 1))) · (((𝑗 + 1) / e)↑(𝑗 + 1)))) ∈ ℂ)
130	81, 89, 80, 129	fvmptd 7012	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (𝐴‘(𝑗 + 1)) = ((!‘(𝑗 + 1)) / ((√‘(2 · (𝑗 + 1))) · (((𝑗 + 1) / e)↑(𝑗 + 1)))))
131		nnrp 13145	. . . . . . . . . . . 12 ⊢ ((!‘(𝑗 + 1)) ∈ ℕ → (!‘(𝑗 + 1)) ∈ ℝ+)
132	90, 91, 131	3syl 19	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → (!‘(𝑗 + 1)) ∈ ℝ+)
133	120	rpsqrtcld 15594	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (√‘(2 · (𝑗 + 1))) ∈ ℝ+)
134		epr 16391	. . . . . . . . . . . . . . 15 ⊢ e ∈ ℝ+
135	134	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ → e ∈ ℝ+)
136	119, 135	rpdivcld 13194	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → ((𝑗 + 1) / e) ∈ ℝ+)
137	136, 126	rpexpcld 14404	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (((𝑗 + 1) / e)↑(𝑗 + 1)) ∈ ℝ+)
138	133, 137	rpmulcld 13193	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((√‘(2 · (𝑗 + 1))) · (((𝑗 + 1) / e)↑(𝑗 + 1))) ∈ ℝ+)
139	132, 138	rpdivcld 13194	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → ((!‘(𝑗 + 1)) / ((√‘(2 · (𝑗 + 1))) · (((𝑗 + 1) / e)↑(𝑗 + 1)))) ∈ ℝ+)
140	130, 139	eqeltrd 2864	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (𝐴‘(𝑗 + 1)) ∈ ℝ+)
141	140	relogcld 26966	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (log‘(𝐴‘(𝑗 + 1))) ∈ ℝ)
142		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑗 + 1)
143	21, 142	nffv 6906	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝐴‘(𝑗 + 1))
144	19, 143	nffv 6906	. . . . . . . . 9 ⊢ Ⅎ𝑛(log‘(𝐴‘(𝑗 + 1)))
145		2fveq3 6901	. . . . . . . . 9 ⊢ (𝑛 = (𝑗 + 1) → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘(𝑗 + 1))))
146	142, 144, 145, 2	fvmptf 7026	. . . . . . . 8 ⊢ (((𝑗 + 1) ∈ ℕ ∧ (log‘(𝐴‘(𝑗 + 1))) ∈ ℝ) → (𝐵‘(𝑗 + 1)) = (log‘(𝐴‘(𝑗 + 1))))
147	80, 141, 146	syl2anc 596	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → (𝐵‘(𝑗 + 1)) = (log‘(𝐴‘(𝑗 + 1))))
148	147, 141	eqeltrd 2864	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝐵‘(𝑗 + 1)) ∈ ℝ)
149	78	ffvelcdmi 7094	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝐵‘𝑗) ∈ ℝ)
150		eqid 2763	. . . . . . 7 ⊢ (𝑧 ∈ ℕ ↦ ((1 / ((2 · 𝑧) + 1)) · ((1 / ((2 · 𝑗) + 1))↑(2 · 𝑧)))) = (𝑧 ∈ ℕ ↦ ((1 / ((2 · 𝑧) + 1)) · ((1 / ((2 · 𝑗) + 1))↑(2 · 𝑧))))
151	6, 2, 150	stirlinglem11 47236	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝐵‘(𝑗 + 1)) < (𝐵‘𝑗))
152	148, 149, 151	ltled 11471	. . . . 5 ⊢ (𝑗 ∈ ℕ → (𝐵‘(𝑗 + 1)) ≤ (𝐵‘𝑗))
153	152	adantl 487	. . . 4 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → (𝐵‘(𝑗 + 1)) ≤ (𝐵‘𝑗))
154	52	a1i 11	. . . 4 ⊢ (⊤ → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ 𝑥 ≤ (𝐵‘𝑗))
155	76, 77, 79, 153, 154	climinf 46760	. . 3 ⊢ (⊤ → 𝐵 ⇝ inf(ran 𝐵, ℝ, < ))
156	155	mptru 1576	. 2 ⊢ 𝐵 ⇝ inf(ran 𝐵, ℝ, < )
157		breq2 5110	. . 3 ⊢ (𝑑 = inf(ran 𝐵, ℝ, < ) → (𝐵 ⇝ 𝑑 ↔ 𝐵 ⇝ inf(ran 𝐵, ℝ, < )))
158	157	rspcev 3580	. 2 ⊢ ((inf(ran 𝐵, ℝ, < ) ∈ ℝ ∧ 𝐵 ⇝ inf(ran 𝐵, ℝ, < )) → ∃𝑑 ∈ ℝ 𝐵 ⇝ 𝑑)
159	75, 156, 158	mp2an 705	1 ⊢ ∃𝑑 ∈ ℝ 𝐵 ⇝ 𝑑

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569  ⊤wtru 1570   ∈ wcel 2146   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900  ∅c0 4281   class class class wbr 5106   ↦ cmpt 5189  ran crn 5656   Fn wfn 6542  ⟶wf 6543  ‘cfv 6547  (class class class)co 7430  infcinf 9446  ℂcc 11211  ℝcr 11212  0cc0 11213  1c1 11214   + caddc 11216   · cmul 11218   < clt 11356   ≤ cle 11357   − cmin 11554   / cdiv 11986  ℕcn 12348  2c2 12410  4c4 12412  ℕ₀cn0 12619  ℝ⁺crp 13133  ↑cexp 14217  !cfa 14430  √csqrt 15415   ⇝ cli 15666  eceu 16243  logclog 26897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761  ax-inf2 9655  ax-cnex 11269  ax-resscn 11270  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-addrcl 11274  ax-mulcl 11275  ax-mulrcl 11276  ax-mulcom 11277  ax-addass 11278  ax-mulass 11279  ax-distr 11280  ax-i2m1 11281  ax-1ne0 11282  ax-1rid 11283  ax-rnegex 11284  ax-rrecex 11285  ax-cnre 11286  ax-pre-lttri 11287  ax-pre-lttrn 11288  ax-pre-ltadd 11289  ax-pre-mulgt0 11290  ax-pre-sup 11291  ax-addf 11292

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6311  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-isom 6556  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7703  df-om 7888  df-1st 8011  df-2nd 8012  df-supp 8191  df-frecs 8313  df-wrecs 8344  df-recs 8393  df-rdg 8432  df-1o 8490  df-2o 8491  df-oadd 8494  df-er 8731  df-map 8863  df-pm 8864  df-ixp 8940  df-en 8988  df-dom 8989  df-sdom 8990  df-fin 8991  df-fsupp 9368  df-fi 9416  df-sup 9447  df-inf 9448  df-oi 9517  df-card 10033  df-pnf 11358  df-mnf 11359  df-xr 11360  df-ltxr 11361  df-le 11362  df-sub 11556  df-neg 11557  df-div 11987  df-nn 12349  df-2 12418  df-3 12419  df-4 12420  df-5 12421  df-6 12422  df-7 12423  df-8 12424  df-9 12425  df-n0 12620  df-xnn0 12693  df-z 12707  df-dec 12828  df-uz 12979  df-q 13089  df-rp 13134  df-xneg 13254  df-xadd 13255  df-xmul 13256  df-ioo 13493  df-ioc 13494  df-ico 13495  df-icc 13496  df-fz 13653  df-fzo 13802  df-fl 13945  df-mod 14023  df-seq 14158  df-exp 14218  df-fac 14431  df-bc 14460  df-hash 14488  df-shft 15235  df-cj 15281  df-re 15282  df-im 15283  df-sqrt 15417  df-abs 15418  df-limsup 15653  df-clim 15670  df-rlim 15671  df-sum 15869  df-ef 16248  df-e 16249  df-sin 16250  df-cos 16251  df-tan 16252  df-pi 16253  df-dvds 16438  df-struct 17340  df-sets 17357  df-slot 17375  df-ndx 17387  df-base 17403  df-ress 17424  df-plusg 17456  df-mulr 17457  df-starv 17458  df-sca 17459  df-vsca 17460  df-ip 17461  df-tset 17462  df-ple 17463  df-ds 17465  df-unif 17466  df-hom 17467  df-cco 17468  df-rest 17608  df-topn 17609  df-0g 17627  df-gsum 17628  df-topgen 17629  df-pt 17630  df-prds 17633  df-xrs 17689  df-qtop 17694  df-imas 17695  df-xps 17697  df-mre 17771  df-mrc 17772  df-acs 17774  df-mgm 18831  df-sgrp 18923  df-mnd 18939  df-submnd 18994  df-mulg 19293  df-cntz 19546  df-cmn 20011  df-psmet 21685  df-xmet 21686  df-met 21687  df-bl 21688  df-mopn 21689  df-fbas 21690  df-fg 21691  df-cnfld 21694  df-top 23227  df-topon 23244  df-topsp 23266  df-bases 23279  df-cld 23352  df-ntr 23353  df-cls 23354  df-nei 23431  df-lp 23469  df-perf 23470  df-cn 23560  df-cnp 23561  df-haus 23648  df-cmp 23720  df-tx 23896  df-hmeo 24089  df-fil 24180  df-fm 24272  df-flim 24273  df-flf 24274  df-xms 24654  df-ms 24655  df-tms 24656  df-cncf 25214  df-limc 26201  df-dv 26202  df-ulm 26719  df-log 26899  df-cxp 26900

This theorem is used by:  stirlinglem14  47239