Step | Hyp | Ref
| Expression |
1 | | fzfi 13692 |
. . . . . 6
⊢
(3...𝐽) ∈
Fin |
2 | | ssrab2 4013 |
. . . . . 6
⊢ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (3...𝐽) |
3 | | ssfi 8956 |
. . . . . 6
⊢
(((3...𝐽) ∈ Fin
∧ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (3...𝐽)) → {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
4 | 1, 2, 3 | mp2an 689 |
. . . . 5
⊢ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
6 | | nnnn0 12240 |
. . . . . . . 8
⊢ (𝐽 ∈ ℕ → 𝐽 ∈
ℕ0) |
7 | 6 | 3ad2ant3 1134 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 𝐽 ∈
ℕ0) |
8 | 2 | sseli 3917 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ (3...𝐽)) |
9 | | elfzelz 13256 |
. . . . . . . 8
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ ℤ) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ ℤ) |
11 | | bccl 14036 |
. . . . . . 7
⊢ ((𝐽 ∈ ℕ0
∧ 𝑎 ∈ ℤ)
→ (𝐽C𝑎) ∈
ℕ0) |
12 | 7, 10, 11 | syl2an 596 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈
ℕ0) |
13 | 12 | nn0zd 12424 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈ ℤ) |
14 | | simpl1 1190 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝐴 ∈
(ℤ≥‘2)) |
15 | | simpl2 1191 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑁 ∈ ℤ) |
16 | | frmx 40735 |
. . . . . . . . . 10
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
17 | 16 | fovcl 7402 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
18 | 14, 15, 17 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
19 | 18 | nn0zd 12424 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈ ℤ) |
20 | 8 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ (3...𝐽)) |
21 | | fznn0sub 13288 |
. . . . . . . 8
⊢ (𝑎 ∈ (3...𝐽) → (𝐽 − 𝑎) ∈
ℕ0) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽 − 𝑎) ∈
ℕ0) |
23 | | zexpcl 13797 |
. . . . . . 7
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐽 − 𝑎) ∈ ℕ0) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℤ) |
24 | 19, 22, 23 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℤ) |
25 | | rmspecnonsq 40729 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈ (ℕ ∖
◻NN)) |
26 | 25 | eldifad 3899 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℕ) |
27 | 26 | nnzd 12425 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℤ) |
28 | 27 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴↑2) − 1) ∈
ℤ) |
29 | | breq2 5078 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑎 → (2 ∥ 𝑏 ↔ 2 ∥ 𝑎)) |
30 | 29 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑎 → (¬ 2 ∥ 𝑏 ↔ ¬ 2 ∥ 𝑎)) |
31 | 30 | elrab 3624 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ (𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
32 | 31 | simprbi 497 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 𝑎) |
33 | | 1zzd 12351 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 1 ∈ ℤ) |
34 | | n2dvds1 16077 |
. . . . . . . . . . . 12
⊢ ¬ 2
∥ 1 |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 1) |
36 | | omoe 16073 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℤ ∧ ¬ 2
∥ 𝑎) ∧ (1 ∈
ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑎 − 1)) |
37 | 10, 32, 33, 35, 36 | syl22anc 836 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∥ (𝑎 − 1)) |
38 | | 2z 12352 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∈ ℤ) |
40 | | 2ne0 12077 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
41 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ≠ 0) |
42 | | peano2zm 12363 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℤ → (𝑎 − 1) ∈
ℤ) |
43 | 10, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℤ) |
44 | | dvdsval2 15966 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ (𝑎 − 1) ∈ ℤ) → (2 ∥
(𝑎 − 1) ↔
((𝑎 − 1) / 2) ∈
ℤ)) |
45 | 39, 41, 43, 44 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (2 ∥ (𝑎 − 1) ↔ ((𝑎 − 1) / 2) ∈
ℤ)) |
46 | 37, 45 | mpbid 231 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℤ) |
47 | 43 | zred 12426 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℝ) |
48 | | 0red 10978 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 0 ∈ ℝ) |
49 | | 3re 12053 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 3 ∈ ℝ) |
51 | 9 | zred 12426 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ ℝ) |
52 | | 3pos 12078 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
3 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 0 < 3) |
54 | | elfzle1 13259 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 3 ≤ 𝑎) |
55 | 48, 50, 51, 53, 54 | ltletrd 11135 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (3...𝐽) → 0 < 𝑎) |
56 | | elnnz 12329 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 0 <
𝑎)) |
57 | 9, 55, 56 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ ℕ) |
58 | | nnm1nn0 12274 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → (𝑎 − 1) ∈
ℕ0) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → (𝑎 − 1) ∈
ℕ0) |
60 | 59 | nn0ge0d 12296 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (3...𝐽) → 0 ≤ (𝑎 − 1)) |
61 | 8, 60 | syl 17 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ (𝑎 − 1)) |
62 | | 2re 12047 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
63 | 62 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∈ ℝ) |
64 | | 2pos 12076 |
. . . . . . . . . . 11
⊢ 0 <
2 |
65 | 64 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 < 2) |
66 | | divge0 11844 |
. . . . . . . . . 10
⊢ ((((𝑎 − 1) ∈ ℝ ∧
0 ≤ (𝑎 − 1)) ∧
(2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑎 − 1) / 2)) |
67 | 47, 61, 63, 65, 66 | syl22anc 836 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ ((𝑎 − 1) / 2)) |
68 | | elnn0z 12332 |
. . . . . . . . 9
⊢ (((𝑎 − 1) / 2) ∈
ℕ0 ↔ (((𝑎 − 1) / 2) ∈ ℤ ∧ 0 ≤
((𝑎 − 1) /
2))) |
69 | 46, 67, 68 | sylanbrc 583 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℕ0) |
70 | | zexpcl 13797 |
. . . . . . . 8
⊢ ((((𝐴↑2) − 1) ∈
ℤ ∧ ((𝑎 −
1) / 2) ∈ ℕ0) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℤ) |
71 | 28, 69, 70 | syl2an 596 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℤ) |
72 | | frmy 40736 |
. . . . . . . . . 10
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
73 | 72 | fovcl 7402 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
74 | 14, 15, 73 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Yrm 𝑁) ∈ ℤ) |
75 | | elfzel1 13255 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → 3 ∈ ℤ) |
76 | 9, 75 | zsubcld 12431 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (3...𝐽) → (𝑎 − 3) ∈ ℤ) |
77 | | subge0 11488 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 3 ∈
ℝ) → (0 ≤ (𝑎
− 3) ↔ 3 ≤ 𝑎)) |
78 | 51, 49, 77 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → (0 ≤ (𝑎 − 3) ↔ 3 ≤ 𝑎)) |
79 | 54, 78 | mpbird 256 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (3...𝐽) → 0 ≤ (𝑎 − 3)) |
80 | | elnn0z 12332 |
. . . . . . . . . . 11
⊢ ((𝑎 − 3) ∈
ℕ0 ↔ ((𝑎 − 3) ∈ ℤ ∧ 0 ≤
(𝑎 −
3))) |
81 | 76, 79, 80 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (3...𝐽) → (𝑎 − 3) ∈
ℕ0) |
82 | 8, 81 | syl 17 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 3) ∈
ℕ0) |
83 | 82 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝑎 − 3) ∈
ℕ0) |
84 | | zexpcl 13797 |
. . . . . . . 8
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝑎 − 3) ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℤ) |
85 | 74, 83, 84 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℤ) |
86 | 71, 85 | zmulcld 12432 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) ∈
ℤ) |
87 | 24, 86 | zmulcld 12432 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) ∈
ℤ) |
88 | 13, 87 | zmulcld 12432 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℤ) |
89 | 5, 88 | fsumzcl 15447 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℤ) |
90 | 73 | 3adant3 1131 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
91 | | 3nn0 12251 |
. . . 4
⊢ 3 ∈
ℕ0 |
92 | | zexpcl 13797 |
. . . 4
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ 3 ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ) |
93 | 90, 91, 92 | sylancl 586 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ) |
94 | | dvdsmul2 15988 |
. . 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 584 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ (Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3))) |
96 | | jm2.22 40817 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ0) → (𝐴 Yrm (𝑁 · 𝐽)) = Σ𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
97 | 6, 96 | syl3an3 1164 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm (𝑁 · 𝐽)) = Σ𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
98 | | 1lt3 12146 |
. . . . . . . . . . . 12
⊢ 1 <
3 |
99 | | 1re 10975 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
100 | 99, 49 | ltnlei 11096 |
. . . . . . . . . . . 12
⊢ (1 < 3
↔ ¬ 3 ≤ 1) |
101 | 98, 100 | mpbi 229 |
. . . . . . . . . . 11
⊢ ¬ 3
≤ 1 |
102 | | elfzle1 13259 |
. . . . . . . . . . 11
⊢ (1 ∈
(3...𝐽) → 3 ≤
1) |
103 | 101, 102 | mto 196 |
. . . . . . . . . 10
⊢ ¬ 1
∈ (3...𝐽) |
104 | 103 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ¬ 1 ∈
(3...𝐽)) |
105 | 104 | intnanrd 490 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ¬ (1 ∈
(3...𝐽) ∧ ¬ 2
∥ 1)) |
106 | | breq2 5078 |
. . . . . . . . . 10
⊢ (𝑏 = 1 → (2 ∥ 𝑏 ↔ 2 ∥
1)) |
107 | 106 | notbid 318 |
. . . . . . . . 9
⊢ (𝑏 = 1 → (¬ 2 ∥
𝑏 ↔ ¬ 2 ∥
1)) |
108 | 107 | elrab 3624 |
. . . . . . . 8
⊢ (1 ∈
{𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ (1 ∈ (3...𝐽) ∧ ¬ 2 ∥
1)) |
109 | 105, 108 | sylnibr 329 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ¬ 1 ∈
{𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) |
110 | | disjsn 4647 |
. . . . . . 7
⊢ (({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∩ {1}) = ∅ ↔ ¬ 1 ∈
{𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) |
111 | 109, 110 | sylibr 233 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∩ {1}) = ∅) |
112 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 = 1) → 𝑎 = 1) |
113 | 112 | olcd 871 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 = 1) → ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
114 | | 3z 12353 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℤ |
115 | 114 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 3 ∈
ℤ) |
116 | | nnz 12342 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ ℕ → 𝐽 ∈
ℤ) |
117 | 116 | 3ad2ant3 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 𝐽 ∈ ℤ) |
118 | 117 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝐽 ∈ ℤ) |
119 | | elfzelz 13256 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (0...𝐽) → 𝑎 ∈ ℤ) |
120 | 119 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → 𝑎 ∈ ℤ) |
121 | 120 | ad2antlr 724 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ∈ ℤ) |
122 | | elfznn0 13349 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (0...𝐽) → 𝑎 ∈ ℕ0) |
123 | 122 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → 𝑎 ∈ ℕ0) |
124 | 123 | ad2antlr 724 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ∈ ℕ0) |
125 | | simplrr 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → ¬ 2 ∥ 𝑎) |
126 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ≠ 1) |
127 | | elnn1uz2 12665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℕ ↔ (𝑎 = 1 ∨ 𝑎 ∈
(ℤ≥‘2))) |
128 | | df-ne 2944 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ≠ 1 ↔ ¬ 𝑎 = 1) |
129 | 128 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ≠ 1 → ¬ 𝑎 = 1) |
130 | 129 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) →
¬ 𝑎 =
1) |
131 | 130 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) →
(𝑎 = 1 → 3 ≤ 𝑎)) |
132 | 131 | imp 407 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 1) → 3 ≤ 𝑎) |
133 | | uzp1 12619 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈
(ℤ≥‘2) → (𝑎 = 2 ∨ 𝑎 ∈ (ℤ≥‘(2 +
1)))) |
134 | | 1z 12350 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℤ |
135 | | dvdsmul1 15987 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ ℤ ∧ 1 ∈ ℤ) → 2 ∥ (2 ·
1)) |
136 | 38, 134, 135 | mp2an 689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∥
(2 · 1) |
137 | | 2t1e2 12136 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2
· 1) = 2 |
138 | 136, 137 | breqtri 5099 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∥
2 |
139 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 2 → (2 ∥ 𝑎 ↔ 2 ∥
2)) |
140 | 139 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → (2 ∥ 𝑎 ↔ 2 ∥
2)) |
141 | 138, 140 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → 2 ∥ 𝑎) |
142 | | simpl2 1191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → ¬ 2 ∥
𝑎) |
143 | 141, 142 | pm2.21dd 194 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → 3 ≤ 𝑎) |
144 | | eluzle 12595 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈
(ℤ≥‘3) → 3 ≤ 𝑎) |
145 | | 2p1e3 12115 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 + 1) =
3 |
146 | 145 | fveq2i 6777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(ℤ≥‘(2 + 1)) =
(ℤ≥‘3) |
147 | 144, 146 | eleq2s 2857 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈
(ℤ≥‘(2 + 1)) → 3 ≤ 𝑎) |
148 | 147 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 ∈
(ℤ≥‘(2 + 1))) → 3 ≤ 𝑎) |
149 | 143, 148 | jaodan 955 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧
(𝑎 = 2 ∨ 𝑎 ∈
(ℤ≥‘(2 + 1)))) → 3 ≤ 𝑎) |
150 | 133, 149 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 ∈
(ℤ≥‘2)) → 3 ≤ 𝑎) |
151 | 132, 150 | jaodan 955 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧
(𝑎 = 1 ∨ 𝑎 ∈
(ℤ≥‘2))) → 3 ≤ 𝑎) |
152 | 127, 151 | sylan2b 594 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 ∈ ℕ) → 3 ≤
𝑎) |
153 | | dvds0 15981 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℤ → 2 ∥ 0) |
154 | 38, 153 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∥
0 |
155 | | breq2 5078 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 0 → (2 ∥ 𝑎 ↔ 2 ∥
0)) |
156 | 154, 155 | mpbiri 257 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 0 → 2 ∥ 𝑎) |
157 | 156 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 0) → 2 ∥ 𝑎) |
158 | | simpl2 1191 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 0) → ¬ 2 ∥
𝑎) |
159 | 157, 158 | pm2.21dd 194 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 0) → 3 ≤ 𝑎) |
160 | | elnn0 12235 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ℕ0
↔ (𝑎 ∈ ℕ
∨ 𝑎 =
0)) |
161 | 160 | biimpi 215 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℕ0
→ (𝑎 ∈ ℕ
∨ 𝑎 =
0)) |
162 | 161 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) →
(𝑎 ∈ ℕ ∨
𝑎 = 0)) |
163 | 152, 159,
162 | mpjaodan 956 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) → 3
≤ 𝑎) |
164 | 124, 125,
126, 163 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 3 ≤ 𝑎) |
165 | | elfzle2 13260 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (0...𝐽) → 𝑎 ≤ 𝐽) |
166 | 165 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → 𝑎 ≤ 𝐽) |
167 | 166 | ad2antlr 724 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ≤ 𝐽) |
168 | 115, 118,
121, 164, 167 | elfzd 13247 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ∈ (3...𝐽)) |
169 | 168, 125 | jca 512 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → (𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
170 | 169 | orcd 870 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
171 | 113, 170 | pm2.61dane 3032 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) → ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
172 | | nn0uz 12620 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
173 | 91, 172 | eleqtri 2837 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
(ℤ≥‘0) |
174 | | fzss1 13295 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
(ℤ≥‘0) → (3...𝐽) ⊆ (0...𝐽)) |
175 | 173, 174 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(3...𝐽) ⊆
(0...𝐽) |
176 | 175 | sseli 3917 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ (0...𝐽)) |
177 | 176 | anim1i 615 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
178 | 177 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎)) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
179 | | 0zd 12331 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 0 ∈
ℤ) |
180 | 117 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 𝐽 ∈ ℤ) |
181 | | 1zzd 12351 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 1 ∈
ℤ) |
182 | | 0le1 11498 |
. . . . . . . . . . . . 13
⊢ 0 ≤
1 |
183 | 182 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 0 ≤ 1) |
184 | | nnge1 12001 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ ℕ → 1 ≤
𝐽) |
185 | 184 | 3ad2ant3 1134 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 1 ≤ 𝐽) |
186 | 185 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 1 ≤ 𝐽) |
187 | 179, 180,
181, 183, 186 | elfzd 13247 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 1 ∈ (0...𝐽)) |
188 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → ¬ 2 ∥
1) |
189 | | eleq1 2826 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 → (𝑎 ∈ (0...𝐽) ↔ 1 ∈ (0...𝐽))) |
190 | | breq2 5078 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 1 → (2 ∥ 𝑎 ↔ 2 ∥
1)) |
191 | 190 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 → (¬ 2 ∥
𝑎 ↔ ¬ 2 ∥
1)) |
192 | 189, 191 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ (𝑎 = 1 → ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) ↔ (1 ∈ (0...𝐽) ∧ ¬ 2 ∥
1))) |
193 | 192 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) ↔ (1 ∈ (0...𝐽) ∧ ¬ 2 ∥
1))) |
194 | 187, 188,
193 | mpbir2and 710 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
195 | 178, 194 | jaodan 955 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
196 | 171, 195 | impbida 798 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) ↔ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1))) |
197 | 30 | elrab 3624 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
198 | | elun 4083 |
. . . . . . . . 9
⊢ (𝑎 ∈ ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1}) ↔ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∨ 𝑎 ∈ {1})) |
199 | | velsn 4577 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {1} ↔ 𝑎 = 1) |
200 | 31, 199 | orbi12i 912 |
. . . . . . . . 9
⊢ ((𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∨ 𝑎 ∈ {1}) ↔ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
201 | 198, 200 | bitri 274 |
. . . . . . . 8
⊢ (𝑎 ∈ ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1}) ↔ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
202 | 196, 197,
201 | 3bitr4g 314 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ 𝑎 ∈ ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1}))) |
203 | 202 | eqrdv 2736 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} = ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1})) |
204 | | fzfi 13692 |
. . . . . . . 8
⊢
(0...𝐽) ∈
Fin |
205 | | ssrab2 4013 |
. . . . . . . 8
⊢ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (0...𝐽) |
206 | | ssfi 8956 |
. . . . . . . 8
⊢
(((0...𝐽) ∈ Fin
∧ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (0...𝐽)) → {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
207 | 204, 205,
206 | mp2an 689 |
. . . . . . 7
⊢ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin |
208 | 207 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
209 | 205 | sseli 3917 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ (0...𝐽)) |
210 | 209, 119 | syl 17 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ ℤ) |
211 | 7, 210, 11 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈
ℕ0) |
212 | 211 | nn0cnd 12295 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈ ℂ) |
213 | 17 | 3adant3 1131 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
214 | 213 | nn0cnd 12295 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈ ℂ) |
215 | 214 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈ ℂ) |
216 | 209 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ (0...𝐽)) |
217 | | fznn0sub 13288 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0...𝐽) → (𝐽 − 𝑎) ∈
ℕ0) |
218 | 216, 217 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽 − 𝑎) ∈
ℕ0) |
219 | 215, 218 | expcld 13864 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℂ) |
220 | 90 | zcnd 12427 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℂ) |
221 | 209, 122 | syl 17 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ ℕ0) |
222 | | expcl 13800 |
. . . . . . . . . 10
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ 𝑎 ∈ ℕ0)
→ ((𝐴 Yrm
𝑁)↑𝑎) ∈ ℂ) |
223 | 220, 221,
222 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑𝑎) ∈ ℂ) |
224 | | rmspecpos 40738 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℝ+) |
225 | 224 | rpcnd 12774 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℂ) |
226 | 225 | 3ad2ant1 1132 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴↑2) − 1) ∈
ℂ) |
227 | 197 | simprbi 497 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 𝑎) |
228 | | 1zzd 12351 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 1 ∈ ℤ) |
229 | 34 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 1) |
230 | 210, 227,
228, 229, 36 | syl22anc 836 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∥ (𝑎 − 1)) |
231 | 38 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∈ ℤ) |
232 | 40 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ≠ 0) |
233 | 210, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℤ) |
234 | 231, 232,
233, 44 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (2 ∥ (𝑎 − 1) ↔ ((𝑎 − 1) / 2) ∈
ℤ)) |
235 | 230, 234 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℤ) |
236 | 233 | zred 12426 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℝ) |
237 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (0...𝐽) → (𝑎 = 0 → 2 ∥ 𝑎)) |
238 | 237 | con3dimp 409 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → ¬ 𝑎 = 0) |
239 | 197, 238 | sylbi 216 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 𝑎 = 0) |
240 | 221, 161 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 ∈ ℕ ∨ 𝑎 = 0)) |
241 | | orel2 888 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑎 = 0 → ((𝑎 ∈ ℕ ∨ 𝑎 = 0) → 𝑎 ∈ ℕ)) |
242 | 239, 240,
241 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ ℕ) |
243 | 242, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈
ℕ0) |
244 | 243 | nn0ge0d 12296 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ (𝑎 − 1)) |
245 | 62 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∈ ℝ) |
246 | 64 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 < 2) |
247 | 236, 244,
245, 246, 66 | syl22anc 836 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ ((𝑎 − 1) / 2)) |
248 | 235, 247,
68 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℕ0) |
249 | | expcl 13800 |
. . . . . . . . . 10
⊢ ((((𝐴↑2) − 1) ∈
ℂ ∧ ((𝑎 −
1) / 2) ∈ ℕ0) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℂ) |
250 | 226, 248,
249 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℂ) |
251 | 223, 250 | mulcld 10995 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))) ∈
ℂ) |
252 | 219, 251 | mulcld 10995 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)))) ∈
ℂ) |
253 | 212, 252 | mulcld 10995 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) ∈
ℂ) |
254 | 111, 203,
208, 253 | fsumsplit 15453 |
. . . . 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))))))) |
255 | | expcl 13800 |
. . . . . . . . 9
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ 3 ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑3) ∈ ℂ) |
256 | 220, 91, 255 | sylancl 586 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∈ ℂ) |
257 | 88 | zcnd 12427 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℂ) |
258 | 5, 256, 257 | fsummulc1 15497 |
. . . . . . 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))) |
259 | 12 | nn0cnd 12295 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈ ℂ) |
260 | 214 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈ ℂ) |
261 | 260, 22 | expcld 13864 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℂ) |
262 | 226, 69, 249 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℂ) |
263 | | expcl 13800 |
. . . . . . . . . . . . 13
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ (𝑎 − 3) ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℂ) |
264 | 220, 82, 263 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℂ) |
265 | 262, 264 | mulcld 10995 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) ∈
ℂ) |
266 | 261, 265 | mulcld 10995 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) ∈
ℂ) |
267 | 256 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑3) ∈ ℂ) |
268 | 259, 266,
267 | mulassd 10998 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) = ((𝐽C𝑎) · ((((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) · ((𝐴 Yrm 𝑁)↑3)))) |
269 | 261, 265,
267 | mulassd 10998 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) · ((𝐴 Yrm 𝑁)↑3)) = (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) · ((𝐴 Yrm 𝑁)↑3)))) |
270 | 262, 264,
267 | mulassd 10998 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) · ((𝐴 Yrm 𝑁)↑3)) = ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
(((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)))) |
271 | 264, 267 | mulcld 10995 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) ∈ ℂ) |
272 | 262, 271 | mulcomd 10996 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
(((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3))) = ((((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))) |
273 | 220 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Yrm 𝑁) ∈ ℂ) |
274 | 91 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 3 ∈
ℕ0) |
275 | 273, 274,
83 | expaddd 13866 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑((𝑎 − 3) + 3)) = (((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3))) |
276 | 10 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ ℤ) |
277 | 276 | zcnd 12427 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ ℂ) |
278 | | 3cn 12054 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℂ |
279 | | npcan 11230 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℂ ∧ 3 ∈
ℂ) → ((𝑎 −
3) + 3) = 𝑎) |
280 | 277, 278,
279 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝑎 − 3) + 3) = 𝑎) |
281 | 280 | oveq2d 7291 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑((𝑎 − 3) + 3)) = ((𝐴 Yrm 𝑁)↑𝑎)) |
282 | 275, 281 | eqtr3d 2780 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) = ((𝐴 Yrm 𝑁)↑𝑎)) |
283 | 282 | oveq1d 7290 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))) = (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))) |
284 | 270, 272,
283 | 3eqtrd 2782 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) · ((𝐴 Yrm 𝑁)↑3)) = (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))) |
285 | 284 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) · ((𝐴 Yrm 𝑁)↑3))) = (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2))))) |
286 | 269, 285 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) · ((𝐴 Yrm 𝑁)↑3)) = (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2))))) |
287 | 286 | oveq2d 7291 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · ((((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) · ((𝐴 Yrm 𝑁)↑3))) = ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
288 | 268, 287 | eqtrd 2778 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) = ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
289 | 288 | sumeq2dv 15415 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} (((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) = Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
290 | 258, 289 | eqtr2d 2779 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) =
(Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3))) |
291 | | 1nn 11984 |
. . . . . . 7
⊢ 1 ∈
ℕ |
292 | | bccl 14036 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ ℕ0
∧ 1 ∈ ℤ) → (𝐽C1) ∈
ℕ0) |
293 | 6, 134, 292 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝐽 ∈ ℕ → (𝐽C1) ∈
ℕ0) |
294 | 293 | nn0cnd 12295 |
. . . . . . . . 9
⊢ (𝐽 ∈ ℕ → (𝐽C1) ∈
ℂ) |
295 | 294 | 3ad2ant3 1134 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽C1) ∈ ℂ) |
296 | | nnm1nn0 12274 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ ℕ → (𝐽 − 1) ∈
ℕ0) |
297 | 296 | 3ad2ant3 1134 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽 − 1) ∈
ℕ0) |
298 | 214, 297 | expcld 13864 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Xrm 𝑁)↑(𝐽 − 1)) ∈
ℂ) |
299 | | 1nn0 12249 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
300 | | expcl 13800 |
. . . . . . . . . . 11
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ 1 ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑1) ∈ ℂ) |
301 | 220, 299,
300 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑1) ∈ ℂ) |
302 | | 1m1e0 12045 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
303 | 302 | oveq1i 7285 |
. . . . . . . . . . . . 13
⊢ ((1
− 1) / 2) = (0 / 2) |
304 | | 2cn 12048 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
305 | 304, 40 | div0i 11709 |
. . . . . . . . . . . . 13
⊢ (0 / 2) =
0 |
306 | 303, 305 | eqtri 2766 |
. . . . . . . . . . . 12
⊢ ((1
− 1) / 2) = 0 |
307 | | 0nn0 12248 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
308 | 306, 307 | eqeltri 2835 |
. . . . . . . . . . 11
⊢ ((1
− 1) / 2) ∈ ℕ0 |
309 | | expcl 13800 |
. . . . . . . . . . 11
⊢ ((((𝐴↑2) − 1) ∈
ℂ ∧ ((1 − 1) / 2) ∈ ℕ0) → (((𝐴↑2) − 1)↑((1
− 1) / 2)) ∈ ℂ) |
310 | 226, 308,
309 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑((1 − 1) /
2)) ∈ ℂ) |
311 | 301, 310 | mulcld 10995 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))) ∈ ℂ) |
312 | 298, 311 | mulcld 10995 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))) ∈ ℂ) |
313 | 295, 312 | mulcld 10995 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))) ∈ ℂ) |
314 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑎 = 1 → (𝐽C𝑎) = (𝐽C1)) |
315 | | oveq2 7283 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → (𝐽 − 𝑎) = (𝐽 − 1)) |
316 | 315 | oveq2d 7291 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) = ((𝐴 Xrm 𝑁)↑(𝐽 − 1))) |
317 | | oveq2 7283 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → ((𝐴 Yrm 𝑁)↑𝑎) = ((𝐴 Yrm 𝑁)↑1)) |
318 | | oveq1 7282 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 → (𝑎 − 1) = (1 − 1)) |
319 | 318 | oveq1d 7290 |
. . . . . . . . . . . 12
⊢ (𝑎 = 1 → ((𝑎 − 1) / 2) = ((1 − 1) /
2)) |
320 | 319 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) = (((𝐴↑2) − 1)↑((1
− 1) / 2))) |
321 | 317, 320 | oveq12d 7293 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))) = (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1
− 1) / 2)))) |
322 | 316, 321 | oveq12d 7293 |
. . . . . . . . 9
⊢ (𝑎 = 1 → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)))) = (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))) |
323 | 314, 322 | oveq12d 7293 |
. . . . . . . 8
⊢ (𝑎 = 1 → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) = ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) |
324 | 323 | sumsn 15458 |
. . . . . . 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)))))) |
325 | 291, 313,
324 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {1} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) = ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) |
326 | 290, 325 | oveq12d 7293 |
. . . . 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))))))) |
327 | 97, 254, 326 | 3eqtrd 2782 |
. . . 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))))))) |
328 | | bcn1 14027 |
. . . . . . 7
⊢ (𝐽 ∈ ℕ0
→ (𝐽C1) = 𝐽) |
329 | 7, 328 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽C1) = 𝐽) |
330 | 329 | eqcomd 2744 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 𝐽 = (𝐽C1)) |
331 | 220 | exp1d 13859 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑1) = (𝐴 Yrm 𝑁)) |
332 | 306 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((1 − 1) / 2)
= 0) |
333 | 332 | oveq2d 7291 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑((1 − 1) /
2)) = (((𝐴↑2) −
1)↑0)) |
334 | 226 | exp0d 13858 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑0) =
1) |
335 | 333, 334 | eqtrd 2778 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑((1 − 1) /
2)) = 1) |
336 | 331, 335 | oveq12d 7293 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))) = ((𝐴 Yrm
𝑁) ·
1)) |
337 | 220 | mulid1d 10992 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁) · 1) = (𝐴 Yrm 𝑁)) |
338 | 336, 337 | eqtr2d 2779 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm 𝑁) = (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))) |
339 | 338 | oveq2d 7291 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁)) = (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))) |
340 | 330, 339 | oveq12d 7293 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁))) = ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) |
341 | 327, 340 | oveq12d 7293 |
. . 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))))))) |
342 | 5, 257 | fsumcl 15445 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℂ) |
343 | 342, 256 | mulcld 10995 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) ∈ ℂ) |
344 | 343, 313 | pncand 11333 |
. . 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))) |
345 | 341, 344 | eqtrd 2778 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁)))) = (Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3))) |
346 | 95, 345 | breqtrrd 5102 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁))))) |