Theorem etransclem48 46273

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 3923	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
3		0zd 12517	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
4		etransclem48.a	. . . . . . . . . 10 ⊢ 𝐴 = (coeff‘𝑄)
5	4	coef2 26169	. . . . . . . . 9 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ0⟶ℤ)
6	2, 3, 5	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ0⟶ℤ)
7		0nn0 12433	. . . . . . . . 9 ⊢ 0 ∈ ℕ0
8	7	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℕ0)
9	6, 8	ffvelcdmd 7039	. . . . . . 7 ⊢ (𝜑 → (𝐴‘0) ∈ ℤ)
10		zabscl 15255	. . . . . . 7 ⊢ ((𝐴‘0) ∈ ℤ → (abs‘(𝐴‘0)) ∈ ℤ)
11	9, 10	syl 17	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐴‘0)) ∈ ℤ)
12		etransclem48.m	. . . . . . . . 9 ⊢ 𝑀 = (deg‘𝑄)
13		dgrcl 26171	. . . . . . . . . 10 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ0)
14	2, 13	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ0)
15	12, 14	eqeltrid 2832	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
16	15	faccld 14225	. . . . . . 7 ⊢ (𝜑 → (!‘𝑀) ∈ ℕ)
17	16	nnzd 12532	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) ∈ ℤ)
18		ssrab2 4039	. . . . . . . 8 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ ℕ0
19		nn0ssz 12528	. . . . . . . 8 ⊢ ℕ0 ⊆ ℤ
20	18, 19	sstri 3953	. . . . . . 7 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ ℤ
21		etransclem48.i	. . . . . . . 8 ⊢ 𝐼 = inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < )
22		nn0uz 12811	. . . . . . . . . 10 ⊢ ℕ0 = (ℤ≥‘0)
23	18, 22	sseqtri 3992	. . . . . . . . 9 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ (ℤ≥‘0)
24		1rp 12931	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ+
25		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝜑
26		nfmpt1 5201	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ 𝐶)
27		nfmpt1 5201	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
28		etransclem48.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
29		nfmpt1 5201	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
30	28, 29	nfcxfr 2889	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝑆
31		nn0ex 12424	. . . . . . . . . . . . . . . . 17 ⊢ ℕ0 ∈ V
32	31	mptex 7179	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ 𝐶) ∈ V
33	32	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ 𝐶) ∈ V)
34		etransclem48.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1))))
35		fzfid 13914	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
36	6	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ)
37		elfznn0 13557	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
38	37	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
39	36, 38	ffvelcdmd 7039	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
40	39	zcnd 12615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
41		ere 16031	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ e ∈ ℝ
42	41	recni 11164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ e ∈ ℂ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ)
44		elfzelz 13461	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
45	44	zcnd 12615	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
46	45	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
47	43, 46	cxpcld 26650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈ ℂ)
48	40, 47	mulcld 11170	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑐𝑗)) ∈ ℂ)
49	48	abscld 15381	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈ ℝ)
50	49	recnd 11178	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈ ℂ)
51	15	nn0cnd 12481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
52		peano2nn0 12458	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
53	15, 52	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ0)
54	51, 53	expcld 14087	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ)
55	51, 54	mulcld 11170	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
56	55	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
57	50, 56	mulcld 11170	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
58	35, 57	fsumcl 15675	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
59	34, 58	eqeltrid 2832	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℂ)
60		eqidd 2730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑛 ∈ ℕ0 ↦ 𝐶) = (𝑛 ∈ ℕ0 ↦ 𝐶))
61		eqidd 2730	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 = 𝑖) → 𝐶 = 𝐶)
62		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
63	59	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐶 ∈ ℂ)
64	60, 61, 62, 63	fvmptd 6957	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑖) = 𝐶)
65	22, 3, 33, 59, 64	climconst 15485	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ 𝐶) ⇝ 𝐶)
66	31	mptex 7179	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))) ∈ V
67	28, 66	eqeltri 2824	. . . . . . . . . . . . . . 15 ⊢ 𝑆 ∈ V
68	67	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ V)
69		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
70	69	expfac 45648	. . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ0 ↦ 𝐶) = (𝑛 ∈ ℕ0 ↦ 𝐶)
75	74	fvmpt2 6961	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ0 ∧ 𝐶 ∈ ℂ) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) = 𝐶)
76	72, 73, 75	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) = 𝐶)
77	76, 73	eqeltrd 2828	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) ∈ ℂ)
78		ovex 7402	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ V
79	69	fvmpt2 6961	. . . . . . . . . . . . . . . . 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 14087	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑀↑(𝑀 + 1))↑𝑛) ∈ ℂ)
84	72	faccld 14225	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ∈ ℕ)
85	84	nncnd 12178	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ∈ ℂ)
86	84	nnne0d 12212	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ≠ 0)
87	83, 85, 86	divcld 11934	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ ℂ)
88	81, 87	eqeltrd 2828	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) ∈ ℂ)
89		ovex 7402	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ∈ V
90	28	fvmpt2 6961	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ0 ∧ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ∈ V) → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
91	89, 90	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
92	91	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
93	76, 81	oveq12d 7387	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
94	92, 93	eqtr4d 2767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)))
95	25, 26, 27, 30, 22, 3, 65, 68, 71, 77, 88, 94	climmulf 45595	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ⇝ (𝐶 · 0))
96	59	mul01d 11349	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 · 0) = 0)
97	95, 96	breqtrd 5128	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ⇝ 0)
98		eqidd 2730	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (𝑆‘𝑛))
99	77, 88	mulcld 11170	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)) ∈ ℂ)
100	94, 99	eqeltrd 2828	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) ∈ ℂ)
101	30, 22, 3, 68, 98, 100	clim0cf 45645	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ⇝ 0 ↔ ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒))
102	97, 101	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒)
103		breq2 5106	. . . . . . . . . . . . 13 ⊢ (𝑒 = 1 → ((abs‘(𝑆‘𝑛)) < 𝑒 ↔ (abs‘(𝑆‘𝑛)) < 1))
104	103	rexralbidv 3201	. . . . . . . . . . . 12 ⊢ (𝑒 = 1 → (∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒 ↔ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1))
105	104	rspcva 3583	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ+ ∧ ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒) → ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
106	24, 102, 105	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
107		rabn0 4348	. . . . . . . . . 10 ⊢ ({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅ ↔ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
108	106, 107	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅)
109		infssuzcl 12867	. . . . . . . . 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 2832	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
112	20, 111	sselid 3941	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
113		tpssi 4798	. . . . . 6 ⊢ (((abs‘(𝐴‘0)) ∈ ℤ ∧ (!‘𝑀) ∈ ℤ ∧ 𝐼 ∈ ℤ) → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℤ)
114	11, 17, 112, 113	syl3anc 1373	. . . . 5 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℤ)
115		etransclem48.t	. . . . . 6 ⊢ 𝑇 = sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < )
116		xrltso 13077	. . . . . . . 8 ⊢ < Or ℝ*
117	116	a1i 11	. . . . . . 7 ⊢ (𝜑 → < Or ℝ*)
118		tpfi 9252	. . . . . . . 8 ⊢ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin
119	118	a1i 11	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin)
120	11	tpnzd 4740	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ≠ ∅)
121		zssre 12512	. . . . . . . . 9 ⊢ ℤ ⊆ ℝ
122		ressxr 11194	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ*
123	121, 122	sstri 3953	. . . . . . . 8 ⊢ ℤ ⊆ ℝ*
124	114, 123	sstrdi 3956	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)
125		fisupcl 9397	. . . . . . 7 ⊢ (( < Or ℝ* ∧ ({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin ∧ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ≠ ∅ ∧ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)) → sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
126	117, 119, 120, 124, 125	syl13anc 1374	. . . . . 6 ⊢ (𝜑 → sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
127	115, 126	eqeltrid 2832	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
128	114, 127	sseldd 3944	. . . 4 ⊢ (𝜑 → 𝑇 ∈ ℤ)
129		0red 11153	. . . . 5 ⊢ (𝜑 → 0 ∈ ℝ)
130	16	nnred 12177	. . . . 5 ⊢ (𝜑 → (!‘𝑀) ∈ ℝ)
131	128	zred 12614	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℝ)
132	16	nngt0d 12211	. . . . 5 ⊢ (𝜑 → 0 < (!‘𝑀))
133		fvex 6853	. . . . . . . 8 ⊢ (!‘𝑀) ∈ V
134	133	tpid2 4730	. . . . . . 7 ⊢ (!‘𝑀) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}
135		supxrub 13260	. . . . . . 7 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ (!‘𝑀) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → (!‘𝑀) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
136	124, 134, 135	sylancl 586	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
137	136, 115	breqtrrdi 5144	. . . . 5 ⊢ (𝜑 → (!‘𝑀) ≤ 𝑇)
138	129, 130, 131, 132, 137	ltletrd 11310	. . . 4 ⊢ (𝜑 → 0 < 𝑇)
139		elnnz 12515	. . . 4 ⊢ (𝑇 ∈ ℕ ↔ (𝑇 ∈ ℤ ∧ 0 < 𝑇))
140	128, 138, 139	sylanbrc 583	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℕ)
141		prmunb 16861	. . 3 ⊢ (𝑇 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑇 < 𝑝)
142	140, 141	syl 17	. 2 ⊢ (𝜑 → ∃𝑝 ∈ ℙ 𝑇 < 𝑝)
143	1	3ad2ant1 1133	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
144		etransclem48.qe0	. . . . 5 ⊢ (𝜑 → (𝑄‘e) = 0)
145	144	3ad2ant1 1133	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑄‘e) = 0)
146		etransclem48.a0	. . . . 5 ⊢ (𝜑 → (𝐴‘0) ≠ 0)
147	146	3ad2ant1 1133	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐴‘0) ≠ 0)
148		simp2 1137	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℙ)
149	9	zcnd 12615	. . . . . . 7 ⊢ (𝜑 → (𝐴‘0) ∈ ℂ)
150	149	3ad2ant1 1133	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐴‘0) ∈ ℂ)
151	150	abscld 15381	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) ∈ ℝ)
152	131	3ad2ant1 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑇 ∈ ℝ)
153		prmz 16621	. . . . . . 7 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
154	153	zred 12614	. . . . . 6 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
155	154	3ad2ant2 1134	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℝ)
156	124	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)
157		fvex 6853	. . . . . . . . 9 ⊢ (abs‘(𝐴‘0)) ∈ V
158	157	tpid1 4728	. . . . . . . 8 ⊢ (abs‘(𝐴‘0)) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}
159		supxrub 13260	. . . . . . . 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 5144	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (abs‘(𝐴‘0)) ≤ 𝑇)
162	161	3adant3 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) ≤ 𝑇)
163		simp3 1138	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑇 < 𝑝)
164	151, 152, 155, 162, 163	lelttrd 11308	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) < 𝑝)
165	130	3ad2ant1 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) ∈ ℝ)
166	137	3ad2ant1 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) ≤ 𝑇)
167	165, 152, 155, 166, 163	lelttrd 11308	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) < 𝑝)
168	34	a1i 11	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))))
169		oveq2 7377	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → ((𝑀↑(𝑀 + 1))↑𝑛) = ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)))
170		fveq2 6840	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → (!‘𝑛) = (!‘(𝑝 − 1)))
171	169, 170	oveq12d 7387	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) = (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))))
172	168, 171	oveq12d 7387	. . . . . . . 8 ⊢ (𝑛 = (𝑝 − 1) → (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
173		prmnn 16620	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
174		nnm1nn0 12459	. . . . . . . . . 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 14087	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) ∈ ℂ)
180	175	faccld 14225	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℕ)
181	180	nncnd 12178	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℂ)
182	181	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ∈ ℂ)
183	180	nnne0d 12212	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ≠ 0)
184	183	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ≠ 0)
185	179, 182, 184	divcld 11934	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))) ∈ ℂ)
186	177, 185	mulcld 11170	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ ℂ)
187	28, 172, 176, 186	fvmptd3 6973	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
188	187	eqcomd 2735	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) = (𝑆‘(𝑝 − 1)))
189	188	3adant3 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) = (𝑆‘(𝑝 − 1)))
190	112	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ ℤ)
191		1zzd 12540	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 1 ∈ ℤ)
192	153, 191	zsubcld 12619	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → (𝑝 − 1) ∈ ℤ)
193	192	3ad2ant2 1134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑝 − 1) ∈ ℤ)
194	190	zred 12614	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ ℝ)
195		tpid3g 4732	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
196	112, 195	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
197		supxrub 13260	. . . . . . . . . . . . . 14 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → 𝐼 ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
198	124, 196, 197	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
199	198, 115	breqtrrdi 5144	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ≤ 𝑇)
200	199	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ≤ 𝑇)
201	194, 152, 155, 200, 163	lelttrd 11308	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 < 𝑝)
202	153	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℤ)
203		zltlem1 12562	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℤ ∧ 𝑝 ∈ ℤ) → (𝐼 < 𝑝 ↔ 𝐼 ≤ (𝑝 − 1)))
204	190, 202, 203	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐼 < 𝑝 ↔ 𝐼 ≤ (𝑝 − 1)))
205	201, 204	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ≤ (𝑝 − 1))
206		eluz2 12775	. . . . . . . . 9 ⊢ ((𝑝 − 1) ∈ (ℤ≥‘𝐼) ↔ (𝐼 ∈ ℤ ∧ (𝑝 − 1) ∈ ℤ ∧ 𝐼 ≤ (𝑝 − 1)))
207	190, 193, 205, 206	syl3anbrc 1344	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑝 − 1) ∈ (ℤ≥‘𝐼))
208	111	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
209		fveq2 6840	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝐼 → (ℤ≥‘𝑖) = (ℤ≥‘𝐼))
210	209	raleqdv 3296	. . . . . . . . . . 11 ⊢ (𝑖 = 𝐼 → (∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1 ↔ ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1))
211	210	elrab 3656	. . . . . . . . . 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 2891	. . . . . . . . . . 11 ⊢ Ⅎ𝑛abs
215		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑝 − 1)
216	30, 215	nffv 6850	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑆‘(𝑝 − 1))
217	214, 216	nffv 6850	. . . . . . . . . 10 ⊢ Ⅎ𝑛(abs‘(𝑆‘(𝑝 − 1)))
218		nfcv 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑛 <
219		nfcv 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑛1
220	217, 218, 219	nfbr 5149	. . . . . . . . 9 ⊢ Ⅎ𝑛(abs‘(𝑆‘(𝑝 − 1))) < 1
221		2fveq3 6845	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → (abs‘(𝑆‘𝑛)) = (abs‘(𝑆‘(𝑝 − 1))))
222	221	breq1d 5112	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → ((abs‘(𝑆‘𝑛)) < 1 ↔ (abs‘(𝑆‘(𝑝 − 1))) < 1))
223	220, 222	rspc 3573	. . . . . . . 8 ⊢ ((𝑝 − 1) ∈ (ℤ≥‘𝐼) → (∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1 → (abs‘(𝑆‘(𝑝 − 1))) < 1))
224	207, 213, 223	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝑆‘(𝑝 − 1))) < 1)
225	171	oveq2d 7385	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝 − 1) → (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
226		ovexd 7404	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ V)
227	28, 225, 176, 226	fvmptd3 6973	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) = (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
228	15	nn0red 12480	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℝ)
229	228, 53	reexpcld 14104	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ)
230	228, 229	remulcld 11180	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℝ)
231	230	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℝ)
232	49, 231	remulcld 11180	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℝ)
233	35, 232	fsumrecl 15676	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℝ)
234	34, 233	eqeltrid 2832	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℝ)
235	234	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝐶 ∈ ℝ)
236	229	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀↑(𝑀 + 1)) ∈ ℝ)
237	236, 176	reexpcld 14104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) ∈ ℝ)
238	180	nnred 12177	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℝ)
239	238	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ∈ ℝ)
240	237, 239, 184	redivcld 11986	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))) ∈ ℝ)
241	235, 240	remulcld 11180	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ ℝ)
242	227, 241	eqeltrd 2828	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) ∈ ℝ)
243	242	3adant3 1132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑆‘(𝑝 − 1)) ∈ ℝ)
244		1red 11151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 1 ∈ ℝ)
245	243, 244	absltd 15374	. . . . . . 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 5124	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) < 1)
249		etransclem6 46231	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑝 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑝)))
250		eqid 2729	. . . 4 ⊢ Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥)
251		eqid 2729	. . . 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 46272	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))
253	252	rexlimdv3a 3138	. 2 ⊢ (𝜑 → (∃𝑝 ∈ ℙ 𝑇 < 𝑝 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1)))
254	142, 253	mpd 15	1 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3402  Vcvv 3444   ∖ cdif 3908   ⊆ wss 3911  ∅c0 4292  {csn 4585  {ctp 4589   class class class wbr 5102   ↦ cmpt 5183   Or wor 5538  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369  Fincfn 8895  supcsup 9367  infcinf 9368  ℂcc 11042  ℝcr 11043  0cc0 11044  1c1 11045   + caddc 11047   · cmul 11049  ℝ^*cxr 11183   < clt 11184   ≤ cle 11185   − cmin 11381  -cneg 11382   / cdiv 11811  ℕcn 12162  ℕ₀cn0 12418  ℤcz 12505  ℤ_≥cuz 12769  ℝ⁺crp 12927  (,)cioo 13282  ...cfz 13444  ↑cexp 14002  !cfa 14214  abscabs 15176   ⇝ cli 15426  Σcsu 15628  ∏cprod 15845  eceu 16004  ℙcprime 16617  ∫citg 25552  0_𝑝c0p 25603  Polycply 26122  coeffccoe 26124  degcdgr 26125  ↑_𝑐ccxp 26497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-inf2 9570  ax-cc 10364  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122  ax-addf 11123

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-symdif 4212  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-disj 5070  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-ofr 7634  df-om 7823  df-1st 7947  df-2nd 7948  df-supp 8117  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-2o 8412  df-oadd 8415  df-omul 8416  df-er 8648  df-map 8778  df-pm 8779  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9289  df-fi 9338  df-sup 9369  df-inf 9370  df-oi 9439  df-dju 9830  df-card 9868  df-acn 9871  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12419  df-z 12506  df-dec 12626  df-uz 12770  df-q 12884  df-rp 12928  df-xneg 13048  df-xadd 13049  df-xmul 13050  df-ioo 13286  df-ioc 13287  df-ico 13288  df-icc 13289  df-fz 13445  df-fzo 13592  df-fl 13730  df-mod 13808  df-seq 13943  df-exp 14003  df-fac 14215  df-bc 14244  df-hash 14272  df-shft 15009  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178  df-limsup 15413  df-clim 15430  df-rlim 15431  df-sum 15629  df-prod 15846  df-ef 16009  df-e 16010  df-sin 16011  df-cos 16012  df-tan 16013  df-pi 16014  df-dvds 16199  df-gcd 16441  df-prm 16618  df-struct 17093  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17361  df-topn 17362  df-0g 17380  df-gsum 17381  df-topgen 17382  df-pt 17383  df-prds 17386  df-xrs 17441  df-qtop 17446  df-imas 17447  df-xps 17449  df-mre 17523  df-mrc 17524  df-acs 17526  df-mgm 18549  df-sgrp 18628  df-mnd 18644  df-submnd 18693  df-mulg 18982  df-cntz 19231  df-cmn 19696  df-psmet 21288  df-xmet 21289  df-met 21290  df-bl 21291  df-mopn 21292  df-fbas 21293  df-fg 21294  df-cnfld 21297  df-top 22814  df-topon 22831  df-topsp 22853  df-bases 22866  df-cld 22939  df-ntr 22940  df-cls 22941  df-nei 23018  df-lp 23056  df-perf 23057  df-cn 23147  df-cnp 23148  df-haus 23235  df-cmp 23307  df-tx 23482  df-hmeo 23675  df-fil 23766  df-fm 23858  df-flim 23859  df-flf 23860  df-xms 24241  df-ms 24242  df-tms 24243  df-cncf 24804  df-ovol 25398  df-vol 25399  df-mbf 25553  df-itg1 25554  df-itg2 25555  df-ibl 25556  df-itg 25557  df-0p 25604  df-limc 25800  df-dv 25801  df-dvn 25802  df-ply 26126  df-coe 26128  df-dgr 26129  df-log 26498  df-cxp 26499

This theorem is referenced by:  etransc  46274