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

Theorem oddfl 38971
Description: Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Assertion
Ref Expression
oddfl ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1))

Proof of Theorem oddfl
StepHypRef Expression
1 zre 11328 . . . . . . . . 9 (𝐾 ∈ ℤ → 𝐾 ∈ ℝ)
2 1red 10002 . . . . . . . . 9 (𝐾 ∈ ℤ → 1 ∈ ℝ)
31, 2resubcld 10405 . . . . . . . 8 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℝ)
4 2rp 11784 . . . . . . . . 9 2 ∈ ℝ+
54a1i 11 . . . . . . . 8 (𝐾 ∈ ℤ → 2 ∈ ℝ+)
61lem1d 10904 . . . . . . . 8 (𝐾 ∈ ℤ → (𝐾 − 1) ≤ 𝐾)
73, 1, 5, 6lediv1dd 11877 . . . . . . 7 (𝐾 ∈ ℤ → ((𝐾 − 1) / 2) ≤ (𝐾 / 2))
81rehalfcld 11226 . . . . . . . . 9 (𝐾 ∈ ℤ → (𝐾 / 2) ∈ ℝ)
95rpreccld 11829 . . . . . . . . 9 (𝐾 ∈ ℤ → (1 / 2) ∈ ℝ+)
108, 9ltaddrpd 11852 . . . . . . . 8 (𝐾 ∈ ℤ → (𝐾 / 2) < ((𝐾 / 2) + (1 / 2)))
11 zcn 11329 . . . . . . . . . . 11 (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
122recnd 10015 . . . . . . . . . . 11 (𝐾 ∈ ℤ → 1 ∈ ℂ)
13 2cnd 11040 . . . . . . . . . . 11 (𝐾 ∈ ℤ → 2 ∈ ℂ)
145rpne0d 11824 . . . . . . . . . . 11 (𝐾 ∈ ℤ → 2 ≠ 0)
1511, 12, 13, 14divsubdird 10787 . . . . . . . . . 10 (𝐾 ∈ ℤ → ((𝐾 − 1) / 2) = ((𝐾 / 2) − (1 / 2)))
1615oveq1d 6622 . . . . . . . . 9 (𝐾 ∈ ℤ → (((𝐾 − 1) / 2) + 1) = (((𝐾 / 2) − (1 / 2)) + 1))
1711halfcld 11224 . . . . . . . . . 10 (𝐾 ∈ ℤ → (𝐾 / 2) ∈ ℂ)
1813, 14reccld 10741 . . . . . . . . . 10 (𝐾 ∈ ℤ → (1 / 2) ∈ ℂ)
1917, 18, 12subadd23d 10361 . . . . . . . . 9 (𝐾 ∈ ℤ → (((𝐾 / 2) − (1 / 2)) + 1) = ((𝐾 / 2) + (1 − (1 / 2))))
20 1mhlfehlf 11198 . . . . . . . . . . 11 (1 − (1 / 2)) = (1 / 2)
2120oveq2i 6618 . . . . . . . . . 10 ((𝐾 / 2) + (1 − (1 / 2))) = ((𝐾 / 2) + (1 / 2))
2221a1i 11 . . . . . . . . 9 (𝐾 ∈ ℤ → ((𝐾 / 2) + (1 − (1 / 2))) = ((𝐾 / 2) + (1 / 2)))
2316, 19, 223eqtrrd 2660 . . . . . . . 8 (𝐾 ∈ ℤ → ((𝐾 / 2) + (1 / 2)) = (((𝐾 − 1) / 2) + 1))
2410, 23breqtrd 4641 . . . . . . 7 (𝐾 ∈ ℤ → (𝐾 / 2) < (((𝐾 − 1) / 2) + 1))
257, 24jca 554 . . . . . 6 (𝐾 ∈ ℤ → (((𝐾 − 1) / 2) ≤ (𝐾 / 2) ∧ (𝐾 / 2) < (((𝐾 − 1) / 2) + 1)))
2625adantr 481 . . . . 5 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (((𝐾 − 1) / 2) ≤ (𝐾 / 2) ∧ (𝐾 / 2) < (((𝐾 − 1) / 2) + 1)))
271adantr 481 . . . . . . 7 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 ∈ ℝ)
2827rehalfcld 11226 . . . . . 6 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (𝐾 / 2) ∈ ℝ)
2911, 12npcand 10343 . . . . . . . . . 10 (𝐾 ∈ ℤ → ((𝐾 − 1) + 1) = 𝐾)
3029oveq1d 6622 . . . . . . . . 9 (𝐾 ∈ ℤ → (((𝐾 − 1) + 1) / 2) = (𝐾 / 2))
3130adantr 481 . . . . . . . 8 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (((𝐾 − 1) + 1) / 2) = (𝐾 / 2))
32 simpr 477 . . . . . . . . . 10 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (𝐾 mod 2) ≠ 0)
3332neneqd 2795 . . . . . . . . 9 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ¬ (𝐾 mod 2) = 0)
34 mod0 12618 . . . . . . . . . . 11 ((𝐾 ∈ ℝ ∧ 2 ∈ ℝ+) → ((𝐾 mod 2) = 0 ↔ (𝐾 / 2) ∈ ℤ))
351, 5, 34syl2anc 692 . . . . . . . . . 10 (𝐾 ∈ ℤ → ((𝐾 mod 2) = 0 ↔ (𝐾 / 2) ∈ ℤ))
3635adantr 481 . . . . . . . . 9 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((𝐾 mod 2) = 0 ↔ (𝐾 / 2) ∈ ℤ))
3733, 36mtbid 314 . . . . . . . 8 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ¬ (𝐾 / 2) ∈ ℤ)
3831, 37eqneltrd 2717 . . . . . . 7 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ¬ (((𝐾 − 1) + 1) / 2) ∈ ℤ)
39 simpl 473 . . . . . . . . 9 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 ∈ ℤ)
40 1zzd 11355 . . . . . . . . 9 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 1 ∈ ℤ)
4139, 40zsubcld 11434 . . . . . . . 8 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (𝐾 − 1) ∈ ℤ)
42 zeo2 11411 . . . . . . . 8 ((𝐾 − 1) ∈ ℤ → (((𝐾 − 1) / 2) ∈ ℤ ↔ ¬ (((𝐾 − 1) + 1) / 2) ∈ ℤ))
4341, 42syl 17 . . . . . . 7 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (((𝐾 − 1) / 2) ∈ ℤ ↔ ¬ (((𝐾 − 1) + 1) / 2) ∈ ℤ))
4438, 43mpbird 247 . . . . . 6 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((𝐾 − 1) / 2) ∈ ℤ)
45 flbi 12560 . . . . . 6 (((𝐾 / 2) ∈ ℝ ∧ ((𝐾 − 1) / 2) ∈ ℤ) → ((⌊‘(𝐾 / 2)) = ((𝐾 − 1) / 2) ↔ (((𝐾 − 1) / 2) ≤ (𝐾 / 2) ∧ (𝐾 / 2) < (((𝐾 − 1) / 2) + 1))))
4628, 44, 45syl2anc 692 . . . . 5 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((⌊‘(𝐾 / 2)) = ((𝐾 − 1) / 2) ↔ (((𝐾 − 1) / 2) ≤ (𝐾 / 2) ∧ (𝐾 / 2) < (((𝐾 − 1) / 2) + 1))))
4726, 46mpbird 247 . . . 4 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (⌊‘(𝐾 / 2)) = ((𝐾 − 1) / 2))
4847oveq2d 6623 . . 3 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (2 · (⌊‘(𝐾 / 2))) = (2 · ((𝐾 − 1) / 2)))
4948oveq1d 6622 . 2 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((2 · (⌊‘(𝐾 / 2))) + 1) = ((2 · ((𝐾 − 1) / 2)) + 1))
5011, 12subcld 10339 . . . . 5 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℂ)
5150, 13, 14divcan2d 10750 . . . 4 (𝐾 ∈ ℤ → (2 · ((𝐾 − 1) / 2)) = (𝐾 − 1))
5251oveq1d 6622 . . 3 (𝐾 ∈ ℤ → ((2 · ((𝐾 − 1) / 2)) + 1) = ((𝐾 − 1) + 1))
5352adantr 481 . 2 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((2 · ((𝐾 − 1) / 2)) + 1) = ((𝐾 − 1) + 1))
5429adantr 481 . 2 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((𝐾 − 1) + 1) = 𝐾)
5549, 53, 543eqtrrd 2660 1 ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790   class class class wbr 4615  cfv 5849  (class class class)co 6607  cr 9882  0cc0 9883  1c1 9884   + caddc 9886   · cmul 9888   < clt 10021  cle 10022  cmin 10213   / cdiv 10631  2c2 11017  cz 11324  +crp 11779  cfl 12534   mod cmo 12611
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-pre-sup 9961
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-er 7690  df-en 7903  df-dom 7904  df-sdom 7905  df-sup 8295  df-inf 8296  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-nn 10968  df-2 11026  df-n0 11240  df-z 11325  df-uz 11635  df-rp 11780  df-fl 12536  df-mod 12612
This theorem is referenced by:  dirkertrigeqlem3  39640  dirkertrigeq  39641
  Copyright terms: Public domain W3C validator