Theorem etransclem48 46710

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 3901	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
3		0zd 12536	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
4		etransclem48.a	. . . . . . . . . 10 ⊢ 𝐴 = (coeff‘𝑄)
5	4	coef2 26196	. . . . . . . . 9 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ0⟶ℤ)
6	2, 3, 5	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ0⟶ℤ)
7		0nn0 12452	. . . . . . . . 9 ⊢ 0 ∈ ℕ0
8	7	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℕ0)
9	6, 8	ffvelcdmd 7037	. . . . . . 7 ⊢ (𝜑 → (𝐴‘0) ∈ ℤ)
10		zabscl 15275	. . . . . . 7 ⊢ ((𝐴‘0) ∈ ℤ → (abs‘(𝐴‘0)) ∈ ℤ)
11	9, 10	syl 17	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐴‘0)) ∈ ℤ)
12		etransclem48.m	. . . . . . . . 9 ⊢ 𝑀 = (deg‘𝑄)
13		dgrcl 26198	. . . . . . . . . 10 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ0)
14	2, 13	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ0)
15	12, 14	eqeltrid 2840	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
16	15	faccld 14246	. . . . . . 7 ⊢ (𝜑 → (!‘𝑀) ∈ ℕ)
17	16	nnzd 12550	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) ∈ ℤ)
18		ssrab2 4020	. . . . . . . 8 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ ℕ0
19		nn0ssz 12547	. . . . . . . 8 ⊢ ℕ0 ⊆ ℤ
20	18, 19	sstri 3931	. . . . . . 7 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ ℤ
21		etransclem48.i	. . . . . . . 8 ⊢ 𝐼 = inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < )
22		nn0uz 12826	. . . . . . . . . 10 ⊢ ℕ0 = (ℤ≥‘0)
23	18, 22	sseqtri 3970	. . . . . . . . 9 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ (ℤ≥‘0)
24		1rp 12946	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ+
25		nfv 1916	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝜑
26		nfmpt1 5184	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ 𝐶)
27		nfmpt1 5184	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
28		etransclem48.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
29		nfmpt1 5184	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
30	28, 29	nfcxfr 2896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝑆
31		nn0ex 12443	. . . . . . . . . . . . . . . . 17 ⊢ ℕ0 ∈ V
32	31	mptex 7178	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ 𝐶) ∈ V
33	32	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ 𝐶) ∈ V)
34		etransclem48.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1))))
35		fzfid 13935	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
36	6	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ)
37		elfznn0 13574	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
38	37	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
39	36, 38	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
40	39	zcnd 12634	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
41		ere 16054	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ e ∈ ℝ
42	41	recni 11159	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ e ∈ ℂ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ)
44		elfzelz 13478	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
45	44	zcnd 12634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
46	45	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
47	43, 46	cxpcld 26672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈ ℂ)
48	40, 47	mulcld 11165	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑐𝑗)) ∈ ℂ)
49	48	abscld 15401	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈ ℝ)
50	49	recnd 11173	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈ ℂ)
51	15	nn0cnd 12500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
52		peano2nn0 12477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
53	15, 52	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ0)
54	51, 53	expcld 14108	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ)
55	51, 54	mulcld 11165	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
56	55	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
57	50, 56	mulcld 11165	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
58	35, 57	fsumcl 15695	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
59	34, 58	eqeltrid 2840	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℂ)
60		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑛 ∈ ℕ0 ↦ 𝐶) = (𝑛 ∈ ℕ0 ↦ 𝐶))
61		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 = 𝑖) → 𝐶 = 𝐶)
62		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
63	59	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐶 ∈ ℂ)
64	60, 61, 62, 63	fvmptd 6955	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑖) = 𝐶)
65	22, 3, 33, 59, 64	climconst 15505	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ 𝐶) ⇝ 𝐶)
66	31	mptex 7178	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))) ∈ V
67	28, 66	eqeltri 2832	. . . . . . . . . . . . . . 15 ⊢ 𝑆 ∈ V
68	67	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ V)
69		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
70	69	expfac 46085	. . . . . . . . . . . . . . 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 2736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ0 ↦ 𝐶) = (𝑛 ∈ ℕ0 ↦ 𝐶)
75	74	fvmpt2 6959	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ0 ∧ 𝐶 ∈ ℂ) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) = 𝐶)
76	72, 73, 75	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) = 𝐶)
77	76, 73	eqeltrd 2836	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) ∈ ℂ)
78		ovex 7400	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ V
79	69	fvmpt2 6959	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ0 ∧ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ V) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) = (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
80	78, 79	mpan2 692	. . . . . . . . . . . . . . . 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 14108	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑀↑(𝑀 + 1))↑𝑛) ∈ ℂ)
84	72	faccld 14246	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ∈ ℕ)
85	84	nncnd 12190	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ∈ ℂ)
86	84	nnne0d 12227	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ≠ 0)
87	83, 85, 86	divcld 11931	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ ℂ)
88	81, 87	eqeltrd 2836	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) ∈ ℂ)
89		ovex 7400	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ∈ V
90	28	fvmpt2 6959	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ0 ∧ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ∈ V) → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
91	89, 90	mpan2 692	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
92	91	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
93	76, 81	oveq12d 7385	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
94	92, 93	eqtr4d 2774	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)))
95	25, 26, 27, 30, 22, 3, 65, 68, 71, 77, 88, 94	climmulf 46034	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ⇝ (𝐶 · 0))
96	59	mul01d 11345	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 · 0) = 0)
97	95, 96	breqtrd 5111	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ⇝ 0)
98		eqidd 2737	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (𝑆‘𝑛))
99	77, 88	mulcld 11165	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)) ∈ ℂ)
100	94, 99	eqeltrd 2836	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) ∈ ℂ)
101	30, 22, 3, 68, 98, 100	clim0cf 46082	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ⇝ 0 ↔ ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒))
102	97, 101	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒)
103		breq2 5089	. . . . . . . . . . . . 13 ⊢ (𝑒 = 1 → ((abs‘(𝑆‘𝑛)) < 𝑒 ↔ (abs‘(𝑆‘𝑛)) < 1))
104	103	rexralbidv 3203	. . . . . . . . . . . 12 ⊢ (𝑒 = 1 → (∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒 ↔ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1))
105	104	rspcva 3562	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ+ ∧ ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒) → ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
106	24, 102, 105	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
107		rabn0 4329	. . . . . . . . . 10 ⊢ ({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅ ↔ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
108	106, 107	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅)
109		infssuzcl 12882	. . . . . . . . 9 ⊢ (({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ (ℤ≥‘0) ∧ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅) → inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < ) ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
110	23, 108, 109	sylancr 588	. . . . . . . 8 ⊢ (𝜑 → inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < ) ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
111	21, 110	eqeltrid 2840	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
112	20, 111	sselid 3919	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
113		tpssi 4781	. . . . . 6 ⊢ (((abs‘(𝐴‘0)) ∈ ℤ ∧ (!‘𝑀) ∈ ℤ ∧ 𝐼 ∈ ℤ) → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℤ)
114	11, 17, 112, 113	syl3anc 1374	. . . . 5 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℤ)
115		etransclem48.t	. . . . . 6 ⊢ 𝑇 = sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < )
116		xrltso 13092	. . . . . . . 8 ⊢ < Or ℝ*
117	116	a1i 11	. . . . . . 7 ⊢ (𝜑 → < Or ℝ*)
118		tpfi 9236	. . . . . . . 8 ⊢ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin
119	118	a1i 11	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin)
120	11	tpnzd 4724	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ≠ ∅)
121		zssre 12531	. . . . . . . . 9 ⊢ ℤ ⊆ ℝ
122		ressxr 11189	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ*
123	121, 122	sstri 3931	. . . . . . . 8 ⊢ ℤ ⊆ ℝ*
124	114, 123	sstrdi 3934	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)
125		fisupcl 9383	. . . . . . 7 ⊢ (( < Or ℝ* ∧ ({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin ∧ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ≠ ∅ ∧ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)) → sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
126	117, 119, 120, 124, 125	syl13anc 1375	. . . . . 6 ⊢ (𝜑 → sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
127	115, 126	eqeltrid 2840	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
128	114, 127	sseldd 3922	. . . 4 ⊢ (𝜑 → 𝑇 ∈ ℤ)
129		0red 11147	. . . . 5 ⊢ (𝜑 → 0 ∈ ℝ)
130	16	nnred 12189	. . . . 5 ⊢ (𝜑 → (!‘𝑀) ∈ ℝ)
131	128	zred 12633	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℝ)
132	16	nngt0d 12226	. . . . 5 ⊢ (𝜑 → 0 < (!‘𝑀))
133		fvex 6853	. . . . . . . 8 ⊢ (!‘𝑀) ∈ V
134	133	tpid2 4714	. . . . . . 7 ⊢ (!‘𝑀) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}
135		supxrub 13276	. . . . . . 7 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ (!‘𝑀) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → (!‘𝑀) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
136	124, 134, 135	sylancl 587	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
137	136, 115	breqtrrdi 5127	. . . . 5 ⊢ (𝜑 → (!‘𝑀) ≤ 𝑇)
138	129, 130, 131, 132, 137	ltletrd 11306	. . . 4 ⊢ (𝜑 → 0 < 𝑇)
139		elnnz 12534	. . . 4 ⊢ (𝑇 ∈ ℕ ↔ (𝑇 ∈ ℤ ∧ 0 < 𝑇))
140	128, 138, 139	sylanbrc 584	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℕ)
141		prmunb 16885	. . 3 ⊢ (𝑇 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑇 < 𝑝)
142	140, 141	syl 17	. 2 ⊢ (𝜑 → ∃𝑝 ∈ ℙ 𝑇 < 𝑝)
143	1	3ad2ant1 1134	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
144		etransclem48.qe0	. . . . 5 ⊢ (𝜑 → (𝑄‘e) = 0)
145	144	3ad2ant1 1134	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑄‘e) = 0)
146		etransclem48.a0	. . . . 5 ⊢ (𝜑 → (𝐴‘0) ≠ 0)
147	146	3ad2ant1 1134	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐴‘0) ≠ 0)
148		simp2 1138	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℙ)
149	9	zcnd 12634	. . . . . . 7 ⊢ (𝜑 → (𝐴‘0) ∈ ℂ)
150	149	3ad2ant1 1134	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐴‘0) ∈ ℂ)
151	150	abscld 15401	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) ∈ ℝ)
152	131	3ad2ant1 1134	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑇 ∈ ℝ)
153		prmz 16644	. . . . . . 7 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
154	153	zred 12633	. . . . . 6 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
155	154	3ad2ant2 1135	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℝ)
156	124	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)
157		fvex 6853	. . . . . . . . 9 ⊢ (abs‘(𝐴‘0)) ∈ V
158	157	tpid1 4712	. . . . . . . 8 ⊢ (abs‘(𝐴‘0)) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}
159		supxrub 13276	. . . . . . . 8 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ (abs‘(𝐴‘0)) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → (abs‘(𝐴‘0)) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
160	156, 158, 159	sylancl 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (abs‘(𝐴‘0)) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
161	160, 115	breqtrrdi 5127	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (abs‘(𝐴‘0)) ≤ 𝑇)
162	161	3adant3 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) ≤ 𝑇)
163		simp3 1139	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑇 < 𝑝)
164	151, 152, 155, 162, 163	lelttrd 11304	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) < 𝑝)
165	130	3ad2ant1 1134	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) ∈ ℝ)
166	137	3ad2ant1 1134	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) ≤ 𝑇)
167	165, 152, 155, 166, 163	lelttrd 11304	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) < 𝑝)
168	34	a1i 11	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))))
169		oveq2 7375	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → ((𝑀↑(𝑀 + 1))↑𝑛) = ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)))
170		fveq2 6840	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → (!‘𝑛) = (!‘(𝑝 − 1)))
171	169, 170	oveq12d 7385	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) = (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))))
172	168, 171	oveq12d 7385	. . . . . . . 8 ⊢ (𝑛 = (𝑝 − 1) → (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
173		prmnn 16643	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
174		nnm1nn0 12478	. . . . . . . . . 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 14108	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) ∈ ℂ)
180	175	faccld 14246	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℕ)
181	180	nncnd 12190	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℂ)
182	181	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ∈ ℂ)
183	180	nnne0d 12227	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ≠ 0)
184	183	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ≠ 0)
185	179, 182, 184	divcld 11931	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))) ∈ ℂ)
186	177, 185	mulcld 11165	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ ℂ)
187	28, 172, 176, 186	fvmptd3 6971	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
188	187	eqcomd 2742	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) = (𝑆‘(𝑝 − 1)))
189	188	3adant3 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) = (𝑆‘(𝑝 − 1)))
190	112	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ ℤ)
191		1zzd 12558	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 1 ∈ ℤ)
192	153, 191	zsubcld 12638	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → (𝑝 − 1) ∈ ℤ)
193	192	3ad2ant2 1135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑝 − 1) ∈ ℤ)
194	190	zred 12633	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ ℝ)
195		tpid3g 4716	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
196	112, 195	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
197		supxrub 13276	. . . . . . . . . . . . . 14 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → 𝐼 ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
198	124, 196, 197	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
199	198, 115	breqtrrdi 5127	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ≤ 𝑇)
200	199	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ≤ 𝑇)
201	194, 152, 155, 200, 163	lelttrd 11304	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 < 𝑝)
202	153	3ad2ant2 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℤ)
203		zltlem1 12580	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℤ ∧ 𝑝 ∈ ℤ) → (𝐼 < 𝑝 ↔ 𝐼 ≤ (𝑝 − 1)))
204	190, 202, 203	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐼 < 𝑝 ↔ 𝐼 ≤ (𝑝 − 1)))
205	201, 204	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ≤ (𝑝 − 1))
206		eluz2 12794	. . . . . . . . 9 ⊢ ((𝑝 − 1) ∈ (ℤ≥‘𝐼) ↔ (𝐼 ∈ ℤ ∧ (𝑝 − 1) ∈ ℤ ∧ 𝐼 ≤ (𝑝 − 1)))
207	190, 193, 205, 206	syl3anbrc 1345	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑝 − 1) ∈ (ℤ≥‘𝐼))
208	111	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
209		fveq2 6840	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝐼 → (ℤ≥‘𝑖) = (ℤ≥‘𝐼))
210	209	raleqdv 3295	. . . . . . . . . . 11 ⊢ (𝑖 = 𝐼 → (∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1 ↔ ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1))
211	210	elrab 3634	. . . . . . . . . 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 2898	. . . . . . . . . . 11 ⊢ Ⅎ𝑛abs
215		nfcv 2898	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑝 − 1)
216	30, 215	nffv 6850	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑆‘(𝑝 − 1))
217	214, 216	nffv 6850	. . . . . . . . . 10 ⊢ Ⅎ𝑛(abs‘(𝑆‘(𝑝 − 1)))
218		nfcv 2898	. . . . . . . . . 10 ⊢ Ⅎ𝑛 <
219		nfcv 2898	. . . . . . . . . 10 ⊢ Ⅎ𝑛1
220	217, 218, 219	nfbr 5132	. . . . . . . . 9 ⊢ Ⅎ𝑛(abs‘(𝑆‘(𝑝 − 1))) < 1
221		2fveq3 6845	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → (abs‘(𝑆‘𝑛)) = (abs‘(𝑆‘(𝑝 − 1))))
222	221	breq1d 5095	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → ((abs‘(𝑆‘𝑛)) < 1 ↔ (abs‘(𝑆‘(𝑝 − 1))) < 1))
223	220, 222	rspc 3552	. . . . . . . 8 ⊢ ((𝑝 − 1) ∈ (ℤ≥‘𝐼) → (∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1 → (abs‘(𝑆‘(𝑝 − 1))) < 1))
224	207, 213, 223	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝑆‘(𝑝 − 1))) < 1)
225	171	oveq2d 7383	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝 − 1) → (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
226		ovexd 7402	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ V)
227	28, 225, 176, 226	fvmptd3 6971	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) = (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
228	15	nn0red 12499	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℝ)
229	228, 53	reexpcld 14125	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ)
230	228, 229	remulcld 11175	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℝ)
231	230	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℝ)
232	49, 231	remulcld 11175	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℝ)
233	35, 232	fsumrecl 15696	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℝ)
234	34, 233	eqeltrid 2840	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℝ)
235	234	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝐶 ∈ ℝ)
236	229	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀↑(𝑀 + 1)) ∈ ℝ)
237	236, 176	reexpcld 14125	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) ∈ ℝ)
238	180	nnred 12189	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℝ)
239	238	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ∈ ℝ)
240	237, 239, 184	redivcld 11983	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))) ∈ ℝ)
241	235, 240	remulcld 11175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ ℝ)
242	227, 241	eqeltrd 2836	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) ∈ ℝ)
243	242	3adant3 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑆‘(𝑝 − 1)) ∈ ℝ)
244		1red 11145	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 1 ∈ ℝ)
245	243, 244	absltd 15394	. . . . . . 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 5107	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) < 1)
249		etransclem6 46668	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑝 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑝)))
250		eqid 2736	. . . 4 ⊢ Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥)
251		eqid 2736	. . . 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 46709	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))
253	252	rexlimdv3a 3142	. 2 ⊢ (𝜑 → (∃𝑝 ∈ ℙ 𝑇 < 𝑝 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1)))
254	142, 253	mpd 15	1 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2932  ∀wral 3051  ∃wrex 3061  {crab 3389  Vcvv 3429   ∖ cdif 3886   ⊆ wss 3889  ∅c0 4273  {csn 4567  {ctp 4571   class class class wbr 5085   ↦ cmpt 5166   Or wor 5538  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367  Fincfn 8893  supcsup 9353  infcinf 9354  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043  ℝ^*cxr 11178   < clt 11179   ≤ cle 11180   − cmin 11377  -cneg 11378   / cdiv 11807  ℕcn 12174  ℕ₀cn0 12437  ℤcz 12524  ℤ_≥cuz 12788  ℝ⁺crp 12942  (,)cioo 13298  ...cfz 13461  ↑cexp 14023  !cfa 14235  abscabs 15196   ⇝ cli 15446  Σcsu 15648  ∏cprod 15868  eceu 16027  ℙcprime 16640  ∫citg 25585  0_𝑝c0p 25636  Polycply 26149  coeffccoe 26151  degcdgr 26152  ↑_𝑐ccxp 26519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-inf2 9562  ax-cc 10357  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-symdif 4193  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-iin 4936  df-disj 5053  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  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 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-ofr 7632  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-oadd 8409  df-omul 8410  df-er 8643  df-map 8775  df-pm 8776  df-ixp 8846  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-fi 9324  df-sup 9355  df-inf 9356  df-oi 9425  df-dju 9825  df-card 9863  df-acn 9866  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-z 12525  df-dec 12645  df-uz 12789  df-q 12899  df-rp 12943  df-xneg 13063  df-xadd 13064  df-xmul 13065  df-ioo 13302  df-ioc 13303  df-ico 13304  df-icc 13305  df-fz 13462  df-fzo 13609  df-fl 13751  df-mod 13829  df-seq 13964  df-exp 14024  df-fac 14236  df-bc 14265  df-hash 14293  df-shft 15029  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198  df-limsup 15433  df-clim 15450  df-rlim 15451  df-sum 15649  df-prod 15869  df-ef 16032  df-e 16033  df-sin 16034  df-cos 16035  df-tan 16036  df-pi 16037  df-dvds 16222  df-gcd 16464  df-prm 16641  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-starv 17235  df-sca 17236  df-vsca 17237  df-ip 17238  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-hom 17244  df-cco 17245  df-rest 17385  df-topn 17386  df-0g 17404  df-gsum 17405  df-topgen 17406  df-pt 17407  df-prds 17410  df-xrs 17466  df-qtop 17471  df-imas 17472  df-xps 17474  df-mre 17548  df-mrc 17549  df-acs 17551  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-submnd 18752  df-mulg 19044  df-cntz 19292  df-cmn 19757  df-psmet 21344  df-xmet 21345  df-met 21346  df-bl 21347  df-mopn 21348  df-fbas 21349  df-fg 21350  df-cnfld 21353  df-top 22859  df-topon 22876  df-topsp 22898  df-bases 22911  df-cld 22984  df-ntr 22985  df-cls 22986  df-nei 23063  df-lp 23101  df-perf 23102  df-cn 23192  df-cnp 23193  df-haus 23280  df-cmp 23352  df-tx 23527  df-hmeo 23720  df-fil 23811  df-fm 23903  df-flim 23904  df-flf 23905  df-xms 24285  df-ms 24286  df-tms 24287  df-cncf 24845  df-ovol 25431  df-vol 25432  df-mbf 25586  df-itg1 25587  df-itg2 25588  df-ibl 25589  df-itg 25590  df-0p 25637  df-limc 25833  df-dv 25834  df-dvn 25835  df-ply 26153  df-coe 26155  df-dgr 26156  df-log 26520  df-cxp 26521

This theorem is referenced by:  etransc  46711