Proof of Theorem chfacfscmul0
Step | Hyp | Ref
| Expression |
1 | | eluz2 11569 |
. . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘(𝑠 + 2)) ↔ ((𝑠 + 2) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝐾)) |
2 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) ∧ (𝑠 + 2) ≤ 𝐾) → 𝐾 ∈ ℤ) |
3 | | nngt0 10926 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ → 0 <
𝑠) |
4 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℝ) |
5 | 4 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 𝑠 ∈
ℝ) |
6 | | 2rp 11713 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℝ+ |
7 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 2 ∈
ℝ+) |
8 | 5, 7 | ltaddrpd 11781 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 𝑠 < (𝑠 + 2)) |
9 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 0 ∈
ℝ) |
10 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 2 ∈
ℝ) |
12 | 5, 11 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝑠 + 2) ∈
ℝ) |
13 | | lttr 9993 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℝ ∧ 𝑠
∈ ℝ ∧ (𝑠 +
2) ∈ ℝ) → ((0 < 𝑠 ∧ 𝑠 < (𝑠 + 2)) → 0 < (𝑠 + 2))) |
14 | 9, 5, 12, 13 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((0 <
𝑠 ∧ 𝑠 < (𝑠 + 2)) → 0 < (𝑠 + 2))) |
15 | 8, 14 | mpan2d 706 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (0 <
𝑠 → 0 < (𝑠 + 2))) |
16 | 15 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℤ → (𝑠 ∈ ℕ → (0 <
𝑠 → 0 < (𝑠 + 2)))) |
17 | 16 | com13 86 |
. . . . . . . . . . . . . . . 16
⊢ (0 <
𝑠 → (𝑠 ∈ ℕ → (𝐾 ∈ ℤ → 0 <
(𝑠 + 2)))) |
18 | 3, 17 | mpcom 37 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℕ → (𝐾 ∈ ℤ → 0 <
(𝑠 + 2))) |
19 | 18 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 0 <
(𝑠 + 2)) |
20 | | zre 11258 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 𝐾 ∈
ℝ) |
22 | | ltleletr 10009 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ (𝑠 +
2) ∈ ℝ ∧ 𝐾
∈ ℝ) → ((0 < (𝑠 + 2) ∧ (𝑠 + 2) ≤ 𝐾) → 0 ≤ 𝐾)) |
23 | 9, 12, 21, 22 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((0 <
(𝑠 + 2) ∧ (𝑠 + 2) ≤ 𝐾) → 0 ≤ 𝐾)) |
24 | 19, 23 | mpand 707 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 2) ≤ 𝐾 → 0 ≤ 𝐾)) |
25 | 24 | imp 444 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) ∧ (𝑠 + 2) ≤ 𝐾) → 0 ≤ 𝐾) |
26 | | elnn0z 11267 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℤ
∧ 0 ≤ 𝐾)) |
27 | 2, 25, 26 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) ∧ (𝑠 + 2) ≤ 𝐾) → 𝐾 ∈
ℕ0) |
28 | | nncn 10905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℂ) |
29 | | add1p1 11160 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℂ → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
32 | 31 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝑠 + 2) = ((𝑠 + 1) + 1)) |
33 | 32 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 2) ≤ 𝐾 ↔ ((𝑠 + 1) + 1) ≤ 𝐾)) |
34 | | nnz 11276 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℤ) |
35 | 34 | peano2zd 11361 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℤ) |
36 | 35 | anim2i 591 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝐾 ∈ ℤ ∧ (𝑠 + 1) ∈
ℤ)) |
37 | 36 | ancomd 466 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 1) ∈ ℤ ∧ 𝐾 ∈
ℤ)) |
38 | | zltp1le 11304 |
. . . . . . . . . . . . . . 15
⊢ (((𝑠 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑠 + 1) < 𝐾 ↔ ((𝑠 + 1) + 1) ≤ 𝐾)) |
39 | 38 | bicomd 212 |
. . . . . . . . . . . . . 14
⊢ (((𝑠 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (((𝑠 + 1) + 1) ≤ 𝐾 ↔ (𝑠 + 1) < 𝐾)) |
40 | 37, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (((𝑠 + 1) + 1) ≤ 𝐾 ↔ (𝑠 + 1) < 𝐾)) |
41 | 33, 40 | bitrd 267 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 2) ≤ 𝐾 ↔ (𝑠 + 1) < 𝐾)) |
42 | 41 | biimpa 500 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) ∧ (𝑠 + 2) ≤ 𝐾) → (𝑠 + 1) < 𝐾) |
43 | 27, 42 | jca 553 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) ∧ (𝑠 + 2) ≤ 𝐾) → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾)) |
44 | 43 | ex 449 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 2) ≤ 𝐾 → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) |
45 | 44 | impancom 455 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝐾) → (𝑠 ∈ ℕ → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) |
46 | 45 | 3adant1 1072 |
. . . . . . 7
⊢ (((𝑠 + 2) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝐾) → (𝑠 ∈ ℕ → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) |
47 | 46 | com12 32 |
. . . . . 6
⊢ (𝑠 ∈ ℕ → (((𝑠 + 2) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝐾) → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) |
48 | 1, 47 | syl5bi 231 |
. . . . 5
⊢ (𝑠 ∈ ℕ → (𝐾 ∈
(ℤ≥‘(𝑠 + 2)) → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) |
49 | 48 | adantr 480 |
. . . 4
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (𝐾 ∈ (ℤ≥‘(𝑠 + 2)) → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) |
50 | 49 | adantl 481 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝐾 ∈ (ℤ≥‘(𝑠 + 2)) → (𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾))) |
51 | | chfacfisf.g |
. . . . . . . 8
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
52 | 51 | a1i 11 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))) |
53 | | 0red 9920 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 0 ∈ ℝ) |
54 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℝ → (𝑠 + 1) ∈
ℝ) |
55 | 4, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℝ) |
56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (𝑠 + 1) ∈ ℝ) |
57 | 56 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑠 + 1) ∈ ℝ) |
58 | 57 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → (𝑠 + 1) ∈ ℝ) |
59 | | nn0re 11178 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
60 | 59 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 𝐾 ∈ ℝ) |
61 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℕ0) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → 𝑠 ∈ ℕ0) |
63 | 62 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → 𝑠 ∈
ℕ0) |
64 | | nn0p1gt0 11199 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ0
→ 0 < (𝑠 +
1)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → 0 <
(𝑠 + 1)) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 0 < (𝑠 + 1)) |
67 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → (𝑠 + 1) < 𝐾) |
68 | 53, 58, 60, 66, 67 | lttrd 10077 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 0 < 𝐾) |
69 | 68 | gt0ne0d 10471 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 𝐾 ≠ 0) |
70 | 69 | neneqd 2787 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → ¬ 𝐾 = 0) |
71 | 70 | adantr 480 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → ¬ 𝐾 = 0) |
72 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝐾 → (𝑛 = 0 ↔ 𝐾 = 0)) |
73 | 72 | notbid 307 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝐾 → (¬ 𝑛 = 0 ↔ ¬ 𝐾 = 0)) |
74 | 73 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → (¬ 𝑛 = 0 ↔ ¬ 𝐾 = 0)) |
75 | 71, 74 | mpbird 246 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → ¬ 𝑛 = 0) |
76 | 75 | iffalsed 4047 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) = if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) |
77 | 56 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → (𝑠 + 1) ∈
ℝ) |
78 | | ltne 10013 |
. . . . . . . . . . . . 13
⊢ (((𝑠 + 1) ∈ ℝ ∧
(𝑠 + 1) < 𝐾) → 𝐾 ≠ (𝑠 + 1)) |
79 | 77, 78 | sylan 487 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 𝐾 ≠ (𝑠 + 1)) |
80 | 79 | neneqd 2787 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → ¬ 𝐾 = (𝑠 + 1)) |
81 | 80 | adantr 480 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → ¬ 𝐾 = (𝑠 + 1)) |
82 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝐾 → (𝑛 = (𝑠 + 1) ↔ 𝐾 = (𝑠 + 1))) |
83 | 82 | notbid 307 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝐾 → (¬ 𝑛 = (𝑠 + 1) ↔ ¬ 𝐾 = (𝑠 + 1))) |
84 | 83 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → (¬ 𝑛 = (𝑠 + 1) ↔ ¬ 𝐾 = (𝑠 + 1))) |
85 | 81, 84 | mpbird 246 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → ¬ 𝑛 = (𝑠 + 1)) |
86 | 85 | iffalsed 4047 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) = if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) |
87 | | simplr 788 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → (𝑠 + 1) < 𝐾) |
88 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝐾 → ((𝑠 + 1) < 𝑛 ↔ (𝑠 + 1) < 𝐾)) |
89 | 88 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → ((𝑠 + 1) < 𝑛 ↔ (𝑠 + 1) < 𝐾)) |
90 | 87, 89 | mpbird 246 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → (𝑠 + 1) < 𝑛) |
91 | 90 | iftrued 4044 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))) = 0 ) |
92 | 76, 86, 91 | 3eqtrd 2648 |
. . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) ∧ 𝑛 = 𝐾) → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) = 0 ) |
93 | | simplr 788 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 𝐾 ∈
ℕ0) |
94 | | chfacfisf.0 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑌) |
95 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝑌) ∈ V |
96 | 94, 95 | eqeltri 2684 |
. . . . . . . 8
⊢ 0 ∈
V |
97 | 96 | a1i 11 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → 0 ∈ V) |
98 | 52, 92, 93, 97 | fvmptd 6197 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → (𝐺‘𝐾) = 0 ) |
99 | 98 | oveq2d 6565 |
. . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = ((𝐾 ↑ 𝑋) · 0 )) |
100 | | crngring 18381 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
101 | | chfacfisf.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (Poly1‘𝑅) |
102 | | chfacfisf.y |
. . . . . . . . . . . 12
⊢ 𝑌 = (𝑁 Mat 𝑃) |
103 | 101, 102 | pmatlmod 20318 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ LMod) |
104 | 100, 103 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ LMod) |
105 | 104 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ LMod) |
106 | 105 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → 𝑌 ∈ LMod) |
107 | 101 | ply1ring 19439 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
108 | 100, 107 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) |
109 | 108 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ Ring) |
110 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
111 | 110 | ringmgp 18376 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
112 | 109, 111 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝑃) ∈ Mnd) |
113 | 112 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) →
(mulGrp‘𝑃) ∈
Mnd) |
114 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℕ0) |
115 | 100 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
116 | | chfacfscmulcl.x |
. . . . . . . . . . . . 13
⊢ 𝑋 = (var1‘𝑅) |
117 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑃) =
(Base‘𝑃) |
118 | 116, 101,
117 | vr1cl 19408 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
119 | 115, 118 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑋 ∈ (Base‘𝑃)) |
120 | 119 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → 𝑋 ∈ (Base‘𝑃)) |
121 | 110, 117 | mgpbas 18318 |
. . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
122 | | chfacfscmulcl.e |
. . . . . . . . . . 11
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
123 | 121, 122 | mulgnn0cl 17381 |
. . . . . . . . . 10
⊢
(((mulGrp‘𝑃)
∈ Mnd ∧ 𝐾 ∈
ℕ0 ∧ 𝑋
∈ (Base‘𝑃))
→ (𝐾 ↑ 𝑋) ∈ (Base‘𝑃)) |
124 | 113, 114,
120, 123 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → (𝐾 ↑ 𝑋) ∈ (Base‘𝑃)) |
125 | 101 | ply1crng 19389 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
126 | 125 | anim2i 591 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) |
127 | 126 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) |
128 | 102 | matsca2 20045 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝑌)) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑃 = (Scalar‘𝑌)) |
130 | 129 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝑌) = 𝑃) |
131 | 130 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Base‘(Scalar‘𝑌)) = (Base‘𝑃)) |
132 | 131 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝐾 ↑ 𝑋) ∈ (Base‘𝑃))) |
133 | 132 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → ((𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝐾 ↑ 𝑋) ∈ (Base‘𝑃))) |
134 | 124, 133 | mpbird 246 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → (𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌))) |
135 | 106, 134 | jca 553 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) → (𝑌 ∈ LMod ∧ (𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)))) |
136 | 135 | adantr 480 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → (𝑌 ∈ LMod ∧ (𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)))) |
137 | | eqid 2610 |
. . . . . . 7
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) |
138 | | chfacfscmulcl.m |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑌) |
139 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌)) |
140 | 137, 138,
139, 94 | lmodvs0 18720 |
. . . . . 6
⊢ ((𝑌 ∈ LMod ∧ (𝐾 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌))) → ((𝐾 ↑ 𝑋) · 0 ) = 0 ) |
141 | 136, 140 | syl 17 |
. . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → ((𝐾 ↑ 𝑋) · 0 ) = 0 ) |
142 | 99, 141 | eqtrd 2644 |
. . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝐾 ∈ ℕ0) ∧ (𝑠 + 1) < 𝐾) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 ) |
143 | 142 | expl 646 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((𝐾 ∈ ℕ0 ∧ (𝑠 + 1) < 𝐾) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 )) |
144 | 50, 143 | syld 46 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝐾 ∈ (ℤ≥‘(𝑠 + 2)) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 )) |
145 | 144 | 3impia 1253 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) ∧ 𝐾 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 ) |