![]() |
Mathbox for Steve Rodriguez |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > nzin | Structured version Visualization version GIF version |
Description: The intersection of the set of multiples of m, mℤ, and those of n, nℤ, is the set of multiples of their least common multiple. Roughly Lemma 2.1(c) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5 and Problem 1(b) of https://people.math.binghamton.edu/mazur/teach/40107/40107h16sol.pdf p. 1, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
Ref | Expression |
---|---|
nzin.m | ⊢ (𝜑 → 𝑀 ∈ ℤ) |
nzin.n | ⊢ (𝜑 → 𝑁 ∈ ℤ) |
Ref | Expression |
---|---|
nzin | ⊢ (𝜑 → (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) = ( ∥ “ {(𝑀 lcm 𝑁)})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvdszrcl 16027 | . . . . . . . . 9 ⊢ (𝑀 ∥ 𝑛 → (𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ)) | |
2 | dvdszrcl 16027 | . . . . . . . . 9 ⊢ (𝑁 ∥ 𝑛 → (𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ)) | |
3 | 1, 2 | anim12i 613 | . . . . . . . 8 ⊢ ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → ((𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ))) |
4 | anandir 674 | . . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ))) | |
5 | 3, 4 | sylibr 233 | . . . . . . 7 ⊢ ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑛 ∈ ℤ)) |
6 | 5 | ancomd 462 | . . . . . 6 ⊢ ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → (𝑛 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) |
7 | lcmdvds 16372 | . . . . . . 7 ⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → (𝑀 lcm 𝑁) ∥ 𝑛)) | |
8 | 7 | 3expb 1119 | . . . . . 6 ⊢ ((𝑛 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → (𝑀 lcm 𝑁) ∥ 𝑛)) |
9 | 6, 8 | mpcom 38 | . . . . 5 ⊢ ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → (𝑀 lcm 𝑁) ∥ 𝑛) |
10 | elin 3907 | . . . . . 6 ⊢ (𝑛 ∈ (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) ↔ (𝑛 ∈ ( ∥ “ {𝑀}) ∧ 𝑛 ∈ ( ∥ “ {𝑁}))) | |
11 | reldvds 42159 | . . . . . . . 8 ⊢ Rel ∥ | |
12 | elrelimasn 6003 | . . . . . . . 8 ⊢ (Rel ∥ → (𝑛 ∈ ( ∥ “ {𝑀}) ↔ 𝑀 ∥ 𝑛)) | |
13 | 11, 12 | ax-mp 5 | . . . . . . 7 ⊢ (𝑛 ∈ ( ∥ “ {𝑀}) ↔ 𝑀 ∥ 𝑛) |
14 | elrelimasn 6003 | . . . . . . . 8 ⊢ (Rel ∥ → (𝑛 ∈ ( ∥ “ {𝑁}) ↔ 𝑁 ∥ 𝑛)) | |
15 | 11, 14 | ax-mp 5 | . . . . . . 7 ⊢ (𝑛 ∈ ( ∥ “ {𝑁}) ↔ 𝑁 ∥ 𝑛) |
16 | 13, 15 | anbi12i 627 | . . . . . 6 ⊢ ((𝑛 ∈ ( ∥ “ {𝑀}) ∧ 𝑛 ∈ ( ∥ “ {𝑁})) ↔ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)) |
17 | 10, 16 | bitri 274 | . . . . 5 ⊢ (𝑛 ∈ (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) ↔ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)) |
18 | elrelimasn 6003 | . . . . . 6 ⊢ (Rel ∥ → (𝑛 ∈ ( ∥ “ {(𝑀 lcm 𝑁)}) ↔ (𝑀 lcm 𝑁) ∥ 𝑛)) | |
19 | 11, 18 | ax-mp 5 | . . . . 5 ⊢ (𝑛 ∈ ( ∥ “ {(𝑀 lcm 𝑁)}) ↔ (𝑀 lcm 𝑁) ∥ 𝑛) |
20 | 9, 17, 19 | 3imtr4i 291 | . . . 4 ⊢ (𝑛 ∈ (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) → 𝑛 ∈ ( ∥ “ {(𝑀 lcm 𝑁)})) |
21 | 20 | ssriv 3929 | . . 3 ⊢ (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) ⊆ ( ∥ “ {(𝑀 lcm 𝑁)}) |
22 | 21 | a1i 11 | . 2 ⊢ (𝜑 → (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) ⊆ ( ∥ “ {(𝑀 lcm 𝑁)})) |
23 | nzin.m | . . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ) | |
24 | nzin.n | . . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℤ) | |
25 | dvdslcm 16362 | . . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁))) | |
26 | 23, 24, 25 | syl2anc 584 | . . . . 5 ⊢ (𝜑 → (𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁))) |
27 | 26 | simpld 495 | . . . 4 ⊢ (𝜑 → 𝑀 ∥ (𝑀 lcm 𝑁)) |
28 | lcmcl 16365 | . . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈ ℕ0) | |
29 | 23, 24, 28 | syl2anc 584 | . . . . . 6 ⊢ (𝜑 → (𝑀 lcm 𝑁) ∈ ℕ0) |
30 | 29 | nn0zd 12484 | . . . . 5 ⊢ (𝜑 → (𝑀 lcm 𝑁) ∈ ℤ) |
31 | 30, 23 | nzss 42161 | . . . 4 ⊢ (𝜑 → (( ∥ “ {(𝑀 lcm 𝑁)}) ⊆ ( ∥ “ {𝑀}) ↔ 𝑀 ∥ (𝑀 lcm 𝑁))) |
32 | 27, 31 | mpbird 256 | . . 3 ⊢ (𝜑 → ( ∥ “ {(𝑀 lcm 𝑁)}) ⊆ ( ∥ “ {𝑀})) |
33 | 26 | simprd 496 | . . . 4 ⊢ (𝜑 → 𝑁 ∥ (𝑀 lcm 𝑁)) |
34 | 30, 24 | nzss 42161 | . . . 4 ⊢ (𝜑 → (( ∥ “ {(𝑀 lcm 𝑁)}) ⊆ ( ∥ “ {𝑁}) ↔ 𝑁 ∥ (𝑀 lcm 𝑁))) |
35 | 33, 34 | mpbird 256 | . . 3 ⊢ (𝜑 → ( ∥ “ {(𝑀 lcm 𝑁)}) ⊆ ( ∥ “ {𝑁})) |
36 | 32, 35 | ssind 4171 | . 2 ⊢ (𝜑 → ( ∥ “ {(𝑀 lcm 𝑁)}) ⊆ (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁}))) |
37 | 22, 36 | eqssd 3942 | 1 ⊢ (𝜑 → (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) = ( ∥ “ {(𝑀 lcm 𝑁)})) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1538 ∈ wcel 2103 ∩ cin 3890 ⊆ wss 3891 {csn 4564 class class class wbr 5080 “ cima 5603 Rel wrel 5605 (class class class)co 7308 ℕ0cn0 12293 ℤcz 12379 ∥ cdvds 16022 lcm clcm 16352 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1910 ax-6 1968 ax-7 2008 ax-8 2105 ax-9 2113 ax-10 2134 ax-11 2151 ax-12 2168 ax-ext 2706 ax-sep 5231 ax-nul 5238 ax-pow 5296 ax-pr 5360 ax-un 7621 ax-cnex 10987 ax-resscn 10988 ax-1cn 10989 ax-icn 10990 ax-addcl 10991 ax-addrcl 10992 ax-mulcl 10993 ax-mulrcl 10994 ax-mulcom 10995 ax-addass 10996 ax-mulass 10997 ax-distr 10998 ax-i2m1 10999 ax-1ne0 11000 ax-1rid 11001 ax-rnegex 11002 ax-rrecex 11003 ax-cnre 11004 ax-pre-lttri 11005 ax-pre-lttrn 11006 ax-pre-ltadd 11007 ax-pre-mulgt0 11008 ax-pre-sup 11009 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1541 df-fal 1551 df-ex 1779 df-nf 1783 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2727 df-clel 2813 df-nfc 2885 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3339 df-reu 3340 df-rab 3357 df-v 3438 df-sbc 3721 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-pss 3910 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4565 df-pr 4567 df-op 4571 df-uni 4844 df-iun 4932 df-br 5081 df-opab 5143 df-mpt 5164 df-tr 5198 df-id 5500 df-eprel 5506 df-po 5514 df-so 5515 df-fr 5555 df-we 5557 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-pred 6217 df-ord 6284 df-on 6285 df-lim 6286 df-suc 6287 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-riota 7265 df-ov 7311 df-oprab 7312 df-mpo 7313 df-om 7749 df-2nd 7868 df-frecs 8132 df-wrecs 8163 df-recs 8237 df-rdg 8276 df-er 8534 df-en 8770 df-dom 8771 df-sdom 8772 df-sup 9259 df-inf 9260 df-pnf 11071 df-mnf 11072 df-xr 11073 df-ltxr 11074 df-le 11075 df-sub 11267 df-neg 11268 df-div 11693 df-nn 12034 df-2 12096 df-3 12097 df-n0 12294 df-z 12380 df-uz 12643 df-rp 12791 df-fl 13572 df-mod 13650 df-seq 13782 df-exp 13843 df-cj 14869 df-re 14870 df-im 14871 df-sqrt 15005 df-abs 15006 df-dvds 16023 df-gcd 16261 df-lcm 16354 |
This theorem is referenced by: nzprmdif 42163 |
Copyright terms: Public domain | W3C validator |