![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > modfsummodslem1 | Structured version Visualization version GIF version |
Description: Lemma 1 for modfsummods 15843. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
Ref | Expression |
---|---|
modfsummodslem1 | ⊢ (∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vsnid 4685 | . . 3 ⊢ 𝑧 ∈ {𝑧} | |
2 | elun2 4206 | . . 3 ⊢ (𝑧 ∈ {𝑧} → 𝑧 ∈ (𝐴 ∪ {𝑧})) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ 𝑧 ∈ (𝐴 ∪ {𝑧}) |
4 | rspcsbela 4461 | . 2 ⊢ ((𝑧 ∈ (𝐴 ∪ {𝑧}) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) | |
5 | 3, 4 | mpan 689 | 1 ⊢ (∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2108 ∀wral 3067 ⦋csb 3921 ∪ cun 3974 {csn 4648 ℤcz 12641 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ral 3068 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-ss 3993 df-nul 4353 df-sn 4649 |
This theorem is referenced by: modfsummods 15843 |
Copyright terms: Public domain | W3C validator |