Metamath Proof Explorer

Theorem etransclem48

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 p is chosen: it will be used by subsequent lemmas. (Contributed by Glauco Siliprandi, 5-Apr-2020) (Revised by AV, 28-Sep-2020)

Ref Expression
Hypotheses 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 etransclem48 ( 𝜑 → ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) )

Proof

Step Hyp Ref Expression
1 etransclem48.q ⊢ ( 𝜑 → 𝑄 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
2 etransclem48.qe0 ⊢ ( 𝜑 → ( 𝑄 ‘ e ) = 0 )
3 etransclem48.a ⊢ 𝐴 = ( coeff ‘ 𝑄 )
4 etransclem48.a0 ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) ≠ 0 )
5 etransclem48.m ⊢ 𝑀 = ( deg ‘ 𝑄 )
6 etransclem48.c ⊢ 𝐶 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) )
7 etransclem48.s ⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) )
8 etransclem48.i ⊢ 𝐼 = inf ( { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } , ℝ , < )
9 etransclem48.t ⊢ 𝑇 = sup ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } , ℝ* , < )
10 1 eldifad ⊢ ( 𝜑 → 𝑄 ∈ ( Poly ‘ ℤ ) )
11 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
12 3 coef2 ⊢ ( ( 𝑄 ∈ ( Poly ‘ ℤ ) ∧ 0 ∈ ℤ ) → 𝐴 : ℕ0 ⟶ ℤ )
13 10 11 12 syl2anc ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℤ )
14 0nn0 ⊢ 0 ∈ ℕ0
15 14 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
16 13 15 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) ∈ ℤ )
17 zabscl ⊢ ( ( 𝐴 ‘ 0 ) ∈ ℤ → ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℤ )
18 16 17 syl ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℤ )
19 dgrcl ⊢ ( 𝑄 ∈ ( Poly ‘ ℤ ) → ( deg ‘ 𝑄 ) ∈ ℕ0 )
20 10 19 syl ⊢ ( 𝜑 → ( deg ‘ 𝑄 ) ∈ ℕ0 )
21 5 20 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
22 21 faccld ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) ∈ ℕ )
23 22 nnzd ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) ∈ ℤ )
24 ssrab2 ⊢ { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } ⊆ ℕ0
25 nn0ssz ⊢ ℕ0 ⊆ ℤ
26 24 25 sstri ⊢ { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } ⊆ ℤ
27 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
28 24 27 sseqtri ⊢ { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } ⊆ ( ℤ≥ ‘ 0 )
29 1rp ⊢ 1 ∈ ℝ+
30 nfv ⊢ Ⅎ 𝑛 𝜑
31 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ0 ↦ 𝐶 )
32 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
33 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ0 ↦ ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) )
34 7 33 nfcxfr ⊢ Ⅎ 𝑛 𝑆
35 nn0ex ⊢ ℕ0 ∈ V
36 35 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) ∈ V
37 36 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) ∈ V )
38 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
39 13 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝐴 : ℕ0 ⟶ ℤ )
40 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℕ0 )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ℕ0 )
42 39 41 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℤ )
43 42 zcnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
44 ere ⊢ e ∈ ℝ
45 44 recni ⊢ e ∈ ℂ
46 45 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → e ∈ ℂ )
47 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
48 47 zcnd ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℂ )
49 48 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ℂ )
50 46 49 cxpcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( e ↑𝑐 𝑗 ) ∈ ℂ )
51 43 50 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ∈ ℂ )
52 51 abscld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) ∈ ℝ )
53 52 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) ∈ ℂ )
54 21 nn0cnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
55 peano2nn0 ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
56 21 55 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ0 )
57 54 56 expcld ⊢ ( 𝜑 → ( 𝑀 ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
58 54 57 mulcld ⊢ ( 𝜑 → ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ∈ ℂ )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ∈ ℂ )
60 53 59 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) ∈ ℂ )
61 38 60 fsumcl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) ∈ ℂ )
62 6 61 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
63 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) = ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) )
64 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑛 = 𝑖 ) → 𝐶 = 𝐶 )
65 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
66 62 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
67 63 64 65 66 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑖 ) = 𝐶 )
68 27 11 37 62 67 climconst ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) ⇝ 𝐶 )
69 35 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ∈ V
70 7 69 eqeltri ⊢ 𝑆 ∈ V
71 70 a1i ⊢ ( 𝜑 → 𝑆 ∈ V )
72 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
73 72 expfac ⊢ ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ∈ ℂ → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ⇝ 0 )
74 57 73 syl ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ⇝ 0 )
75 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
76 62 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
77 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) = ( 𝑛 ∈ ℕ0 ↦ 𝐶 )
78 77 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝐶 ∈ ℂ ) → ( ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑛 ) = 𝐶 )
79 75 76 78 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑛 ) = 𝐶 )
80 79 76 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑛 ) ∈ ℂ )
81 ovex ⊢ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ∈ V
82 72 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ∈ V ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑛 ) = ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
83 81 82 mpan2 ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑛 ) = ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑛 ) = ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
85 57 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
86 85 75 expcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) ∈ ℂ )
87 75 faccld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ! ‘ 𝑛 ) ∈ ℕ )
88 87 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ! ‘ 𝑛 ) ∈ ℂ )
89 87 nnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ! ‘ 𝑛 ) ≠ 0 )
90 86 88 89 divcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ∈ ℂ )
91 84 90 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑛 ) ∈ ℂ )
92 ovex ⊢ ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ∈ V
93 7 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ∈ V ) → ( 𝑆 ‘ 𝑛 ) = ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) )
94 92 93 mpan2 ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑆 ‘ 𝑛 ) = ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) )
95 94 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑛 ) = ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) )
96 79 84 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑛 ) · ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑛 ) ) = ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) )
97 95 96 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑛 ) = ( ( ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑛 ) · ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑛 ) ) )
98 30 31 32 34 27 11 68 71 74 80 91 97 climmulf ⊢ ( 𝜑 → 𝑆 ⇝ ( 𝐶 · 0 ) )
99 62 mul01d ⊢ ( 𝜑 → ( 𝐶 · 0 ) = 0 )
100 98 99 breqtrd ⊢ ( 𝜑 → 𝑆 ⇝ 0 )
101 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ 𝑛 ) )
102 80 91 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑛 ) · ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑛 ) ) ∈ ℂ )
103 97 102 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑛 ) ∈ ℂ )
104 34 27 11 71 101 103 clim0cf ⊢ ( 𝜑 → ( 𝑆 ⇝ 0 ↔ ∀ 𝑒 ∈ ℝ+ ∃ 𝑖 ∈ ℕ0 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 𝑒 ) )
105 100 104 mpbid ⊢ ( 𝜑 → ∀ 𝑒 ∈ ℝ+ ∃ 𝑖 ∈ ℕ0 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 𝑒 )
106 breq2 ⊢ ( 𝑒 = 1 → ( ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 𝑒 ↔ ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 ) )
107 106 rexralbidv ⊢ ( 𝑒 = 1 → ( ∃ 𝑖 ∈ ℕ0 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 𝑒 ↔ ∃ 𝑖 ∈ ℕ0 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 ) )
108 107 rspcva ⊢ ( ( 1 ∈ ℝ+ ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑖 ∈ ℕ0 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 𝑒 ) → ∃ 𝑖 ∈ ℕ0 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 )
109 29 105 108 sylancr ⊢ ( 𝜑 → ∃ 𝑖 ∈ ℕ0 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 )
110 rabn0 ⊢ ( { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } ≠ ∅ ↔ ∃ 𝑖 ∈ ℕ0 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 )
111 109 110 sylibr ⊢ ( 𝜑 → { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } ≠ ∅ )
112 infssuzcl ⊢ ( ( { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } ⊆ ( ℤ≥ ‘ 0 ) ∧ { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } ≠ ∅ ) → inf ( { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } , ℝ , < ) ∈ { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } )
113 28 111 112 sylancr ⊢ ( 𝜑 → inf ( { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } , ℝ , < ) ∈ { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } )
114 8 113 eqeltrid ⊢ ( 𝜑 → 𝐼 ∈ { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } )
115 26 114 sselid ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
116 tpssi ⊢ ( ( ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℤ ∧ ( ! ‘ 𝑀 ) ∈ ℤ ∧ 𝐼 ∈ ℤ ) → { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ⊆ ℤ )
117 18 23 115 116 syl3anc ⊢ ( 𝜑 → { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ⊆ ℤ )
118 xrltso ⊢ < Or ℝ*
119 118 a1i ⊢ ( 𝜑 → < Or ℝ* )
120 tpfi ⊢ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ∈ Fin
121 120 a1i ⊢ ( 𝜑 → { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ∈ Fin )
122 18 tpnzd ⊢ ( 𝜑 → { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ≠ ∅ )
123 zssre ⊢ ℤ ⊆ ℝ
124 ressxr ⊢ ℝ ⊆ ℝ*
125 123 124 sstri ⊢ ℤ ⊆ ℝ*
126 117 125 sstrdi ⊢ ( 𝜑 → { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ⊆ ℝ* )
127 fisupcl ⊢ ( ( < Or ℝ* ∧ ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ∈ Fin ∧ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ≠ ∅ ∧ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ⊆ ℝ* ) ) → sup ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } , ℝ* , < ) ∈ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } )
128 119 121 122 126 127 syl13anc ⊢ ( 𝜑 → sup ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } , ℝ* , < ) ∈ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } )
129 9 128 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } )
130 117 129 sseldd ⊢ ( 𝜑 → 𝑇 ∈ ℤ )
131 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
132 22 nnred ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) ∈ ℝ )
133 130 zred ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
134 22 nngt0d ⊢ ( 𝜑 → 0 < ( ! ‘ 𝑀 ) )
135 fvex ⊢ ( ! ‘ 𝑀 ) ∈ V
136 135 tpid2 ⊢ ( ! ‘ 𝑀 ) ∈ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 }
137 supxrub ⊢ ( ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ⊆ ℝ* ∧ ( ! ‘ 𝑀 ) ∈ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ) → ( ! ‘ 𝑀 ) ≤ sup ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } , ℝ* , < ) )
138 126 136 137 sylancl ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) ≤ sup ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } , ℝ* , < ) )
139 138 9 breqtrrdi ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) ≤ 𝑇 )
140 131 132 133 134 139 ltletrd ⊢ ( 𝜑 → 0 < 𝑇 )
141 elnnz ⊢ ( 𝑇 ∈ ℕ ↔ ( 𝑇 ∈ ℤ ∧ 0 < 𝑇 ) )
142 130 140 141 sylanbrc ⊢ ( 𝜑 → 𝑇 ∈ ℕ )
143 prmunb ⊢ ( 𝑇 ∈ ℕ → ∃ 𝑝 ∈ ℙ 𝑇 < 𝑝 )
144 142 143 syl ⊢ ( 𝜑 → ∃ 𝑝 ∈ ℙ 𝑇 < 𝑝 )
145 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝑄 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
146 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( 𝑄 ‘ e ) = 0 )
147 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( 𝐴 ‘ 0 ) ≠ 0 )
148 simp2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝑝 ∈ ℙ )
149 16 zcnd ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) ∈ ℂ )
150 149 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
151 150 abscld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℝ )
152 133 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝑇 ∈ ℝ )
153 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
154 153 zred ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ )
155 154 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝑝 ∈ ℝ )
156 126 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ⊆ ℝ* )
157 fvex ⊢ ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ V
158 157 tpid1 ⊢ ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 }
159 supxrub ⊢ ( ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ⊆ ℝ* ∧ ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ) → ( abs ‘ ( 𝐴 ‘ 0 ) ) ≤ sup ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } , ℝ* , < ) )
160 156 158 159 sylancl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( abs ‘ ( 𝐴 ‘ 0 ) ) ≤ sup ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } , ℝ* , < ) )
161 160 9 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( abs ‘ ( 𝐴 ‘ 0 ) ) ≤ 𝑇 )
162 161 3adant3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( abs ‘ ( 𝐴 ‘ 0 ) ) ≤ 𝑇 )
163 simp3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝑇 < 𝑝 )
164 151 152 155 162 163 lelttrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( abs ‘ ( 𝐴 ‘ 0 ) ) < 𝑝 )
165 132 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( ! ‘ 𝑀 ) ∈ ℝ )
166 139 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( ! ‘ 𝑀 ) ≤ 𝑇 )
167 165 152 155 166 163 lelttrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( ! ‘ 𝑀 ) < 𝑝 )
168 6 a1i ⊢ ( 𝑛 = ( 𝑝 − 1 ) → 𝐶 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) )
169 oveq2 ⊢ ( 𝑛 = ( 𝑝 − 1 ) → ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) = ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) )
170 fveq2 ⊢ ( 𝑛 = ( 𝑝 − 1 ) → ( ! ‘ 𝑛 ) = ( ! ‘ ( 𝑝 − 1 ) ) )
171 169 170 oveq12d ⊢ ( 𝑛 = ( 𝑝 − 1 ) → ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) = ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) )
172 168 171 oveq12d ⊢ ( 𝑛 = ( 𝑝 − 1 ) → ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ) )
173 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
174 nnm1nn0 ⊢ ( 𝑝 ∈ ℕ → ( 𝑝 − 1 ) ∈ ℕ0 )
175 173 174 syl ⊢ ( 𝑝 ∈ ℙ → ( 𝑝 − 1 ) ∈ ℕ0 )
176 175 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 − 1 ) ∈ ℕ0 )
177 61 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) ∈ ℂ )
178 57 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑀 ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
179 178 176 expcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) ∈ ℂ )
180 175 faccld ⊢ ( 𝑝 ∈ ℙ → ( ! ‘ ( 𝑝 − 1 ) ) ∈ ℕ )
181 180 nncnd ⊢ ( 𝑝 ∈ ℙ → ( ! ‘ ( 𝑝 − 1 ) ) ∈ ℂ )
182 181 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ! ‘ ( 𝑝 − 1 ) ) ∈ ℂ )
183 180 nnne0d ⊢ ( 𝑝 ∈ ℙ → ( ! ‘ ( 𝑝 − 1 ) ) ≠ 0 )
184 183 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ! ‘ ( 𝑝 − 1 ) ) ≠ 0 )
185 179 182 184 divcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ∈ ℂ )
186 177 185 mulcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ) ∈ ℂ )
187 7 172 176 186 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑆 ‘ ( 𝑝 − 1 ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ) )
188 187 eqcomd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝑝 − 1 ) ) )
189 188 3adant3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝑝 − 1 ) ) )
190 115 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝐼 ∈ ℤ )
191 1zzd ⊢ ( 𝑝 ∈ ℙ → 1 ∈ ℤ )
192 153 191 zsubcld ⊢ ( 𝑝 ∈ ℙ → ( 𝑝 − 1 ) ∈ ℤ )
193 192 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( 𝑝 − 1 ) ∈ ℤ )
194 190 zred ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝐼 ∈ ℝ )
195 tpid3g ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } )
196 115 195 syl ⊢ ( 𝜑 → 𝐼 ∈ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } )
197 supxrub ⊢ ( ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ⊆ ℝ* ∧ 𝐼 ∈ { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } ) → 𝐼 ≤ sup ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } , ℝ* , < ) )
198 126 196 197 syl2anc ⊢ ( 𝜑 → 𝐼 ≤ sup ( { ( abs ‘ ( 𝐴 ‘ 0 ) ) , ( ! ‘ 𝑀 ) , 𝐼 } , ℝ* , < ) )
199 198 9 breqtrrdi ⊢ ( 𝜑 → 𝐼 ≤ 𝑇 )
200 199 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝐼 ≤ 𝑇 )
201 194 152 155 200 163 lelttrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝐼 < 𝑝 )
202 153 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝑝 ∈ ℤ )
203 zltlem1 ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑝 ∈ ℤ ) → ( 𝐼 < 𝑝 ↔ 𝐼 ≤ ( 𝑝 − 1 ) ) )
204 190 202 203 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( 𝐼 < 𝑝 ↔ 𝐼 ≤ ( 𝑝 − 1 ) ) )
205 201 204 mpbid ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝐼 ≤ ( 𝑝 − 1 ) )
206 eluz2 ⊢ ( ( 𝑝 − 1 ) ∈ ( ℤ≥ ‘ 𝐼 ) ↔ ( 𝐼 ∈ ℤ ∧ ( 𝑝 − 1 ) ∈ ℤ ∧ 𝐼 ≤ ( 𝑝 − 1 ) ) )
207 190 193 205 206 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( 𝑝 − 1 ) ∈ ( ℤ≥ ‘ 𝐼 ) )
208 114 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 𝐼 ∈ { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } )
209 fveq2 ⊢ ( 𝑖 = 𝐼 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝐼 ) )
210 209 raleqdv ⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝐼 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 ) )
211 210 elrab ⊢ ( 𝐼 ∈ { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 } ↔ ( 𝐼 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝐼 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 ) )
212 208 211 sylib ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( 𝐼 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝐼 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 ) )
213 212 simprd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝐼 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 )
214 nfcv ⊢ Ⅎ 𝑛 abs
215 nfcv ⊢ Ⅎ 𝑛 ( 𝑝 − 1 )
216 34 215 nffv ⊢ Ⅎ 𝑛 ( 𝑆 ‘ ( 𝑝 − 1 ) )
217 214 216 nffv ⊢ Ⅎ 𝑛 ( abs ‘ ( 𝑆 ‘ ( 𝑝 − 1 ) ) )
218 nfcv ⊢ Ⅎ 𝑛 <
219 nfcv ⊢ Ⅎ 𝑛 1
220 217 218 219 nfbr ⊢ Ⅎ 𝑛 ( abs ‘ ( 𝑆 ‘ ( 𝑝 − 1 ) ) ) < 1
221 2fveq3 ⊢ ( 𝑛 = ( 𝑝 − 1 ) → ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) = ( abs ‘ ( 𝑆 ‘ ( 𝑝 − 1 ) ) ) )
222 221 breq1d ⊢ ( 𝑛 = ( 𝑝 − 1 ) → ( ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 ↔ ( abs ‘ ( 𝑆 ‘ ( 𝑝 − 1 ) ) ) < 1 ) )
223 220 222 rspc ⊢ ( ( 𝑝 − 1 ) ∈ ( ℤ≥ ‘ 𝐼 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝐼 ) ( abs ‘ ( 𝑆 ‘ 𝑛 ) ) < 1 → ( abs ‘ ( 𝑆 ‘ ( 𝑝 − 1 ) ) ) < 1 ) )
224 207 213 223 sylc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( abs ‘ ( 𝑆 ‘ ( 𝑝 − 1 ) ) ) < 1 )
225 171 oveq2d ⊢ ( 𝑛 = ( 𝑝 − 1 ) → ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ) )
226 ovexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ) ∈ V )
227 7 225 176 226 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑆 ‘ ( 𝑝 − 1 ) ) = ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ) )
228 21 nn0red ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
229 228 56 reexpcld ⊢ ( 𝜑 → ( 𝑀 ↑ ( 𝑀 + 1 ) ) ∈ ℝ )
230 228 229 remulcld ⊢ ( 𝜑 → ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ∈ ℝ )
231 230 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ∈ ℝ )
232 52 231 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) ∈ ℝ )
233 38 232 fsumrecl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) ∈ ℝ )
234 6 233 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
235 234 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝐶 ∈ ℝ )
236 229 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑀 ↑ ( 𝑀 + 1 ) ) ∈ ℝ )
237 236 176 reexpcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) ∈ ℝ )
238 180 nnred ⊢ ( 𝑝 ∈ ℙ → ( ! ‘ ( 𝑝 − 1 ) ) ∈ ℝ )
239 238 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ! ‘ ( 𝑝 − 1 ) ) ∈ ℝ )
240 237 239 184 redivcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ∈ ℝ )
241 235 240 remulcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝐶 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ) ∈ ℝ )
242 227 241 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑆 ‘ ( 𝑝 − 1 ) ) ∈ ℝ )
243 242 3adant3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( 𝑆 ‘ ( 𝑝 − 1 ) ) ∈ ℝ )
244 1red ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → 1 ∈ ℝ )
245 243 244 absltd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( ( abs ‘ ( 𝑆 ‘ ( 𝑝 − 1 ) ) ) < 1 ↔ ( - 1 < ( 𝑆 ‘ ( 𝑝 − 1 ) ) ∧ ( 𝑆 ‘ ( 𝑝 − 1 ) ) < 1 ) ) )
246 224 245 mpbid ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( - 1 < ( 𝑆 ‘ ( 𝑝 − 1 ) ) ∧ ( 𝑆 ‘ ( 𝑝 − 1 ) ) < 1 ) )
247 246 simprd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( 𝑆 ‘ ( 𝑝 − 1 ) ) < 1 )
248 189 247 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑝 − 1 ) ) / ( ! ‘ ( 𝑝 − 1 ) ) ) ) < 1 )
249 etransclem6 ⊢ ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑝 − 1 ) ) · ∏ 𝑧 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑧 ) ↑ 𝑝 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑝 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑝 ) ) )
250 eqid ⊢ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑝 − 1 ) ) · ∏ 𝑧 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑧 ) ↑ 𝑝 ) ) ) ‘ 𝑥 ) ) d 𝑥 ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑝 − 1 ) ) · ∏ 𝑧 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑧 ) ↑ 𝑝 ) ) ) ‘ 𝑥 ) ) d 𝑥 )
251 eqid ⊢ ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑝 − 1 ) ) · ∏ 𝑧 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑧 ) ↑ 𝑝 ) ) ) ‘ 𝑥 ) ) d 𝑥 ) / ( ! ‘ ( 𝑝 − 1 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑝 − 1 ) ) · ∏ 𝑧 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑧 ) ↑ 𝑝 ) ) ) ‘ 𝑥 ) ) d 𝑥 ) / ( ! ‘ ( 𝑝 − 1 ) ) )
252 145 146 3 147 5 148 164 167 248 249 250 251 etransclem47 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝 ) → ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) )
253 252 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ 𝑇 < 𝑝 → ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) ) )
254 144 253 mpd ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) )