Step | Hyp | Ref
| Expression |
1 | | fzfi 13155 |
. . . . . 6
⊢
(3...𝐽) ∈
Fin |
2 | | ssrab2 3946 |
. . . . . 6
⊢ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (3...𝐽) |
3 | | ssfi 8533 |
. . . . . 6
⊢
(((3...𝐽) ∈ Fin
∧ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (3...𝐽)) → {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
4 | 1, 2, 3 | mp2an 679 |
. . . . 5
⊢ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
6 | | nnnn0 11715 |
. . . . . . . 8
⊢ (𝐽 ∈ ℕ → 𝐽 ∈
ℕ0) |
7 | 6 | 3ad2ant3 1115 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 𝐽 ∈
ℕ0) |
8 | 2 | sseli 3854 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ (3...𝐽)) |
9 | | elfzelz 12724 |
. . . . . . . 8
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ ℤ) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ ℤ) |
11 | | bccl 13497 |
. . . . . . 7
⊢ ((𝐽 ∈ ℕ0
∧ 𝑎 ∈ ℤ)
→ (𝐽C𝑎) ∈
ℕ0) |
12 | 7, 10, 11 | syl2an 586 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈
ℕ0) |
13 | 12 | nn0zd 11898 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈ ℤ) |
14 | | simpl1 1171 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝐴 ∈
(ℤ≥‘2)) |
15 | | simpl2 1172 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑁 ∈ ℤ) |
16 | | frmx 38912 |
. . . . . . . . . 10
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
17 | 16 | fovcl 7095 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
18 | 14, 15, 17 | syl2anc 576 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
19 | 18 | nn0zd 11898 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈ ℤ) |
20 | 8 | adantl 474 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ (3...𝐽)) |
21 | | fznn0sub 12755 |
. . . . . . . 8
⊢ (𝑎 ∈ (3...𝐽) → (𝐽 − 𝑎) ∈
ℕ0) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽 − 𝑎) ∈
ℕ0) |
23 | | zexpcl 13259 |
. . . . . . 7
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐽 − 𝑎) ∈ ℕ0) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℤ) |
24 | 19, 22, 23 | syl2anc 576 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℤ) |
25 | | rmspecnonsq 38906 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈ (ℕ ∖
◻NN)) |
26 | 25 | eldifad 3841 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℕ) |
27 | 26 | nnzd 11899 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℤ) |
28 | 27 | 3ad2ant1 1113 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴↑2) − 1) ∈
ℤ) |
29 | | breq2 4933 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑎 → (2 ∥ 𝑏 ↔ 2 ∥ 𝑎)) |
30 | 29 | notbid 310 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑎 → (¬ 2 ∥ 𝑏 ↔ ¬ 2 ∥ 𝑎)) |
31 | 30 | elrab 3595 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ (𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
32 | 31 | simprbi 489 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 𝑎) |
33 | | 1zzd 11826 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 1 ∈ ℤ) |
34 | | n2dvds1 15577 |
. . . . . . . . . . . 12
⊢ ¬ 2
∥ 1 |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 1) |
36 | | omoe 15573 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℤ ∧ ¬ 2
∥ 𝑎) ∧ (1 ∈
ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑎 − 1)) |
37 | 10, 32, 33, 35, 36 | syl22anc 826 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∥ (𝑎 − 1)) |
38 | | 2z 11827 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∈ ℤ) |
40 | | 2ne0 11551 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
41 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ≠ 0) |
42 | | peano2zm 11838 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℤ → (𝑎 − 1) ∈
ℤ) |
43 | 10, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℤ) |
44 | | dvdsval2 15470 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ (𝑎 − 1) ∈ ℤ) → (2 ∥
(𝑎 − 1) ↔
((𝑎 − 1) / 2) ∈
ℤ)) |
45 | 39, 41, 43, 44 | syl3anc 1351 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (2 ∥ (𝑎 − 1) ↔ ((𝑎 − 1) / 2) ∈
ℤ)) |
46 | 37, 45 | mpbid 224 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℤ) |
47 | 43 | zred 11900 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℝ) |
48 | | 0red 10443 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 0 ∈ ℝ) |
49 | | 3re 11520 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 3 ∈ ℝ) |
51 | 9 | zred 11900 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ ℝ) |
52 | | 3pos 11552 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
3 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 0 < 3) |
54 | | elfzle1 12726 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 3 ≤ 𝑎) |
55 | 48, 50, 51, 53, 54 | ltletrd 10600 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (3...𝐽) → 0 < 𝑎) |
56 | | elnnz 11803 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 0 <
𝑎)) |
57 | 9, 55, 56 | sylanbrc 575 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ ℕ) |
58 | | nnm1nn0 11750 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → (𝑎 − 1) ∈
ℕ0) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → (𝑎 − 1) ∈
ℕ0) |
60 | 59 | nn0ge0d 11770 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (3...𝐽) → 0 ≤ (𝑎 − 1)) |
61 | 8, 60 | syl 17 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ (𝑎 − 1)) |
62 | | 2re 11514 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
63 | 62 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∈ ℝ) |
64 | | 2pos 11550 |
. . . . . . . . . . 11
⊢ 0 <
2 |
65 | 64 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 < 2) |
66 | | divge0 11310 |
. . . . . . . . . 10
⊢ ((((𝑎 − 1) ∈ ℝ ∧
0 ≤ (𝑎 − 1)) ∧
(2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑎 − 1) / 2)) |
67 | 47, 61, 63, 65, 66 | syl22anc 826 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ ((𝑎 − 1) / 2)) |
68 | | elnn0z 11806 |
. . . . . . . . 9
⊢ (((𝑎 − 1) / 2) ∈
ℕ0 ↔ (((𝑎 − 1) / 2) ∈ ℤ ∧ 0 ≤
((𝑎 − 1) /
2))) |
69 | 46, 67, 68 | sylanbrc 575 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℕ0) |
70 | | zexpcl 13259 |
. . . . . . . 8
⊢ ((((𝐴↑2) − 1) ∈
ℤ ∧ ((𝑎 −
1) / 2) ∈ ℕ0) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℤ) |
71 | 28, 69, 70 | syl2an 586 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℤ) |
72 | | frmy 38913 |
. . . . . . . . . 10
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
73 | 72 | fovcl 7095 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
74 | 14, 15, 73 | syl2anc 576 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Yrm 𝑁) ∈ ℤ) |
75 | | elfzel1 12723 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → 3 ∈ ℤ) |
76 | 9, 75 | zsubcld 11905 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (3...𝐽) → (𝑎 − 3) ∈ ℤ) |
77 | | subge0 10954 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 3 ∈
ℝ) → (0 ≤ (𝑎
− 3) ↔ 3 ≤ 𝑎)) |
78 | 51, 49, 77 | sylancl 577 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → (0 ≤ (𝑎 − 3) ↔ 3 ≤ 𝑎)) |
79 | 54, 78 | mpbird 249 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (3...𝐽) → 0 ≤ (𝑎 − 3)) |
80 | | elnn0z 11806 |
. . . . . . . . . . 11
⊢ ((𝑎 − 3) ∈
ℕ0 ↔ ((𝑎 − 3) ∈ ℤ ∧ 0 ≤
(𝑎 −
3))) |
81 | 76, 79, 80 | sylanbrc 575 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (3...𝐽) → (𝑎 − 3) ∈
ℕ0) |
82 | 8, 81 | syl 17 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 3) ∈
ℕ0) |
83 | 82 | adantl 474 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝑎 − 3) ∈
ℕ0) |
84 | | zexpcl 13259 |
. . . . . . . 8
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝑎 − 3) ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℤ) |
85 | 74, 83, 84 | syl2anc 576 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℤ) |
86 | 71, 85 | zmulcld 11906 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) ∈
ℤ) |
87 | 24, 86 | zmulcld 11906 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) ∈
ℤ) |
88 | 13, 87 | zmulcld 11906 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℤ) |
89 | 5, 88 | fsumzcl 14952 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℤ) |
90 | 73 | 3adant3 1112 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
91 | | 3nn0 11727 |
. . . 4
⊢ 3 ∈
ℕ0 |
92 | | zexpcl 13259 |
. . . 4
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ 3 ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ) |
93 | 90, 91, 92 | sylancl 577 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ) |
94 | | dvdsmul2 15492 |
. . 3
⊢
((Σ𝑎 ∈
{𝑏 ∈ (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 576 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ (Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3))) |
96 | | jm2.22 38994 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ0) → (𝐴 Yrm (𝑁 · 𝐽)) = Σ𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
97 | 6, 96 | syl3an3 1145 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm (𝑁 · 𝐽)) = Σ𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
98 | | 1lt3 11620 |
. . . . . . . . . . . 12
⊢ 1 <
3 |
99 | | 1re 10439 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
100 | 99, 49 | ltnlei 10561 |
. . . . . . . . . . . 12
⊢ (1 < 3
↔ ¬ 3 ≤ 1) |
101 | 98, 100 | mpbi 222 |
. . . . . . . . . . 11
⊢ ¬ 3
≤ 1 |
102 | | elfzle1 12726 |
. . . . . . . . . . 11
⊢ (1 ∈
(3...𝐽) → 3 ≤
1) |
103 | 101, 102 | mto 189 |
. . . . . . . . . 10
⊢ ¬ 1
∈ (3...𝐽) |
104 | 103 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ¬ 1 ∈
(3...𝐽)) |
105 | 104 | intnanrd 482 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ¬ (1 ∈
(3...𝐽) ∧ ¬ 2
∥ 1)) |
106 | | breq2 4933 |
. . . . . . . . . 10
⊢ (𝑏 = 1 → (2 ∥ 𝑏 ↔ 2 ∥
1)) |
107 | 106 | notbid 310 |
. . . . . . . . 9
⊢ (𝑏 = 1 → (¬ 2 ∥
𝑏 ↔ ¬ 2 ∥
1)) |
108 | 107 | elrab 3595 |
. . . . . . . 8
⊢ (1 ∈
{𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ (1 ∈ (3...𝐽) ∧ ¬ 2 ∥
1)) |
109 | 105, 108 | sylnibr 321 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ¬ 1 ∈
{𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) |
110 | | disjsn 4521 |
. . . . . . 7
⊢ (({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∩ {1}) = ∅ ↔ ¬ 1 ∈
{𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) |
111 | 109, 110 | sylibr 226 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∩ {1}) = ∅) |
112 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 = 1) → 𝑎 = 1) |
113 | 112 | olcd 860 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 = 1) → ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
114 | | elfznn0 12816 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (0...𝐽) → 𝑎 ∈ ℕ0) |
115 | 114 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → 𝑎 ∈ ℕ0) |
116 | 115 | ad2antlr 714 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ∈ ℕ0) |
117 | | simplrr 765 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → ¬ 2 ∥ 𝑎) |
118 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ≠ 1) |
119 | | elnn1uz2 12139 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℕ ↔ (𝑎 = 1 ∨ 𝑎 ∈
(ℤ≥‘2))) |
120 | | df-ne 2968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ≠ 1 ↔ ¬ 𝑎 = 1) |
121 | 120 | biimpi 208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ≠ 1 → ¬ 𝑎 = 1) |
122 | 121 | 3ad2ant3 1115 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) →
¬ 𝑎 =
1) |
123 | 122 | pm2.21d 119 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) →
(𝑎 = 1 → 3 ≤ 𝑎)) |
124 | 123 | imp 398 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 1) → 3 ≤ 𝑎) |
125 | | uzp1 12093 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈
(ℤ≥‘2) → (𝑎 = 2 ∨ 𝑎 ∈ (ℤ≥‘(2 +
1)))) |
126 | | 1z 11825 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℤ |
127 | | dvdsmul1 15491 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ ℤ ∧ 1 ∈ ℤ) → 2 ∥ (2 ·
1)) |
128 | 38, 126, 127 | mp2an 679 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∥
(2 · 1) |
129 | | 2t1e2 11610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2
· 1) = 2 |
130 | 128, 129 | breqtri 4954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∥
2 |
131 | | breq2 4933 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 2 → (2 ∥ 𝑎 ↔ 2 ∥
2)) |
132 | 131 | adantl 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → (2 ∥ 𝑎 ↔ 2 ∥
2)) |
133 | 130, 132 | mpbiri 250 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → 2 ∥ 𝑎) |
134 | | simpl2 1172 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → ¬ 2 ∥
𝑎) |
135 | 133, 134 | pm2.21dd 187 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → 3 ≤ 𝑎) |
136 | | eluzle 12071 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈
(ℤ≥‘3) → 3 ≤ 𝑎) |
137 | | 2p1e3 11589 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 + 1) =
3 |
138 | 137 | fveq2i 6502 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(ℤ≥‘(2 + 1)) =
(ℤ≥‘3) |
139 | 136, 138 | eleq2s 2884 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈
(ℤ≥‘(2 + 1)) → 3 ≤ 𝑎) |
140 | 139 | adantl 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 ∈
(ℤ≥‘(2 + 1))) → 3 ≤ 𝑎) |
141 | 135, 140 | jaodan 940 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧
(𝑎 = 2 ∨ 𝑎 ∈
(ℤ≥‘(2 + 1)))) → 3 ≤ 𝑎) |
142 | 125, 141 | sylan2 583 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 ∈
(ℤ≥‘2)) → 3 ≤ 𝑎) |
143 | 124, 142 | jaodan 940 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧
(𝑎 = 1 ∨ 𝑎 ∈
(ℤ≥‘2))) → 3 ≤ 𝑎) |
144 | 119, 143 | sylan2b 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 ∈ ℕ) → 3 ≤
𝑎) |
145 | | dvds0 15485 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℤ → 2 ∥ 0) |
146 | 38, 145 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∥
0 |
147 | | breq2 4933 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 0 → (2 ∥ 𝑎 ↔ 2 ∥
0)) |
148 | 146, 147 | mpbiri 250 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 0 → 2 ∥ 𝑎) |
149 | 148 | adantl 474 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 0) → 2 ∥ 𝑎) |
150 | | simpl2 1172 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 0) → ¬ 2 ∥
𝑎) |
151 | 149, 150 | pm2.21dd 187 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 0) → 3 ≤ 𝑎) |
152 | | elnn0 11709 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ℕ0
↔ (𝑎 ∈ ℕ
∨ 𝑎 =
0)) |
153 | 152 | biimpi 208 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℕ0
→ (𝑎 ∈ ℕ
∨ 𝑎 =
0)) |
154 | 153 | 3ad2ant1 1113 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) →
(𝑎 ∈ ℕ ∨
𝑎 = 0)) |
155 | 144, 151,
154 | mpjaodan 941 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) → 3
≤ 𝑎) |
156 | 116, 117,
118, 155 | syl3anc 1351 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 3 ≤ 𝑎) |
157 | | elfzle2 12727 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (0...𝐽) → 𝑎 ≤ 𝐽) |
158 | 157 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → 𝑎 ≤ 𝐽) |
159 | 158 | ad2antlr 714 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ≤ 𝐽) |
160 | | elfzelz 12724 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (0...𝐽) → 𝑎 ∈ ℤ) |
161 | 160 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → 𝑎 ∈ ℤ) |
162 | 161 | ad2antlr 714 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ∈ ℤ) |
163 | | 3z 11828 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℤ |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 3 ∈
ℤ) |
165 | | nnz 11817 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ ℕ → 𝐽 ∈
ℤ) |
166 | 165 | 3ad2ant3 1115 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 𝐽 ∈ ℤ) |
167 | 166 | ad2antrr 713 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝐽 ∈ ℤ) |
168 | | elfz 12714 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℤ ∧ 3 ∈
ℤ ∧ 𝐽 ∈
ℤ) → (𝑎 ∈
(3...𝐽) ↔ (3 ≤
𝑎 ∧ 𝑎 ≤ 𝐽))) |
169 | 162, 164,
167, 168 | syl3anc 1351 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → (𝑎 ∈ (3...𝐽) ↔ (3 ≤ 𝑎 ∧ 𝑎 ≤ 𝐽))) |
170 | 156, 159,
169 | mpbir2and 700 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ∈ (3...𝐽)) |
171 | 170, 117 | jca 504 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → (𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
172 | 171 | orcd 859 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
173 | 113, 172 | pm2.61dane 3055 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) → ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
174 | | nn0uz 12094 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
175 | 91, 174 | eleqtri 2864 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
(ℤ≥‘0) |
176 | | fzss1 12762 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
(ℤ≥‘0) → (3...𝐽) ⊆ (0...𝐽)) |
177 | 175, 176 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(3...𝐽) ⊆
(0...𝐽) |
178 | 177 | sseli 3854 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ (0...𝐽)) |
179 | 178 | anim1i 605 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
180 | 179 | adantl 474 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎)) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
181 | | 0le1 10964 |
. . . . . . . . . . . . 13
⊢ 0 ≤
1 |
182 | 181 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 0 ≤ 1) |
183 | | nnge1 11468 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ ℕ → 1 ≤
𝐽) |
184 | 183 | 3ad2ant3 1115 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 1 ≤ 𝐽) |
185 | 184 | adantr 473 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 1 ≤ 𝐽) |
186 | | 1zzd 11826 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 1 ∈
ℤ) |
187 | | 0zd 11805 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 0 ∈
ℤ) |
188 | 166 | adantr 473 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 𝐽 ∈ ℤ) |
189 | | elfz 12714 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℤ ∧ 0 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (1 ∈ (0...𝐽) ↔ (0 ≤ 1 ∧ 1 ≤
𝐽))) |
190 | 186, 187,
188, 189 | syl3anc 1351 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → (1 ∈ (0...𝐽) ↔ (0 ≤ 1 ∧ 1 ≤ 𝐽))) |
191 | 182, 185,
190 | mpbir2and 700 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 1 ∈ (0...𝐽)) |
192 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → ¬ 2 ∥
1) |
193 | | eleq1 2853 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 → (𝑎 ∈ (0...𝐽) ↔ 1 ∈ (0...𝐽))) |
194 | | breq2 4933 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 1 → (2 ∥ 𝑎 ↔ 2 ∥
1)) |
195 | 194 | notbid 310 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 → (¬ 2 ∥
𝑎 ↔ ¬ 2 ∥
1)) |
196 | 193, 195 | anbi12d 621 |
. . . . . . . . . . . 12
⊢ (𝑎 = 1 → ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) ↔ (1 ∈ (0...𝐽) ∧ ¬ 2 ∥
1))) |
197 | 196 | adantl 474 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) ↔ (1 ∈ (0...𝐽) ∧ ¬ 2 ∥
1))) |
198 | 191, 192,
197 | mpbir2and 700 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
199 | 180, 198 | jaodan 940 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
200 | 173, 199 | impbida 788 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) ↔ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1))) |
201 | 30 | elrab 3595 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
202 | | elun 4014 |
. . . . . . . . 9
⊢ (𝑎 ∈ ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1}) ↔ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∨ 𝑎 ∈ {1})) |
203 | | velsn 4457 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {1} ↔ 𝑎 = 1) |
204 | 31, 203 | orbi12i 898 |
. . . . . . . . 9
⊢ ((𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∨ 𝑎 ∈ {1}) ↔ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
205 | 202, 204 | bitri 267 |
. . . . . . . 8
⊢ (𝑎 ∈ ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1}) ↔ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
206 | 200, 201,
205 | 3bitr4g 306 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ 𝑎 ∈ ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1}))) |
207 | 206 | eqrdv 2776 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} = ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1})) |
208 | | fzfi 13155 |
. . . . . . . 8
⊢
(0...𝐽) ∈
Fin |
209 | | ssrab2 3946 |
. . . . . . . 8
⊢ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (0...𝐽) |
210 | | ssfi 8533 |
. . . . . . . 8
⊢
(((0...𝐽) ∈ Fin
∧ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (0...𝐽)) → {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
211 | 208, 209,
210 | mp2an 679 |
. . . . . . 7
⊢ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin |
212 | 211 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
213 | 209 | sseli 3854 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ (0...𝐽)) |
214 | 213, 160 | syl 17 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ ℤ) |
215 | 7, 214, 11 | syl2an 586 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈
ℕ0) |
216 | 215 | nn0cnd 11769 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈ ℂ) |
217 | 17 | 3adant3 1112 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
218 | 217 | nn0cnd 11769 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈ ℂ) |
219 | 218 | adantr 473 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈ ℂ) |
220 | 213 | adantl 474 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ (0...𝐽)) |
221 | | fznn0sub 12755 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0...𝐽) → (𝐽 − 𝑎) ∈
ℕ0) |
222 | 220, 221 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽 − 𝑎) ∈
ℕ0) |
223 | 219, 222 | expcld 13325 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℂ) |
224 | 90 | zcnd 11901 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℂ) |
225 | 213, 114 | syl 17 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ ℕ0) |
226 | | expcl 13262 |
. . . . . . . . . 10
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ 𝑎 ∈ ℕ0)
→ ((𝐴 Yrm
𝑁)↑𝑎) ∈ ℂ) |
227 | 224, 225,
226 | syl2an 586 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑𝑎) ∈ ℂ) |
228 | | rmspecpos 38915 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℝ+) |
229 | 228 | rpcnd 12250 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℂ) |
230 | 229 | 3ad2ant1 1113 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴↑2) − 1) ∈
ℂ) |
231 | 201 | simprbi 489 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 𝑎) |
232 | | 1zzd 11826 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 1 ∈ ℤ) |
233 | 34 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 1) |
234 | 214, 231,
232, 233, 36 | syl22anc 826 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∥ (𝑎 − 1)) |
235 | 38 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∈ ℤ) |
236 | 40 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ≠ 0) |
237 | 214, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℤ) |
238 | 235, 236,
237, 44 | syl3anc 1351 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (2 ∥ (𝑎 − 1) ↔ ((𝑎 − 1) / 2) ∈
ℤ)) |
239 | 234, 238 | mpbid 224 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℤ) |
240 | 237 | zred 11900 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℝ) |
241 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (0...𝐽) → (𝑎 = 0 → 2 ∥ 𝑎)) |
242 | 241 | con3dimp 400 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → ¬ 𝑎 = 0) |
243 | 201, 242 | sylbi 209 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 𝑎 = 0) |
244 | 225, 153 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 ∈ ℕ ∨ 𝑎 = 0)) |
245 | | orel2 874 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑎 = 0 → ((𝑎 ∈ ℕ ∨ 𝑎 = 0) → 𝑎 ∈ ℕ)) |
246 | 243, 244,
245 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ ℕ) |
247 | 246, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈
ℕ0) |
248 | 247 | nn0ge0d 11770 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ (𝑎 − 1)) |
249 | 62 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∈ ℝ) |
250 | 64 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 < 2) |
251 | 240, 248,
249, 250, 66 | syl22anc 826 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ ((𝑎 − 1) / 2)) |
252 | 239, 251,
68 | sylanbrc 575 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℕ0) |
253 | | expcl 13262 |
. . . . . . . . . 10
⊢ ((((𝐴↑2) − 1) ∈
ℂ ∧ ((𝑎 −
1) / 2) ∈ ℕ0) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℂ) |
254 | 230, 252,
253 | syl2an 586 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℂ) |
255 | 227, 254 | mulcld 10460 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))) ∈
ℂ) |
256 | 223, 255 | mulcld 10460 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)))) ∈
ℂ) |
257 | 216, 256 | mulcld 10460 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) ∈
ℂ) |
258 | 111, 207,
212, 257 | fsumsplit 14957 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘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 13262 |
. . . . . . . . 9
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ 3 ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑3) ∈ ℂ) |
260 | 224, 91, 259 | sylancl 577 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∈ ℂ) |
261 | 88 | zcnd 11901 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℂ) |
262 | 5, 260, 261 | fsummulc1 15000 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘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 11769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈ ℂ) |
264 | 218 | adantr 473 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈ ℂ) |
265 | 264, 22 | expcld 13325 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℂ) |
266 | 230, 69, 253 | syl2an 586 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℂ) |
267 | | expcl 13262 |
. . . . . . . . . . . . 13
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ (𝑎 − 3) ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℂ) |
268 | 224, 82, 267 | syl2an 586 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℂ) |
269 | 266, 268 | mulcld 10460 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) ∈
ℂ) |
270 | 265, 269 | mulcld 10460 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) ∈
ℂ) |
271 | 260 | adantr 473 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑3) ∈ ℂ) |
272 | 263, 270,
271 | mulassd 10463 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘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 10463 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘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 10463 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) · ((𝐴 Yrm 𝑁)↑3)) = ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
(((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)))) |
275 | 268, 271 | mulcld 10460 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) ∈ ℂ) |
276 | 266, 275 | mulcomd 10461 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
(((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3))) = ((((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))) |
277 | 224 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Yrm 𝑁) ∈ ℂ) |
278 | 91 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 3 ∈
ℕ0) |
279 | 277, 278,
83 | expaddd 13327 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑((𝑎 − 3) + 3)) = (((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3))) |
280 | 10 | adantl 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ ℤ) |
281 | 280 | zcnd 11901 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ ℂ) |
282 | | 3cn 11521 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℂ |
283 | | npcan 10696 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℂ ∧ 3 ∈
ℂ) → ((𝑎 −
3) + 3) = 𝑎) |
284 | 281, 282,
283 | sylancl 577 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝑎 − 3) + 3) = 𝑎) |
285 | 284 | oveq2d 6992 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑((𝑎 − 3) + 3)) = ((𝐴 Yrm 𝑁)↑𝑎)) |
286 | 279, 285 | eqtr3d 2816 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) = ((𝐴 Yrm 𝑁)↑𝑎)) |
287 | 286 | oveq1d 6991 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))) = (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))) |
288 | 274, 276,
287 | 3eqtrd 2818 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) · ((𝐴 Yrm 𝑁)↑3)) = (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))) |
289 | 288 | oveq2d 6992 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) · ((𝐴 Yrm 𝑁)↑3))) = (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2))))) |
290 | 273, 289 | eqtrd 2814 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) · ((𝐴 Yrm 𝑁)↑3)) = (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2))))) |
291 | 290 | oveq2d 6992 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · ((((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) · ((𝐴 Yrm 𝑁)↑3))) = ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
292 | 272, 291 | eqtrd 2814 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) = ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
293 | 292 | sumeq2dv 14920 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘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 2815 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) =
(Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3))) |
295 | | 1nn 11452 |
. . . . . . 7
⊢ 1 ∈
ℕ |
296 | | bccl 13497 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ ℕ0
∧ 1 ∈ ℤ) → (𝐽C1) ∈
ℕ0) |
297 | 6, 126, 296 | sylancl 577 |
. . . . . . . . . 10
⊢ (𝐽 ∈ ℕ → (𝐽C1) ∈
ℕ0) |
298 | 297 | nn0cnd 11769 |
. . . . . . . . 9
⊢ (𝐽 ∈ ℕ → (𝐽C1) ∈
ℂ) |
299 | 298 | 3ad2ant3 1115 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽C1) ∈ ℂ) |
300 | | nnm1nn0 11750 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ ℕ → (𝐽 − 1) ∈
ℕ0) |
301 | 300 | 3ad2ant3 1115 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽 − 1) ∈
ℕ0) |
302 | 218, 301 | expcld 13325 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Xrm 𝑁)↑(𝐽 − 1)) ∈
ℂ) |
303 | | 1nn0 11725 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
304 | | expcl 13262 |
. . . . . . . . . . 11
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ 1 ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑1) ∈ ℂ) |
305 | 224, 303,
304 | sylancl 577 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑1) ∈ ℂ) |
306 | | 1m1e0 11512 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
307 | 306 | oveq1i 6986 |
. . . . . . . . . . . . 13
⊢ ((1
− 1) / 2) = (0 / 2) |
308 | | 2cn 11515 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
309 | 308, 40 | div0i 11175 |
. . . . . . . . . . . . 13
⊢ (0 / 2) =
0 |
310 | 307, 309 | eqtri 2802 |
. . . . . . . . . . . 12
⊢ ((1
− 1) / 2) = 0 |
311 | | 0nn0 11724 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
312 | 310, 311 | eqeltri 2862 |
. . . . . . . . . . 11
⊢ ((1
− 1) / 2) ∈ ℕ0 |
313 | | expcl 13262 |
. . . . . . . . . . 11
⊢ ((((𝐴↑2) − 1) ∈
ℂ ∧ ((1 − 1) / 2) ∈ ℕ0) → (((𝐴↑2) − 1)↑((1
− 1) / 2)) ∈ ℂ) |
314 | 230, 312,
313 | sylancl 577 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑((1 − 1) /
2)) ∈ ℂ) |
315 | 305, 314 | mulcld 10460 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))) ∈ ℂ) |
316 | 302, 315 | mulcld 10460 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))) ∈ ℂ) |
317 | 299, 316 | mulcld 10460 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))) ∈ ℂ) |
318 | | oveq2 6984 |
. . . . . . . . 9
⊢ (𝑎 = 1 → (𝐽C𝑎) = (𝐽C1)) |
319 | | oveq2 6984 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → (𝐽 − 𝑎) = (𝐽 − 1)) |
320 | 319 | oveq2d 6992 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) = ((𝐴 Xrm 𝑁)↑(𝐽 − 1))) |
321 | | oveq2 6984 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → ((𝐴 Yrm 𝑁)↑𝑎) = ((𝐴 Yrm 𝑁)↑1)) |
322 | | oveq1 6983 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 → (𝑎 − 1) = (1 − 1)) |
323 | 322 | oveq1d 6991 |
. . . . . . . . . . . 12
⊢ (𝑎 = 1 → ((𝑎 − 1) / 2) = ((1 − 1) /
2)) |
324 | 323 | oveq2d 6992 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) = (((𝐴↑2) − 1)↑((1
− 1) / 2))) |
325 | 321, 324 | oveq12d 6994 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))) = (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1
− 1) / 2)))) |
326 | 320, 325 | oveq12d 6994 |
. . . . . . . . 9
⊢ (𝑎 = 1 → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)))) = (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))) |
327 | 318, 326 | oveq12d 6994 |
. . . . . . . 8
⊢ (𝑎 = 1 → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) = ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) |
328 | 327 | sumsn 14961 |
. . . . . . 7
⊢ ((1
∈ ℕ ∧ ((𝐽C1)
· (((𝐴
Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))) ∈ ℂ) → Σ𝑎 ∈ {1} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) = ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) |
329 | 295, 317,
328 | sylancr 578 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {1} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) = ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) |
330 | 294, 329 | oveq12d 6994 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘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)) + ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))))) |
331 | 97, 258, 330 | 3eqtrd 2818 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm (𝑁 · 𝐽)) = ((Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) + ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))))) |
332 | | bcn1 13488 |
. . . . . . 7
⊢ (𝐽 ∈ ℕ0
→ (𝐽C1) = 𝐽) |
333 | 7, 332 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽C1) = 𝐽) |
334 | 333 | eqcomd 2784 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 𝐽 = (𝐽C1)) |
335 | 224 | exp1d 13320 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑1) = (𝐴 Yrm 𝑁)) |
336 | 310 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((1 − 1) / 2)
= 0) |
337 | 336 | oveq2d 6992 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑((1 − 1) /
2)) = (((𝐴↑2) −
1)↑0)) |
338 | 230 | exp0d 13319 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑0) =
1) |
339 | 337, 338 | eqtrd 2814 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑((1 − 1) /
2)) = 1) |
340 | 335, 339 | oveq12d 6994 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))) = ((𝐴 Yrm
𝑁) ·
1)) |
341 | 224 | mulid1d 10457 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁) · 1) = (𝐴 Yrm 𝑁)) |
342 | 340, 341 | eqtr2d 2815 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm 𝑁) = (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))) |
343 | 342 | oveq2d 6992 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁)) = (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))) |
344 | 334, 343 | oveq12d 6994 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁))) = ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) |
345 | 331, 344 | oveq12d 6994 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁)))) = (((Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) + ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) − ((𝐽C1)
· (((𝐴
Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))))) |
346 | 5, 261 | fsumcl 14950 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℂ) |
347 | 346, 260 | mulcld 10460 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) ∈ ℂ) |
348 | 347, 317 | pncand 10799 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) + ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) − ((𝐽C1)
· (((𝐴
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 2814 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁)))) = (Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3))) |
350 | 95, 349 | breqtrrd 4957 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁))))) |