Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  etransclem44 Structured version   Visualization version   GIF version

Theorem etransclem44 46233
Description: The given finite sum is nonzero. This is the claim proved after equation (7) in [Juillerat] p. 12 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
etransclem44.a (𝜑𝐴:ℕ0⟶ℤ)
etransclem44.a0 (𝜑 → (𝐴‘0) ≠ 0)
etransclem44.m (𝜑𝑀 ∈ ℕ0)
etransclem44.p (𝜑𝑃 ∈ ℙ)
etransclem44.ap (𝜑 → (abs‘(𝐴‘0)) < 𝑃)
etransclem44.mp (𝜑 → (!‘𝑀) < 𝑃)
etransclem44.f 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)))
etransclem44.k 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1)))
Assertion
Ref Expression
etransclem44 (𝜑𝐾 ≠ 0)
Distinct variable groups:   𝐴,𝑘   𝑘,𝐹   𝑗,𝑀,𝑘,𝑥   𝑃,𝑗,𝑘,𝑥   𝜑,𝑗,𝑘,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑗)   𝐹(𝑥,𝑗)   𝐾(𝑥,𝑗,𝑘)

Proof of Theorem etransclem44
Dummy variables 𝑐 𝑑 𝑛 𝑚 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 etransclem44.k . . . 4 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1)))
21a1i 11 . . 3 (𝜑𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
3 nfv 1911 . . . . 5 𝑘𝜑
4 nfcv 2902 . . . . 5 𝑘((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0))
5 fzfi 14009 . . . . . . 7 (0...𝑀) ∈ Fin
6 fzfi 14009 . . . . . . 7 (0...((𝑀 · 𝑃) + (𝑃 − 1))) ∈ Fin
7 xpfi 9355 . . . . . . 7 (((0...𝑀) ∈ Fin ∧ (0...((𝑀 · 𝑃) + (𝑃 − 1))) ∈ Fin) → ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin)
85, 6, 7mp2an 692 . . . . . 6 ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin
98a1i 11 . . . . 5 (𝜑 → ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin)
10 etransclem44.a . . . . . . . . 9 (𝜑𝐴:ℕ0⟶ℤ)
1110adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝐴:ℕ0⟶ℤ)
12 fzssnn0 45267 . . . . . . . . . 10 (0...𝑀) ⊆ ℕ0
13 xp1st 8044 . . . . . . . . . 10 (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (1st𝑘) ∈ (0...𝑀))
1412, 13sselid 3992 . . . . . . . . 9 (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (1st𝑘) ∈ ℕ0)
1514adantl 481 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st𝑘) ∈ ℕ0)
1611, 15ffvelcdmd 7104 . . . . . . 7 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (𝐴‘(1st𝑘)) ∈ ℤ)
17 reelprrecn 11244 . . . . . . . . 9 ℝ ∈ {ℝ, ℂ}
1817a1i 11 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ℝ ∈ {ℝ, ℂ})
19 reopn 45239 . . . . . . . . . 10 ℝ ∈ (topGen‘ran (,))
20 eqid 2734 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
2120tgioo2 24838 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
2219, 21eleqtri 2836 . . . . . . . . 9 ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ)
2322a1i 11 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
24 etransclem44.p . . . . . . . . . 10 (𝜑𝑃 ∈ ℙ)
25 prmnn 16707 . . . . . . . . . 10 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2624, 25syl 17 . . . . . . . . 9 (𝜑𝑃 ∈ ℕ)
2726adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝑃 ∈ ℕ)
28 etransclem44.m . . . . . . . . 9 (𝜑𝑀 ∈ ℕ0)
2928adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝑀 ∈ ℕ0)
30 etransclem44.f . . . . . . . 8 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)))
31 xp2nd 8045 . . . . . . . . . 10 (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (2nd𝑘) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))))
32 elfznn0 13656 . . . . . . . . . 10 ((2nd𝑘) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))) → (2nd𝑘) ∈ ℕ0)
3331, 32syl 17 . . . . . . . . 9 (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (2nd𝑘) ∈ ℕ0)
3433adantl 481 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (2nd𝑘) ∈ ℕ0)
3515nn0red 12585 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st𝑘) ∈ ℝ)
3615nn0zd 12636 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st𝑘) ∈ ℤ)
3718, 23, 27, 29, 30, 34, 35, 36etransclem42 46231 . . . . . . 7 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ∈ ℤ)
3816, 37zmulcld 12725 . . . . . 6 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℤ)
3938zcnd 12720 . . . . 5 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℂ)
40 nn0uz 12917 . . . . . . . 8 0 = (ℤ‘0)
4128, 40eleqtrdi 2848 . . . . . . 7 (𝜑𝑀 ∈ (ℤ‘0))
42 eluzfz1 13567 . . . . . . 7 (𝑀 ∈ (ℤ‘0) → 0 ∈ (0...𝑀))
4341, 42syl 17 . . . . . 6 (𝜑 → 0 ∈ (0...𝑀))
44 0zd 12622 . . . . . . 7 (𝜑 → 0 ∈ ℤ)
4528nn0zd 12636 . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
4626nnzd 12637 . . . . . . . . 9 (𝜑𝑃 ∈ ℤ)
4745, 46zmulcld 12725 . . . . . . . 8 (𝜑 → (𝑀 · 𝑃) ∈ ℤ)
48 nnm1nn0 12564 . . . . . . . . . 10 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
4926, 48syl 17 . . . . . . . . 9 (𝜑 → (𝑃 − 1) ∈ ℕ0)
5049nn0zd 12636 . . . . . . . 8 (𝜑 → (𝑃 − 1) ∈ ℤ)
5147, 50zaddcld 12723 . . . . . . 7 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℤ)
5249nn0ge0d 12587 . . . . . . 7 (𝜑 → 0 ≤ (𝑃 − 1))
5326nnnn0d 12584 . . . . . . . . . 10 (𝜑𝑃 ∈ ℕ0)
5428, 53nn0mulcld 12589 . . . . . . . . 9 (𝜑 → (𝑀 · 𝑃) ∈ ℕ0)
5554nn0ge0d 12587 . . . . . . . 8 (𝜑 → 0 ≤ (𝑀 · 𝑃))
5649nn0red 12585 . . . . . . . . 9 (𝜑 → (𝑃 − 1) ∈ ℝ)
5747zred 12719 . . . . . . . . 9 (𝜑 → (𝑀 · 𝑃) ∈ ℝ)
5856, 57addge02d 11849 . . . . . . . 8 (𝜑 → (0 ≤ (𝑀 · 𝑃) ↔ (𝑃 − 1) ≤ ((𝑀 · 𝑃) + (𝑃 − 1))))
5955, 58mpbid 232 . . . . . . 7 (𝜑 → (𝑃 − 1) ≤ ((𝑀 · 𝑃) + (𝑃 − 1)))
6044, 51, 50, 52, 59elfzd 13551 . . . . . 6 (𝜑 → (𝑃 − 1) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))))
61 opelxp 5724 . . . . . 6 (⟨0, (𝑃 − 1)⟩ ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ↔ (0 ∈ (0...𝑀) ∧ (𝑃 − 1) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))))
6243, 60, 61sylanbrc 583 . . . . 5 (𝜑 → ⟨0, (𝑃 − 1)⟩ ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))))
63 fveq2 6906 . . . . . . . 8 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (1st𝑘) = (1st ‘⟨0, (𝑃 − 1)⟩))
64 0re 11260 . . . . . . . . 9 0 ∈ ℝ
65 ovex 7463 . . . . . . . . 9 (𝑃 − 1) ∈ V
66 op1stg 8024 . . . . . . . . 9 ((0 ∈ ℝ ∧ (𝑃 − 1) ∈ V) → (1st ‘⟨0, (𝑃 − 1)⟩) = 0)
6764, 65, 66mp2an 692 . . . . . . . 8 (1st ‘⟨0, (𝑃 − 1)⟩) = 0
6863, 67eqtrdi 2790 . . . . . . 7 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (1st𝑘) = 0)
6968fveq2d 6910 . . . . . 6 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (𝐴‘(1st𝑘)) = (𝐴‘0))
70 fveq2 6906 . . . . . . . . 9 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (2nd𝑘) = (2nd ‘⟨0, (𝑃 − 1)⟩))
71 op2ndg 8025 . . . . . . . . . 10 ((0 ∈ ℝ ∧ (𝑃 − 1) ∈ V) → (2nd ‘⟨0, (𝑃 − 1)⟩) = (𝑃 − 1))
7264, 65, 71mp2an 692 . . . . . . . . 9 (2nd ‘⟨0, (𝑃 − 1)⟩) = (𝑃 − 1)
7370, 72eqtrdi 2790 . . . . . . . 8 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (2nd𝑘) = (𝑃 − 1))
7473fveq2d 6910 . . . . . . 7 (𝑘 = ⟨0, (𝑃 − 1)⟩ → ((ℝ D𝑛 𝐹)‘(2nd𝑘)) = ((ℝ D𝑛 𝐹)‘(𝑃 − 1)))
7574, 68fveq12d 6913 . . . . . 6 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) = (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0))
7669, 75oveq12d 7448 . . . . 5 (𝑘 = ⟨0, (𝑃 − 1)⟩ → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = ((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)))
773, 4, 9, 39, 62, 76fsumsplit1 15777 . . . 4 (𝜑 → Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = (((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) + Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))))
7877oveq1d 7445 . . 3 (𝜑 → (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))) = ((((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) + Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))) / (!‘(𝑃 − 1))))
7912, 43sselid 3992 . . . . . . 7 (𝜑 → 0 ∈ ℕ0)
8010, 79ffvelcdmd 7104 . . . . . 6 (𝜑 → (𝐴‘0) ∈ ℤ)
8117a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ {ℝ, ℂ})
8222a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
8364a1i 11 . . . . . . 7 (𝜑 → 0 ∈ ℝ)
8481, 82, 26, 28, 30, 49, 83, 44etransclem42 46231 . . . . . 6 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈ ℤ)
8580, 84zmulcld 12725 . . . . 5 (𝜑 → ((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) ∈ ℤ)
8685zcnd 12720 . . . 4 (𝜑 → ((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) ∈ ℂ)
87 difss 4145 . . . . . . . 8 (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ⊆ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))
88 ssfi 9211 . . . . . . . 8 ((((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin ∧ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ⊆ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∈ Fin)
898, 87, 88mp2an 692 . . . . . . 7 (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∈ Fin
9089a1i 11 . . . . . 6 (𝜑 → (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∈ Fin)
91 eldifi 4140 . . . . . . 7 (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) → 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))))
9291, 38sylan2 593 . . . . . 6 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℤ)
9390, 92fsumzcl 15767 . . . . 5 (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℤ)
9493zcnd 12720 . . . 4 (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℂ)
9549faccld 14319 . . . . 5 (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
9695nncnd 12279 . . . 4 (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
9795nnne0d 12313 . . . 4 (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
9886, 94, 96, 97divdird 12078 . . 3 (𝜑 → ((((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) + Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))) / (!‘(𝑃 − 1))) = ((((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) + (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1)))))
992, 78, 983eqtrd 2778 . 2 (𝜑𝐾 = ((((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) + (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1)))))
10026nnne0d 12313 . . 3 (𝜑𝑃 ≠ 0)
10180zcnd 12720 . . . . 5 (𝜑 → (𝐴‘0) ∈ ℂ)
10284zcnd 12720 . . . . 5 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈ ℂ)
103101, 102, 96, 97divassd 12075 . . . 4 (𝜑 → (((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) = ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))))
104 etransclem5 46194 . . . . . . 7 (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
105 etransclem11 46200 . . . . . . 7 (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑𝑘) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = 𝑛})
10681, 82, 26, 28, 30, 49, 104, 105, 43, 83etransclem37 46226 . . . . . 6 (𝜑 → (!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0))
10795nnzd 12637 . . . . . . 7 (𝜑 → (!‘(𝑃 − 1)) ∈ ℤ)
108 dvdsval2 16289 . . . . . . 7 (((!‘(𝑃 − 1)) ∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0 ∧ (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈ ℤ) → ((!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ↔ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈ ℤ))
109107, 97, 84, 108syl3anc 1370 . . . . . 6 (𝜑 → ((!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ↔ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈ ℤ))
110106, 109mpbid 232 . . . . 5 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈ ℤ)
11180, 110zmulcld 12725 . . . 4 (𝜑 → ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ∈ ℤ)
112103, 111eqeltrd 2838 . . 3 (𝜑 → (((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) ∈ ℤ)
11391, 39sylan2 593 . . . . 5 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℂ)
11490, 96, 113, 97fsumdivc 15818 . . . 4 (𝜑 → (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))) = Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})(((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
11516zcnd 12720 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (𝐴‘(1st𝑘)) ∈ ℂ)
11691, 115sylan2 593 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (𝐴‘(1st𝑘)) ∈ ℂ)
11791, 37sylan2 593 . . . . . . . 8 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ∈ ℤ)
118117zcnd 12720 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ∈ ℂ)
11996adantr 480 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (!‘(𝑃 − 1)) ∈ ℂ)
12097adantr 480 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (!‘(𝑃 − 1)) ≠ 0)
121116, 118, 119, 120divassd 12075 . . . . . 6 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))) = ((𝐴‘(1st𝑘)) · ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1)))))
12291, 16sylan2 593 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (𝐴‘(1st𝑘)) ∈ ℤ)
12317a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ℝ ∈ {ℝ, ℂ})
12422a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
12526adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑃 ∈ ℕ)
12628adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑀 ∈ ℕ0)
12791adantl 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))))
128127, 33syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (2nd𝑘) ∈ ℕ0)
129127, 13syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (1st𝑘) ∈ (0...𝑀))
13091, 35sylan2 593 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (1st𝑘) ∈ ℝ)
131123, 124, 125, 126, 30, 128, 104, 105, 129, 130etransclem37 46226 . . . . . . . 8 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))
132107adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (!‘(𝑃 − 1)) ∈ ℤ)
133 dvdsval2 16289 . . . . . . . . 9 (((!‘(𝑃 − 1)) ∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0 ∧ (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ∈ ℤ) → ((!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ↔ ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))) ∈ ℤ))
134132, 120, 117, 133syl3anc 1370 . . . . . . . 8 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ((!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ↔ ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))) ∈ ℤ))
135131, 134mpbid 232 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))) ∈ ℤ)
136122, 135zmulcld 12725 . . . . . 6 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ((𝐴‘(1st𝑘)) · ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1)))) ∈ ℤ)
137121, 136eqeltrd 2838 . . . . 5 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))) ∈ ℤ)
13890, 137fsumzcl 15767 . . . 4 (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})(((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))) ∈ ℤ)
139114, 138eqeltrd 2838 . . 3 (𝜑 → (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))) ∈ ℤ)
140 1zzd 12645 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
141 zabscl 15348 . . . . . . . . . . 11 ((𝐴‘0) ∈ ℤ → (abs‘(𝐴‘0)) ∈ ℤ)
14280, 141syl 17 . . . . . . . . . 10 (𝜑 → (abs‘(𝐴‘0)) ∈ ℤ)
143 nn0abscl 15347 . . . . . . . . . . . . 13 ((𝐴‘0) ∈ ℤ → (abs‘(𝐴‘0)) ∈ ℕ0)
14480, 143syl 17 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐴‘0)) ∈ ℕ0)
145 etransclem44.a0 . . . . . . . . . . . . 13 (𝜑 → (𝐴‘0) ≠ 0)
146101, 145absne0d 15482 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐴‘0)) ≠ 0)
147 elnnne0 12537 . . . . . . . . . . . 12 ((abs‘(𝐴‘0)) ∈ ℕ ↔ ((abs‘(𝐴‘0)) ∈ ℕ0 ∧ (abs‘(𝐴‘0)) ≠ 0))
148144, 146, 147sylanbrc 583 . . . . . . . . . . 11 (𝜑 → (abs‘(𝐴‘0)) ∈ ℕ)
149148nnge1d 12311 . . . . . . . . . 10 (𝜑 → 1 ≤ (abs‘(𝐴‘0)))
150 etransclem44.ap . . . . . . . . . . 11 (𝜑 → (abs‘(𝐴‘0)) < 𝑃)
151 zltlem1 12667 . . . . . . . . . . . 12 (((abs‘(𝐴‘0)) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((abs‘(𝐴‘0)) < 𝑃 ↔ (abs‘(𝐴‘0)) ≤ (𝑃 − 1)))
152142, 46, 151syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐴‘0)) < 𝑃 ↔ (abs‘(𝐴‘0)) ≤ (𝑃 − 1)))
153150, 152mpbid 232 . . . . . . . . . 10 (𝜑 → (abs‘(𝐴‘0)) ≤ (𝑃 − 1))
154140, 50, 142, 149, 153elfzd 13551 . . . . . . . . 9 (𝜑 → (abs‘(𝐴‘0)) ∈ (1...(𝑃 − 1)))
155 fzm1ndvds 16355 . . . . . . . . 9 ((𝑃 ∈ ℕ ∧ (abs‘(𝐴‘0)) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (abs‘(𝐴‘0)))
15626, 154, 155syl2anc 584 . . . . . . . 8 (𝜑 → ¬ 𝑃 ∥ (abs‘(𝐴‘0)))
157 dvdsabsb 16309 . . . . . . . . 9 ((𝑃 ∈ ℤ ∧ (𝐴‘0) ∈ ℤ) → (𝑃 ∥ (𝐴‘0) ↔ 𝑃 ∥ (abs‘(𝐴‘0))))
15846, 80, 157syl2anc 584 . . . . . . . 8 (𝜑 → (𝑃 ∥ (𝐴‘0) ↔ 𝑃 ∥ (abs‘(𝐴‘0))))
159156, 158mtbird 325 . . . . . . 7 (𝜑 → ¬ 𝑃 ∥ (𝐴‘0))
160 etransclem44.mp . . . . . . . 8 (𝜑 → (!‘𝑀) < 𝑃)
16128, 24, 160, 30etransclem41 46230 . . . . . . 7 (𝜑 → ¬ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))
162159, 161jca 511 . . . . . 6 (𝜑 → (¬ 𝑃 ∥ (𝐴‘0) ∧ ¬ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))))
163 pm4.56 990 . . . . . 6 ((¬ 𝑃 ∥ (𝐴‘0) ∧ ¬ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ ¬ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))))
164162, 163sylib 218 . . . . 5 (𝜑 → ¬ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))))
165 euclemma 16746 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝐴‘0) ∈ ℤ ∧ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈ ℤ) → (𝑃 ∥ ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))))
16624, 80, 110, 165syl3anc 1370 . . . . 5 (𝜑 → (𝑃 ∥ ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))))
167164, 166mtbird 325 . . . 4 (𝜑 → ¬ 𝑃 ∥ ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))))
168103breq2d 5159 . . . 4 (𝜑 → (𝑃 ∥ (((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) ↔ 𝑃 ∥ ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))))
169167, 168mtbird 325 . . 3 (𝜑 → ¬ 𝑃 ∥ (((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))))
17046adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑃 ∈ ℤ)
171170, 122, 1353jca 1127 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (𝑃 ∈ ℤ ∧ (𝐴‘(1st𝑘)) ∈ ℤ ∧ ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))) ∈ ℤ))
172 eldifn 4141 . . . . . . . . . 10 (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) → ¬ 𝑘 ∈ {⟨0, (𝑃 − 1)⟩})
17391adantr 480 . . . . . . . . . . . . 13 ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∧ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0)) → 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))))
174 1st2nd2 8051 . . . . . . . . . . . . 13 (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → 𝑘 = ⟨(1st𝑘), (2nd𝑘)⟩)
175173, 174syl 17 . . . . . . . . . . . 12 ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∧ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0)) → 𝑘 = ⟨(1st𝑘), (2nd𝑘)⟩)
176 simpr 484 . . . . . . . . . . . . . 14 (((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0) → (1st𝑘) = 0)
177 simpl 482 . . . . . . . . . . . . . 14 (((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0) → (2nd𝑘) = (𝑃 − 1))
178176, 177opeq12d 4885 . . . . . . . . . . . . 13 (((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0) → ⟨(1st𝑘), (2nd𝑘)⟩ = ⟨0, (𝑃 − 1)⟩)
179178adantl 481 . . . . . . . . . . . 12 ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∧ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0)) → ⟨(1st𝑘), (2nd𝑘)⟩ = ⟨0, (𝑃 − 1)⟩)
180175, 179eqtrd 2774 . . . . . . . . . . 11 ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∧ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0)) → 𝑘 = ⟨0, (𝑃 − 1)⟩)
181 velsn 4646 . . . . . . . . . . 11 (𝑘 ∈ {⟨0, (𝑃 − 1)⟩} ↔ 𝑘 = ⟨0, (𝑃 − 1)⟩)
182180, 181sylibr 234 . . . . . . . . . 10 ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∧ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0)) → 𝑘 ∈ {⟨0, (𝑃 − 1)⟩})
183172, 182mtand 816 . . . . . . . . 9 (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) → ¬ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0))
184183adantl 481 . . . . . . . 8 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ¬ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0))
185125, 126, 30, 128, 129, 184, 105etransclem38 46227 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))))
186 dvdsmultr2 16331 . . . . . . 7 ((𝑃 ∈ ℤ ∧ (𝐴‘(1st𝑘)) ∈ ℤ ∧ ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))) ∈ ℤ) → (𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))) → 𝑃 ∥ ((𝐴‘(1st𝑘)) · ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))))))
187171, 185, 186sylc 65 . . . . . 6 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑃 ∥ ((𝐴‘(1st𝑘)) · ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1)))))
188187, 121breqtrrd 5175 . . . . 5 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑃 ∥ (((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
18990, 46, 137, 188fsumdvds 16341 . . . 4 (𝜑𝑃 ∥ Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})(((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
190189, 114breqtrrd 5175 . . 3 (𝜑𝑃 ∥ (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
19146, 100, 112, 139, 169, 190etransclem9 46198 . 2 (𝜑 → ((((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) + (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1)))) ≠ 0)
19299, 191eqnetrd 3005 1 (𝜑𝐾 ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1536  wcel 2105  wne 2937  {crab 3432  Vcvv 3477  cdif 3959  wss 3962  ifcif 4530  {csn 4630  {cpr 4632  cop 4636   class class class wbr 5147  cmpt 5230   × cxp 5686  ran crn 5689  wf 6558  cfv 6562  (class class class)co 7430  1st c1st 8010  2nd c2nd 8011  m cmap 8864  Fincfn 8983  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292  cle 11293  cmin 11489   / cdiv 11917  cn 12263  0cn0 12523  cz 12610  cuz 12875  (,)cioo 13383  ...cfz 13543  cexp 14098  !cfa 14308  abscabs 15269  Σcsu 15718  cprod 15935  cdvds 16286  cprime 16704  t crest 17466  TopOpenctopn 17467  topGenctg 17483  fldccnfld 21381   D𝑛 cdvn 25913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-prod 15936  df-dvds 16287  df-gcd 16528  df-prm 16705  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-mulg 19098  df-cntz 19347  df-cmn 19814  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-haus 23338  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-limc 25915  df-dv 25916  df-dvn 25917
This theorem is referenced by:  etransclem47  46236
  Copyright terms: Public domain W3C validator