Proof of Theorem chfacfscmul0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eluz2 12884 | . . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘(𝑠 + 2)) ↔ ((𝑠 + 2) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝐾)) | 
| 2 |  | simpll 767 | . . . . . . . . . . . 12
⊢ (((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) ∧ (𝑠 + 2) ≤ 𝐾) → 𝐾 ∈ ℤ) | 
| 3 |  | nngt0 12297 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ → 0 <
𝑠) | 
| 4 |  | nnre 12273 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℝ) | 
| 5 | 4 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 𝑠 ∈
ℝ) | 
| 6 |  | 2rp 13039 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℝ+ | 
| 7 | 6 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 2 ∈
ℝ+) | 
| 8 | 5, 7 | ltaddrpd 13110 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 𝑠 < (𝑠 + 2)) | 
| 9 |  | 0red 11264 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 0 ∈
ℝ) | 
| 10 |  | 2re 12340 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ | 
| 11 | 10 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 2 ∈
ℝ) | 
| 12 | 5, 11 | readdcld 11290 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝑠 + 2) ∈
ℝ) | 
| 13 |  | lttr 11337 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℝ ∧ 𝑠
∈ ℝ ∧ (𝑠 +
2) ∈ ℝ) → ((0 < 𝑠 ∧ 𝑠 < (𝑠 + 2)) → 0 < (𝑠 + 2))) | 
| 14 | 9, 5, 12, 13 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((0 <
𝑠 ∧ 𝑠 < (𝑠 + 2)) → 0 < (𝑠 + 2))) | 
| 15 | 8, 14 | mpan2d 694 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (0 <
𝑠 → 0 < (𝑠 + 2))) | 
| 16 | 15 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℤ → (𝑠 ∈ ℕ → (0 <
𝑠 → 0 < (𝑠 + 2)))) | 
| 17 | 16 | com13 88 | . . . . . . . . . . . . . . . 16
⊢ (0 <
𝑠 → (𝑠 ∈ ℕ → (𝐾 ∈ ℤ → 0 <
(𝑠 + 2)))) | 
| 18 | 3, 17 | mpcom 38 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℕ → (𝐾 ∈ ℤ → 0 <
(𝑠 + 2))) | 
| 19 | 18 | impcom 407 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 0 <
(𝑠 + 2)) | 
| 20 |  | zre 12617 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 𝐾 ∈
ℝ) | 
| 22 |  | ltleletr 11354 | . . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ (𝑠 +
2) ∈ ℝ ∧ 𝐾
∈ ℝ) → ((0 < (𝑠 + 2) ∧ (𝑠 + 2) ≤ 𝐾) → 0 ≤ 𝐾)) | 
| 23 | 9, 12, 21, 22 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((0 <
(𝑠 + 2) ∧ (𝑠 + 2) ≤ 𝐾) → 0 ≤ 𝐾)) | 
| 24 | 19, 23 | mpand 695 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 2) ≤ 𝐾 → 0 ≤ 𝐾)) | 
| 25 | 24 | imp 406 | . . . . . . . . . . . 12
⊢ (((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) ∧ (𝑠 + 2) ≤ 𝐾) → 0 ≤ 𝐾) | 
| 26 |  | elnn0z 12626 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℤ
∧ 0 ≤ 𝐾)) | 
| 27 | 2, 25, 26 | sylanbrc 583 | . . . . . . . . . . 11
⊢ (((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) ∧ (𝑠 + 2) ≤ 𝐾) → 𝐾 ∈
ℕ0) | 
| 28 |  | nncn 12274 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℂ) | 
| 29 |  | add1p1 12517 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℂ → ((𝑠 + 1) + 1) = (𝑠 + 2)) | 
| 30 | 28, 29 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ → ((𝑠 + 1) + 1) = (𝑠 + 2)) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 1) + 1) = (𝑠 + 2)) | 
| 32 | 31 | eqcomd 2743 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝑠 + 2) = ((𝑠 + 1) + 1)) | 
| 33 | 32 | breq1d 5153 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 2) ≤ 𝐾 ↔ ((𝑠 + 1) + 1) ≤ 𝐾)) | 
| 34 |  | nnz 12634 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℤ) | 
| 35 | 34 | peano2zd 12725 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℤ) | 
| 36 | 35 | anim2i 617 | . . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝐾 ∈ ℤ ∧ (𝑠 + 1) ∈
ℤ)) | 
| 37 | 36 | ancomd 461 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 1) ∈ ℤ ∧ 𝐾 ∈
ℤ)) | 
| 38 |  | zltp1le 12667 | . . . . . . . . . . . . . . 15
⊢ (((𝑠 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑠 + 1) < 𝐾 ↔ ((𝑠 + 1) + 1) ≤ 𝐾)) | 
| 39 | 38 | bicomd 223 | . . . . . . . . . . . . . 14
⊢ (((𝑠 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (((𝑠 + 1) + 1) ≤ 𝐾 ↔ (𝑠 + 1) < 𝐾)) | 
| 40 | 37, 39 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (((𝑠 + 1) + 1) ≤ 𝐾 ↔ (𝑠 + 1) < 𝐾)) | 
| 41 | 33, 40 | bitrd 279 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 2) ≤ 𝐾 ↔ (𝑠 + 1) < 𝐾)) | 
| 42 | 41 | biimpa 476 | . . . . . . . . . . 11
⊢ (((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) ∧ (𝑠 + 2) ≤ 𝐾) → (𝑠 + 1) < 𝐾) | 
| 43 | 27, 42 | jca 511 | . . . . . . . . . 10
⊢ (((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) ∧ (𝑠 + 2) ≤ 𝐾) → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾)) | 
| 44 | 43 | ex 412 | . . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 2) ≤ 𝐾 → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) | 
| 45 | 44 | impancom 451 | . . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝐾) → (𝑠 ∈ ℕ → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) | 
| 46 | 45 | 3adant1 1131 | . . . . . . 7
⊢ (((𝑠 + 2) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝐾) → (𝑠 ∈ ℕ → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) | 
| 47 | 46 | com12 32 | . . . . . 6
⊢ (𝑠 ∈ ℕ → (((𝑠 + 2) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝐾) → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) | 
| 48 | 1, 47 | biimtrid 242 | . . . . 5
⊢ (𝑠 ∈ ℕ → (𝐾 ∈
(ℤ≥‘(𝑠 + 2)) → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) | 
| 49 | 48 | adantr 480 | . . . 4
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐾 ∈ (ℤ≥‘(𝑠 + 2)) → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) | 
| 50 | 49 | adantl 481 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝐾 ∈ (ℤ≥‘(𝑠 + 2)) → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) | 
| 51 |  | chfacfisf.g | . . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) | 
| 52 |  | 0red 11264 | . . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 0 ∈ ℝ) | 
| 53 |  | peano2re 11434 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℝ → (𝑠 + 1) ∈
ℝ) | 
| 54 | 4, 53 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℝ) | 
| 55 | 54 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑠 + 1) ∈ ℝ) | 
| 56 | 55 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈ ℝ) | 
| 57 | 56 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → (𝑠 + 1) ∈ ℝ) | 
| 58 |  | nn0re 12535 | . . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) | 
| 59 | 58 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 𝐾 ∈ ℝ) | 
| 60 |  | nnnn0 12533 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℕ0) | 
| 61 | 60 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑠 ∈ ℕ0) | 
| 62 | 61 | ad2antlr 727 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → 𝑠 ∈
ℕ0) | 
| 63 |  | nn0p1gt0 12555 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ0
→ 0 < (𝑠 +
1)) | 
| 64 | 62, 63 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → 0 <
(𝑠 + 1)) | 
| 65 | 64 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 0 < (𝑠 + 1)) | 
| 66 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → (𝑠 + 1) < 𝐾) | 
| 67 | 52, 57, 59, 65, 66 | lttrd 11422 | . . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 0 < 𝐾) | 
| 68 | 67 | gt0ne0d 11827 | . . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 𝐾 ≠ 0) | 
| 69 | 68 | neneqd 2945 | . . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → ¬ 𝐾 = 0) | 
| 70 | 69 | adantr 480 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → ¬ 𝐾 = 0) | 
| 71 |  | eqeq1 2741 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝐾 → (𝑛 = 0 ↔ 𝐾 = 0)) | 
| 72 | 71 | notbid 318 | . . . . . . . . . . 11
⊢ (𝑛 = 𝐾 → (¬ 𝑛 = 0 ↔ ¬ 𝐾 = 0)) | 
| 73 | 72 | adantl 481 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → (¬ 𝑛 = 0 ↔ ¬ 𝐾 = 0)) | 
| 74 | 70, 73 | mpbird 257 | . . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → ¬ 𝑛 = 0) | 
| 75 | 74 | iffalsed 4536 | . . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) = if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) | 
| 76 | 55 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → (𝑠 + 1) ∈
ℝ) | 
| 77 |  | ltne 11358 | . . . . . . . . . . . . 13
⊢ (((𝑠 + 1) ∈ ℝ ∧
(𝑠 + 1) < 𝐾) → 𝐾 ≠ (𝑠 + 1)) | 
| 78 | 76, 77 | sylan 580 | . . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 𝐾 ≠ (𝑠 + 1)) | 
| 79 | 78 | neneqd 2945 | . . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → ¬ 𝐾 = (𝑠 + 1)) | 
| 80 | 79 | adantr 480 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → ¬ 𝐾 = (𝑠 + 1)) | 
| 81 |  | eqeq1 2741 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝐾 → (𝑛 = (𝑠 + 1) ↔ 𝐾 = (𝑠 + 1))) | 
| 82 | 81 | notbid 318 | . . . . . . . . . . 11
⊢ (𝑛 = 𝐾 → (¬ 𝑛 = (𝑠 + 1) ↔ ¬ 𝐾 = (𝑠 + 1))) | 
| 83 | 82 | adantl 481 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → (¬ 𝑛 = (𝑠 + 1) ↔ ¬ 𝐾 = (𝑠 + 1))) | 
| 84 | 80, 83 | mpbird 257 | . . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → ¬ 𝑛 = (𝑠 + 1)) | 
| 85 | 84 | iffalsed 4536 | . . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) = if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) | 
| 86 |  | simplr 769 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → (𝑠 + 1) < 𝐾) | 
| 87 |  | breq2 5147 | . . . . . . . . . . 11
⊢ (𝑛 = 𝐾 → ((𝑠 + 1) < 𝑛 ↔ (𝑠 + 1) < 𝐾)) | 
| 88 | 87 | adantl 481 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → ((𝑠 + 1) < 𝑛 ↔ (𝑠 + 1) < 𝐾)) | 
| 89 | 86, 88 | mpbird 257 | . . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → (𝑠 + 1) < 𝑛) | 
| 90 | 89 | iftrued 4533 | . . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))) = 0 ) | 
| 91 | 75, 85, 90 | 3eqtrd 2781 | . . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) = 0 ) | 
| 92 |  | simplr 769 | . . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 𝐾 ∈
ℕ0) | 
| 93 |  | chfacfisf.0 | . . . . . . . . 9
⊢  0 =
(0g‘𝑌) | 
| 94 | 93 | fvexi 6920 | . . . . . . . 8
⊢  0 ∈
V | 
| 95 | 94 | a1i 11 | . . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 0 ∈ V) | 
| 96 | 51, 91, 92, 95 | fvmptd2 7024 | . . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → (𝐺‘𝐾) = 0 ) | 
| 97 | 96 | oveq2d 7447 | . . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = ((𝐾 ↑ 𝑋) · 0 )) | 
| 98 |  | crngring 20242 | . . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 99 |  | chfacfisf.p | . . . . . . . . . . . 12
⊢ 𝑃 = (Poly1‘𝑅) | 
| 100 |  | chfacfisf.y | . . . . . . . . . . . 12
⊢ 𝑌 = (𝑁 Mat 𝑃) | 
| 101 | 99, 100 | pmatlmod 22699 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ LMod) | 
| 102 | 98, 101 | sylan2 593 | . . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ LMod) | 
| 103 | 102 | 3adant3 1133 | . . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ LMod) | 
| 104 | 103 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → 𝑌 ∈ LMod) | 
| 105 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) | 
| 106 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘𝑃) | 
| 107 | 105, 106 | mgpbas 20142 | . . . . . . . . . 10
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) | 
| 108 |  | chfacfscmulcl.e | . . . . . . . . . 10
⊢  ↑ =
(.g‘(mulGrp‘𝑃)) | 
| 109 | 99 | ply1ring 22249 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) | 
| 110 | 98, 109 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) | 
| 111 | 110 | 3ad2ant2 1135 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ Ring) | 
| 112 | 105 | ringmgp 20236 | . . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) | 
| 113 | 111, 112 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝑃) ∈ Mnd) | 
| 114 | 113 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) →
(mulGrp‘𝑃) ∈
Mnd) | 
| 115 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℕ0) | 
| 116 | 98 | 3ad2ant2 1135 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) | 
| 117 |  | chfacfscmulcl.x | . . . . . . . . . . . . 13
⊢ 𝑋 = (var1‘𝑅) | 
| 118 | 117, 99, 106 | vr1cl 22219 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) | 
| 119 | 116, 118 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑋 ∈ (Base‘𝑃)) | 
| 120 | 119 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → 𝑋 ∈ (Base‘𝑃)) | 
| 121 | 107, 108,
114, 115, 120 | mulgnn0cld 19113 | . . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → (𝐾 ↑ 𝑋) ∈ (Base‘𝑃)) | 
| 122 | 99 | ply1crng 22200 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) | 
| 123 | 122 | anim2i 617 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) | 
| 124 | 123 | 3adant3 1133 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) | 
| 125 | 100 | matsca2 22426 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝑌)) | 
| 126 | 124, 125 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑃 = (Scalar‘𝑌)) | 
| 127 | 126 | eqcomd 2743 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝑌) = 𝑃) | 
| 128 | 127 | fveq2d 6910 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Base‘(Scalar‘𝑌)) = (Base‘𝑃)) | 
| 129 | 128 | eleq2d 2827 | . . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝐾 ↑ 𝑋) ∈ (Base‘𝑃))) | 
| 130 | 129 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → ((𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝐾 ↑ 𝑋) ∈ (Base‘𝑃))) | 
| 131 | 121, 130 | mpbird 257 | . . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → (𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌))) | 
| 132 | 104, 131 | jca 511 | . . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → (𝑌 ∈ LMod ∧ (𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)))) | 
| 133 | 132 | adantr 480 | . . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → (𝑌 ∈ LMod ∧ (𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)))) | 
| 134 |  | eqid 2737 | . . . . . . 7
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) | 
| 135 |  | chfacfscmulcl.m | . . . . . . 7
⊢  · = (
·𝑠 ‘𝑌) | 
| 136 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌)) | 
| 137 | 134, 135,
136, 93 | lmodvs0 20894 | . . . . . 6
⊢ ((𝑌 ∈ LMod ∧ (𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌))) → ((𝐾 ↑ 𝑋) · 0 ) = 0 ) | 
| 138 | 133, 137 | syl 17 | . . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → ((𝐾 ↑ 𝑋) · 0 ) = 0 ) | 
| 139 | 97, 138 | eqtrd 2777 | . . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 ) | 
| 140 | 139 | expl 457 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 )) | 
| 141 | 50, 140 | syld 47 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝐾 ∈ (ℤ≥‘(𝑠 + 2)) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 )) | 
| 142 | 141 | 3impia 1118 | 1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝐾 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 ) |