Theorem etransclem48 46203

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 3988	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
3		0zd 12651	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
4		etransclem48.a	. . . . . . . . . 10 ⊢ 𝐴 = (coeff‘𝑄)
5	4	coef2 26290	. . . . . . . . 9 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ0⟶ℤ)
6	2, 3, 5	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ0⟶ℤ)
7		0nn0 12568	. . . . . . . . 9 ⊢ 0 ∈ ℕ0
8	7	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℕ0)
9	6, 8	ffvelcdmd 7119	. . . . . . 7 ⊢ (𝜑 → (𝐴‘0) ∈ ℤ)
10		zabscl 15362	. . . . . . 7 ⊢ ((𝐴‘0) ∈ ℤ → (abs‘(𝐴‘0)) ∈ ℤ)
11	9, 10	syl 17	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐴‘0)) ∈ ℤ)
12		etransclem48.m	. . . . . . . . 9 ⊢ 𝑀 = (deg‘𝑄)
13		dgrcl 26292	. . . . . . . . . 10 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ0)
14	2, 13	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ0)
15	12, 14	eqeltrid 2848	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
16	15	faccld 14333	. . . . . . 7 ⊢ (𝜑 → (!‘𝑀) ∈ ℕ)
17	16	nnzd 12666	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) ∈ ℤ)
18		ssrab2 4103	. . . . . . . 8 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ ℕ0
19		nn0ssz 12662	. . . . . . . 8 ⊢ ℕ0 ⊆ ℤ
20	18, 19	sstri 4018	. . . . . . 7 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ ℤ
21		etransclem48.i	. . . . . . . 8 ⊢ 𝐼 = inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < )
22		nn0uz 12945	. . . . . . . . . 10 ⊢ ℕ0 = (ℤ≥‘0)
23	18, 22	sseqtri 4045	. . . . . . . . 9 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ (ℤ≥‘0)
24		1rp 13061	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ+
25		nfv 1913	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝜑
26		nfmpt1 5274	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ 𝐶)
27		nfmpt1 5274	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
28		etransclem48.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
29		nfmpt1 5274	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
30	28, 29	nfcxfr 2906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝑆
31		nn0ex 12559	. . . . . . . . . . . . . . . . 17 ⊢ ℕ0 ∈ V
32	31	mptex 7260	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ 𝐶) ∈ V
33	32	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ 𝐶) ∈ V)
34		etransclem48.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1))))
35		fzfid 14024	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
36	6	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ)
37		elfznn0 13677	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
38	37	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
39	36, 38	ffvelcdmd 7119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
40	39	zcnd 12748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
41		ere 16137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ e ∈ ℝ
42	41	recni 11304	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ e ∈ ℂ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ)
44		elfzelz 13584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
45	44	zcnd 12748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
46	45	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
47	43, 46	cxpcld 26768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈ ℂ)
48	40, 47	mulcld 11310	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑐𝑗)) ∈ ℂ)
49	48	abscld 15485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈ ℝ)
50	49	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈ ℂ)
51	15	nn0cnd 12615	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
52		peano2nn0 12593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
53	15, 52	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ0)
54	51, 53	expcld 14196	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ)
55	51, 54	mulcld 11310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
56	55	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
57	50, 56	mulcld 11310	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
58	35, 57	fsumcl 15781	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
59	34, 58	eqeltrid 2848	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℂ)
60		eqidd 2741	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑛 ∈ ℕ0 ↦ 𝐶) = (𝑛 ∈ ℕ0 ↦ 𝐶))
61		eqidd 2741	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 = 𝑖) → 𝐶 = 𝐶)
62		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
63	59	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐶 ∈ ℂ)
64	60, 61, 62, 63	fvmptd 7036	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑖) = 𝐶)
65	22, 3, 33, 59, 64	climconst 15589	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ 𝐶) ⇝ 𝐶)
66	31	mptex 7260	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))) ∈ V
67	28, 66	eqeltri 2840	. . . . . . . . . . . . . . 15 ⊢ 𝑆 ∈ V
68	67	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ V)
69		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
70	69	expfac 45578	. . . . . . . . . . . . . . 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 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ0 ↦ 𝐶) = (𝑛 ∈ ℕ0 ↦ 𝐶)
75	74	fvmpt2 7040	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ0 ∧ 𝐶 ∈ ℂ) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) = 𝐶)
76	72, 73, 75	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) = 𝐶)
77	76, 73	eqeltrd 2844	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) ∈ ℂ)
78		ovex 7481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ V
79	69	fvmpt2 7040	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ0 ∧ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ V) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) = (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
80	78, 79	mpan2 690	. . . . . . . . . . . . . . . 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 14196	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑀↑(𝑀 + 1))↑𝑛) ∈ ℂ)
84	72	faccld 14333	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ∈ ℕ)
85	84	nncnd 12309	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ∈ ℂ)
86	84	nnne0d 12343	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ≠ 0)
87	83, 85, 86	divcld 12070	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ ℂ)
88	81, 87	eqeltrd 2844	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) ∈ ℂ)
89		ovex 7481	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ∈ V
90	28	fvmpt2 7040	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ0 ∧ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ∈ V) → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
91	89, 90	mpan2 690	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
92	91	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
93	76, 81	oveq12d 7466	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
94	92, 93	eqtr4d 2783	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)))
95	25, 26, 27, 30, 22, 3, 65, 68, 71, 77, 88, 94	climmulf 45525	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ⇝ (𝐶 · 0))
96	59	mul01d 11489	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 · 0) = 0)
97	95, 96	breqtrd 5192	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ⇝ 0)
98		eqidd 2741	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (𝑆‘𝑛))
99	77, 88	mulcld 11310	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)) ∈ ℂ)
100	94, 99	eqeltrd 2844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) ∈ ℂ)
101	30, 22, 3, 68, 98, 100	clim0cf 45575	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ⇝ 0 ↔ ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒))
102	97, 101	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒)
103		breq2 5170	. . . . . . . . . . . . 13 ⊢ (𝑒 = 1 → ((abs‘(𝑆‘𝑛)) < 𝑒 ↔ (abs‘(𝑆‘𝑛)) < 1))
104	103	rexralbidv 3229	. . . . . . . . . . . 12 ⊢ (𝑒 = 1 → (∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒 ↔ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1))
105	104	rspcva 3633	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ+ ∧ ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒) → ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
106	24, 102, 105	sylancr 586	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
107		rabn0 4412	. . . . . . . . . 10 ⊢ ({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅ ↔ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
108	106, 107	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅)
109		infssuzcl 12997	. . . . . . . . 9 ⊢ (({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ (ℤ≥‘0) ∧ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅) → inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < ) ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
110	23, 108, 109	sylancr 586	. . . . . . . 8 ⊢ (𝜑 → inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < ) ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
111	21, 110	eqeltrid 2848	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
112	20, 111	sselid 4006	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
113		tpssi 4863	. . . . . 6 ⊢ (((abs‘(𝐴‘0)) ∈ ℤ ∧ (!‘𝑀) ∈ ℤ ∧ 𝐼 ∈ ℤ) → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℤ)
114	11, 17, 112, 113	syl3anc 1371	. . . . 5 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℤ)
115		etransclem48.t	. . . . . 6 ⊢ 𝑇 = sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < )
116		xrltso 13203	. . . . . . . 8 ⊢ < Or ℝ*
117	116	a1i 11	. . . . . . 7 ⊢ (𝜑 → < Or ℝ*)
118		tpfi 9393	. . . . . . . 8 ⊢ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin
119	118	a1i 11	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin)
120	11	tpnzd 4805	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ≠ ∅)
121		zssre 12646	. . . . . . . . 9 ⊢ ℤ ⊆ ℝ
122		ressxr 11334	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ*
123	121, 122	sstri 4018	. . . . . . . 8 ⊢ ℤ ⊆ ℝ*
124	114, 123	sstrdi 4021	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)
125		fisupcl 9538	. . . . . . 7 ⊢ (( < Or ℝ* ∧ ({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin ∧ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ≠ ∅ ∧ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)) → sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
126	117, 119, 120, 124, 125	syl13anc 1372	. . . . . 6 ⊢ (𝜑 → sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
127	115, 126	eqeltrid 2848	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
128	114, 127	sseldd 4009	. . . 4 ⊢ (𝜑 → 𝑇 ∈ ℤ)
129		0red 11293	. . . . 5 ⊢ (𝜑 → 0 ∈ ℝ)
130	16	nnred 12308	. . . . 5 ⊢ (𝜑 → (!‘𝑀) ∈ ℝ)
131	128	zred 12747	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℝ)
132	16	nngt0d 12342	. . . . 5 ⊢ (𝜑 → 0 < (!‘𝑀))
133		fvex 6933	. . . . . . . 8 ⊢ (!‘𝑀) ∈ V
134	133	tpid2 4795	. . . . . . 7 ⊢ (!‘𝑀) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}
135		supxrub 13386	. . . . . . 7 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ (!‘𝑀) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → (!‘𝑀) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
136	124, 134, 135	sylancl 585	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
137	136, 115	breqtrrdi 5208	. . . . 5 ⊢ (𝜑 → (!‘𝑀) ≤ 𝑇)
138	129, 130, 131, 132, 137	ltletrd 11450	. . . 4 ⊢ (𝜑 → 0 < 𝑇)
139		elnnz 12649	. . . 4 ⊢ (𝑇 ∈ ℕ ↔ (𝑇 ∈ ℤ ∧ 0 < 𝑇))
140	128, 138, 139	sylanbrc 582	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℕ)
141		prmunb 16961	. . 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 12748	. . . . . . 7 ⊢ (𝜑 → (𝐴‘0) ∈ ℂ)
150	149	3ad2ant1 1133	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐴‘0) ∈ ℂ)
151	150	abscld 15485	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) ∈ ℝ)
152	131	3ad2ant1 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑇 ∈ ℝ)
153		prmz 16722	. . . . . . 7 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
154	153	zred 12747	. . . . . 6 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
155	154	3ad2ant2 1134	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℝ)
156	124	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)
157		fvex 6933	. . . . . . . . 9 ⊢ (abs‘(𝐴‘0)) ∈ V
158	157	tpid1 4793	. . . . . . . 8 ⊢ (abs‘(𝐴‘0)) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}
159		supxrub 13386	. . . . . . . 8 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ (abs‘(𝐴‘0)) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → (abs‘(𝐴‘0)) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
160	156, 158, 159	sylancl 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (abs‘(𝐴‘0)) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
161	160, 115	breqtrrdi 5208	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (abs‘(𝐴‘0)) ≤ 𝑇)
162	161	3adant3 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) ≤ 𝑇)
163		simp3 1138	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑇 < 𝑝)
164	151, 152, 155, 162, 163	lelttrd 11448	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) < 𝑝)
165	130	3ad2ant1 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) ∈ ℝ)
166	137	3ad2ant1 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) ≤ 𝑇)
167	165, 152, 155, 166, 163	lelttrd 11448	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) < 𝑝)
168	34	a1i 11	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))))
169		oveq2 7456	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → ((𝑀↑(𝑀 + 1))↑𝑛) = ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)))
170		fveq2 6920	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → (!‘𝑛) = (!‘(𝑝 − 1)))
171	169, 170	oveq12d 7466	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) = (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))))
172	168, 171	oveq12d 7466	. . . . . . . 8 ⊢ (𝑛 = (𝑝 − 1) → (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
173		prmnn 16721	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
174		nnm1nn0 12594	. . . . . . . . . 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 14196	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) ∈ ℂ)
180	175	faccld 14333	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℕ)
181	180	nncnd 12309	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℂ)
182	181	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ∈ ℂ)
183	180	nnne0d 12343	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ≠ 0)
184	183	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ≠ 0)
185	179, 182, 184	divcld 12070	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))) ∈ ℂ)
186	177, 185	mulcld 11310	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ ℂ)
187	28, 172, 176, 186	fvmptd3 7052	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
188	187	eqcomd 2746	. . . . . 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 12674	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 1 ∈ ℤ)
192	153, 191	zsubcld 12752	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → (𝑝 − 1) ∈ ℤ)
193	192	3ad2ant2 1134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑝 − 1) ∈ ℤ)
194	190	zred 12747	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ ℝ)
195		tpid3g 4797	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
196	112, 195	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
197		supxrub 13386	. . . . . . . . . . . . . 14 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → 𝐼 ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
198	124, 196, 197	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
199	198, 115	breqtrrdi 5208	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ≤ 𝑇)
200	199	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ≤ 𝑇)
201	194, 152, 155, 200, 163	lelttrd 11448	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 < 𝑝)
202	153	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℤ)
203		zltlem1 12696	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℤ ∧ 𝑝 ∈ ℤ) → (𝐼 < 𝑝 ↔ 𝐼 ≤ (𝑝 − 1)))
204	190, 202, 203	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐼 < 𝑝 ↔ 𝐼 ≤ (𝑝 − 1)))
205	201, 204	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ≤ (𝑝 − 1))
206		eluz2 12909	. . . . . . . . 9 ⊢ ((𝑝 − 1) ∈ (ℤ≥‘𝐼) ↔ (𝐼 ∈ ℤ ∧ (𝑝 − 1) ∈ ℤ ∧ 𝐼 ≤ (𝑝 − 1)))
207	190, 193, 205, 206	syl3anbrc 1343	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑝 − 1) ∈ (ℤ≥‘𝐼))
208	111	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
209		fveq2 6920	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝐼 → (ℤ≥‘𝑖) = (ℤ≥‘𝐼))
210	209	raleqdv 3334	. . . . . . . . . . 11 ⊢ (𝑖 = 𝐼 → (∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1 ↔ ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1))
211	210	elrab 3708	. . . . . . . . . 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 2908	. . . . . . . . . . 11 ⊢ Ⅎ𝑛abs
215		nfcv 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑝 − 1)
216	30, 215	nffv 6930	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑆‘(𝑝 − 1))
217	214, 216	nffv 6930	. . . . . . . . . 10 ⊢ Ⅎ𝑛(abs‘(𝑆‘(𝑝 − 1)))
218		nfcv 2908	. . . . . . . . . 10 ⊢ Ⅎ𝑛 <
219		nfcv 2908	. . . . . . . . . 10 ⊢ Ⅎ𝑛1
220	217, 218, 219	nfbr 5213	. . . . . . . . 9 ⊢ Ⅎ𝑛(abs‘(𝑆‘(𝑝 − 1))) < 1
221		2fveq3 6925	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → (abs‘(𝑆‘𝑛)) = (abs‘(𝑆‘(𝑝 − 1))))
222	221	breq1d 5176	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → ((abs‘(𝑆‘𝑛)) < 1 ↔ (abs‘(𝑆‘(𝑝 − 1))) < 1))
223	220, 222	rspc 3623	. . . . . . . 8 ⊢ ((𝑝 − 1) ∈ (ℤ≥‘𝐼) → (∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1 → (abs‘(𝑆‘(𝑝 − 1))) < 1))
224	207, 213, 223	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝑆‘(𝑝 − 1))) < 1)
225	171	oveq2d 7464	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝 − 1) → (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
226		ovexd 7483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ V)
227	28, 225, 176, 226	fvmptd3 7052	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) = (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
228	15	nn0red 12614	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℝ)
229	228, 53	reexpcld 14213	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ)
230	228, 229	remulcld 11320	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℝ)
231	230	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℝ)
232	49, 231	remulcld 11320	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℝ)
233	35, 232	fsumrecl 15782	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℝ)
234	34, 233	eqeltrid 2848	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℝ)
235	234	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝐶 ∈ ℝ)
236	229	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀↑(𝑀 + 1)) ∈ ℝ)
237	236, 176	reexpcld 14213	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) ∈ ℝ)
238	180	nnred 12308	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℝ)
239	238	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ∈ ℝ)
240	237, 239, 184	redivcld 12122	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))) ∈ ℝ)
241	235, 240	remulcld 11320	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ ℝ)
242	227, 241	eqeltrd 2844	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) ∈ ℝ)
243	242	3adant3 1132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑆‘(𝑝 − 1)) ∈ ℝ)
244		1red 11291	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 1 ∈ ℝ)
245	243, 244	absltd 15478	. . . . . . 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 5188	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) < 1)
249		etransclem6 46161	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑝 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑝)))
250		eqid 2740	. . . 4 ⊢ Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥)
251		eqid 2740	. . . 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 46202	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))
253	252	rexlimdv3a 3165	. 2 ⊢ (𝜑 → (∃𝑝 ∈ ℙ 𝑇 < 𝑝 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1)))
254	142, 253	mpd 15	1 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  {crab 3443  Vcvv 3488   ∖ cdif 3973   ⊆ wss 3976  ∅c0 4352  {csn 4648  {ctp 4652   class class class wbr 5166   ↦ cmpt 5249   Or wor 5606  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448  Fincfn 9003  supcsup 9509  infcinf 9510  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325   − cmin 11520  -cneg 11521   / cdiv 11947  ℕcn 12293  ℕ₀cn0 12553  ℤcz 12639  ℤ_≥cuz 12903  ℝ⁺crp 13057  (,)cioo 13407  ...cfz 13567  ↑cexp 14112  !cfa 14322  abscabs 15283   ⇝ cli 15530  Σcsu 15734  ∏cprod 15951  eceu 16110  ℙcprime 16718  ∫citg 25672  0_𝑝c0p 25723  Polycply 26243  coeffccoe 26245  degcdgr 26246  ↑_𝑐ccxp 26615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cc 10504  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-symdif 4272  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-disj 5134  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-ofr 7715  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-oadd 8526  df-omul 8527  df-er 8763  df-map 8886  df-pm 8887  df-ixp 8956  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-fi 9480  df-sup 9511  df-inf 9512  df-oi 9579  df-dju 9970  df-card 10008  df-acn 10011  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-z 12640  df-dec 12759  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-ioo 13411  df-ioc 13412  df-ico 13413  df-icc 13414  df-fz 13568  df-fzo 13712  df-fl 13843  df-mod 13921  df-seq 14053  df-exp 14113  df-fac 14323  df-bc 14352  df-hash 14380  df-shft 15116  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-limsup 15517  df-clim 15534  df-rlim 15535  df-sum 15735  df-prod 15952  df-ef 16115  df-e 16116  df-sin 16117  df-cos 16118  df-tan 16119  df-pi 16120  df-dvds 16303  df-gcd 16541  df-prm 16719  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-starv 17326  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ds 17333  df-unif 17334  df-hom 17335  df-cco 17336  df-rest 17482  df-topn 17483  df-0g 17501  df-gsum 17502  df-topgen 17503  df-pt 17504  df-prds 17507  df-xrs 17562  df-qtop 17567  df-imas 17568  df-xps 17570  df-mre 17644  df-mrc 17645  df-acs 17647  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-submnd 18819  df-mulg 19108  df-cntz 19357  df-cmn 19824  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-fbas 21384  df-fg 21385  df-cnfld 21388  df-top 22921  df-topon 22938  df-topsp 22960  df-bases 22974  df-cld 23048  df-ntr 23049  df-cls 23050  df-nei 23127  df-lp 23165  df-perf 23166  df-cn 23256  df-cnp 23257  df-haus 23344  df-cmp 23416  df-tx 23591  df-hmeo 23784  df-fil 23875  df-fm 23967  df-flim 23968  df-flf 23969  df-xms 24351  df-ms 24352  df-tms 24353  df-cncf 24923  df-ovol 25518  df-vol 25519  df-mbf 25673  df-itg1 25674  df-itg2 25675  df-ibl 25676  df-itg 25677  df-0p 25724  df-limc 25921  df-dv 25922  df-dvn 25923  df-ply 26247  df-coe 26249  df-dgr 26250  df-log 26616  df-cxp 26617

This theorem is referenced by:  etransc  46204