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 44489
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 1917 . . . . 5 𝑘𝜑
4 nfcv 2906 . . . . 5 𝑘((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0))
5 fzfi 13874 . . . . . . 7 (0...𝑀) ∈ Fin
6 fzfi 13874 . . . . . . 7 (0...((𝑀 · 𝑃) + (𝑃 − 1))) ∈ Fin
7 xpfi 9258 . . . . . . 7 (((0...𝑀) ∈ Fin ∧ (0...((𝑀 · 𝑃) + (𝑃 − 1))) ∈ Fin) → ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin)
85, 6, 7mp2an 690 . . . . . 6 ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin
98a1i 11 . . . . 5 (𝜑 → ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin)
10 etransclem44.a . . . . . . . . 9 (𝜑𝐴:ℕ0⟶ℤ)
1110adantr 481 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝐴:ℕ0⟶ℤ)
12 fzssnn0 43525 . . . . . . . . . 10 (0...𝑀) ⊆ ℕ0
13 xp1st 7950 . . . . . . . . . 10 (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (1st𝑘) ∈ (0...𝑀))
1412, 13sselid 3941 . . . . . . . . 9 (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (1st𝑘) ∈ ℕ0)
1514adantl 482 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st𝑘) ∈ ℕ0)
1611, 15ffvelcdmd 7033 . . . . . . 7 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (𝐴‘(1st𝑘)) ∈ ℤ)
17 reelprrecn 11140 . . . . . . . . 9 ℝ ∈ {ℝ, ℂ}
1817a1i 11 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ℝ ∈ {ℝ, ℂ})
19 reopn 43497 . . . . . . . . . 10 ℝ ∈ (topGen‘ran (,))
20 eqid 2736 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
2120tgioo2 24162 . . . . . . . . . 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 16547 . . . . . . . . . 10 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2624, 25syl 17 . . . . . . . . 9 (𝜑𝑃 ∈ ℕ)
2726adantr 481 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝑃 ∈ ℕ)
28 etransclem44.m . . . . . . . . 9 (𝜑𝑀 ∈ ℕ0)
2928adantr 481 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝑀 ∈ ℕ0)
30 etransclem44.f . . . . . . . 8 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)))
31 xp2nd 7951 . . . . . . . . . 10 (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (2nd𝑘) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))))
32 elfznn0 13531 . . . . . . . . . 10 ((2nd𝑘) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))) → (2nd𝑘) ∈ ℕ0)
3331, 32syl 17 . . . . . . . . 9 (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (2nd𝑘) ∈ ℕ0)
3433adantl 482 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (2nd𝑘) ∈ ℕ0)
3515nn0red 12471 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st𝑘) ∈ ℝ)
3615nn0zd 12522 . . . . . . . 8 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st𝑘) ∈ ℤ)
3718, 23, 27, 29, 30, 34, 35, 36etransclem42 44487 . . . . . . 7 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ∈ ℤ)
3816, 37zmulcld 12610 . . . . . 6 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℤ)
3938zcnd 12605 . . . . 5 ((𝜑𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℂ)
40 nn0uz 12802 . . . . . . . 8 0 = (ℤ‘0)
4128, 40eleqtrdi 2848 . . . . . . 7 (𝜑𝑀 ∈ (ℤ‘0))
42 eluzfz1 13445 . . . . . . 7 (𝑀 ∈ (ℤ‘0) → 0 ∈ (0...𝑀))
4341, 42syl 17 . . . . . 6 (𝜑 → 0 ∈ (0...𝑀))
44 0zd 12508 . . . . . . 7 (𝜑 → 0 ∈ ℤ)
4528nn0zd 12522 . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
4626nnzd 12523 . . . . . . . . 9 (𝜑𝑃 ∈ ℤ)
4745, 46zmulcld 12610 . . . . . . . 8 (𝜑 → (𝑀 · 𝑃) ∈ ℤ)
48 nnm1nn0 12451 . . . . . . . . . 10 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
4926, 48syl 17 . . . . . . . . 9 (𝜑 → (𝑃 − 1) ∈ ℕ0)
5049nn0zd 12522 . . . . . . . 8 (𝜑 → (𝑃 − 1) ∈ ℤ)
5147, 50zaddcld 12608 . . . . . . 7 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℤ)
5249nn0ge0d 12473 . . . . . . 7 (𝜑 → 0 ≤ (𝑃 − 1))
5326nnnn0d 12470 . . . . . . . . . 10 (𝜑𝑃 ∈ ℕ0)
5428, 53nn0mulcld 12475 . . . . . . . . 9 (𝜑 → (𝑀 · 𝑃) ∈ ℕ0)
5554nn0ge0d 12473 . . . . . . . 8 (𝜑 → 0 ≤ (𝑀 · 𝑃))
5649nn0red 12471 . . . . . . . . 9 (𝜑 → (𝑃 − 1) ∈ ℝ)
5747zred 12604 . . . . . . . . 9 (𝜑 → (𝑀 · 𝑃) ∈ ℝ)
5856, 57addge02d 11741 . . . . . . . 8 (𝜑 → (0 ≤ (𝑀 · 𝑃) ↔ (𝑃 − 1) ≤ ((𝑀 · 𝑃) + (𝑃 − 1))))
5955, 58mpbid 231 . . . . . . 7 (𝜑 → (𝑃 − 1) ≤ ((𝑀 · 𝑃) + (𝑃 − 1)))
6044, 51, 50, 52, 59elfzd 13429 . . . . . 6 (𝜑 → (𝑃 − 1) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))))
61 opelxp 5668 . . . . . 6 (⟨0, (𝑃 − 1)⟩ ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ↔ (0 ∈ (0...𝑀) ∧ (𝑃 − 1) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))))
6243, 60, 61sylanbrc 583 . . . . 5 (𝜑 → ⟨0, (𝑃 − 1)⟩ ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))))
63 fveq2 6840 . . . . . . . 8 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (1st𝑘) = (1st ‘⟨0, (𝑃 − 1)⟩))
64 0re 11154 . . . . . . . . 9 0 ∈ ℝ
65 ovex 7387 . . . . . . . . 9 (𝑃 − 1) ∈ V
66 op1stg 7930 . . . . . . . . 9 ((0 ∈ ℝ ∧ (𝑃 − 1) ∈ V) → (1st ‘⟨0, (𝑃 − 1)⟩) = 0)
6764, 65, 66mp2an 690 . . . . . . . 8 (1st ‘⟨0, (𝑃 − 1)⟩) = 0
6863, 67eqtrdi 2792 . . . . . . 7 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (1st𝑘) = 0)
6968fveq2d 6844 . . . . . 6 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (𝐴‘(1st𝑘)) = (𝐴‘0))
70 fveq2 6840 . . . . . . . . 9 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (2nd𝑘) = (2nd ‘⟨0, (𝑃 − 1)⟩))
71 op2ndg 7931 . . . . . . . . . 10 ((0 ∈ ℝ ∧ (𝑃 − 1) ∈ V) → (2nd ‘⟨0, (𝑃 − 1)⟩) = (𝑃 − 1))
7264, 65, 71mp2an 690 . . . . . . . . 9 (2nd ‘⟨0, (𝑃 − 1)⟩) = (𝑃 − 1)
7370, 72eqtrdi 2792 . . . . . . . 8 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (2nd𝑘) = (𝑃 − 1))
7473fveq2d 6844 . . . . . . 7 (𝑘 = ⟨0, (𝑃 − 1)⟩ → ((ℝ D𝑛 𝐹)‘(2nd𝑘)) = ((ℝ D𝑛 𝐹)‘(𝑃 − 1)))
7574, 68fveq12d 6847 . . . . . 6 (𝑘 = ⟨0, (𝑃 − 1)⟩ → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) = (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0))
7669, 75oveq12d 7372 . . . . 5 (𝑘 = ⟨0, (𝑃 − 1)⟩ → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = ((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)))
773, 4, 9, 39, 62, 76fsumsplit1 15627 . . . 4 (𝜑 → Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = (((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) + Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))))
7877oveq1d 7369 . . 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 3941 . . . . . . 7 (𝜑 → 0 ∈ ℕ0)
8010, 79ffvelcdmd 7033 . . . . . 6 (𝜑 → (𝐴‘0) ∈ ℤ)
8117a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ {ℝ, ℂ})
8222a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
8364a1i 11 . . . . . . 7 (𝜑 → 0 ∈ ℝ)
8481, 82, 26, 28, 30, 49, 83, 44etransclem42 44487 . . . . . 6 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈ ℤ)
8580, 84zmulcld 12610 . . . . 5 (𝜑 → ((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) ∈ ℤ)
8685zcnd 12605 . . . 4 (𝜑 → ((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) ∈ ℂ)
87 difss 4090 . . . . . . . 8 (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ⊆ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))
88 ssfi 9114 . . . . . . . 8 ((((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin ∧ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ⊆ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∈ Fin)
898, 87, 88mp2an 690 . . . . . . 7 (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∈ Fin
9089a1i 11 . . . . . 6 (𝜑 → (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∈ Fin)
91 eldifi 4085 . . . . . . 7 (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) → 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))))
9291, 38sylan2 593 . . . . . 6 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℤ)
9390, 92fsumzcl 15617 . . . . 5 (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℤ)
9493zcnd 12605 . . . 4 (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) ∈ ℂ)
9549faccld 14181 . . . . 5 (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
9695nncnd 12166 . . . 4 (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
9795nnne0d 12200 . . . 4 (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
9886, 94, 96, 97divdird 11966 . . 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 2780 . 2 (𝜑𝐾 = ((((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) + (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1)))))
10026nnne0d 12200 . . 3 (𝜑𝑃 ≠ 0)
10180zcnd 12605 . . . . 5 (𝜑 → (𝐴‘0) ∈ ℂ)
10284zcnd 12605 . . . . 5 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈ ℂ)
103101, 102, 96, 97divassd 11963 . . . 4 (𝜑 → (((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) = ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))))
104 etransclem5 44450 . . . . . . 7 (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
105 etransclem11 44456 . . . . . . 7 (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑𝑘) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = 𝑛})
10681, 82, 26, 28, 30, 49, 104, 105, 43, 83etransclem37 44482 . . . . . 6 (𝜑 → (!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0))
10795nnzd 12523 . . . . . . 7 (𝜑 → (!‘(𝑃 − 1)) ∈ ℤ)
108 dvdsval2 16136 . . . . . . 7 (((!‘(𝑃 − 1)) ∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0 ∧ (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈ ℤ) → ((!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ↔ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈ ℤ))
109107, 97, 84, 108syl3anc 1371 . . . . . 6 (𝜑 → ((!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ↔ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈ ℤ))
110106, 109mpbid 231 . . . . 5 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈ ℤ)
11180, 110zmulcld 12610 . . . 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 15668 . . . 4 (𝜑 → (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))) = Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})(((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
11516zcnd 12605 . . . . . . . 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 12605 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ∈ ℂ)
11996adantr 481 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (!‘(𝑃 − 1)) ∈ ℂ)
12097adantr 481 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (!‘(𝑃 − 1)) ≠ 0)
121116, 118, 119, 120divassd 11963 . . . . . 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 481 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑃 ∈ ℕ)
12628adantr 481 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑀 ∈ ℕ0)
12791adantl 482 . . . . . . . . . 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 44482 . . . . . . . 8 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))
132107adantr 481 . . . . . . . . 9 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (!‘(𝑃 − 1)) ∈ ℤ)
133 dvdsval2 16136 . . . . . . . . 9 (((!‘(𝑃 − 1)) ∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0 ∧ (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ∈ ℤ) → ((!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ↔ ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))) ∈ ℤ))
134132, 120, 117, 133syl3anc 1371 . . . . . . . 8 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ((!‘(𝑃 − 1)) ∥ (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) ↔ ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))) ∈ ℤ))
135131, 134mpbid 231 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))) ∈ ℤ)
136122, 135zmulcld 12610 . . . . . 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 15617 . . . 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 12531 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
141 zabscl 15195 . . . . . . . . . . 11 ((𝐴‘0) ∈ ℤ → (abs‘(𝐴‘0)) ∈ ℤ)
14280, 141syl 17 . . . . . . . . . 10 (𝜑 → (abs‘(𝐴‘0)) ∈ ℤ)
143 nn0abscl 15194 . . . . . . . . . . . . 13 ((𝐴‘0) ∈ ℤ → (abs‘(𝐴‘0)) ∈ ℕ0)
14480, 143syl 17 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐴‘0)) ∈ ℕ0)
145 etransclem44.a0 . . . . . . . . . . . . 13 (𝜑 → (𝐴‘0) ≠ 0)
146101, 145absne0d 15329 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐴‘0)) ≠ 0)
147 elnnne0 12424 . . . . . . . . . . . 12 ((abs‘(𝐴‘0)) ∈ ℕ ↔ ((abs‘(𝐴‘0)) ∈ ℕ0 ∧ (abs‘(𝐴‘0)) ≠ 0))
148144, 146, 147sylanbrc 583 . . . . . . . . . . 11 (𝜑 → (abs‘(𝐴‘0)) ∈ ℕ)
149148nnge1d 12198 . . . . . . . . . 10 (𝜑 → 1 ≤ (abs‘(𝐴‘0)))
150 etransclem44.ap . . . . . . . . . . 11 (𝜑 → (abs‘(𝐴‘0)) < 𝑃)
151 zltlem1 12553 . . . . . . . . . . . 12 (((abs‘(𝐴‘0)) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((abs‘(𝐴‘0)) < 𝑃 ↔ (abs‘(𝐴‘0)) ≤ (𝑃 − 1)))
152142, 46, 151syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐴‘0)) < 𝑃 ↔ (abs‘(𝐴‘0)) ≤ (𝑃 − 1)))
153150, 152mpbid 231 . . . . . . . . . 10 (𝜑 → (abs‘(𝐴‘0)) ≤ (𝑃 − 1))
154140, 50, 142, 149, 153elfzd 13429 . . . . . . . . 9 (𝜑 → (abs‘(𝐴‘0)) ∈ (1...(𝑃 − 1)))
155 fzm1ndvds 16201 . . . . . . . . 9 ((𝑃 ∈ ℕ ∧ (abs‘(𝐴‘0)) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (abs‘(𝐴‘0)))
15626, 154, 155syl2anc 584 . . . . . . . 8 (𝜑 → ¬ 𝑃 ∥ (abs‘(𝐴‘0)))
157 dvdsabsb 16155 . . . . . . . . 9 ((𝑃 ∈ ℤ ∧ (𝐴‘0) ∈ ℤ) → (𝑃 ∥ (𝐴‘0) ↔ 𝑃 ∥ (abs‘(𝐴‘0))))
15846, 80, 157syl2anc 584 . . . . . . . 8 (𝜑 → (𝑃 ∥ (𝐴‘0) ↔ 𝑃 ∥ (abs‘(𝐴‘0))))
159156, 158mtbird 324 . . . . . . 7 (𝜑 → ¬ 𝑃 ∥ (𝐴‘0))
160 etransclem44.mp . . . . . . . 8 (𝜑 → (!‘𝑀) < 𝑃)
16128, 24, 160, 30etransclem41 44486 . . . . . . 7 (𝜑 → ¬ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))
162159, 161jca 512 . . . . . 6 (𝜑 → (¬ 𝑃 ∥ (𝐴‘0) ∧ ¬ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))))
163 pm4.56 987 . . . . . 6 ((¬ 𝑃 ∥ (𝐴‘0) ∧ ¬ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ ¬ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))))
164162, 163sylib 217 . . . . 5 (𝜑 → ¬ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))))
165 euclemma 16586 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝐴‘0) ∈ ℤ ∧ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈ ℤ) → (𝑃 ∥ ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))))
16624, 80, 110, 165syl3anc 1371 . . . . 5 (𝜑 → (𝑃 ∥ ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))))
167164, 166mtbird 324 . . . 4 (𝜑 → ¬ 𝑃 ∥ ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))))
168103breq2d 5116 . . . 4 (𝜑 → (𝑃 ∥ (((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) ↔ 𝑃 ∥ ((𝐴‘0) · ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))))
169167, 168mtbird 324 . . 3 (𝜑 → ¬ 𝑃 ∥ (((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))))
17046adantr 481 . . . . . . . 8 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑃 ∈ ℤ)
171170, 122, 1353jca 1128 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → (𝑃 ∈ ℤ ∧ (𝐴‘(1st𝑘)) ∈ ℤ ∧ ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))) ∈ ℤ))
172 eldifn 4086 . . . . . . . . . 10 (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) → ¬ 𝑘 ∈ {⟨0, (𝑃 − 1)⟩})
17391adantr 481 . . . . . . . . . . . . 13 ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∧ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0)) → 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))))
174 1st2nd2 7957 . . . . . . . . . . . . 13 (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → 𝑘 = ⟨(1st𝑘), (2nd𝑘)⟩)
175173, 174syl 17 . . . . . . . . . . . 12 ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∧ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0)) → 𝑘 = ⟨(1st𝑘), (2nd𝑘)⟩)
176 simpr 485 . . . . . . . . . . . . . 14 (((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0) → (1st𝑘) = 0)
177 simpl 483 . . . . . . . . . . . . . 14 (((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0) → (2nd𝑘) = (𝑃 − 1))
178176, 177opeq12d 4837 . . . . . . . . . . . . 13 (((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0) → ⟨(1st𝑘), (2nd𝑘)⟩ = ⟨0, (𝑃 − 1)⟩)
179178adantl 482 . . . . . . . . . . . 12 ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∧ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0)) → ⟨(1st𝑘), (2nd𝑘)⟩ = ⟨0, (𝑃 − 1)⟩)
180175, 179eqtrd 2776 . . . . . . . . . . 11 ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∧ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0)) → 𝑘 = ⟨0, (𝑃 − 1)⟩)
181 velsn 4601 . . . . . . . . . . 11 (𝑘 ∈ {⟨0, (𝑃 − 1)⟩} ↔ 𝑘 = ⟨0, (𝑃 − 1)⟩)
182180, 181sylibr 233 . . . . . . . . . 10 ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) ∧ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0)) → 𝑘 ∈ {⟨0, (𝑃 − 1)⟩})
183172, 182mtand 814 . . . . . . . . 9 (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩}) → ¬ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0))
184183adantl 482 . . . . . . . 8 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → ¬ ((2nd𝑘) = (𝑃 − 1) ∧ (1st𝑘) = 0))
185125, 126, 30, 128, 129, 184, 105etransclem38 44483 . . . . . . 7 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) / (!‘(𝑃 − 1))))
186 dvdsmultr2 16177 . . . . . . 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 5132 . . . . 5 ((𝜑𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})) → 𝑃 ∥ (((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
18990, 46, 137, 188fsumdvds 16187 . . . 4 (𝜑𝑃 ∥ Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})(((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
190189, 114breqtrrd 5132 . . 3 (𝜑𝑃 ∥ (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
19146, 100, 112, 139, 169, 190etransclem9 44454 . 2 (𝜑 → ((((𝐴‘0) · (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) + (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {⟨0, (𝑃 − 1)⟩})((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1)))) ≠ 0)
19299, 191eqnetrd 3010 1 (𝜑𝐾 ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2942  {crab 3406  Vcvv 3444  cdif 3906  wss 3909  ifcif 4485  {csn 4585  {cpr 4587  cop 4591   class class class wbr 5104  cmpt 5187   × cxp 5630  ran crn 5633  wf 6490  cfv 6494  (class class class)co 7354  1st c1st 7916  2nd c2nd 7917  m cmap 8762  Fincfn 8880  cc 11046  cr 11047  0cc0 11048  1c1 11049   + caddc 11051   · cmul 11053   < clt 11186  cle 11187  cmin 11382   / cdiv 11809  cn 12150  0cn0 12410  cz 12496  cuz 12760  (,)cioo 13261  ...cfz 13421  cexp 13964  !cfa 14170  abscabs 15116  Σcsu 15567  cprod 15785  cdvds 16133  cprime 16544  t crest 17299  TopOpenctopn 17300  topGenctg 17316  fldccnfld 20792   D𝑛 cdvn 25224
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7669  ax-inf2 9574  ax-cnex 11104  ax-resscn 11105  ax-1cn 11106  ax-icn 11107  ax-addcl 11108  ax-addrcl 11109  ax-mulcl 11110  ax-mulrcl 11111  ax-mulcom 11112  ax-addass 11113  ax-mulass 11114  ax-distr 11115  ax-i2m1 11116  ax-1ne0 11117  ax-1rid 11118  ax-rnegex 11119  ax-rrecex 11120  ax-cnre 11121  ax-pre-lttri 11122  ax-pre-lttrn 11123  ax-pre-ltadd 11124  ax-pre-mulgt0 11125  ax-pre-sup 11126  ax-addf 11127  ax-mulf 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-iin 4956  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5530  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5587  df-se 5588  df-we 5589  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6252  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-isom 6503  df-riota 7310  df-ov 7357  df-oprab 7358  df-mpo 7359  df-of 7614  df-om 7800  df-1st 7918  df-2nd 7919  df-supp 8090  df-frecs 8209  df-wrecs 8240  df-recs 8314  df-rdg 8353  df-1o 8409  df-2o 8410  df-er 8645  df-map 8764  df-pm 8765  df-ixp 8833  df-en 8881  df-dom 8882  df-sdom 8883  df-fin 8884  df-fsupp 9303  df-fi 9344  df-sup 9375  df-inf 9376  df-oi 9443  df-card 9872  df-pnf 11188  df-mnf 11189  df-xr 11190  df-ltxr 11191  df-le 11192  df-sub 11384  df-neg 11385  df-div 11810  df-nn 12151  df-2 12213  df-3 12214  df-4 12215  df-5 12216  df-6 12217  df-7 12218  df-8 12219  df-9 12220  df-n0 12411  df-z 12497  df-dec 12616  df-uz 12761  df-q 12871  df-rp 12913  df-xneg 13030  df-xadd 13031  df-xmul 13032  df-ioo 13265  df-ico 13267  df-icc 13268  df-fz 13422  df-fzo 13565  df-fl 13694  df-mod 13772  df-seq 13904  df-exp 13965  df-fac 14171  df-bc 14200  df-hash 14228  df-cj 14981  df-re 14982  df-im 14983  df-sqrt 15117  df-abs 15118  df-clim 15367  df-sum 15568  df-prod 15786  df-dvds 16134  df-gcd 16372  df-prm 16545  df-struct 17016  df-sets 17033  df-slot 17051  df-ndx 17063  df-base 17081  df-ress 17110  df-plusg 17143  df-mulr 17144  df-starv 17145  df-sca 17146  df-vsca 17147  df-ip 17148  df-tset 17149  df-ple 17150  df-ds 17152  df-unif 17153  df-hom 17154  df-cco 17155  df-rest 17301  df-topn 17302  df-0g 17320  df-gsum 17321  df-topgen 17322  df-pt 17323  df-prds 17326  df-xrs 17381  df-qtop 17386  df-imas 17387  df-xps 17389  df-mre 17463  df-mrc 17464  df-acs 17466  df-mgm 18494  df-sgrp 18543  df-mnd 18554  df-submnd 18599  df-mulg 18869  df-cntz 19093  df-cmn 19560  df-psmet 20784  df-xmet 20785  df-met 20786  df-bl 20787  df-mopn 20788  df-fbas 20789  df-fg 20790  df-cnfld 20793  df-top 22239  df-topon 22256  df-topsp 22278  df-bases 22292  df-cld 22366  df-ntr 22367  df-cls 22368  df-nei 22445  df-lp 22483  df-perf 22484  df-cn 22574  df-cnp 22575  df-haus 22662  df-tx 22909  df-hmeo 23102  df-fil 23193  df-fm 23285  df-flim 23286  df-flf 23287  df-xms 23669  df-ms 23670  df-tms 23671  df-cncf 24237  df-limc 25226  df-dv 25227  df-dvn 25228
This theorem is referenced by:  etransclem47  44492
  Copyright terms: Public domain W3C validator