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	$⊢ φ \to N \in ℕ$
	lcmineqlem4.2	$⊢ φ \to M \in ℕ$
	lcmineqlem4.3	$⊢ φ \to M \leq N$
	lcmineqlem4.4	$⊢ φ \to K \in (0 \dots N - M)$
Assertion	lcmineqlem4	$⊢ φ \to \frac{\underline{lcm} ((1 \dots N))}{M + K} \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem4.1	$⊢ φ \to N \in ℕ$
2		lcmineqlem4.2	$⊢ φ \to M \in ℕ$
3		lcmineqlem4.3	$⊢ φ \to M \leq N$
4		lcmineqlem4.4	$⊢ φ \to K \in (0 \dots N - M)$
5		breq1	$⊢ k = M + K \to (k ∥ \underline{lcm} ((1 \dots N)) \leftrightarrow (M + K) ∥ \underline{lcm} ((1 \dots N)))$
6		fzssz	$⊢ (1 \dots N) \subseteq ℤ$
7		fzfi	$⊢ (1 \dots N) \in Fin$
8	6 7	pm3.2i	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin)$
9	8	a1i	$⊢ φ \to ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin)$
10		dvdslcmf	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin) \to \forall k \in (1 \dots N) k ∥ \underline{lcm} ((1 \dots N))$
11	9 10	syl	$⊢ φ \to \forall k \in (1 \dots N) k ∥ \underline{lcm} ((1 \dots N))$
12		1zzd	$⊢ φ \to 1 \in ℤ$
13	2	nnzd	$⊢ φ \to M \in ℤ$
14		0zd	$⊢ φ \to 0 \in ℤ$
15	1	nnzd	$⊢ φ \to N \in ℤ$
16	15 13	zsubcld	$⊢ φ \to N - M \in ℤ$
17	2	nnred	$⊢ φ \to M \in ℝ$
18	17	leidd	$⊢ φ \to M \leq M$
19		fznn	$⊢ M \in ℤ \to (M \in (1 \dots M) \leftrightarrow (M \in ℕ \land M \leq M))$
20	13 19	syl	$⊢ φ \to (M \in (1 \dots M) \leftrightarrow (M \in ℕ \land M \leq M))$
21	2 18 20	mpbir2and	$⊢ φ \to M \in (1 \dots M)$
22		1cnd	$⊢ φ \to 1 \in ℂ$
23	22	addridd	$⊢ φ \to 1 + 0 = 1$
24	23	eqcomd	$⊢ φ \to 1 = 1 + 0$
25	1	nncnd	$⊢ φ \to N \in ℂ$
26	2	nncnd	$⊢ φ \to M \in ℂ$
27	25 26	npcand	$⊢ φ \to N - M + M = N$
28		eqcom	$⊢ N - M + M = N \leftrightarrow N = N - M + M$
29	28	a1i	$⊢ φ \to (N - M + M = N \leftrightarrow N = N - M + M)$
30	25 26	jca	$⊢ φ \to (N \in ℂ \land M \in ℂ)$
31		subcl	$⊢ (N \in ℂ \land M \in ℂ) \to N - M \in ℂ$
32	30 31	syl	$⊢ φ \to N - M \in ℂ$
33	32 26	jca	$⊢ φ \to (N - M \in ℂ \land M \in ℂ)$
34		addcom	$⊢ (N - M \in ℂ \land M \in ℂ) \to N - M + M = M + N - M$
35	33 34	syl	$⊢ φ \to N - M + M = M + N - M$
36		eqeq2	$⊢ N - M + M = M + N - M \to (N = N - M + M \leftrightarrow N = M + N - M)$
37	35 36	syl	$⊢ φ \to (N = N - M + M \leftrightarrow N = M + N - M)$
38	29 37	bitrd	$⊢ φ \to (N - M + M = N \leftrightarrow N = M + N - M)$
39	38	pm5.74i	$⊢ (φ \to N - M + M = N) \leftrightarrow (φ \to N = M + N - M)$
40	27 39	mpbi	$⊢ φ \to N = M + N - M$
41	12 13 14 16 21 4 24 40	fzadd2d	$⊢ φ \to M + K \in (1 \dots N)$
42	5 11 41	rspcdva	$⊢ φ \to (M + K) ∥ \underline{lcm} ((1 \dots N))$
43		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
44	43 7	pm3.2i	$⊢ ((1 \dots N) \subseteq ℕ \land (1 \dots N) \in Fin)$
45		lcmfnncl	$⊢ ((1 \dots N) \subseteq ℕ \land (1 \dots N) \in Fin) \to \underline{lcm} ((1 \dots N)) \in ℕ$
46	44 45	ax-mp	$⊢ \underline{lcm} ((1 \dots N)) \in ℕ$
47	46	a1i	$⊢ φ \to \underline{lcm} ((1 \dots N)) \in ℕ$
48		elfznn0	$⊢ K \in (0 \dots N - M) \to K \in ℕ_{0}$
49	4 48	syl	$⊢ φ \to K \in ℕ_{0}$
50		nnnn0addcl	$⊢ (M \in ℕ \land K \in ℕ_{0}) \to M + K \in ℕ$
51	2 49 50	syl2anc	$⊢ φ \to M + K \in ℕ$
52		nndivdvds	$⊢ (\underline{lcm} ((1 \dots N)) \in ℕ \land M + K \in ℕ) \to ((M + K) ∥ \underline{lcm} ((1 \dots N)) \leftrightarrow \frac{\underline{lcm} ((1 \dots N))}{M + K} \in ℕ)$
53	47 51 52	syl2anc	$⊢ φ \to ((M + K) ∥ \underline{lcm} ((1 \dots N)) \leftrightarrow \frac{\underline{lcm} ((1 \dots N))}{M + K} \in ℕ)$
54	42 53	mpbid	$⊢ φ \to \frac{\underline{lcm} ((1 \dots N))}{M + K} \in ℕ$
55	54	nnzd	$⊢ φ \to \frac{\underline{lcm} ((1 \dots N))}{M + K} \in ℤ$

Metamath Proof Explorer

Theorem lcmineqlem4

Proof