Theorem etransclem48 46237

Description: e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. In this lemma, a large enough prime 𝑝 is chosen: it will be used by subsequent lemmas. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 28-Sep-2020.)

Hypotheses

Ref	Expression
etransclem48.q	⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
etransclem48.qe0	⊢ (𝜑 → (𝑄‘e) = 0)
etransclem48.a	⊢ 𝐴 = (coeff‘𝑄)
etransclem48.a0	⊢ (𝜑 → (𝐴‘0) ≠ 0)
etransclem48.m	⊢ 𝑀 = (deg‘𝑄)
etransclem48.c	⊢ 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1))))
etransclem48.s	⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
etransclem48.i	⊢ 𝐼 = inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < )
etransclem48.t	⊢ 𝑇 = sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < )

Assertion

Ref	Expression
etransclem48	⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))

Distinct variable groups:   𝐴,𝑗,𝑘   𝐴,𝑛,𝑗   𝐶,𝑖,𝑛   𝑖,𝐼,𝑛   𝑗,𝑀,𝑘   𝑛,𝑀   𝑄,𝑗   𝑆,𝑖   𝑇,𝑗,𝑘   𝜑,𝑖,𝑛   𝜑,𝑗,𝑘

Allowed substitution hints:   𝐴(𝑖)   𝐶(𝑗,𝑘)   𝑄(𝑖,𝑘,𝑛)   𝑆(𝑗,𝑘,𝑛)   𝑇(𝑖,𝑛)   𝐼(𝑗,𝑘)   𝑀(𝑖)

Proof of Theorem etransclem48

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

