Metamath Proof Explorer

Theorem jm2.23

Description: Lemma for jm2.20nn . Truncate binomial expansion p-adicly. (Contributed by Stefan O'Rear, 26-Sep-2014)

Ref Expression
Assertion jm2.23 ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) − ( 𝐽 · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fzfi ⊢ ( 3 ... 𝐽 ) ∈ Fin
2 ssrab2 ⊢ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ⊆ ( 3 ... 𝐽 )
3 ssfi ⊢ ( ( ( 3 ... 𝐽 ) ∈ Fin ∧ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ⊆ ( 3 ... 𝐽 ) ) → { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∈ Fin )
4 1 2 3 mp2an ⊢ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∈ Fin
5 4 a1i ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∈ Fin )
6 nnnn0 ⊢ ( 𝐽 ∈ ℕ → 𝐽 ∈ ℕ0 )
7 6 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → 𝐽 ∈ ℕ0 )
8 2 sseli ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 𝑎 ∈ ( 3 ... 𝐽 ) )
9 elfzelz ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 𝑎 ∈ ℤ )
10 8 9 syl ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 𝑎 ∈ ℤ )
11 bccl ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑎 ∈ ℤ ) → ( 𝐽 C 𝑎 ) ∈ ℕ0 )
12 7 10 11 syl2an ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐽 C 𝑎 ) ∈ ℕ0 )
13 12 nn0zd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐽 C 𝑎 ) ∈ ℤ )
14 simpl1 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
15 simpl2 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → 𝑁 ∈ ℤ )
16 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
17 16 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
18 14 15 17 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
19 18 nn0zd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐴 Xrm 𝑁 ) ∈ ℤ )
20 8 adantl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → 𝑎 ∈ ( 3 ... 𝐽 ) )
21 fznn0sub ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → ( 𝐽 − 𝑎 ) ∈ ℕ0 )
22 20 21 syl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐽 − 𝑎 ) ∈ ℕ0 )
23 zexpcl ⊢ ( ( ( 𝐴 Xrm 𝑁 ) ∈ ℤ ∧ ( 𝐽 − 𝑎 ) ∈ ℕ0 ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) ∈ ℤ )
24 19 22 23 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) ∈ ℤ )
25 rmspecnonsq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
26 25 eldifad ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ )
27 26 nnzd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℤ )
28 27 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℤ )
29 breq2 ⊢ ( 𝑏 = 𝑎 → ( 2 ∥ 𝑏 ↔ 2 ∥ 𝑎 ) )
30 29 notbid ⊢ ( 𝑏 = 𝑎 → ( ¬ 2 ∥ 𝑏 ↔ ¬ 2 ∥ 𝑎 ) )
31 30 elrab ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ↔ ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) )
32 31 simprbi ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ¬ 2 ∥ 𝑎 )
33 1zzd ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 1 ∈ ℤ )
34 n2dvds1 ⊢ ¬ 2 ∥ 1
35 34 a1i ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ¬ 2 ∥ 1 )
36 omoe ⊢ ( ( ( 𝑎 ∈ ℤ ∧ ¬ 2 ∥ 𝑎 ) ∧ ( 1 ∈ ℤ ∧ ¬ 2 ∥ 1 ) ) → 2 ∥ ( 𝑎 − 1 ) )
37 10 32 33 35 36 syl22anc ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 2 ∥ ( 𝑎 − 1 ) )
38 2z ⊢ 2 ∈ ℤ
39 38 a1i ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 2 ∈ ℤ )
40 2ne0 ⊢ 2 ≠ 0
41 40 a1i ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 2 ≠ 0 )
42 peano2zm ⊢ ( 𝑎 ∈ ℤ → ( 𝑎 − 1 ) ∈ ℤ )
43 10 42 syl ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( 𝑎 − 1 ) ∈ ℤ )
44 dvdsval2 ⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ ( 𝑎 − 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝑎 − 1 ) ↔ ( ( 𝑎 − 1 ) / 2 ) ∈ ℤ ) )
45 39 41 43 44 syl3anc ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( 2 ∥ ( 𝑎 − 1 ) ↔ ( ( 𝑎 − 1 ) / 2 ) ∈ ℤ ) )
46 37 45 mpbid ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( ( 𝑎 − 1 ) / 2 ) ∈ ℤ )
47 43 zred ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( 𝑎 − 1 ) ∈ ℝ )
48 0red ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 0 ∈ ℝ )
49 3re ⊢ 3 ∈ ℝ
50 49 a1i ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 3 ∈ ℝ )
51 9 zred ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 𝑎 ∈ ℝ )
52 3pos ⊢ 0 < 3
53 52 a1i ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 0 < 3 )
54 elfzle1 ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 3 ≤ 𝑎 )
55 48 50 51 53 54 ltletrd ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 0 < 𝑎 )
56 elnnz ⊢ ( 𝑎 ∈ ℕ ↔ ( 𝑎 ∈ ℤ ∧ 0 < 𝑎 ) )
57 9 55 56 sylanbrc ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 𝑎 ∈ ℕ )
58 nnm1nn0 ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 − 1 ) ∈ ℕ0 )
59 57 58 syl ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → ( 𝑎 − 1 ) ∈ ℕ0 )
60 59 nn0ge0d ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 0 ≤ ( 𝑎 − 1 ) )
61 8 60 syl ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 0 ≤ ( 𝑎 − 1 ) )
62 2re ⊢ 2 ∈ ℝ
63 62 a1i ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 2 ∈ ℝ )
64 2pos ⊢ 0 < 2
65 64 a1i ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 0 < 2 )
66 divge0 ⊢ ( ( ( ( 𝑎 − 1 ) ∈ ℝ ∧ 0 ≤ ( 𝑎 − 1 ) ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → 0 ≤ ( ( 𝑎 − 1 ) / 2 ) )
67 47 61 63 65 66 syl22anc ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 0 ≤ ( ( 𝑎 − 1 ) / 2 ) )
68 elnn0z ⊢ ( ( ( 𝑎 − 1 ) / 2 ) ∈ ℕ0 ↔ ( ( ( 𝑎 − 1 ) / 2 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑎 − 1 ) / 2 ) ) )
69 46 67 68 sylanbrc ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( ( 𝑎 − 1 ) / 2 ) ∈ ℕ0 )
70 zexpcl ⊢ ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℤ ∧ ( ( 𝑎 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ∈ ℤ )
71 28 69 70 syl2an ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ∈ ℤ )
72 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
73 72 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
74 14 15 73 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
75 elfzel1 ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 3 ∈ ℤ )
76 9 75 zsubcld ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → ( 𝑎 − 3 ) ∈ ℤ )
77 subge0 ⊢ ( ( 𝑎 ∈ ℝ ∧ 3 ∈ ℝ ) → ( 0 ≤ ( 𝑎 − 3 ) ↔ 3 ≤ 𝑎 ) )
78 51 49 77 sylancl ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → ( 0 ≤ ( 𝑎 − 3 ) ↔ 3 ≤ 𝑎 ) )
79 54 78 mpbird ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 0 ≤ ( 𝑎 − 3 ) )
80 elnn0z ⊢ ( ( 𝑎 − 3 ) ∈ ℕ0 ↔ ( ( 𝑎 − 3 ) ∈ ℤ ∧ 0 ≤ ( 𝑎 − 3 ) ) )
81 76 79 80 sylanbrc ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → ( 𝑎 − 3 ) ∈ ℕ0 )
82 8 81 syl ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( 𝑎 − 3 ) ∈ ℕ0 )
83 82 adantl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝑎 − 3 ) ∈ ℕ0 )
84 zexpcl ⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ ( 𝑎 − 3 ) ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ∈ ℤ )
85 74 83 84 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ∈ ℤ )
86 71 85 zmulcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ∈ ℤ )
87 24 86 zmulcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ∈ ℤ )
88 13 87 zmulcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) ∈ ℤ )
89 5 88 fsumzcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) ∈ ℤ )
90 73 3adant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
91 3nn0 ⊢ 3 ∈ ℕ0
92 zexpcl ⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ 3 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∈ ℤ )
93 90 91 92 sylancl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∈ ℤ )
94 dvdsmul2 ⊢ ( ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∥ ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) )
95 89 93 94 syl2anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∥ ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) )
96 jm2.22 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ0 ) → ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) = Σ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) )
97 6 96 syl3an3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) = Σ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) )
98 1lt3 ⊢ 1 < 3
99 1re ⊢ 1 ∈ ℝ
100 99 49 ltnlei ⊢ ( 1 < 3 ↔ ¬ 3 ≤ 1 )
101 98 100 mpbi ⊢ ¬ 3 ≤ 1
102 elfzle1 ⊢ ( 1 ∈ ( 3 ... 𝐽 ) → 3 ≤ 1 )
103 101 102 mto ⊢ ¬ 1 ∈ ( 3 ... 𝐽 )
104 103 a1i ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ¬ 1 ∈ ( 3 ... 𝐽 ) )
105 104 intnanrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ¬ ( 1 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 1 ) )
106 breq2 ⊢ ( 𝑏 = 1 → ( 2 ∥ 𝑏 ↔ 2 ∥ 1 ) )
107 106 notbid ⊢ ( 𝑏 = 1 → ( ¬ 2 ∥ 𝑏 ↔ ¬ 2 ∥ 1 ) )
108 107 elrab ⊢ ( 1 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ↔ ( 1 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 1 ) )
109 105 108 sylnibr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ¬ 1 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } )
110 disjsn ⊢ ( ( { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∩ { 1 } ) = ∅ ↔ ¬ 1 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } )
111 109 110 sylibr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∩ { 1 } ) = ∅ )
112 simpr ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 = 1 ) → 𝑎 = 1 )
113 112 olcd ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 = 1 ) → ( ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ∨ 𝑎 = 1 ) )
114 elfznn0 ⊢ ( 𝑎 ∈ ( 0 ... 𝐽 ) → 𝑎 ∈ ℕ0 )
115 114 adantr ⊢ ( ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) → 𝑎 ∈ ℕ0 )
116 115 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → 𝑎 ∈ ℕ0 )
117 simplrr ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → ¬ 2 ∥ 𝑎 )
118 simpr ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → 𝑎 ≠ 1 )
119 elnn1uz2 ⊢ ( 𝑎 ∈ ℕ ↔ ( 𝑎 = 1 ∨ 𝑎 ∈ ( ℤ≥ ‘ 2 ) ) )
120 df-ne ⊢ ( 𝑎 ≠ 1 ↔ ¬ 𝑎 = 1 )
121 120 biimpi ⊢ ( 𝑎 ≠ 1 → ¬ 𝑎 = 1 )
122 121 3ad2ant3 ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) → ¬ 𝑎 = 1 )
123 122 pm2.21d ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) → ( 𝑎 = 1 → 3 ≤ 𝑎 ) )
124 123 imp ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 = 1 ) → 3 ≤ 𝑎 )
125 uzp1 ⊢ ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑎 = 2 ∨ 𝑎 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) ) )
126 1z ⊢ 1 ∈ ℤ
127 dvdsmul1 ⊢ ( ( 2 ∈ ℤ ∧ 1 ∈ ℤ ) → 2 ∥ ( 2 · 1 ) )
128 38 126 127 mp2an ⊢ 2 ∥ ( 2 · 1 )
129 2t1e2 ⊢ ( 2 · 1 ) = 2
130 128 129 breqtri ⊢ 2 ∥ 2
131 breq2 ⊢ ( 𝑎 = 2 → ( 2 ∥ 𝑎 ↔ 2 ∥ 2 ) )
132 131 adantl ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 = 2 ) → ( 2 ∥ 𝑎 ↔ 2 ∥ 2 ) )
133 130 132 mpbiri ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 = 2 ) → 2 ∥ 𝑎 )
134 simpl2 ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 = 2 ) → ¬ 2 ∥ 𝑎 )
135 133 134 pm2.21dd ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 = 2 ) → 3 ≤ 𝑎 )
136 eluzle ⊢ ( 𝑎 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑎 )
137 2p1e3 ⊢ ( 2 + 1 ) = 3
138 137 fveq2i ⊢ ( ℤ≥ ‘ ( 2 + 1 ) ) = ( ℤ≥ ‘ 3 )
139 136 138 eleq2s ⊢ ( 𝑎 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) → 3 ≤ 𝑎 )
140 139 adantl ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) ) → 3 ≤ 𝑎 )
141 135 140 jaodan ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ ( 𝑎 = 2 ∨ 𝑎 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) ) ) → 3 ≤ 𝑎 )
142 125 141 sylan2 ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 ∈ ( ℤ≥ ‘ 2 ) ) → 3 ≤ 𝑎 )
143 124 142 jaodan ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ ( 𝑎 = 1 ∨ 𝑎 ∈ ( ℤ≥ ‘ 2 ) ) ) → 3 ≤ 𝑎 )
144 119 143 sylan2b ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 ∈ ℕ ) → 3 ≤ 𝑎 )
145 dvds0 ⊢ ( 2 ∈ ℤ → 2 ∥ 0 )
146 38 145 ax-mp ⊢ 2 ∥ 0
147 breq2 ⊢ ( 𝑎 = 0 → ( 2 ∥ 𝑎 ↔ 2 ∥ 0 ) )
148 146 147 mpbiri ⊢ ( 𝑎 = 0 → 2 ∥ 𝑎 )
149 148 adantl ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 = 0 ) → 2 ∥ 𝑎 )
150 simpl2 ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 = 0 ) → ¬ 2 ∥ 𝑎 )
151 149 150 pm2.21dd ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) ∧ 𝑎 = 0 ) → 3 ≤ 𝑎 )
152 elnn0 ⊢ ( 𝑎 ∈ ℕ0 ↔ ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) )
153 152 biimpi ⊢ ( 𝑎 ∈ ℕ0 → ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) )
154 153 3ad2ant1 ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) → ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) )
155 144 151 154 mpjaodan ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑎 ∧ 𝑎 ≠ 1 ) → 3 ≤ 𝑎 )
156 116 117 118 155 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → 3 ≤ 𝑎 )
157 elfzle2 ⊢ ( 𝑎 ∈ ( 0 ... 𝐽 ) → 𝑎 ≤ 𝐽 )
158 157 adantr ⊢ ( ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) → 𝑎 ≤ 𝐽 )
159 158 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → 𝑎 ≤ 𝐽 )
160 elfzelz ⊢ ( 𝑎 ∈ ( 0 ... 𝐽 ) → 𝑎 ∈ ℤ )
161 160 adantr ⊢ ( ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) → 𝑎 ∈ ℤ )
162 161 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → 𝑎 ∈ ℤ )
163 3z ⊢ 3 ∈ ℤ
164 163 a1i ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → 3 ∈ ℤ )
165 nnz ⊢ ( 𝐽 ∈ ℕ → 𝐽 ∈ ℤ )
166 165 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → 𝐽 ∈ ℤ )
167 166 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → 𝐽 ∈ ℤ )
168 elfz ⊢ ( ( 𝑎 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝑎 ∈ ( 3 ... 𝐽 ) ↔ ( 3 ≤ 𝑎 ∧ 𝑎 ≤ 𝐽 ) ) )
169 162 164 167 168 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → ( 𝑎 ∈ ( 3 ... 𝐽 ) ↔ ( 3 ≤ 𝑎 ∧ 𝑎 ≤ 𝐽 ) ) )
170 156 159 169 mpbir2and ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → 𝑎 ∈ ( 3 ... 𝐽 ) )
171 170 117 jca ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) )
172 171 orcd ⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) ∧ 𝑎 ≠ 1 ) → ( ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ∨ 𝑎 = 1 ) )
173 113 172 pm2.61dane ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) → ( ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ∨ 𝑎 = 1 ) )
174 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
175 91 174 eleqtri ⊢ 3 ∈ ( ℤ≥ ‘ 0 )
176 fzss1 ⊢ ( 3 ∈ ( ℤ≥ ‘ 0 ) → ( 3 ... 𝐽 ) ⊆ ( 0 ... 𝐽 ) )
177 175 176 ax-mp ⊢ ( 3 ... 𝐽 ) ⊆ ( 0 ... 𝐽 )
178 177 sseli ⊢ ( 𝑎 ∈ ( 3 ... 𝐽 ) → 𝑎 ∈ ( 0 ... 𝐽 ) )
179 178 anim1i ⊢ ( ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) → ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) )
180 179 adantl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ) → ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) )
181 0le1 ⊢ 0 ≤ 1
182 181 a1i ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 = 1 ) → 0 ≤ 1 )
183 nnge1 ⊢ ( 𝐽 ∈ ℕ → 1 ≤ 𝐽 )
184 183 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → 1 ≤ 𝐽 )
185 184 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 = 1 ) → 1 ≤ 𝐽 )
186 1zzd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 = 1 ) → 1 ∈ ℤ )
187 0zd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 = 1 ) → 0 ∈ ℤ )
188 166 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 = 1 ) → 𝐽 ∈ ℤ )
189 elfz ⊢ ( ( 1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 1 ∈ ( 0 ... 𝐽 ) ↔ ( 0 ≤ 1 ∧ 1 ≤ 𝐽 ) ) )
190 186 187 188 189 syl3anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 = 1 ) → ( 1 ∈ ( 0 ... 𝐽 ) ↔ ( 0 ≤ 1 ∧ 1 ≤ 𝐽 ) ) )
191 182 185 190 mpbir2and ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 = 1 ) → 1 ∈ ( 0 ... 𝐽 ) )
192 34 a1i ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 = 1 ) → ¬ 2 ∥ 1 )
193 eleq1 ⊢ ( 𝑎 = 1 → ( 𝑎 ∈ ( 0 ... 𝐽 ) ↔ 1 ∈ ( 0 ... 𝐽 ) ) )
194 breq2 ⊢ ( 𝑎 = 1 → ( 2 ∥ 𝑎 ↔ 2 ∥ 1 ) )
195 194 notbid ⊢ ( 𝑎 = 1 → ( ¬ 2 ∥ 𝑎 ↔ ¬ 2 ∥ 1 ) )
196 193 195 anbi12d ⊢ ( 𝑎 = 1 → ( ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ↔ ( 1 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 1 ) ) )
197 196 adantl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 = 1 ) → ( ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ↔ ( 1 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 1 ) ) )
198 191 192 197 mpbir2and ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 = 1 ) → ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) )
199 180 198 jaodan ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ ( ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ∨ 𝑎 = 1 ) ) → ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) )
200 173 199 impbida ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ↔ ( ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ∨ 𝑎 = 1 ) ) )
201 30 elrab ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ↔ ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) )
202 elun ⊢ ( 𝑎 ∈ ( { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∪ { 1 } ) ↔ ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∨ 𝑎 ∈ { 1 } ) )
203 velsn ⊢ ( 𝑎 ∈ { 1 } ↔ 𝑎 = 1 )
204 31 203 orbi12i ⊢ ( ( 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∨ 𝑎 ∈ { 1 } ) ↔ ( ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ∨ 𝑎 = 1 ) )
205 202 204 bitri ⊢ ( 𝑎 ∈ ( { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∪ { 1 } ) ↔ ( ( 𝑎 ∈ ( 3 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) ∨ 𝑎 = 1 ) )
206 200 201 205 3bitr4g ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ↔ 𝑎 ∈ ( { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∪ { 1 } ) ) )
207 206 eqrdv ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } = ( { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∪ { 1 } ) )
208 fzfi ⊢ ( 0 ... 𝐽 ) ∈ Fin
209 ssrab2 ⊢ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ⊆ ( 0 ... 𝐽 )
210 ssfi ⊢ ( ( ( 0 ... 𝐽 ) ∈ Fin ∧ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ⊆ ( 0 ... 𝐽 ) ) → { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∈ Fin )
211 208 209 210 mp2an ⊢ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∈ Fin
212 211 a1i ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ∈ Fin )
213 209 sseli ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 𝑎 ∈ ( 0 ... 𝐽 ) )
214 213 160 syl ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 𝑎 ∈ ℤ )
215 7 214 11 syl2an ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐽 C 𝑎 ) ∈ ℕ0 )
216 215 nn0cnd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐽 C 𝑎 ) ∈ ℂ )
217 17 3adant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
218 217 nn0cnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
219 218 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
220 213 adantl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → 𝑎 ∈ ( 0 ... 𝐽 ) )
221 fznn0sub ⊢ ( 𝑎 ∈ ( 0 ... 𝐽 ) → ( 𝐽 − 𝑎 ) ∈ ℕ0 )
222 220 221 syl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐽 − 𝑎 ) ∈ ℕ0 )
223 219 222 expcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) ∈ ℂ )
224 90 zcnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
225 213 114 syl ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 𝑎 ∈ ℕ0 )
226 expcl ⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℂ ∧ 𝑎 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) ∈ ℂ )
227 224 225 226 syl2an ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) ∈ ℂ )
228 rmspecpos ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ+ )
229 228 rpcnd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
230 229 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
231 201 simprbi ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ¬ 2 ∥ 𝑎 )
232 1zzd ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 1 ∈ ℤ )
233 34 a1i ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ¬ 2 ∥ 1 )
234 214 231 232 233 36 syl22anc ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 2 ∥ ( 𝑎 − 1 ) )
235 38 a1i ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 2 ∈ ℤ )
236 40 a1i ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 2 ≠ 0 )
237 214 42 syl ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( 𝑎 − 1 ) ∈ ℤ )
238 235 236 237 44 syl3anc ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( 2 ∥ ( 𝑎 − 1 ) ↔ ( ( 𝑎 − 1 ) / 2 ) ∈ ℤ ) )
239 234 238 mpbid ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( ( 𝑎 − 1 ) / 2 ) ∈ ℤ )
240 237 zred ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( 𝑎 − 1 ) ∈ ℝ )
241 148 a1i ⊢ ( 𝑎 ∈ ( 0 ... 𝐽 ) → ( 𝑎 = 0 → 2 ∥ 𝑎 ) )
242 241 con3dimp ⊢ ( ( 𝑎 ∈ ( 0 ... 𝐽 ) ∧ ¬ 2 ∥ 𝑎 ) → ¬ 𝑎 = 0 )
243 201 242 sylbi ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ¬ 𝑎 = 0 )
244 225 153 syl ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) )
245 orel2 ⊢ ( ¬ 𝑎 = 0 → ( ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) → 𝑎 ∈ ℕ ) )
246 243 244 245 sylc ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 𝑎 ∈ ℕ )
247 246 58 syl ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( 𝑎 − 1 ) ∈ ℕ0 )
248 247 nn0ge0d ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 0 ≤ ( 𝑎 − 1 ) )
249 62 a1i ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 2 ∈ ℝ )
250 64 a1i ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 0 < 2 )
251 240 248 249 250 66 syl22anc ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → 0 ≤ ( ( 𝑎 − 1 ) / 2 ) )
252 239 251 68 sylanbrc ⊢ ( 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } → ( ( 𝑎 − 1 ) / 2 ) ∈ ℕ0 )
253 expcl ⊢ ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ ∧ ( ( 𝑎 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ∈ ℂ )
254 230 252 253 syl2an ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ∈ ℂ )
255 227 254 mulcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ∈ ℂ )
256 223 255 mulcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ∈ ℂ )
257 216 256 mulcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) ∈ ℂ )
258 111 207 212 257 fsumsplit ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → Σ 𝑎 ∈ { 𝑏 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) = ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) + Σ 𝑎 ∈ { 1 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) ) )
259 expcl ⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∈ ℂ )
260 224 91 259 sylancl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∈ ℂ )
261 88 zcnd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) ∈ ℂ )
262 5 260 261 fsummulc1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) = Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) )
263 12 nn0cnd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐽 C 𝑎 ) ∈ ℂ )
264 218 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
265 264 22 expcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) ∈ ℂ )
266 230 69 253 syl2an ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ∈ ℂ )
267 expcl ⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℂ ∧ ( 𝑎 − 3 ) ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ∈ ℂ )
268 224 82 267 syl2an ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ∈ ℂ )
269 266 268 mulcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ∈ ℂ )
270 265 269 mulcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ∈ ℂ )
271 260 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∈ ℂ )
272 263 270 271 mulassd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) = ( ( 𝐽 C 𝑎 ) · ( ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) ) )
273 265 269 271 mulassd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) ) )
274 266 268 271 mulassd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) = ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) ) )
275 268 271 mulcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) ∈ ℂ )
276 266 275 mulcomd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) ) = ( ( ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) )
277 224 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
278 91 a1i ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → 3 ∈ ℕ0 )
279 277 278 83 expaddd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐴 Yrm 𝑁 ) ↑ ( ( 𝑎 − 3 ) + 3 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) )
280 10 adantl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → 𝑎 ∈ ℤ )
281 280 zcnd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → 𝑎 ∈ ℂ )
282 3cn ⊢ 3 ∈ ℂ
283 npcan ⊢ ( ( 𝑎 ∈ ℂ ∧ 3 ∈ ℂ ) → ( ( 𝑎 − 3 ) + 3 ) = 𝑎 )
284 281 282 283 sylancl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝑎 − 3 ) + 3 ) = 𝑎 )
285 284 oveq2d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐴 Yrm 𝑁 ) ↑ ( ( 𝑎 − 3 ) + 3 ) ) = ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) )
286 279 285 eqtr3d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) = ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) )
287 286 oveq1d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) = ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) )
288 274 276 287 3eqtrd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) )
289 288 oveq2d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) )
290 273 289 eqtrd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) )
291 290 oveq2d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( 𝐽 C 𝑎 ) · ( ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) ) = ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) )
292 272 291 eqtrd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) ∧ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ) → ( ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) = ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) )
293 292 sumeq2dv ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) = Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) )
294 262 293 eqtr2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) = ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) )
295 1nn ⊢ 1 ∈ ℕ
296 bccl ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 1 ∈ ℤ ) → ( 𝐽 C 1 ) ∈ ℕ0 )
297 6 126 296 sylancl ⊢ ( 𝐽 ∈ ℕ → ( 𝐽 C 1 ) ∈ ℕ0 )
298 297 nn0cnd ⊢ ( 𝐽 ∈ ℕ → ( 𝐽 C 1 ) ∈ ℂ )
299 298 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐽 C 1 ) ∈ ℂ )
300 nnm1nn0 ⊢ ( 𝐽 ∈ ℕ → ( 𝐽 − 1 ) ∈ ℕ0 )
301 300 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐽 − 1 ) ∈ ℕ0 )
302 218 301 expcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) ∈ ℂ )
303 1nn0 ⊢ 1 ∈ ℕ0
304 expcl ⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℂ ∧ 1 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) ∈ ℂ )
305 224 303 304 sylancl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) ∈ ℂ )
306 1m1e0 ⊢ ( 1 − 1 ) = 0
307 306 oveq1i ⊢ ( ( 1 − 1 ) / 2 ) = ( 0 / 2 )
308 2cn ⊢ 2 ∈ ℂ
309 308 40 div0i ⊢ ( 0 / 2 ) = 0
310 307 309 eqtri ⊢ ( ( 1 − 1 ) / 2 ) = 0
311 0nn0 ⊢ 0 ∈ ℕ0
312 310 311 eqeltri ⊢ ( ( 1 − 1 ) / 2 ) ∈ ℕ0
313 expcl ⊢ ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ ∧ ( ( 1 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ∈ ℂ )
314 230 312 313 sylancl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ∈ ℂ )
315 305 314 mulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ∈ ℂ )
316 302 315 mulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ∈ ℂ )
317 299 316 mulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) ∈ ℂ )
318 oveq2 ⊢ ( 𝑎 = 1 → ( 𝐽 C 𝑎 ) = ( 𝐽 C 1 ) )
319 oveq2 ⊢ ( 𝑎 = 1 → ( 𝐽 − 𝑎 ) = ( 𝐽 − 1 ) )
320 319 oveq2d ⊢ ( 𝑎 = 1 → ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) = ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) )
321 oveq2 ⊢ ( 𝑎 = 1 → ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) = ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) )
322 oveq1 ⊢ ( 𝑎 = 1 → ( 𝑎 − 1 ) = ( 1 − 1 ) )
323 322 oveq1d ⊢ ( 𝑎 = 1 → ( ( 𝑎 − 1 ) / 2 ) = ( ( 1 − 1 ) / 2 ) )
324 323 oveq2d ⊢ ( 𝑎 = 1 → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) )
325 321 324 oveq12d ⊢ ( 𝑎 = 1 → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) = ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) )
326 320 325 oveq12d ⊢ ( 𝑎 = 1 → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) )
327 318 326 oveq12d ⊢ ( 𝑎 = 1 → ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) = ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) )
328 327 sumsn ⊢ ( ( 1 ∈ ℕ ∧ ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) ∈ ℂ ) → Σ 𝑎 ∈ { 1 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) = ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) )
329 295 317 328 sylancr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → Σ 𝑎 ∈ { 1 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) = ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) )
330 294 329 oveq12d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) + Σ 𝑎 ∈ { 1 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑎 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) ) ) ) ) = ( ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) + ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) ) )
331 97 258 330 3eqtrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) = ( ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) + ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) ) )
332 bcn1 ⊢ ( 𝐽 ∈ ℕ0 → ( 𝐽 C 1 ) = 𝐽 )
333 7 332 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐽 C 1 ) = 𝐽 )
334 333 eqcomd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → 𝐽 = ( 𝐽 C 1 ) )
335 224 exp1d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) = ( 𝐴 Yrm 𝑁 ) )
336 310 a1i ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 1 − 1 ) / 2 ) = 0 )
337 336 oveq2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ 0 ) )
338 230 exp0d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ 0 ) = 1 )
339 337 338 eqtrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) = 1 )
340 335 339 oveq12d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) = ( ( 𝐴 Yrm 𝑁 ) · 1 ) )
341 224 mulid1d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) · 1 ) = ( 𝐴 Yrm 𝑁 ) )
342 340 341 eqtr2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) = ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) )
343 342 oveq2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) )
344 334 343 oveq12d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( 𝐽 · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) )
345 331 344 oveq12d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) − ( 𝐽 · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) = ( ( ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) + ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) ) − ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) ) )
346 5 261 fsumcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) ∈ ℂ )
347 346 260 mulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) ∈ ℂ )
348 347 317 pncand ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) + ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) ) − ( ( 𝐽 C 1 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 1 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 1 − 1 ) / 2 ) ) ) ) ) ) = ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) )
349 345 348 eqtrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) − ( 𝐽 · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) = ( Σ 𝑎 ∈ { 𝑏 ∈ ( 3 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑏 } ( ( 𝐽 C 𝑎 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑎 ) ) · ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑎 − 1 ) / 2 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ ( 𝑎 − 3 ) ) ) ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ) )
350 95 349 breqtrrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) − ( 𝐽 · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )