lcmineqlem20 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcmineqlem20		Structured version Visualization version GIF version

Theorem lcmineqlem20 40361

Description: Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.)

**Hypothesis**
Ref	Expression
lcmineqlem20.1	⊢ (𝜑 → 𝑁 ∈ ℕ)

**Assertion**
Ref	Expression
lcmineqlem20	⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1))))

**Proof of Theorem lcmineqlem20**
Step	Hyp	Ref	Expression
1		lcmineqlem20.1	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2	1	nnred 12098	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℝ)
3		2nn0 12360	. . . . . 6 ⊢ 2 ∈ ℕ₀
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℕ₀)
5	1	nnnn0d 12403	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
6	4, 5	nn0mulcld 12408	. . . 4 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ₀)
7		2re 12157	. . . . 5 ⊢ 2 ∈ ℝ
8		reexpcl 13909	. . . . 5 ⊢ ((2 ∈ ℝ ∧ (2 · 𝑁) ∈ ℕ₀) → (2↑(2 · 𝑁)) ∈ ℝ)
9	7, 8	mpan 688	. . . 4 ⊢ ((2 · 𝑁) ∈ ℕ₀ → (2↑(2 · 𝑁)) ∈ ℝ)
10	6, 9	syl 17	. . 3 ⊢ (𝜑 → (2↑(2 · 𝑁)) ∈ ℝ)
11	2, 10	remulcld 11115	. 2 ⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ∈ ℝ)
12	7	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℝ)
13	12, 2	remulcld 11115	. . . . 5 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
14		1red 11086	. . . . 5 ⊢ (𝜑 → 1 ∈ ℝ)
15	13, 14	readdcld 11114	. . . 4 ⊢ (𝜑 → ((2 · 𝑁) + 1) ∈ ℝ)
16		2nn 12156	. . . . . . . 8 ⊢ 2 ∈ ℕ
17	16	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℕ)
18	17, 1	nnmulcld 12136	. . . . . 6 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ)
19	5	nn0ge0d 12406	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝑁)
20	17	nnge1d 12131	. . . . . . 7 ⊢ (𝜑 → 1 ≤ 2)
21	2, 12, 19, 20	lemulge12d 12023	. . . . . 6 ⊢ (𝜑 → 𝑁 ≤ (2 · 𝑁))
22	18, 5, 21	bccl2d 40305	. . . . 5 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
23	22	nnred 12098	. . . 4 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℝ)
24	15, 23	remulcld 11115	. . 3 ⊢ (𝜑 → (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)) ∈ ℝ)
25	2, 24	remulcld 11115	. 2 ⊢ (𝜑 → (𝑁 · (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))) ∈ ℝ)
26		fz1ssnn 13397	. . . . 5 ⊢ (1...((2 · 𝑁) + 1)) ⊆ ℕ
27		fzfi 13802	. . . . 5 ⊢ (1...((2 · 𝑁) + 1)) ∈ Fin
28		lcmfnncl 16436	. . . . 5 ⊢ (((1...((2 · 𝑁) + 1)) ⊆ ℕ ∧ (1...((2 · 𝑁) + 1)) ∈ Fin) → (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℕ)
29	26, 27, 28	mp2an 690	. . . 4 ⊢ (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℕ
30	29	a1i 11	. . 3 ⊢ (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℕ)
31	30	nnred 12098	. 2 ⊢ (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℝ)
32	5	lcmineqlem17 40358	. . 3 ⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
33	1	nnrpd 12880	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
34	10, 24, 33	lemul2d 12926	. . 3 ⊢ (𝜑 → ((2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)) ↔ (𝑁 · (2↑(2 · 𝑁))) ≤ (𝑁 · (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))))
35	32, 34	mpbid 231	. 2 ⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (𝑁 · (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))))
36	2	recnd 11113	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℂ)
37	15	recnd 11113	. . . 4 ⊢ (𝜑 → ((2 · 𝑁) + 1) ∈ ℂ)
38	23	recnd 11113	. . . 4 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℂ)
39	36, 37, 38	mulassd 11108	. . 3 ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) = (𝑁 · (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))))
40	1	lcmineqlem19 40360	. . . 4 ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1))))
41	18	peano2nnd 12100	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝑁) + 1) ∈ ℕ)
42	1, 41	nnmulcld 12136	. . . . . . 7 ⊢ (𝜑 → (𝑁 · ((2 · 𝑁) + 1)) ∈ ℕ)
43	42, 22	nnmulcld 12136	. . . . . 6 ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∈ ℕ)
44	43	nnzd 12535	. . . . 5 ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∈ ℤ)
45		dvdsle 16123	. . . . 5 ⊢ ((((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∈ ℤ ∧ (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℕ) → (((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1))) → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ≤ (lcm‘(1...((2 · 𝑁) + 1)))))
46	44, 30, 45	syl2anc 585	. . . 4 ⊢ (𝜑 → (((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1))) → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ≤ (lcm‘(1...((2 · 𝑁) + 1)))))
47	40, 46	mpd 15	. . 3 ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
48	39, 47	eqbrtrrd 5124	. 2 ⊢ (𝜑 → (𝑁 · (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
49	11, 25, 31, 35, 48	letrd 11242	1 ⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2106 ⊆ wss 3905 class class class wbr 5100 ‘cfv 6488 (class class class)co 7346 Fincfn 8813 ℝcr 10980 1c1 10982 + caddc 10984 · cmul 10986 ≤ cle 11120 ℕcn 12083 2c2 12138 ℕ₀cn0 12343 ℤcz 12429 ...cfz 13349 ↑cexp 13892 Ccbc 14126 ∥ cdvds 16067 lcmclcmf 16396

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5237 ax-sep 5251 ax-nul 5258 ax-pow 5315 ax-pr 5379 ax-un 7659 ax-inf2 9507 ax-cc 10301 ax-cnex 11037 ax-resscn 11038 ax-1cn 11039 ax-icn 11040 ax-addcl 11041 ax-addrcl 11042 ax-mulcl 11043 ax-mulrcl 11044 ax-mulcom 11045 ax-addass 11046 ax-mulass 11047 ax-distr 11048 ax-i2m1 11049 ax-1ne0 11050 ax-1rid 11051 ax-rnegex 11052 ax-rrecex 11053 ax-cnre 11054 ax-pre-lttri 11055 ax-pre-lttrn 11056 ax-pre-ltadd 11057 ax-pre-mulgt0 11058 ax-pre-sup 11059 ax-addf 11060 ax-mulf 11061

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3735 df-csb 3851 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3924 df-symdif 4197 df-nul 4278 df-if 4482 df-pw 4557 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4861 df-int 4903 df-iun 4951 df-iin 4952 df-disj 5066 df-br 5101 df-opab 5163 df-mpt 5184 df-tr 5218 df-id 5525 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5582 df-se 5583 df-we 5584 df-xp 5633 df-rel 5634 df-cnv 5635 df-co 5636 df-dm 5637 df-rn 5638 df-res 5639 df-ima 5640 df-pred 6246 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6440 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-isom 6497 df-riota 7302 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7604 df-ofr 7605 df-om 7790 df-1st 7908 df-2nd 7909 df-supp 8057 df-frecs 8176 df-wrecs 8207 df-recs 8281 df-rdg 8320 df-1o 8376 df-2o 8377 df-oadd 8380 df-omul 8381 df-er 8578 df-map 8697 df-pm 8698 df-ixp 8766 df-en 8814 df-dom 8815 df-sdom 8816 df-fin 8817 df-fsupp 9236 df-fi 9277 df-sup 9308 df-inf 9309 df-oi 9376 df-dju 9767 df-card 9805 df-acn 9808 df-pnf 11121 df-mnf 11122 df-xr 11123 df-ltxr 11124 df-le 11125 df-sub 11317 df-neg 11318 df-div 11743 df-nn 12084 df-2 12146 df-3 12147 df-4 12148 df-5 12149 df-6 12150 df-7 12151 df-8 12152 df-9 12153 df-n0 12344 df-z 12430 df-dec 12548 df-uz 12693 df-q 12799 df-rp 12841 df-xneg 12958 df-xadd 12959 df-xmul 12960 df-ioo 13193 df-ioc 13194 df-ico 13195 df-icc 13196 df-fz 13350 df-fzo 13493 df-fl 13622 df-mod 13700 df-seq 13832 df-exp 13893 df-fac 14098 df-bc 14127 df-hash 14155 df-cj 14914 df-re 14915 df-im 14916 df-sqrt 15050 df-abs 15051 df-limsup 15284 df-clim 15301 df-rlim 15302 df-sum 15502 df-prod 15720 df-dvds 16068 df-gcd 16306 df-lcm 16397 df-lcmf 16398 df-struct 16950 df-sets 16967 df-slot 16985 df-ndx 16997 df-base 17015 df-ress 17044 df-plusg 17077 df-mulr 17078 df-starv 17079 df-sca 17080 df-vsca 17081 df-ip 17082 df-tset 17083 df-ple 17084 df-ds 17086 df-unif 17087 df-hom 17088 df-cco 17089 df-rest 17235 df-topn 17236 df-0g 17254 df-gsum 17255 df-topgen 17256 df-pt 17257 df-prds 17260 df-xrs 17315 df-qtop 17320 df-imas 17321 df-xps 17323 df-mre 17397 df-mrc 17398 df-acs 17400 df-mgm 18428 df-sgrp 18477 df-mnd 18488 df-submnd 18533 df-mulg 18802 df-cntz 19024 df-cmn 19488 df-psmet 20699 df-xmet 20700 df-met 20701 df-bl 20702 df-mopn 20703 df-fbas 20704 df-fg 20705 df-cnfld 20708 df-top 22153 df-topon 22170 df-topsp 22192 df-bases 22206 df-cld 22280 df-ntr 22281 df-cls 22282 df-nei 22359 df-lp 22397 df-perf 22398 df-cn 22488 df-cnp 22489 df-haus 22576 df-cmp 22648 df-tx 22823 df-hmeo 23016 df-fil 23107 df-fm 23199 df-flim 23200 df-flf 23201 df-xms 23583 df-ms 23584 df-tms 23585 df-cncf 24151 df-ovol 24738 df-vol 24739 df-mbf 24893 df-itg1 24894 df-itg2 24895 df-ibl 24896 df-itg 24897 df-0p 24944 df-limc 25140 df-dv 25141

This theorem is referenced by: lcmineqlem21 40362

W3C validator