Theorem lcmineqlem22

Description: The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	lcmineqlem22.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	lcmineqlem22.2	⊢ ( 𝜑 → 4 ≤ 𝑁 )
Assertion	lcmineqlem22	⊢ ( 𝜑 → ( ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∧ ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem22.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		lcmineqlem22.2	⊢ ( 𝜑 → 4 ≤ 𝑁 )
3		2re	⊢ 2 ∈ ℝ
4	3	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
5		2nn0	⊢ 2 ∈ ℕ0
6	5	a1i	⊢ ( 𝜑 → 2 ∈ ℕ0 )
7	1	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
8	6 7	nn0mulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
9		1nn0	⊢ 1 ∈ ℕ0
10	9	a1i	⊢ ( 𝜑 → 1 ∈ ℕ0 )
11	8 10	nn0addcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ0 )
12	4 11	reexpcld	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ )
13	8 6	nn0addcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 2 ) ∈ ℕ0 )
14	4 13	reexpcld	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ∈ ℝ )
15		fz1ssnn	⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ
16		fzfi	⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin
17		lcmfnncl	⊢ ( ( ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ ∧ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
18	15 16 17	mp2an	⊢ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ
19	18	a1i	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
20	19	nnred	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℝ )
21		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
22	1	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
23	4 22	remulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
24		1lt2	⊢ 1 < 2
25	24	a1i	⊢ ( 𝜑 → 1 < 2 )
26	21 4 25	ltled	⊢ ( 𝜑 → 1 ≤ 2 )
27	21 4 23 26	leadd2dd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ≤ ( ( 2 · 𝑁 ) + 2 ) )
28		2z	⊢ 2 ∈ ℤ
29	28	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
30	1	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
31	29 30	zmulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℤ )
32	31	peano2zd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ )
33	31 29	zaddcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 2 ) ∈ ℤ )
34	4 32 33 25	leexp2d	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) ≤ ( ( 2 · 𝑁 ) + 2 ) ↔ ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ) )
35	27 34	mpbid	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) )
36	1 2	lcmineqlem21	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
37	12 14 20 35 36	letrd	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
38		fz1ssnn	⊢ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ⊆ ℕ
39		fzfi	⊢ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ∈ Fin
40		lcmfnncl	⊢ ( ( ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ⊆ ℕ ∧ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ∈ Fin ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℕ )
41	38 39 40	mp2an	⊢ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℕ
42	41	a1i	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℕ )
43	42	nnred	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℝ )
44	19	nnzd	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℤ )
45	44 33	jca	⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℤ ∧ ( ( 2 · 𝑁 ) + 2 ) ∈ ℤ ) )
46		dvdslcm	⊢ ( ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℤ ∧ ( ( 2 · 𝑁 ) + 2 ) ∈ ℤ ) → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) ∧ ( ( 2 · 𝑁 ) + 2 ) ∥ ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) ) )
47	45 46	syl	⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) ∧ ( ( 2 · 𝑁 ) + 2 ) ∥ ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) ) )
48	47	simpld	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) )
49		2nn	⊢ 2 ∈ ℕ
50	49	a1i	⊢ ( 𝜑 → 2 ∈ ℕ )
51	50 1	nnmulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
52	51 50	nnaddcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 2 ) ∈ ℕ )
53	52	lcmfunnnd	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) = ( ( lcm ‘ ( 1 ... ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) )
54	23	recnd	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
55	4	recnd	⊢ ( 𝜑 → 2 ∈ ℂ )
56		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
57	54 55 56	addsubassd	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) = ( ( 2 · 𝑁 ) + ( 2 − 1 ) ) )
58		2m1e1	⊢ ( 2 − 1 ) = 1
59	58	oveq2i	⊢ ( ( 2 · 𝑁 ) + ( 2 − 1 ) ) = ( ( 2 · 𝑁 ) + 1 )
60	57 59	eqtrdi	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) = ( ( 2 · 𝑁 ) + 1 ) )
61	60	oveq2d	⊢ ( 𝜑 → ( 1 ... ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) ) = ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) )
62	61	fveq2d	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) ) ) = ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
63	62	oveq1d	⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) = ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) )
64	53 63	eqtrd	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) = ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) )
65	48 64	breqtrrd	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) )
66	44 42	jca	⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℤ ∧ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℕ ) )
67		dvdsle	⊢ ( ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℤ ∧ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℕ ) → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ) )
68	66 67	syl	⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ) )
69	65 68	mpd	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) )
70	14 20 43 36 69	letrd	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) )
71	37 70	jca	⊢ ( 𝜑 → ( ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∧ ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ) )