Theorem lcmineqlem4

Description: Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. F is found in lcmineqlem6 . (Contributed by metakunt, 10-May-2024)

	Ref	Expression
Hypotheses	lcmineqlem4.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	lcmineqlem4.2	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	lcmineqlem4.3	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
	lcmineqlem4.4	⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) )
Assertion	lcmineqlem4	⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝐾 ) ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem4.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		lcmineqlem4.2	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3		lcmineqlem4.3	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
4		lcmineqlem4.4	⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) )
5		breq1	⊢ ( 𝑘 = ( 𝑀 + 𝐾 ) → ( 𝑘 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ↔ ( 𝑀 + 𝐾 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
6		fzssz	⊢ ( 1 ... 𝑁 ) ⊆ ℤ
7		fzfi	⊢ ( 1 ... 𝑁 ) ∈ Fin
8	6 7	pm3.2i	⊢ ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin )
9	8	a1i	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ) )
10		dvdslcmf	⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
11	9 10	syl	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
12		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
13	2	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
14		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
15	1	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
16	15 13	zsubcld	⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℤ )
17	2	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
18	17	leidd	⊢ ( 𝜑 → 𝑀 ≤ 𝑀 )
19		fznn	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑀 ∈ ℕ ∧ 𝑀 ≤ 𝑀 ) ) )
20	13 19	syl	⊢ ( 𝜑 → ( 𝑀 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑀 ∈ ℕ ∧ 𝑀 ≤ 𝑀 ) ) )
21	2 18 20	mpbir2and	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... 𝑀 ) )
22		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
23	22	addridd	⊢ ( 𝜑 → ( 1 + 0 ) = 1 )
24	23	eqcomd	⊢ ( 𝜑 → 1 = ( 1 + 0 ) )
25	1	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
26	2	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
27	25 26	npcand	⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) + 𝑀 ) = 𝑁 )
28		eqcom	⊢ ( ( ( 𝑁 − 𝑀 ) + 𝑀 ) = 𝑁 ↔ 𝑁 = ( ( 𝑁 − 𝑀 ) + 𝑀 ) )
29	28	a1i	⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑀 ) + 𝑀 ) = 𝑁 ↔ 𝑁 = ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) )
30	25 26	jca	⊢ ( 𝜑 → ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) )
31		subcl	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑁 − 𝑀 ) ∈ ℂ )
32	30 31	syl	⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℂ )
33	32 26	jca	⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) ∈ ℂ ∧ 𝑀 ∈ ℂ ) )
34		addcom	⊢ ( ( ( 𝑁 − 𝑀 ) ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑁 − 𝑀 ) + 𝑀 ) = ( 𝑀 + ( 𝑁 − 𝑀 ) ) )
35	33 34	syl	⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) + 𝑀 ) = ( 𝑀 + ( 𝑁 − 𝑀 ) ) )
36		eqeq2	⊢ ( ( ( 𝑁 − 𝑀 ) + 𝑀 ) = ( 𝑀 + ( 𝑁 − 𝑀 ) ) → ( 𝑁 = ( ( 𝑁 − 𝑀 ) + 𝑀 ) ↔ 𝑁 = ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) )
37	35 36	syl	⊢ ( 𝜑 → ( 𝑁 = ( ( 𝑁 − 𝑀 ) + 𝑀 ) ↔ 𝑁 = ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) )
38	29 37	bitrd	⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑀 ) + 𝑀 ) = 𝑁 ↔ 𝑁 = ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) )
39	38	pm5.74i	⊢ ( ( 𝜑 → ( ( 𝑁 − 𝑀 ) + 𝑀 ) = 𝑁 ) ↔ ( 𝜑 → 𝑁 = ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) )
40	27 39	mpbi	⊢ ( 𝜑 → 𝑁 = ( 𝑀 + ( 𝑁 − 𝑀 ) ) )
41	12 13 14 16 21 4 24 40	fzadd2d	⊢ ( 𝜑 → ( 𝑀 + 𝐾 ) ∈ ( 1 ... 𝑁 ) )
42	5 11 41	rspcdva	⊢ ( 𝜑 → ( 𝑀 + 𝐾 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
43		fz1ssnn	⊢ ( 1 ... 𝑁 ) ⊆ ℕ
44	43 7	pm3.2i	⊢ ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin )
45		lcmfnncl	⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
46	44 45	ax-mp	⊢ ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ
47	46	a1i	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
48		elfznn0	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝐾 ∈ ℕ0 )
49	4 48	syl	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
50		nnnn0addcl	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 + 𝐾 ) ∈ ℕ )
51	2 49 50	syl2anc	⊢ ( 𝜑 → ( 𝑀 + 𝐾 ) ∈ ℕ )
52		nndivdvds	⊢ ( ( ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ ∧ ( 𝑀 + 𝐾 ) ∈ ℕ ) → ( ( 𝑀 + 𝐾 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ↔ ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝐾 ) ) ∈ ℕ ) )
53	47 51 52	syl2anc	⊢ ( 𝜑 → ( ( 𝑀 + 𝐾 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ↔ ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝐾 ) ) ∈ ℕ ) )
54	42 53	mpbid	⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝐾 ) ) ∈ ℕ )
55	54	nnzd	⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝐾 ) ) ∈ ℤ )