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

Theorem lcmineqlem22 40620
Description: The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024.)
Hypotheses
Ref Expression
lcmineqlem22.1 (𝜑𝑁 ∈ ℕ)
lcmineqlem22.2 (𝜑 → 4 ≤ 𝑁)
Assertion
Ref Expression
lcmineqlem22 (𝜑 → ((2↑((2 · 𝑁) + 1)) ≤ (lcm‘(1...((2 · 𝑁) + 1))) ∧ (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 2)))))

Proof of Theorem lcmineqlem22
StepHypRef Expression
1 2re 12258 . . . . 5 2 ∈ ℝ
21a1i 11 . . . 4 (𝜑 → 2 ∈ ℝ)
3 2nn0 12461 . . . . . . 7 2 ∈ ℕ0
43a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℕ0)
5 lcmineqlem22.1 . . . . . . 7 (𝜑𝑁 ∈ ℕ)
65nnnn0d 12504 . . . . . 6 (𝜑𝑁 ∈ ℕ0)
74, 6nn0mulcld 12509 . . . . 5 (𝜑 → (2 · 𝑁) ∈ ℕ0)
8 1nn0 12460 . . . . . 6 1 ∈ ℕ0
98a1i 11 . . . . 5 (𝜑 → 1 ∈ ℕ0)
107, 9nn0addcld 12508 . . . 4 (𝜑 → ((2 · 𝑁) + 1) ∈ ℕ0)
112, 10reexpcld 14100 . . 3 (𝜑 → (2↑((2 · 𝑁) + 1)) ∈ ℝ)
127, 4nn0addcld 12508 . . . 4 (𝜑 → ((2 · 𝑁) + 2) ∈ ℕ0)
132, 12reexpcld 14100 . . 3 (𝜑 → (2↑((2 · 𝑁) + 2)) ∈ ℝ)
14 fz1ssnn 13504 . . . . . 6 (1...((2 · 𝑁) + 1)) ⊆ ℕ
15 fzfi 13909 . . . . . 6 (1...((2 · 𝑁) + 1)) ∈ Fin
16 lcmfnncl 16538 . . . . . 6 (((1...((2 · 𝑁) + 1)) ⊆ ℕ ∧ (1...((2 · 𝑁) + 1)) ∈ Fin) → (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℕ)
1714, 15, 16mp2an 690 . . . . 5 (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℕ
1817a1i 11 . . . 4 (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℕ)
1918nnred 12199 . . 3 (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℝ)
20 1red 11187 . . . . 5 (𝜑 → 1 ∈ ℝ)
215nnred 12199 . . . . . 6 (𝜑𝑁 ∈ ℝ)
222, 21remulcld 11216 . . . . 5 (𝜑 → (2 · 𝑁) ∈ ℝ)
23 1lt2 12355 . . . . . . 7 1 < 2
2423a1i 11 . . . . . 6 (𝜑 → 1 < 2)
2520, 2, 24ltled 11334 . . . . 5 (𝜑 → 1 ≤ 2)
2620, 2, 22, 25leadd2dd 11801 . . . 4 (𝜑 → ((2 · 𝑁) + 1) ≤ ((2 · 𝑁) + 2))
27 2z 12566 . . . . . . . 8 2 ∈ ℤ
2827a1i 11 . . . . . . 7 (𝜑 → 2 ∈ ℤ)
295nnzd 12557 . . . . . . 7 (𝜑𝑁 ∈ ℤ)
3028, 29zmulcld 12644 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ ℤ)
3130peano2zd 12641 . . . . 5 (𝜑 → ((2 · 𝑁) + 1) ∈ ℤ)
3230, 28zaddcld 12642 . . . . 5 (𝜑 → ((2 · 𝑁) + 2) ∈ ℤ)
332, 31, 32, 24leexp2d 14187 . . . 4 (𝜑 → (((2 · 𝑁) + 1) ≤ ((2 · 𝑁) + 2) ↔ (2↑((2 · 𝑁) + 1)) ≤ (2↑((2 · 𝑁) + 2))))
3426, 33mpbid 231 . . 3 (𝜑 → (2↑((2 · 𝑁) + 1)) ≤ (2↑((2 · 𝑁) + 2)))
35 lcmineqlem22.2 . . . 4 (𝜑 → 4 ≤ 𝑁)
365, 35lcmineqlem21 40619 . . 3 (𝜑 → (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
3711, 13, 19, 34, 36letrd 11343 . 2 (𝜑 → (2↑((2 · 𝑁) + 1)) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
38 fz1ssnn 13504 . . . . . 6 (1...((2 · 𝑁) + 2)) ⊆ ℕ
39 fzfi 13909 . . . . . 6 (1...((2 · 𝑁) + 2)) ∈ Fin
40 lcmfnncl 16538 . . . . . 6 (((1...((2 · 𝑁) + 2)) ⊆ ℕ ∧ (1...((2 · 𝑁) + 2)) ∈ Fin) → (lcm‘(1...((2 · 𝑁) + 2))) ∈ ℕ)
4138, 39, 40mp2an 690 . . . . 5 (lcm‘(1...((2 · 𝑁) + 2))) ∈ ℕ
4241a1i 11 . . . 4 (𝜑 → (lcm‘(1...((2 · 𝑁) + 2))) ∈ ℕ)
4342nnred 12199 . . 3 (𝜑 → (lcm‘(1...((2 · 𝑁) + 2))) ∈ ℝ)
4418nnzd 12557 . . . . . . . 8 (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ)
4544, 32jca 512 . . . . . . 7 (𝜑 → ((lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ ∧ ((2 · 𝑁) + 2) ∈ ℤ))
46 dvdslcm 16507 . . . . . . 7 (((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))))
4745, 46syl 17 . . . . . 6 (𝜑 → ((lcm‘(1...((2 · 𝑁) + 1))) ∥ ((lcm‘(1...((2 · 𝑁) + 1))) lcm ((2 · 𝑁) + 2)) ∧ ((2 · 𝑁) + 2) ∥ ((lcm‘(1...((2 · 𝑁) + 1))) lcm ((2 · 𝑁) + 2))))
4847simpld 495 . . . . 5 (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ∥ ((lcm‘(1...((2 · 𝑁) + 1))) lcm ((2 · 𝑁) + 2)))
49 2nn 12257 . . . . . . . . . 10 2 ∈ ℕ
5049a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℕ)
5150, 5nnmulcld 12237 . . . . . . . 8 (𝜑 → (2 · 𝑁) ∈ ℕ)
5251, 50nnaddcld 12236 . . . . . . 7 (𝜑 → ((2 · 𝑁) + 2) ∈ ℕ)
5352lcmfunnnd 40582 . . . . . 6 (𝜑 → (lcm‘(1...((2 · 𝑁) + 2))) = ((lcm‘(1...(((2 · 𝑁) + 2) − 1))) lcm ((2 · 𝑁) + 2)))
5422recnd 11214 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℂ)
552recnd 11214 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
56 1cnd 11181 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
5754, 55, 56addsubassd 11563 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) + 2) − 1) = ((2 · 𝑁) + (2 − 1)))
58 2m1e1 12310 . . . . . . . . . . 11 (2 − 1) = 1
5958oveq2i 7395 . . . . . . . . . 10 ((2 · 𝑁) + (2 − 1)) = ((2 · 𝑁) + 1)
6057, 59eqtrdi 2787 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) + 2) − 1) = ((2 · 𝑁) + 1))
6160oveq2d 7400 . . . . . . . 8 (𝜑 → (1...(((2 · 𝑁) + 2) − 1)) = (1...((2 · 𝑁) + 1)))
6261fveq2d 6873 . . . . . . 7 (𝜑 → (lcm‘(1...(((2 · 𝑁) + 2) − 1))) = (lcm‘(1...((2 · 𝑁) + 1))))
6362oveq1d 7399 . . . . . 6 (𝜑 → ((lcm‘(1...(((2 · 𝑁) + 2) − 1))) lcm ((2 · 𝑁) + 2)) = ((lcm‘(1...((2 · 𝑁) + 1))) lcm ((2 · 𝑁) + 2)))
6453, 63eqtrd 2771 . . . . 5 (𝜑 → (lcm‘(1...((2 · 𝑁) + 2))) = ((lcm‘(1...((2 · 𝑁) + 1))) lcm ((2 · 𝑁) + 2)))
6548, 64breqtrrd 5160 . . . 4 (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ∥ (lcm‘(1...((2 · 𝑁) + 2))))
6644, 42jca 512 . . . . 5 (𝜑 → ((lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ ∧ (lcm‘(1...((2 · 𝑁) + 2))) ∈ ℕ))
67 dvdsle 16225 . . . . 5 (((lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ ∧ (lcm‘(1...((2 · 𝑁) + 2))) ∈ ℕ) → ((lcm‘(1...((2 · 𝑁) + 1))) ∥ (lcm‘(1...((2 · 𝑁) + 2))) → (lcm‘(1...((2 · 𝑁) + 1))) ≤ (lcm‘(1...((2 · 𝑁) + 2)))))
6866, 67syl 17 . . . 4 (𝜑 → ((lcm‘(1...((2 · 𝑁) + 1))) ∥ (lcm‘(1...((2 · 𝑁) + 2))) → (lcm‘(1...((2 · 𝑁) + 1))) ≤ (lcm‘(1...((2 · 𝑁) + 2)))))
6965, 68mpd 15 . . 3 (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ≤ (lcm‘(1...((2 · 𝑁) + 2))))
7013, 19, 43, 36, 69letrd 11343 . 2 (𝜑 → (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 2))))
7137, 70jca 512 1 (𝜑 → ((2↑((2 · 𝑁) + 1)) ≤ (lcm‘(1...((2 · 𝑁) + 1))) ∧ (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 2)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  wss 3935   class class class wbr 5132  cfv 6523  (class class class)co 7384  Fincfn 8912  cr 11081  1c1 11083   + caddc 11085   · cmul 11087   < clt 11220  cle 11221  cmin 11416  cn 12184  2c2 12239  4c4 12241  0cn0 12444  cz 12530  ...cfz 13456  cexp 13999  cdvds 16169   lcm clcm 16497  lcmclcmf 16498
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 2702  ax-rep 5269  ax-sep 5283  ax-nul 5290  ax-pow 5347  ax-pr 5411  ax-un 7699  ax-inf2 9608  ax-cc 10402  ax-cnex 11138  ax-resscn 11139  ax-1cn 11140  ax-icn 11141  ax-addcl 11142  ax-addrcl 11143  ax-mulcl 11144  ax-mulrcl 11145  ax-mulcom 11146  ax-addass 11147  ax-mulass 11148  ax-distr 11149  ax-i2m1 11150  ax-1ne0 11151  ax-1rid 11152  ax-rnegex 11153  ax-rrecex 11154  ax-cnre 11155  ax-pre-lttri 11156  ax-pre-lttrn 11157  ax-pre-ltadd 11158  ax-pre-mulgt0 11159  ax-pre-sup 11160  ax-addf 11161  ax-mulf 11162
This theorem depends on definitions:  df-bi 206  df-an 397  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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3371  df-reu 3372  df-rab 3426  df-v 3468  df-sbc 3765  df-csb 3881  df-dif 3938  df-un 3940  df-in 3942  df-ss 3952  df-pss 3954  df-symdif 4229  df-nul 4310  df-if 4514  df-pw 4589  df-sn 4614  df-pr 4616  df-tp 4618  df-op 4620  df-uni 4893  df-int 4935  df-iun 4983  df-iin 4984  df-disj 5098  df-br 5133  df-opab 5195  df-mpt 5216  df-tr 5250  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5615  df-se 5616  df-we 5617  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6280  df-ord 6347  df-on 6348  df-lim 6349  df-suc 6350  df-iota 6475  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-isom 6532  df-riota 7340  df-ov 7387  df-oprab 7388  df-mpo 7389  df-of 7644  df-ofr 7645  df-om 7830  df-1st 7948  df-2nd 7949  df-supp 8120  df-frecs 8239  df-wrecs 8270  df-recs 8344  df-rdg 8383  df-1o 8439  df-2o 8440  df-oadd 8443  df-omul 8444  df-er 8677  df-map 8796  df-pm 8797  df-ixp 8865  df-en 8913  df-dom 8914  df-sdom 8915  df-fin 8916  df-fsupp 9335  df-fi 9378  df-sup 9409  df-inf 9410  df-oi 9477  df-dju 9868  df-card 9906  df-acn 9909  df-pnf 11222  df-mnf 11223  df-xr 11224  df-ltxr 11225  df-le 11226  df-sub 11418  df-neg 11419  df-div 11844  df-nn 12185  df-2 12247  df-3 12248  df-4 12249  df-5 12250  df-6 12251  df-7 12252  df-8 12253  df-9 12254  df-n0 12445  df-z 12531  df-dec 12650  df-uz 12795  df-q 12905  df-rp 12947  df-xneg 13064  df-xadd 13065  df-xmul 13066  df-ioo 13300  df-ioc 13301  df-ico 13302  df-icc 13303  df-fz 13457  df-fzo 13600  df-fl 13729  df-mod 13807  df-seq 13939  df-exp 14000  df-fac 14206  df-bc 14235  df-hash 14263  df-cj 15018  df-re 15019  df-im 15020  df-sqrt 15154  df-abs 15155  df-limsup 15387  df-clim 15404  df-rlim 15405  df-sum 15605  df-prod 15822  df-dvds 16170  df-gcd 16408  df-lcm 16499  df-lcmf 16500  df-struct 17052  df-sets 17069  df-slot 17087  df-ndx 17099  df-base 17117  df-ress 17146  df-plusg 17182  df-mulr 17183  df-starv 17184  df-sca 17185  df-vsca 17186  df-ip 17187  df-tset 17188  df-ple 17189  df-ds 17191  df-unif 17192  df-hom 17193  df-cco 17194  df-rest 17340  df-topn 17341  df-0g 17359  df-gsum 17360  df-topgen 17361  df-pt 17362  df-prds 17365  df-xrs 17420  df-qtop 17425  df-imas 17426  df-xps 17428  df-mre 17502  df-mrc 17503  df-acs 17505  df-mgm 18533  df-sgrp 18582  df-mnd 18593  df-submnd 18638  df-mulg 18909  df-cntz 19133  df-cmn 19600  df-psmet 20847  df-xmet 20848  df-met 20849  df-bl 20850  df-mopn 20851  df-fbas 20852  df-fg 20853  df-cnfld 20856  df-top 22302  df-topon 22319  df-topsp 22341  df-bases 22355  df-cld 22429  df-ntr 22430  df-cls 22431  df-nei 22508  df-lp 22546  df-perf 22547  df-cn 22637  df-cnp 22638  df-haus 22725  df-cmp 22797  df-tx 22972  df-hmeo 23165  df-fil 23256  df-fm 23348  df-flim 23349  df-flf 23350  df-xms 23732  df-ms 23733  df-tms 23734  df-cncf 24300  df-ovol 24887  df-vol 24888  df-mbf 25042  df-itg1 25043  df-itg2 25044  df-ibl 25045  df-itg 25046  df-0p 25093  df-limc 25289  df-dv 25290
This theorem is referenced by:  lcmineqlem23  40621
  Copyright terms: Public domain W3C validator