Step	Hyp	Ref	Expression
1		etransclem48.q	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
2	1	eldifad 3974	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
3		0zd 12622	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
4		etransclem48.a	. . . . . . . . . 10 ⊢ 𝐴 = (coeff‘𝑄)
5	4	coef2 26284	. . . . . . . . 9 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ0⟶ℤ)
6	2, 3, 5	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ0⟶ℤ)
7		0nn0 12538	. . . . . . . . 9 ⊢ 0 ∈ ℕ0
8	7	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℕ0)
9	6, 8	ffvelcdmd 7104	. . . . . . 7 ⊢ (𝜑 → (𝐴‘0) ∈ ℤ)
10		zabscl 15348	. . . . . . 7 ⊢ ((𝐴‘0) ∈ ℤ → (abs‘(𝐴‘0)) ∈ ℤ)
11	9, 10	syl 17	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐴‘0)) ∈ ℤ)
12		etransclem48.m	. . . . . . . . 9 ⊢ 𝑀 = (deg‘𝑄)
13		dgrcl 26286	. . . . . . . . . 10 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ0)
14	2, 13	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ0)
15	12, 14	eqeltrid 2842	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
16	15	faccld 14319	. . . . . . 7 ⊢ (𝜑 → (!‘𝑀) ∈ ℕ)
17	16	nnzd 12637	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) ∈ ℤ)
18		ssrab2 4089	. . . . . . . 8 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ ℕ0
19		nn0ssz 12633	. . . . . . . 8 ⊢ ℕ0 ⊆ ℤ
20	18, 19	sstri 4004	. . . . . . 7 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ ℤ
21		etransclem48.i	. . . . . . . 8 ⊢ 𝐼 = inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < )
22		nn0uz 12917	. . . . . . . . . 10 ⊢ ℕ0 = (ℤ≥‘0)
23	18, 22	sseqtri 4031	. . . . . . . . 9 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ (ℤ≥‘0)
24		1rp 13035	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ+
25		nfv 1911	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝜑
26		nfmpt1 5255	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ 𝐶)
27		nfmpt1 5255	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
28		etransclem48.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
29		nfmpt1 5255	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
30	28, 29	nfcxfr 2900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝑆
31		nn0ex 12529	. . . . . . . . . . . . . . . . 17 ⊢ ℕ0 ∈ V
32	31	mptex 7242	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ 𝐶) ∈ V
33	32	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ 𝐶) ∈ V)
34		etransclem48.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1))))
35		fzfid 14010	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
36	6	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ)
37		elfznn0 13656	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
38	37	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
39	36, 38	ffvelcdmd 7104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
40	39	zcnd 12720	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
41		ere 16121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ e ∈ ℝ
42	41	recni 11272	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ e ∈ ℂ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ)
44		elfzelz 13560	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
45	44	zcnd 12720	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
46	45	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
47	43, 46	cxpcld 26764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈ ℂ)
48	40, 47	mulcld 11278	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑐𝑗)) ∈ ℂ)
49	48	abscld 15471	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈ ℝ)
50	49	recnd 11286	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈ ℂ)
51	15	nn0cnd 12586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
52		peano2nn0 12563	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
53	15, 52	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ0)
54	51, 53	expcld 14182	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ)
55	51, 54	mulcld 11278	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
56	55	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
57	50, 56	mulcld 11278	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
58	35, 57	fsumcl 15765	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
59	34, 58	eqeltrid 2842	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℂ)
60		eqidd 2735	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑛 ∈ ℕ0 ↦ 𝐶) = (𝑛 ∈ ℕ0 ↦ 𝐶))
61		eqidd 2735	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 = 𝑖) → 𝐶 = 𝐶)
62		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
63	59	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐶 ∈ ℂ)
64	60, 61, 62, 63	fvmptd 7022	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑖) = 𝐶)
65	22, 3, 33, 59, 64	climconst 15575	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ 𝐶) ⇝ 𝐶)
66	31	mptex 7242	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))) ∈ V
67	28, 66	eqeltri 2834	. . . . . . . . . . . . . . 15 ⊢ 𝑆 ∈ V
68	67	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ V)
69		eqid 2734	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
70	69	expfac 45612	. . . . . . . . . . . . . . 15 ⊢ ((𝑀↑(𝑀 + 1)) ∈ ℂ → (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ⇝ 0)
71	54, 70	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ⇝ 0)
72		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
73	59	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝐶 ∈ ℂ)
74		eqid 2734	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ0 ↦ 𝐶) = (𝑛 ∈ ℕ0 ↦ 𝐶)
75	74	fvmpt2 7026	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ0 ∧ 𝐶 ∈ ℂ) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) = 𝐶)
76	72, 73, 75	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) = 𝐶)
77	76, 73	eqeltrd 2838	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) ∈ ℂ)
78		ovex 7463	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ V
79	69	fvmpt2 7026	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ0 ∧ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ V) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) = (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
80	78, 79	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) = (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
81	80	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) = (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
82	54	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑀↑(𝑀 + 1)) ∈ ℂ)
83	82, 72	expcld 14182	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑀↑(𝑀 + 1))↑𝑛) ∈ ℂ)
84	72	faccld 14319	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ∈ ℕ)
85	84	nncnd 12279	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ∈ ℂ)
86	84	nnne0d 12313	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ≠ 0)
87	83, 85, 86	divcld 12040	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ ℂ)
88	81, 87	eqeltrd 2838	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) ∈ ℂ)
89		ovex 7463	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ∈ V
90	28	fvmpt2 7026	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ0 ∧ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ∈ V) → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
91	89, 90	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
92	91	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
93	76, 81	oveq12d 7448	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
94	92, 93	eqtr4d 2777	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)))
95	25, 26, 27, 30, 22, 3, 65, 68, 71, 77, 88, 94	climmulf 45559	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ⇝ (𝐶 · 0))
96	59	mul01d 11457	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 · 0) = 0)
97	95, 96	breqtrd 5173	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ⇝ 0)
98		eqidd 2735	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (𝑆‘𝑛))
99	77, 88	mulcld 11278	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)) ∈ ℂ)
100	94, 99	eqeltrd 2838	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) ∈ ℂ)
101	30, 22, 3, 68, 98, 100	clim0cf 45609	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ⇝ 0 ↔ ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒))
102	97, 101	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒)
103		breq2 5151	. . . . . . . . . . . . 13 ⊢ (𝑒 = 1 → ((abs‘(𝑆‘𝑛)) < 𝑒 ↔ (abs‘(𝑆‘𝑛)) < 1))
104	103	rexralbidv 3220	. . . . . . . . . . . 12 ⊢ (𝑒 = 1 → (∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒 ↔ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1))
105	104	rspcva 3619	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ+ ∧ ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒) → ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
106	24, 102, 105	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
107		rabn0 4394	. . . . . . . . . 10 ⊢ ({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅ ↔ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
108	106, 107	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅)
109		infssuzcl 12971	. . . . . . . . 9 ⊢ (({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ (ℤ≥‘0) ∧ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅) → inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < ) ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
110	23, 108, 109	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < ) ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
111	21, 110	eqeltrid 2842	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
112	20, 111	sselid 3992	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
113		tpssi 4842	. . . . . 6 ⊢ (((abs‘(𝐴‘0)) ∈ ℤ ∧ (!‘𝑀) ∈ ℤ ∧ 𝐼 ∈ ℤ) → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℤ)
114	11, 17, 112, 113	syl3anc 1370	. . . . 5 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℤ)
115		etransclem48.t	. . . . . 6 ⊢ 𝑇 = sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < )
116		xrltso 13179	. . . . . . . 8 ⊢ < Or ℝ*
117	116	a1i 11	. . . . . . 7 ⊢ (𝜑 → < Or ℝ*)
118		tpfi 9362	. . . . . . . 8 ⊢ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin
119	118	a1i 11	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin)
120	11	tpnzd 4784	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ≠ ∅)
121		zssre 12617	. . . . . . . . 9 ⊢ ℤ ⊆ ℝ
122		ressxr 11302	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ*
123	121, 122	sstri 4004	. . . . . . . 8 ⊢ ℤ ⊆ ℝ*
124	114, 123	sstrdi 4007	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)
125		fisupcl 9506	. . . . . . 7 ⊢ (( < Or ℝ* ∧ ({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin ∧ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ≠ ∅ ∧ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)) → sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
126	117, 119, 120, 124, 125	syl13anc 1371	. . . . . 6 ⊢ (𝜑 → sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
127	115, 126	eqeltrid 2842	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
128	114, 127	sseldd 3995	. . . 4 ⊢ (𝜑 → 𝑇 ∈ ℤ)
129		0red 11261	. . . . 5 ⊢ (𝜑 → 0 ∈ ℝ)
130	16	nnred 12278	. . . . 5 ⊢ (𝜑 → (!‘𝑀) ∈ ℝ)
131	128	zred 12719	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℝ)
132	16	nngt0d 12312	. . . . 5 ⊢ (𝜑 → 0 < (!‘𝑀))
133		fvex 6919	. . . . . . . 8 ⊢ (!‘𝑀) ∈ V
134	133	tpid2 4774	. . . . . . 7 ⊢ (!‘𝑀) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}
135		supxrub 13362	. . . . . . 7 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ (!‘𝑀) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → (!‘𝑀) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
136	124, 134, 135	sylancl 586	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
137	136, 115	breqtrrdi 5189	. . . . 5 ⊢ (𝜑 → (!‘𝑀) ≤ 𝑇)
138	129, 130, 131, 132, 137	ltletrd 11418	. . . 4 ⊢ (𝜑 → 0 < 𝑇)
139		elnnz 12620	. . . 4 ⊢ (𝑇 ∈ ℕ ↔ (𝑇 ∈ ℤ ∧ 0 < 𝑇))
140	128, 138, 139	sylanbrc 583	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℕ)
141		prmunb 16947	. . 3 ⊢ (𝑇 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑇 < 𝑝)
142	140, 141	syl 17	. 2 ⊢ (𝜑 → ∃𝑝 ∈ ℙ 𝑇 < 𝑝)
143	1	3ad2ant1 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
144		etransclem48.qe0	. . . . 5 ⊢ (𝜑 → (𝑄‘e) = 0)
145	144	3ad2ant1 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑄‘e) = 0)
146		etransclem48.a0	. . . . 5 ⊢ (𝜑 → (𝐴‘0) ≠ 0)
147	146	3ad2ant1 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐴‘0) ≠ 0)
148		simp2 1136	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℙ)
149	9	zcnd 12720	. . . . . . 7 ⊢ (𝜑 → (𝐴‘0) ∈ ℂ)
150	149	3ad2ant1 1132	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐴‘0) ∈ ℂ)
151	150	abscld 15471	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) ∈ ℝ)
152	131	3ad2ant1 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑇 ∈ ℝ)
153		prmz 16708	. . . . . . 7 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
154	153	zred 12719	. . . . . 6 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
155	154	3ad2ant2 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℝ)
156	124	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)
157		fvex 6919	. . . . . . . . 9 ⊢ (abs‘(𝐴‘0)) ∈ V
158	157	tpid1 4772	. . . . . . . 8 ⊢ (abs‘(𝐴‘0)) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}
159		supxrub 13362	. . . . . . . 8 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ (abs‘(𝐴‘0)) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → (abs‘(𝐴‘0)) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
160	156, 158, 159	sylancl 586	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (abs‘(𝐴‘0)) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
161	160, 115	breqtrrdi 5189	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (abs‘(𝐴‘0)) ≤ 𝑇)
162	161	3adant3 1131	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) ≤ 𝑇)
163		simp3 1137	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑇 < 𝑝)
164	151, 152, 155, 162, 163	lelttrd 11416	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) < 𝑝)
165	130	3ad2ant1 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) ∈ ℝ)
166	137	3ad2ant1 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) ≤ 𝑇)
167	165, 152, 155, 166, 163	lelttrd 11416	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) < 𝑝)
168	34	a1i 11	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))))
169		oveq2 7438	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → ((𝑀↑(𝑀 + 1))↑𝑛) = ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)))
170		fveq2 6906	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → (!‘𝑛) = (!‘(𝑝 − 1)))
171	169, 170	oveq12d 7448	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) = (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))))
172	168, 171	oveq12d 7448	. . . . . . . 8 ⊢ (𝑛 = (𝑝 − 1) → (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
173		prmnn 16707	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
174		nnm1nn0 12564	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℕ → (𝑝 − 1) ∈ ℕ0)
175	173, 174	syl 17	. . . . . . . . 9 ⊢ (𝑝 ∈ ℙ → (𝑝 − 1) ∈ ℕ0)
176	175	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ0)
177	58	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
178	54	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀↑(𝑀 + 1)) ∈ ℂ)
179	178, 176	expcld 14182	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) ∈ ℂ)
180	175	faccld 14319	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℕ)
181	180	nncnd 12279	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℂ)
182	181	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ∈ ℂ)
183	180	nnne0d 12313	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ≠ 0)
184	183	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ≠ 0)
185	179, 182, 184	divcld 12040	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))) ∈ ℂ)
186	177, 185	mulcld 11278	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ ℂ)
187	28, 172, 176, 186	fvmptd3 7038	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
188	187	eqcomd 2740	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) = (𝑆‘(𝑝 − 1)))
189	188	3adant3 1131	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) = (𝑆‘(𝑝 − 1)))
190	112	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ ℤ)
191		1zzd 12645	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 1 ∈ ℤ)
192	153, 191	zsubcld 12724	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → (𝑝 − 1) ∈ ℤ)
193	192	3ad2ant2 1133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑝 − 1) ∈ ℤ)
194	190	zred 12719	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ ℝ)
195		tpid3g 4776	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
196	112, 195	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
197		supxrub 13362	. . . . . . . . . . . . . 14 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → 𝐼 ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
198	124, 196, 197	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
199	198, 115	breqtrrdi 5189	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ≤ 𝑇)
200	199	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ≤ 𝑇)
201	194, 152, 155, 200, 163	lelttrd 11416	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 < 𝑝)
202	153	3ad2ant2 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℤ)
203		zltlem1 12667	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℤ ∧ 𝑝 ∈ ℤ) → (𝐼 < 𝑝 ↔ 𝐼 ≤ (𝑝 − 1)))
204	190, 202, 203	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐼 < 𝑝 ↔ 𝐼 ≤ (𝑝 − 1)))
205	201, 204	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ≤ (𝑝 − 1))
206		eluz2 12881	. . . . . . . . 9 ⊢ ((𝑝 − 1) ∈ (ℤ≥‘𝐼) ↔ (𝐼 ∈ ℤ ∧ (𝑝 − 1) ∈ ℤ ∧ 𝐼 ≤ (𝑝 − 1)))
207	190, 193, 205, 206	syl3anbrc 1342	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑝 − 1) ∈ (ℤ≥‘𝐼))
208	111	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
209		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝐼 → (ℤ≥‘𝑖) = (ℤ≥‘𝐼))
210	209	raleqdv 3323	. . . . . . . . . . 11 ⊢ (𝑖 = 𝐼 → (∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1 ↔ ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1))
211	210	elrab 3694	. . . . . . . . . 10 ⊢ (𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ↔ (𝐼 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1))
212	208, 211	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐼 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1))
213	212	simprd 495	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1)
214		nfcv 2902	. . . . . . . . . . 11 ⊢ Ⅎ𝑛abs
215		nfcv 2902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑝 − 1)
216	30, 215	nffv 6916	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑆‘(𝑝 − 1))
217	214, 216	nffv 6916	. . . . . . . . . 10 ⊢ Ⅎ𝑛(abs‘(𝑆‘(𝑝 − 1)))
218		nfcv 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑛 <
219		nfcv 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑛1
220	217, 218, 219	nfbr 5194	. . . . . . . . 9 ⊢ Ⅎ𝑛(abs‘(𝑆‘(𝑝 − 1))) < 1
221		2fveq3 6911	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → (abs‘(𝑆‘𝑛)) = (abs‘(𝑆‘(𝑝 − 1))))
222	221	breq1d 5157	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → ((abs‘(𝑆‘𝑛)) < 1 ↔ (abs‘(𝑆‘(𝑝 − 1))) < 1))
223	220, 222	rspc 3609	. . . . . . . 8 ⊢ ((𝑝 − 1) ∈ (ℤ≥‘𝐼) → (∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1 → (abs‘(𝑆‘(𝑝 − 1))) < 1))
224	207, 213, 223	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝑆‘(𝑝 − 1))) < 1)
225	171	oveq2d 7446	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝 − 1) → (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
226		ovexd 7465	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ V)
227	28, 225, 176, 226	fvmptd3 7038	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) = (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
228	15	nn0red 12585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℝ)
229	228, 53	reexpcld 14199	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ)
230	228, 229	remulcld 11288	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℝ)
231	230	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℝ)
232	49, 231	remulcld 11288	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℝ)
233	35, 232	fsumrecl 15766	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℝ)
234	34, 233	eqeltrid 2842	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℝ)
235	234	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝐶 ∈ ℝ)
236	229	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀↑(𝑀 + 1)) ∈ ℝ)
237	236, 176	reexpcld 14199	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) ∈ ℝ)
238	180	nnred 12278	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℝ)
239	238	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ∈ ℝ)
240	237, 239, 184	redivcld 12092	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))) ∈ ℝ)
241	235, 240	remulcld 11288	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ ℝ)
242	227, 241	eqeltrd 2838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) ∈ ℝ)
243	242	3adant3 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑆‘(𝑝 − 1)) ∈ ℝ)
244		1red 11259	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 1 ∈ ℝ)
245	243, 244	absltd 15464	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → ((abs‘(𝑆‘(𝑝 − 1))) < 1 ↔ (-1 < (𝑆‘(𝑝 − 1)) ∧ (𝑆‘(𝑝 − 1)) < 1)))
246	224, 245	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (-1 < (𝑆‘(𝑝 − 1)) ∧ (𝑆‘(𝑝 − 1)) < 1))
247	246	simprd 495	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑆‘(𝑝 − 1)) < 1)
248	189, 247	eqbrtrd 5169	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) < 1)
249		etransclem6 46195	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑝 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑝)))
250		eqid 2734	. . . 4 ⊢ Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥)
251		eqid 2734	. . . 4 ⊢ (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥) / (!‘(𝑝 − 1))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥) / (!‘(𝑝 − 1)))
252	143, 145, 4, 147, 12, 148, 164, 167, 248, 249, 250, 251	etransclem47 46236	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))
253	252	rexlimdv3a 3156	. 2 ⊢ (𝜑 → (∃𝑝 ∈ ℙ 𝑇 < 𝑝 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1)))
254	142, 253	mpd 15	1 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105   ≠ wne 2937  ∀wral 3058  ∃wrex 3067  {crab 3432  Vcvv 3477   ∖ cdif 3959   ⊆ wss 3962  ∅c0 4338  {csn 4630  {ctp 4634   class class class wbr 5147   ↦ cmpt 5230   Or wor 5595  ⟶wf 6558  ‘cfv 6562  (class class class)co 7430  Fincfn 8983  supcsup 9477  infcinf 9478  ℂcc 11150  ℝcr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157  ℝ^*cxr 11291   < clt 11292   ≤ cle 11293   − cmin 11489  -cneg 11490   / cdiv 11917  ℕcn 12263  ℕ₀cn0 12523  ℤcz 12610  ℤ_≥cuz 12875  ℝ⁺crp 13031  (,)cioo 13383  ...cfz 13543  ↑cexp 14098  !cfa 14308  abscabs 15269   ⇝ cli 15516  Σcsu 15718  ∏cprod 15935  eceu 16094  ℙcprime 16704  ∫citg 25666  0_𝑝c0p 25717  Polycply 26237  coeffccoe 26239  degcdgr 26240  ↑_𝑐ccxp 26611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cc 10472  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-symdif 4258  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-disj 5115  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-ofr 7697  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-oadd 8508  df-omul 8509  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-dju 9938  df-card 9976  df-acn 9979  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-shft 15102  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-sum 15719  df-prod 15936  df-ef 16099  df-e 16100  df-sin 16101  df-cos 16102  df-tan 16103  df-pi 16104  df-dvds 16287  df-gcd 16528  df-prm 16705  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-mulg 19098  df-cntz 19347  df-cmn 19814  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-haus 23338  df-cmp 23410  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-ovol 25512  df-vol 25513  df-mbf 25667  df-itg1 25668  df-itg2 25669  df-ibl 25670  df-itg 25671  df-0p 25718  df-limc 25915  df-dv 25916  df-dvn 25917  df-ply 26241  df-coe 26243  df-dgr 26244  df-log 26612  df-cxp 26613

This theorem is referenced by:  etransc  46238