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 40704
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 12265 . . . . 5 2 ∈ ℝ
21a1i 11 . . . 4 (𝜑 → 2 ∈ ℝ)
3 2nn0 12468 . . . . . . 7 2 ∈ ℕ0
43a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℕ0)
5 lcmineqlem22.1 . . . . . . 7 (𝜑𝑁 ∈ ℕ)
65nnnn0d 12511 . . . . . 6 (𝜑𝑁 ∈ ℕ0)
74, 6nn0mulcld 12516 . . . . 5 (𝜑 → (2 · 𝑁) ∈ ℕ0)
8 1nn0 12467 . . . . . 6 1 ∈ ℕ0
98a1i 11 . . . . 5 (𝜑 → 1 ∈ ℕ0)
107, 9nn0addcld 12515 . . . 4 (𝜑 → ((2 · 𝑁) + 1) ∈ ℕ0)
112, 10reexpcld 14107 . . 3 (𝜑 → (2↑((2 · 𝑁) + 1)) ∈ ℝ)
127, 4nn0addcld 12515 . . . 4 (𝜑 → ((2 · 𝑁) + 2) ∈ ℕ0)
132, 12reexpcld 14107 . . 3 (𝜑 → (2↑((2 · 𝑁) + 2)) ∈ ℝ)
14 fz1ssnn 13511 . . . . . 6 (1...((2 · 𝑁) + 1)) ⊆ ℕ
15 fzfi 13916 . . . . . 6 (1...((2 · 𝑁) + 1)) ∈ Fin
16 lcmfnncl 16545 . . . . . 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 12206 . . 3 (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℝ)
20 1red 11194 . . . . 5 (𝜑 → 1 ∈ ℝ)
215nnred 12206 . . . . . 6 (𝜑𝑁 ∈ ℝ)
222, 21remulcld 11223 . . . . 5 (𝜑 → (2 · 𝑁) ∈ ℝ)
23 1lt2 12362 . . . . . . 7 1 < 2
2423a1i 11 . . . . . 6 (𝜑 → 1 < 2)
2520, 2, 24ltled 11341 . . . . 5 (𝜑 → 1 ≤ 2)
2620, 2, 22, 25leadd2dd 11808 . . . 4 (𝜑 → ((2 · 𝑁) + 1) ≤ ((2 · 𝑁) + 2))
27 2z 12573 . . . . . . . 8 2 ∈ ℤ
2827a1i 11 . . . . . . 7 (𝜑 → 2 ∈ ℤ)
295nnzd 12564 . . . . . . 7 (𝜑𝑁 ∈ ℤ)
3028, 29zmulcld 12651 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ ℤ)
3130peano2zd 12648 . . . . 5 (𝜑 → ((2 · 𝑁) + 1) ∈ ℤ)
3230, 28zaddcld 12649 . . . . 5 (𝜑 → ((2 · 𝑁) + 2) ∈ ℤ)
332, 31, 32, 24leexp2d 14194 . . . 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 40703 . . 3 (𝜑 → (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
3711, 13, 19, 34, 36letrd 11350 . 2 (𝜑 → (2↑((2 · 𝑁) + 1)) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
38 fz1ssnn 13511 . . . . . 6 (1...((2 · 𝑁) + 2)) ⊆ ℕ
39 fzfi 13916 . . . . . 6 (1...((2 · 𝑁) + 2)) ∈ Fin
40 lcmfnncl 16545 . . . . . 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 12206 . . 3 (𝜑 → (lcm‘(1...((2 · 𝑁) + 2))) ∈ ℝ)
4418nnzd 12564 . . . . . . . 8 (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ)
4544, 32jca 512 . . . . . . 7 (𝜑 → ((lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ ∧ ((2 · 𝑁) + 2) ∈ ℤ))
46 dvdslcm 16514 . . . . . . 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 12264 . . . . . . . . . 10 2 ∈ ℕ
5049a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℕ)
5150, 5nnmulcld 12244 . . . . . . . 8 (𝜑 → (2 · 𝑁) ∈ ℕ)
5251, 50nnaddcld 12243 . . . . . . 7 (𝜑 → ((2 · 𝑁) + 2) ∈ ℕ)
5352lcmfunnnd 40666 . . . . . 6 (𝜑 → (lcm‘(1...((2 · 𝑁) + 2))) = ((lcm‘(1...(((2 · 𝑁) + 2) − 1))) lcm ((2 · 𝑁) + 2)))
5422recnd 11221 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℂ)
552recnd 11221 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
56 1cnd 11188 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
5754, 55, 56addsubassd 11570 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) + 2) − 1) = ((2 · 𝑁) + (2 − 1)))
58 2m1e1 12317 . . . . . . . . . . 11 (2 − 1) = 1
5958oveq2i 7401 . . . . . . . . . 10 ((2 · 𝑁) + (2 − 1)) = ((2 · 𝑁) + 1)
6057, 59eqtrdi 2787 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) + 2) − 1) = ((2 · 𝑁) + 1))
6160oveq2d 7406 . . . . . . . 8 (𝜑 → (1...(((2 · 𝑁) + 2) − 1)) = (1...((2 · 𝑁) + 1)))
6261fveq2d 6879 . . . . . . 7 (𝜑 → (lcm‘(1...(((2 · 𝑁) + 2) − 1))) = (lcm‘(1...((2 · 𝑁) + 1))))
6362oveq1d 7405 . . . . . 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 5166 . . . 4 (𝜑 → (lcm‘(1...((2 · 𝑁) + 1))) ∥ (lcm‘(1...((2 · 𝑁) + 2))))
6644, 42jca 512 . . . . 5 (𝜑 → ((lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ ∧ (lcm‘(1...((2 · 𝑁) + 2))) ∈ ℕ))
67 dvdsle 16232 . . . . 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 11350 . 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 3941   class class class wbr 5138  cfv 6529  (class class class)co 7390  Fincfn 8919  cr 11088  1c1 11090   + caddc 11092   · cmul 11094   < clt 11227  cle 11228  cmin 11423  cn 12191  2c2 12246  4c4 12248  0cn0 12451  cz 12537  ...cfz 13463  cexp 14006  cdvds 16176   lcm clcm 16504  lcmclcmf 16505
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 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7705  ax-inf2 9615  ax-cc 10409  ax-cnex 11145  ax-resscn 11146  ax-1cn 11147  ax-icn 11148  ax-addcl 11149  ax-addrcl 11150  ax-mulcl 11151  ax-mulrcl 11152  ax-mulcom 11153  ax-addass 11154  ax-mulass 11155  ax-distr 11156  ax-i2m1 11157  ax-1ne0 11158  ax-1rid 11159  ax-rnegex 11160  ax-rrecex 11161  ax-cnre 11162  ax-pre-lttri 11163  ax-pre-lttrn 11164  ax-pre-ltadd 11165  ax-pre-mulgt0 11166  ax-pre-sup 11167  ax-addf 11168  ax-mulf 11169
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 3375  df-reu 3376  df-rab 3430  df-v 3472  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-symdif 4235  df-nul 4316  df-if 4520  df-pw 4595  df-sn 4620  df-pr 4622  df-tp 4624  df-op 4626  df-uni 4899  df-int 4941  df-iun 4989  df-iin 4990  df-disj 5104  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6286  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6531  df-fn 6532  df-f 6533  df-f1 6534  df-fo 6535  df-f1o 6536  df-fv 6537  df-isom 6538  df-riota 7346  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7650  df-ofr 7651  df-om 7836  df-1st 7954  df-2nd 7955  df-supp 8126  df-frecs 8245  df-wrecs 8276  df-recs 8350  df-rdg 8389  df-1o 8445  df-2o 8446  df-oadd 8449  df-omul 8450  df-er 8683  df-map 8802  df-pm 8803  df-ixp 8872  df-en 8920  df-dom 8921  df-sdom 8922  df-fin 8923  df-fsupp 9342  df-fi 9385  df-sup 9416  df-inf 9417  df-oi 9484  df-dju 9875  df-card 9913  df-acn 9916  df-pnf 11229  df-mnf 11230  df-xr 11231  df-ltxr 11232  df-le 11233  df-sub 11425  df-neg 11426  df-div 11851  df-nn 12192  df-2 12254  df-3 12255  df-4 12256  df-5 12257  df-6 12258  df-7 12259  df-8 12260  df-9 12261  df-n0 12452  df-z 12538  df-dec 12657  df-uz 12802  df-q 12912  df-rp 12954  df-xneg 13071  df-xadd 13072  df-xmul 13073  df-ioo 13307  df-ioc 13308  df-ico 13309  df-icc 13310  df-fz 13464  df-fzo 13607  df-fl 13736  df-mod 13814  df-seq 13946  df-exp 14007  df-fac 14213  df-bc 14242  df-hash 14270  df-cj 15025  df-re 15026  df-im 15027  df-sqrt 15161  df-abs 15162  df-limsup 15394  df-clim 15411  df-rlim 15412  df-sum 15612  df-prod 15829  df-dvds 16177  df-gcd 16415  df-lcm 16506  df-lcmf 16507  df-struct 17059  df-sets 17076  df-slot 17094  df-ndx 17106  df-base 17124  df-ress 17153  df-plusg 17189  df-mulr 17190  df-starv 17191  df-sca 17192  df-vsca 17193  df-ip 17194  df-tset 17195  df-ple 17196  df-ds 17198  df-unif 17199  df-hom 17200  df-cco 17201  df-rest 17347  df-topn 17348  df-0g 17366  df-gsum 17367  df-topgen 17368  df-pt 17369  df-prds 17372  df-xrs 17427  df-qtop 17432  df-imas 17433  df-xps 17435  df-mre 17509  df-mrc 17510  df-acs 17512  df-mgm 18540  df-sgrp 18589  df-mnd 18600  df-submnd 18645  df-mulg 18920  df-cntz 19144  df-cmn 19611  df-psmet 20865  df-xmet 20866  df-met 20867  df-bl 20868  df-mopn 20869  df-fbas 20870  df-fg 20871  df-cnfld 20874  df-top 22320  df-topon 22337  df-topsp 22359  df-bases 22373  df-cld 22447  df-ntr 22448  df-cls 22449  df-nei 22526  df-lp 22564  df-perf 22565  df-cn 22655  df-cnp 22656  df-haus 22743  df-cmp 22815  df-tx 22990  df-hmeo 23183  df-fil 23274  df-fm 23366  df-flim 23367  df-flf 23368  df-xms 23750  df-ms 23751  df-tms 23752  df-cncf 24318  df-ovol 24905  df-vol 24906  df-mbf 25060  df-itg1 25061  df-itg2 25062  df-ibl 25063  df-itg 25064  df-0p 25111  df-limc 25307  df-dv 25308
This theorem is referenced by:  lcmineqlem23  40705
  Copyright terms: Public domain W3C validator