| Step | Hyp | Ref
| Expression |
| 1 | | ply1mulgsum.a |
. . . 4
⊢ 𝐴 = (coe1‘𝐾) |
| 2 | | ply1mulgsum.b |
. . . 4
⊢ 𝐵 = (Base‘𝑃) |
| 3 | | ply1mulgsum.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
| 4 | | eqid 2737 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 5 | 1, 2, 3, 4 | coe1ae0 22218 |
. . 3
⊢ (𝐾 ∈ 𝐵 → ∃𝑏 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) |
| 6 | 5 | 3ad2ant2 1135 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑏 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) |
| 7 | | ply1mulgsum.c |
. . . . 5
⊢ 𝐶 = (coe1‘𝐿) |
| 8 | 7, 2, 3, 4 | coe1ae0 22218 |
. . . 4
⊢ (𝐿 ∈ 𝐵 → ∃𝑎 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅))) |
| 9 | 8 | 3ad2ant3 1136 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑎 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅))) |
| 10 | | nn0addcl 12561 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → (𝑎 + 𝑏) ∈
ℕ0) |
| 11 | 10 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) → (𝑎 + 𝑏) ∈
ℕ0) |
| 12 | 11 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ (∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ ∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)))) → (𝑎 + 𝑏) ∈
ℕ0) |
| 13 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑎 + 𝑏) → (𝑠 < 𝑛 ↔ (𝑎 + 𝑏) < 𝑛)) |
| 14 | 13 | imbi1d 341 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑎 + 𝑏) → ((𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))) ↔ ((𝑎 + 𝑏) < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))) |
| 15 | 14 | ralbidv 3178 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝑎 + 𝑏) → (∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))) ↔ ∀𝑛 ∈ ℕ0 ((𝑎 + 𝑏) < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))) |
| 16 | 15 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑎 ∈
ℕ0 ∧ 𝑏
∈ ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ (∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ ∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)))) ∧ 𝑠 = (𝑎 + 𝑏)) → (∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))) ↔ ∀𝑛 ∈ ℕ0 ((𝑎 + 𝑏) < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))) |
| 17 | | r19.26 3111 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ0 ((𝑎
< 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) ↔ (∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ ∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)))) |
| 18 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℂ) |
| 19 | 18 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑏 ∈ ℕ0
∧ 𝑎 ∈
ℕ0) → 𝑎 ∈ ℂ) |
| 20 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℂ) |
| 21 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑏 ∈ ℕ0
∧ 𝑎 ∈
ℕ0) → 𝑏 ∈ ℂ) |
| 22 | 19, 21 | addcomd 11463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑏 ∈ ℕ0
∧ 𝑎 ∈
ℕ0) → (𝑎 + 𝑏) = (𝑏 + 𝑎)) |
| 23 | 22 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑏 ∈ ℕ0
∧ 𝑎 ∈
ℕ0 ∧ 𝑛
∈ ℕ0) → (𝑎 + 𝑏) = (𝑏 + 𝑎)) |
| 24 | 23 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑏 ∈ ℕ0
∧ 𝑎 ∈
ℕ0 ∧ 𝑛
∈ ℕ0) → ((𝑎 + 𝑏) < 𝑛 ↔ (𝑏 + 𝑎) < 𝑛)) |
| 25 | | nn0sumltlt 48266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑏 ∈ ℕ0
∧ 𝑎 ∈
ℕ0 ∧ 𝑛
∈ ℕ0) → ((𝑏 + 𝑎) < 𝑛 → 𝑎 < 𝑛)) |
| 26 | 24, 25 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑏 ∈ ℕ0
∧ 𝑎 ∈
ℕ0 ∧ 𝑛
∈ ℕ0) → ((𝑎 + 𝑏) < 𝑛 → 𝑎 < 𝑛)) |
| 27 | 26 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑏 ∈ ℕ0
∧ 𝑎 ∈
ℕ0) → (𝑛 ∈ ℕ0 → ((𝑎 + 𝑏) < 𝑛 → 𝑎 < 𝑛))) |
| 28 | 27 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → (𝑛 ∈ ℕ0 → ((𝑎 + 𝑏) < 𝑛 → 𝑎 < 𝑛))) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) → (𝑛 ∈ ℕ0 → ((𝑎 + 𝑏) < 𝑛 → 𝑎 < 𝑛))) |
| 30 | 29 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑎 + 𝑏) < 𝑛 → 𝑎 < 𝑛)) |
| 31 | 30 | imim1d 82 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) → ((𝑎 + 𝑏) < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)))) |
| 32 | 31 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑎 + 𝑏) < 𝑛 → ((𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) → (𝐶‘𝑛) = (0g‘𝑅)))) |
| 33 | 32 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 ∈
ℕ0 ∧ 𝑏
∈ ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (𝑎 + 𝑏) < 𝑛) → ((𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) → (𝐶‘𝑛) = (0g‘𝑅))) |
| 34 | | nn0sumltlt 48266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0 ∧ 𝑛
∈ ℕ0) → ((𝑎 + 𝑏) < 𝑛 → 𝑏 < 𝑛)) |
| 35 | 34 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → (𝑛 ∈ ℕ0 → ((𝑎 + 𝑏) < 𝑛 → 𝑏 < 𝑛))) |
| 36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) → (𝑛 ∈ ℕ0 → ((𝑎 + 𝑏) < 𝑛 → 𝑏 < 𝑛))) |
| 37 | 36 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑎 + 𝑏) < 𝑛 → 𝑏 < 𝑛)) |
| 38 | 37 | imim1d 82 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → ((𝑎 + 𝑏) < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)))) |
| 39 | 38 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑎 + 𝑏) < 𝑛 → ((𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → (𝐴‘𝑛) = (0g‘𝑅)))) |
| 40 | 39 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 ∈
ℕ0 ∧ 𝑏
∈ ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (𝑎 + 𝑏) < 𝑛) → ((𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → (𝐴‘𝑛) = (0g‘𝑅))) |
| 41 | 33, 40 | anim12d 609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 ∈
ℕ0 ∧ 𝑏
∈ ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (𝑎 + 𝑏) < 𝑛) → (((𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) → ((𝐶‘𝑛) = (0g‘𝑅) ∧ (𝐴‘𝑛) = (0g‘𝑅)))) |
| 42 | 41 | imp 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑎 ∈
ℕ0 ∧ 𝑏
∈ ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (𝑎 + 𝑏) < 𝑛) ∧ ((𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)))) → ((𝐶‘𝑛) = (0g‘𝑅) ∧ (𝐴‘𝑛) = (0g‘𝑅))) |
| 43 | 42 | ancomd 461 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑎 ∈
ℕ0 ∧ 𝑏
∈ ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (𝑎 + 𝑏) < 𝑛) ∧ ((𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)))) → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))) |
| 44 | 43 | exp31 419 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑎 + 𝑏) < 𝑛 → (((𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))) |
| 45 | 44 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (((𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) → ((𝑎 + 𝑏) < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))) |
| 46 | 45 | ralimdva 3167 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) → (∀𝑛 ∈ ℕ0 ((𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) → ∀𝑛 ∈ ℕ0 ((𝑎 + 𝑏) < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))) |
| 47 | 17, 46 | biimtrrid 243 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) → ((∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ ∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) → ∀𝑛 ∈ ℕ0 ((𝑎 + 𝑏) < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))) |
| 48 | 47 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ (∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ ∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)))) → ∀𝑛 ∈ ℕ0 ((𝑎 + 𝑏) < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))) |
| 49 | 12, 16, 48 | rspcedvd 3624 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ (𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵)) ∧ (∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ ∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)))) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))) |
| 50 | 49 | exp31 419 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ((∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ ∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))))) |
| 51 | 50 | com23 86 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → ((∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) ∧ ∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))))) |
| 52 | 51 | expd 415 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → (∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) → (∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))))) |
| 53 | 52 | com34 91 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → (∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))))) |
| 54 | 53 | impancom 451 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℕ0
∧ ∀𝑛 ∈
ℕ0 (𝑎 <
𝑛 → (𝐶‘𝑛) = (0g‘𝑅))) → (𝑏 ∈ ℕ0 → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))))) |
| 55 | 54 | com14 96 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ0 (𝑏 <
𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → (𝑏 ∈ ℕ0 → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ((𝑎 ∈ ℕ0 ∧
∀𝑛 ∈
ℕ0 (𝑎 <
𝑛 → (𝐶‘𝑛) = (0g‘𝑅))) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))))) |
| 56 | 55 | impcom 407 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ ∀𝑛 ∈
ℕ0 (𝑏 <
𝑛 → (𝐴‘𝑛) = (0g‘𝑅))) → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ((𝑎 ∈ ℕ0 ∧
∀𝑛 ∈
ℕ0 (𝑎 <
𝑛 → (𝐶‘𝑛) = (0g‘𝑅))) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))))) |
| 57 | 56 | rexlimiva 3147 |
. . . . 5
⊢
(∃𝑏 ∈
ℕ0 ∀𝑛 ∈ ℕ0 (𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ((𝑎 ∈ ℕ0 ∧
∀𝑛 ∈
ℕ0 (𝑎 <
𝑛 → (𝐶‘𝑛) = (0g‘𝑅))) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))))) |
| 58 | 57 | com13 88 |
. . . 4
⊢ ((𝑎 ∈ ℕ0
∧ ∀𝑛 ∈
ℕ0 (𝑎 <
𝑛 → (𝐶‘𝑛) = (0g‘𝑅))) → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (∃𝑏 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))))) |
| 59 | 58 | rexlimiva 3147 |
. . 3
⊢
(∃𝑎 ∈
ℕ0 ∀𝑛 ∈ ℕ0 (𝑎 < 𝑛 → (𝐶‘𝑛) = (0g‘𝑅)) → ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (∃𝑏 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))))) |
| 60 | 9, 59 | mpcom 38 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (∃𝑏 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑏 < 𝑛 → (𝐴‘𝑛) = (0g‘𝑅)) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))) |
| 61 | 6, 60 | mpd 15 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))) |