| Step | Hyp | Ref
| Expression |
| 1 | | fzfi 14013 |
. . . . . 6
⊢
(3...𝐽) ∈
Fin |
| 2 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (3...𝐽) |
| 3 | | ssfi 9213 |
. . . . . 6
⊢
(((3...𝐽) ∈ Fin
∧ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (3...𝐽)) → {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
| 4 | 1, 2, 3 | mp2an 692 |
. . . . 5
⊢ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin |
| 5 | 4 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
| 6 | | nnnn0 12533 |
. . . . . . . 8
⊢ (𝐽 ∈ ℕ → 𝐽 ∈
ℕ0) |
| 7 | 6 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 𝐽 ∈
ℕ0) |
| 8 | 2 | sseli 3979 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ (3...𝐽)) |
| 9 | | elfzelz 13564 |
. . . . . . . 8
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ ℤ) |
| 10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ ℤ) |
| 11 | | bccl 14361 |
. . . . . . 7
⊢ ((𝐽 ∈ ℕ0
∧ 𝑎 ∈ ℤ)
→ (𝐽C𝑎) ∈
ℕ0) |
| 12 | 7, 10, 11 | syl2an 596 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈
ℕ0) |
| 13 | 12 | nn0zd 12639 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈ ℤ) |
| 14 | | simpl1 1192 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝐴 ∈
(ℤ≥‘2)) |
| 15 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑁 ∈ ℤ) |
| 16 | | frmx 42925 |
. . . . . . . . . 10
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
| 17 | 16 | fovcl 7561 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
| 18 | 14, 15, 17 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
| 19 | 18 | nn0zd 12639 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈ ℤ) |
| 20 | 8 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ (3...𝐽)) |
| 21 | | fznn0sub 13596 |
. . . . . . . 8
⊢ (𝑎 ∈ (3...𝐽) → (𝐽 − 𝑎) ∈
ℕ0) |
| 22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽 − 𝑎) ∈
ℕ0) |
| 23 | | zexpcl 14117 |
. . . . . . 7
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐽 − 𝑎) ∈ ℕ0) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℤ) |
| 24 | 19, 22, 23 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℤ) |
| 25 | | rmspecnonsq 42918 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈ (ℕ ∖
◻NN)) |
| 26 | 25 | eldifad 3963 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℕ) |
| 27 | 26 | nnzd 12640 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℤ) |
| 28 | 27 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴↑2) − 1) ∈
ℤ) |
| 29 | | breq2 5147 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑎 → (2 ∥ 𝑏 ↔ 2 ∥ 𝑎)) |
| 30 | 29 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑎 → (¬ 2 ∥ 𝑏 ↔ ¬ 2 ∥ 𝑎)) |
| 31 | 30 | elrab 3692 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ (𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
| 32 | 31 | simprbi 496 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 𝑎) |
| 33 | | 1zzd 12648 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 1 ∈ ℤ) |
| 34 | | n2dvds1 16405 |
. . . . . . . . . . . 12
⊢ ¬ 2
∥ 1 |
| 35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 1) |
| 36 | | omoe 16401 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℤ ∧ ¬ 2
∥ 𝑎) ∧ (1 ∈
ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑎 − 1)) |
| 37 | 10, 32, 33, 35, 36 | syl22anc 839 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∥ (𝑎 − 1)) |
| 38 | | 2z 12649 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
| 39 | 38 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∈ ℤ) |
| 40 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 41 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ≠ 0) |
| 42 | | peano2zm 12660 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℤ → (𝑎 − 1) ∈
ℤ) |
| 43 | 10, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℤ) |
| 44 | | dvdsval2 16293 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ (𝑎 − 1) ∈ ℤ) → (2 ∥
(𝑎 − 1) ↔
((𝑎 − 1) / 2) ∈
ℤ)) |
| 45 | 39, 41, 43, 44 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (2 ∥ (𝑎 − 1) ↔ ((𝑎 − 1) / 2) ∈
ℤ)) |
| 46 | 37, 45 | mpbid 232 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℤ) |
| 47 | 43 | zred 12722 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℝ) |
| 48 | | 0red 11264 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 0 ∈ ℝ) |
| 49 | | 3re 12346 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ |
| 50 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 3 ∈ ℝ) |
| 51 | 9 | zred 12722 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ ℝ) |
| 52 | | 3pos 12371 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
3 |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 0 < 3) |
| 54 | | elfzle1 13567 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (3...𝐽) → 3 ≤ 𝑎) |
| 55 | 48, 50, 51, 53, 54 | ltletrd 11421 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (3...𝐽) → 0 < 𝑎) |
| 56 | | elnnz 12623 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 0 <
𝑎)) |
| 57 | 9, 55, 56 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ ℕ) |
| 58 | | nnm1nn0 12567 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → (𝑎 − 1) ∈
ℕ0) |
| 59 | 57, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → (𝑎 − 1) ∈
ℕ0) |
| 60 | 59 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (3...𝐽) → 0 ≤ (𝑎 − 1)) |
| 61 | 8, 60 | syl 17 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ (𝑎 − 1)) |
| 62 | | 2re 12340 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
| 63 | 62 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 2 ∈ ℝ) |
| 64 | | 2pos 12369 |
. . . . . . . . . . 11
⊢ 0 <
2 |
| 65 | 64 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 < 2) |
| 66 | | divge0 12137 |
. . . . . . . . . 10
⊢ ((((𝑎 − 1) ∈ ℝ ∧
0 ≤ (𝑎 − 1)) ∧
(2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑎 − 1) / 2)) |
| 67 | 47, 61, 63, 65, 66 | syl22anc 839 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ ((𝑎 − 1) / 2)) |
| 68 | | elnn0z 12626 |
. . . . . . . . 9
⊢ (((𝑎 − 1) / 2) ∈
ℕ0 ↔ (((𝑎 − 1) / 2) ∈ ℤ ∧ 0 ≤
((𝑎 − 1) /
2))) |
| 69 | 46, 67, 68 | sylanbrc 583 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℕ0) |
| 70 | | zexpcl 14117 |
. . . . . . . 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 42926 |
. . . . . . . . . 10
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
| 73 | 72 | fovcl 7561 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
| 74 | 14, 15, 73 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Yrm 𝑁) ∈ ℤ) |
| 75 | | elfzel1 13563 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → 3 ∈ ℤ) |
| 76 | 9, 75 | zsubcld 12727 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (3...𝐽) → (𝑎 − 3) ∈ ℤ) |
| 77 | | subge0 11776 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 3 ∈
ℝ) → (0 ≤ (𝑎
− 3) ↔ 3 ≤ 𝑎)) |
| 78 | 51, 49, 77 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → (0 ≤ (𝑎 − 3) ↔ 3 ≤ 𝑎)) |
| 79 | 54, 78 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (3...𝐽) → 0 ≤ (𝑎 − 3)) |
| 80 | | elnn0z 12626 |
. . . . . . . . . . 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 481 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝑎 − 3) ∈
ℕ0) |
| 84 | | zexpcl 14117 |
. . . . . . . 8
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝑎 − 3) ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℤ) |
| 85 | 74, 83, 84 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℤ) |
| 86 | 71, 85 | zmulcld 12728 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) ∈
ℤ) |
| 87 | 24, 86 | zmulcld 12728 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) ∈
ℤ) |
| 88 | 13, 87 | zmulcld 12728 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℤ) |
| 89 | 5, 88 | fsumzcl 15771 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℤ) |
| 90 | 73 | 3adant3 1133 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
| 91 | | 3nn0 12544 |
. . . 4
⊢ 3 ∈
ℕ0 |
| 92 | | zexpcl 14117 |
. . . 4
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ 3 ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ) |
| 93 | 90, 91, 92 | sylancl 586 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ) |
| 94 | | dvdsmul2 16316 |
. . 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 43007 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ0) → (𝐴 Yrm (𝑁 · 𝐽)) = Σ𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
| 97 | 6, 96 | syl3an3 1166 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm (𝑁 · 𝐽)) = Σ𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
| 98 | | 1lt3 12439 |
. . . . . . . . . . . 12
⊢ 1 <
3 |
| 99 | | 1re 11261 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
| 100 | 99, 49 | ltnlei 11382 |
. . . . . . . . . . . 12
⊢ (1 < 3
↔ ¬ 3 ≤ 1) |
| 101 | 98, 100 | mpbi 230 |
. . . . . . . . . . 11
⊢ ¬ 3
≤ 1 |
| 102 | | elfzle1 13567 |
. . . . . . . . . . 11
⊢ (1 ∈
(3...𝐽) → 3 ≤
1) |
| 103 | 101, 102 | mto 197 |
. . . . . . . . . 10
⊢ ¬ 1
∈ (3...𝐽) |
| 104 | 103 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ¬ 1 ∈
(3...𝐽)) |
| 105 | 104 | intnanrd 489 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ¬ (1 ∈
(3...𝐽) ∧ ¬ 2
∥ 1)) |
| 106 | | breq2 5147 |
. . . . . . . . . 10
⊢ (𝑏 = 1 → (2 ∥ 𝑏 ↔ 2 ∥
1)) |
| 107 | 106 | notbid 318 |
. . . . . . . . 9
⊢ (𝑏 = 1 → (¬ 2 ∥
𝑏 ↔ ¬ 2 ∥
1)) |
| 108 | 107 | elrab 3692 |
. . . . . . . 8
⊢ (1 ∈
{𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ (1 ∈ (3...𝐽) ∧ ¬ 2 ∥
1)) |
| 109 | 105, 108 | sylnibr 329 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ¬ 1 ∈
{𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) |
| 110 | | disjsn 4711 |
. . . . . . 7
⊢ (({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∩ {1}) = ∅ ↔ ¬ 1 ∈
{𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) |
| 111 | 109, 110 | sylibr 234 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∩ {1}) = ∅) |
| 112 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 = 1) → 𝑎 = 1) |
| 113 | 112 | olcd 875 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 = 1) → ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
| 114 | | 3z 12650 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℤ |
| 115 | 114 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 3 ∈
ℤ) |
| 116 | | nnz 12634 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ ℕ → 𝐽 ∈
ℤ) |
| 117 | 116 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 𝐽 ∈ ℤ) |
| 118 | 117 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝐽 ∈ ℤ) |
| 119 | | elfzelz 13564 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (0...𝐽) → 𝑎 ∈ ℤ) |
| 120 | 119 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → 𝑎 ∈ ℤ) |
| 121 | 120 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ∈ ℤ) |
| 122 | | elfznn0 13660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (0...𝐽) → 𝑎 ∈ ℕ0) |
| 123 | 122 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → 𝑎 ∈ ℕ0) |
| 124 | 123 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ∈ ℕ0) |
| 125 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → ¬ 2 ∥ 𝑎) |
| 126 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ≠ 1) |
| 127 | | elnn1uz2 12967 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℕ ↔ (𝑎 = 1 ∨ 𝑎 ∈
(ℤ≥‘2))) |
| 128 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ≠ 1 ↔ ¬ 𝑎 = 1) |
| 129 | 128 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ≠ 1 → ¬ 𝑎 = 1) |
| 130 | 129 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) →
¬ 𝑎 =
1) |
| 131 | 130 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) →
(𝑎 = 1 → 3 ≤ 𝑎)) |
| 132 | 131 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 1) → 3 ≤ 𝑎) |
| 133 | | uzp1 12919 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈
(ℤ≥‘2) → (𝑎 = 2 ∨ 𝑎 ∈ (ℤ≥‘(2 +
1)))) |
| 134 | | 1z 12647 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℤ |
| 135 | | dvdsmul1 16315 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ ℤ ∧ 1 ∈ ℤ) → 2 ∥ (2 ·
1)) |
| 136 | 38, 134, 135 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∥
(2 · 1) |
| 137 | | 2t1e2 12429 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2
· 1) = 2 |
| 138 | 136, 137 | breqtri 5168 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∥
2 |
| 139 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 2 → (2 ∥ 𝑎 ↔ 2 ∥
2)) |
| 140 | 139 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → (2 ∥ 𝑎 ↔ 2 ∥
2)) |
| 141 | 138, 140 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → 2 ∥ 𝑎) |
| 142 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → ¬ 2 ∥
𝑎) |
| 143 | 141, 142 | pm2.21dd 195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 2) → 3 ≤ 𝑎) |
| 144 | | eluzle 12891 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈
(ℤ≥‘3) → 3 ≤ 𝑎) |
| 145 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 + 1) =
3 |
| 146 | 145 | fveq2i 6909 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(ℤ≥‘(2 + 1)) =
(ℤ≥‘3) |
| 147 | 144, 146 | eleq2s 2859 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈
(ℤ≥‘(2 + 1)) → 3 ≤ 𝑎) |
| 148 | 147 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 ∈
(ℤ≥‘(2 + 1))) → 3 ≤ 𝑎) |
| 149 | 143, 148 | jaodan 960 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧
(𝑎 = 2 ∨ 𝑎 ∈
(ℤ≥‘(2 + 1)))) → 3 ≤ 𝑎) |
| 150 | 133, 149 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 ∈
(ℤ≥‘2)) → 3 ≤ 𝑎) |
| 151 | 132, 150 | jaodan 960 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧
(𝑎 = 1 ∨ 𝑎 ∈
(ℤ≥‘2))) → 3 ≤ 𝑎) |
| 152 | 127, 151 | sylan2b 594 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 ∈ ℕ) → 3 ≤
𝑎) |
| 153 | | dvds0 16309 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℤ → 2 ∥ 0) |
| 154 | 38, 153 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∥
0 |
| 155 | | breq2 5147 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 0 → (2 ∥ 𝑎 ↔ 2 ∥
0)) |
| 156 | 154, 155 | mpbiri 258 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 0 → 2 ∥ 𝑎) |
| 157 | 156 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 0) → 2 ∥ 𝑎) |
| 158 | | simpl2 1193 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 0) → ¬ 2 ∥
𝑎) |
| 159 | 157, 158 | pm2.21dd 195 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) ∧ 𝑎 = 0) → 3 ≤ 𝑎) |
| 160 | | elnn0 12528 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ℕ0
↔ (𝑎 ∈ ℕ
∨ 𝑎 =
0)) |
| 161 | 160 | biimpi 216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℕ0
→ (𝑎 ∈ ℕ
∨ 𝑎 =
0)) |
| 162 | 161 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) →
(𝑎 ∈ ℕ ∨
𝑎 = 0)) |
| 163 | 152, 159,
162 | mpjaodan 961 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ0
∧ ¬ 2 ∥ 𝑎
∧ 𝑎 ≠ 1) → 3
≤ 𝑎) |
| 164 | 124, 125,
126, 163 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 3 ≤ 𝑎) |
| 165 | | elfzle2 13568 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (0...𝐽) → 𝑎 ≤ 𝐽) |
| 166 | 165 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → 𝑎 ≤ 𝐽) |
| 167 | 166 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ≤ 𝐽) |
| 168 | 115, 118,
121, 164, 167 | elfzd 13555 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → 𝑎 ∈ (3...𝐽)) |
| 169 | 168, 125 | jca 511 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → (𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
| 170 | 169 | orcd 874 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) ∧ 𝑎 ≠ 1) → ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
| 171 | 113, 170 | pm2.61dane 3029 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) → ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
| 172 | | nn0uz 12920 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
| 173 | 91, 172 | eleqtri 2839 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
(ℤ≥‘0) |
| 174 | | fzss1 13603 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
(ℤ≥‘0) → (3...𝐽) ⊆ (0...𝐽)) |
| 175 | 173, 174 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(3...𝐽) ⊆
(0...𝐽) |
| 176 | 175 | sseli 3979 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (3...𝐽) → 𝑎 ∈ (0...𝐽)) |
| 177 | 176 | anim1i 615 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
| 178 | 177 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ (𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎)) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
| 179 | | 0zd 12625 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 0 ∈
ℤ) |
| 180 | 117 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 𝐽 ∈ ℤ) |
| 181 | | 1zzd 12648 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 1 ∈
ℤ) |
| 182 | | 0le1 11786 |
. . . . . . . . . . . . 13
⊢ 0 ≤
1 |
| 183 | 182 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 0 ≤ 1) |
| 184 | | nnge1 12294 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ ℕ → 1 ≤
𝐽) |
| 185 | 184 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 1 ≤ 𝐽) |
| 186 | 185 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 1 ≤ 𝐽) |
| 187 | 179, 180,
181, 183, 186 | elfzd 13555 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → 1 ∈ (0...𝐽)) |
| 188 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → ¬ 2 ∥
1) |
| 189 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 → (𝑎 ∈ (0...𝐽) ↔ 1 ∈ (0...𝐽))) |
| 190 | | breq2 5147 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 1 → (2 ∥ 𝑎 ↔ 2 ∥
1)) |
| 191 | 190 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 → (¬ 2 ∥
𝑎 ↔ ¬ 2 ∥
1)) |
| 192 | 189, 191 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑎 = 1 → ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) ↔ (1 ∈ (0...𝐽) ∧ ¬ 2 ∥
1))) |
| 193 | 192 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) ↔ (1 ∈ (0...𝐽) ∧ ¬ 2 ∥
1))) |
| 194 | 187, 188,
193 | mpbir2and 713 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 = 1) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
| 195 | 178, 194 | jaodan 960 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) → (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
| 196 | 171, 195 | impbida 801 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) ↔ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1))) |
| 197 | 30 | elrab 3692 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ (𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎)) |
| 198 | | elun 4153 |
. . . . . . . . 9
⊢ (𝑎 ∈ ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1}) ↔ (𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∨ 𝑎 ∈ {1})) |
| 199 | | velsn 4642 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {1} ↔ 𝑎 = 1) |
| 200 | 31, 199 | orbi12i 915 |
. . . . . . . . 9
⊢ ((𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∨ 𝑎 ∈ {1}) ↔ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
| 201 | 198, 200 | bitri 275 |
. . . . . . . 8
⊢ (𝑎 ∈ ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1}) ↔ ((𝑎 ∈ (3...𝐽) ∧ ¬ 2 ∥ 𝑎) ∨ 𝑎 = 1)) |
| 202 | 196, 197,
201 | 3bitr4g 314 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ↔ 𝑎 ∈ ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1}))) |
| 203 | 202 | eqrdv 2735 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} = ({𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ∪ {1})) |
| 204 | | fzfi 14013 |
. . . . . . . 8
⊢
(0...𝐽) ∈
Fin |
| 205 | | ssrab2 4080 |
. . . . . . . 8
⊢ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (0...𝐽) |
| 206 | | ssfi 9213 |
. . . . . . . 8
⊢
(((0...𝐽) ∈ Fin
∧ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ⊆ (0...𝐽)) → {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
| 207 | 204, 205,
206 | mp2an 692 |
. . . . . . 7
⊢ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin |
| 208 | 207 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} ∈ Fin) |
| 209 | 205 | sseli 3979 |
. . . . . . . . . 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 12589 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈ ℂ) |
| 213 | 17 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
| 214 | 213 | nn0cnd 12589 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈ ℂ) |
| 215 | 214 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈ ℂ) |
| 216 | 209 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ (0...𝐽)) |
| 217 | | fznn0sub 13596 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0...𝐽) → (𝐽 − 𝑎) ∈
ℕ0) |
| 218 | 216, 217 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽 − 𝑎) ∈
ℕ0) |
| 219 | 215, 218 | expcld 14186 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℂ) |
| 220 | 90 | zcnd 12723 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℂ) |
| 221 | 209, 122 | syl 17 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 𝑎 ∈ ℕ0) |
| 222 | | expcl 14120 |
. . . . . . . . . 10
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ 𝑎 ∈ ℕ0)
→ ((𝐴 Yrm
𝑁)↑𝑎) ∈ ℂ) |
| 223 | 220, 221,
222 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑𝑎) ∈ ℂ) |
| 224 | | rmspecpos 42928 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℝ+) |
| 225 | 224 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℂ) |
| 226 | 225 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴↑2) − 1) ∈
ℂ) |
| 227 | 197 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 𝑎) |
| 228 | | 1zzd 12648 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 1 ∈ ℤ) |
| 229 | 34 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 2 ∥ 1) |
| 230 | 210, 227,
228, 229, 36 | syl22anc 839 |
. . . . . . . . . . . 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 1373 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (2 ∥ (𝑎 − 1) ↔ ((𝑎 − 1) / 2) ∈
ℤ)) |
| 235 | 230, 234 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℤ) |
| 236 | 233 | zred 12722 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 − 1) ∈ ℝ) |
| 237 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (0...𝐽) → (𝑎 = 0 → 2 ∥ 𝑎)) |
| 238 | 237 | con3dimp 408 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ (0...𝐽) ∧ ¬ 2 ∥ 𝑎) → ¬ 𝑎 = 0) |
| 239 | 197, 238 | sylbi 217 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ¬ 𝑎 = 0) |
| 240 | 221, 161 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → (𝑎 ∈ ℕ ∨ 𝑎 = 0)) |
| 241 | | orel2 891 |
. . . . . . . . . . . . . . 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 12590 |
. . . . . . . . . . . 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 839 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → 0 ≤ ((𝑎 − 1) / 2)) |
| 248 | 235, 247,
68 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏} → ((𝑎 − 1) / 2) ∈
ℕ0) |
| 249 | | expcl 14120 |
. . . . . . . . . 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 11281 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))) ∈
ℂ) |
| 252 | 219, 251 | mulcld 11281 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)))) ∈
ℂ) |
| 253 | 212, 252 | mulcld 11281 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) ∈
ℂ) |
| 254 | 111, 203,
208, 253 | fsumsplit 15777 |
. . . . 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 14120 |
. . . . . . . . 9
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ 3 ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑3) ∈ ℂ) |
| 256 | 220, 91, 255 | sylancl 586 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∈ ℂ) |
| 257 | 88 | zcnd 12723 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℂ) |
| 258 | 5, 256, 257 | fsummulc1 15821 |
. . . . . . 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 12589 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐽C𝑎) ∈ ℂ) |
| 260 | 214 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Xrm 𝑁) ∈ ℂ) |
| 261 | 260, 22 | expcld 14186 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) ∈ ℂ) |
| 262 | 226, 69, 249 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ∈
ℂ) |
| 263 | | expcl 14120 |
. . . . . . . . . . . . 13
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ (𝑎 − 3) ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℂ) |
| 264 | 220, 82, 263 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑(𝑎 − 3)) ∈ ℂ) |
| 265 | 262, 264 | mulcld 11281 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) ∈
ℂ) |
| 266 | 261, 265 | mulcld 11281 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) ∈
ℂ) |
| 267 | 256 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑3) ∈ ℂ) |
| 268 | 259, 266,
267 | mulassd 11284 |
. . . . . . . . 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 11284 |
. . . . . . . . . . 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 11284 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) · ((𝐴 Yrm 𝑁)↑3)) = ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
(((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)))) |
| 271 | 264, 267 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) ∈ ℂ) |
| 272 | 262, 271 | mulcomd 11282 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
(((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3))) = ((((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))) |
| 273 | 220 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (𝐴 Yrm 𝑁) ∈ ℂ) |
| 274 | 91 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 3 ∈
ℕ0) |
| 275 | 273, 274,
83 | expaddd 14188 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑((𝑎 − 3) + 3)) = (((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3))) |
| 276 | 10 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ ℤ) |
| 277 | 276 | zcnd 12723 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → 𝑎 ∈ ℂ) |
| 278 | | 3cn 12347 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℂ |
| 279 | | npcan 11517 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℂ ∧ 3 ∈
ℂ) → ((𝑎 −
3) + 3) = 𝑎) |
| 280 | 277, 278,
279 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝑎 − 3) + 3) = 𝑎) |
| 281 | 280 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((𝐴 Yrm 𝑁)↑((𝑎 − 3) + 3)) = ((𝐴 Yrm 𝑁)↑𝑎)) |
| 282 | 275, 281 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) = ((𝐴 Yrm 𝑁)↑𝑎)) |
| 283 | 282 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴 Yrm 𝑁)↑(𝑎 − 3)) · ((𝐴 Yrm 𝑁)↑3)) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))) = (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))) |
| 284 | 270, 272,
283 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) · ((𝐴 Yrm 𝑁)↑3)) = (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))) |
| 285 | 284 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))) · ((𝐴 Yrm 𝑁)↑3))) = (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2))))) |
| 286 | 269, 285 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → ((((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3)))) · ((𝐴 Yrm 𝑁)↑3)) = (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2))))) |
| 287 | 286 | oveq2d 7447 |
. . . . . . . . 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 2777 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) ∧ 𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏}) → (((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) = ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) /
2)))))) |
| 289 | 288 | sumeq2dv 15738 |
. . . . . . 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 2778 |
. . . . . 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 12277 |
. . . . . . 7
⊢ 1 ∈
ℕ |
| 292 | | bccl 14361 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ ℕ0
∧ 1 ∈ ℤ) → (𝐽C1) ∈
ℕ0) |
| 293 | 6, 134, 292 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝐽 ∈ ℕ → (𝐽C1) ∈
ℕ0) |
| 294 | 293 | nn0cnd 12589 |
. . . . . . . . 9
⊢ (𝐽 ∈ ℕ → (𝐽C1) ∈
ℂ) |
| 295 | 294 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽C1) ∈ ℂ) |
| 296 | | nnm1nn0 12567 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ ℕ → (𝐽 − 1) ∈
ℕ0) |
| 297 | 296 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽 − 1) ∈
ℕ0) |
| 298 | 214, 297 | expcld 14186 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Xrm 𝑁)↑(𝐽 − 1)) ∈
ℂ) |
| 299 | | 1nn0 12542 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
| 300 | | expcl 14120 |
. . . . . . . . . . 11
⊢ (((𝐴 Yrm 𝑁) ∈ ℂ ∧ 1 ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑1) ∈ ℂ) |
| 301 | 220, 299,
300 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑1) ∈ ℂ) |
| 302 | | 1m1e0 12338 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
| 303 | 302 | oveq1i 7441 |
. . . . . . . . . . . . 13
⊢ ((1
− 1) / 2) = (0 / 2) |
| 304 | | 2cn 12341 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
| 305 | 304, 40 | div0i 12001 |
. . . . . . . . . . . . 13
⊢ (0 / 2) =
0 |
| 306 | 303, 305 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((1
− 1) / 2) = 0 |
| 307 | | 0nn0 12541 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
| 308 | 306, 307 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ ((1
− 1) / 2) ∈ ℕ0 |
| 309 | | expcl 14120 |
. . . . . . . . . . 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 11281 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))) ∈ ℂ) |
| 312 | 298, 311 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))) ∈ ℂ) |
| 313 | 295, 312 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))) ∈ ℂ) |
| 314 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑎 = 1 → (𝐽C𝑎) = (𝐽C1)) |
| 315 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → (𝐽 − 𝑎) = (𝐽 − 1)) |
| 316 | 315 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → ((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) = ((𝐴 Xrm 𝑁)↑(𝐽 − 1))) |
| 317 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → ((𝐴 Yrm 𝑁)↑𝑎) = ((𝐴 Yrm 𝑁)↑1)) |
| 318 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 → (𝑎 − 1) = (1 − 1)) |
| 319 | 318 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑎 = 1 → ((𝑎 − 1) / 2) = ((1 − 1) /
2)) |
| 320 | 319 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) = (((𝐴↑2) − 1)↑((1
− 1) / 2))) |
| 321 | 317, 320 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))) = (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1
− 1) / 2)))) |
| 322 | 316, 321 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑎 = 1 → (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2)))) = (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))) |
| 323 | 314, 322 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑎 = 1 → ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · (((𝐴 Yrm 𝑁)↑𝑎) · (((𝐴↑2) − 1)↑((𝑎 − 1) / 2))))) = ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) |
| 324 | 323 | sumsn 15782 |
. . . . . . 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 7449 |
. . . . 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 2781 |
. . . 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 14352 |
. . . . . . 7
⊢ (𝐽 ∈ ℕ0
→ (𝐽C1) = 𝐽) |
| 329 | 7, 328 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽C1) = 𝐽) |
| 330 | 329 | eqcomd 2743 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → 𝐽 = (𝐽C1)) |
| 331 | 220 | exp1d 14181 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑1) = (𝐴 Yrm 𝑁)) |
| 332 | 306 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((1 − 1) / 2)
= 0) |
| 333 | 332 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑((1 − 1) /
2)) = (((𝐴↑2) −
1)↑0)) |
| 334 | 226 | exp0d 14180 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑0) =
1) |
| 335 | 333, 334 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴↑2) − 1)↑((1 − 1) /
2)) = 1) |
| 336 | 331, 335 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))) = ((𝐴 Yrm
𝑁) ·
1)) |
| 337 | 220 | mulridd 11278 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁) · 1) = (𝐴 Yrm 𝑁)) |
| 338 | 336, 337 | eqtr2d 2778 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐴 Yrm 𝑁) = (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))) |
| 339 | 338 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁)) = (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2))))) |
| 340 | 330, 339 | oveq12d 7449 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁))) = ((𝐽C1) · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (((𝐴 Yrm 𝑁)↑1) · (((𝐴↑2) − 1)↑((1 − 1) /
2)))))) |
| 341 | 327, 340 | oveq12d 7449 |
. . 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 15769 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) ∈
ℂ) |
| 343 | 342, 256 | mulcld 11281 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → (Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3)) ∈ ℂ) |
| 344 | 343, 313 | pncand 11621 |
. . 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 2777 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁)))) = (Σ𝑎 ∈ {𝑏 ∈ (3...𝐽) ∣ ¬ 2 ∥ 𝑏} ((𝐽C𝑎) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑎)) · ((((𝐴↑2) − 1)↑((𝑎 − 1) / 2)) ·
((𝐴 Yrm 𝑁)↑(𝑎 − 3))))) · ((𝐴 Yrm 𝑁)↑3))) |
| 346 | 95, 345 | breqtrrd 5171 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁))))) |