Theorem lcmf0val 16718

Description: The value, by convention, of the least common multiple for a set containing 0 is 0. (Contributed by AV, 21-Apr-2020.) (Proof shortened by AV, 16-Sep-2020.)

Assertion

Ref	Expression
lcmf0val	⊢ ((𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍) → (lcm‘𝑍) = 0)

Proof of Theorem lcmf0val

Dummy variables 𝑚 𝑛 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-lcmf 16687	. 2 ⊢ lcm = (𝑧 ∈ 𝒫 ℤ ↦ if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < )))
2		eleq2 2851	. . . 4 ⊢ (𝑧 = 𝑍 → (0 ∈ 𝑧 ↔ 0 ∈ 𝑍))
3		raleq 3318	. . . . . 6 ⊢ (𝑧 = 𝑍 → (∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 ↔ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛))
4	3	rabbidv 3421	. . . . 5 ⊢ (𝑧 = 𝑍 → {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛} = {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛})
5	4	infeq1d 9452	. . . 4 ⊢ (𝑧 = 𝑍 → inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < ) = inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛}, ℝ, < ))
6	2, 5	ifbieq2d 4512	. . 3 ⊢ (𝑧 = 𝑍 → if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < )) = if(0 ∈ 𝑍, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛}, ℝ, < )))
7		iftrue 4491	. . . 4 ⊢ (0 ∈ 𝑍 → if(0 ∈ 𝑍, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛}, ℝ, < )) = 0)
8	7	adantl 487	. . 3 ⊢ ((𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍) → if(0 ∈ 𝑍, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛}, ℝ, < )) = 0)
9	6, 8	sylan9eqr 2819	. 2 ⊢ (((𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍) ∧ 𝑧 = 𝑍) → if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < )) = 0)
10		zex 12628	. . . . . 6 ⊢ ℤ ∈ V
11	10	ssex 5289	. . . . 5 ⊢ (𝑍 ⊆ ℤ → 𝑍 ∈ V)
12		elpwg 4563	. . . . 5 ⊢ (𝑍 ∈ V → (𝑍 ∈ 𝒫 ℤ ↔ 𝑍 ⊆ ℤ))
13	11, 12	syl 18	. . . 4 ⊢ (𝑍 ⊆ ℤ → (𝑍 ∈ 𝒫 ℤ ↔ 𝑍 ⊆ ℤ))
14	13	ibir 271	. . 3 ⊢ (𝑍 ⊆ ℤ → 𝑍 ∈ 𝒫 ℤ)
15	14	adantr 486	. 2 ⊢ ((𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍) → 𝑍 ∈ 𝒫 ℤ)
16		simpr 490	. 2 ⊢ ((𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍) → 0 ∈ 𝑍)
17	1, 9, 15, 16	fvmptd2 6999	1 ⊢ ((𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍) → (lcm‘𝑍) = 0)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078  {crab 3414  Vcvv 3453   ⊆ wss 3902  ifcif 4485  𝒫 cpw 4560   class class class wbr 5107  ‘cfv 6537  infcinf 9415  ℝcr 11127  0cc0 11128   < clt 11271  ℕcn 12261  ℤcz 12619   ∥ cdvds 16348  lcmclcmf 16685

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402  ax-cnex 11184  ax-resscn 11185

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7420  df-sup 9416  df-inf 9417  df-neg 11472  df-z 12620  df-lcmf 16687

This theorem is used by:  lcmfcl  16724  lcmfeq0b  16726  dvdslcmf  16727  lcmftp  16732  lcmfunsnlem2  16736