Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  oddennn GIF version

Theorem oddennn 11942
 Description: There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.)
Assertion
Ref Expression
oddennn {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ≈ ℕ

Proof of Theorem oddennn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnex 8751 . . 3 ℕ ∈ V
21rabex 4080 . 2 {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∈ V
3 elrabi 2841 . . . 4 (𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} → 𝑥 ∈ ℕ)
43peano2nnd 8760 . . 3 (𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} → (𝑥 + 1) ∈ ℕ)
5 breq2 3941 . . . . . . 7 (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥))
65notbid 657 . . . . . 6 (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥))
76elrab 2844 . . . . 5 (𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥))
87simprbi 273 . . . 4 (𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} → ¬ 2 ∥ 𝑥)
93nnzd 9197 . . . . 5 (𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} → 𝑥 ∈ ℤ)
10 oddp1even 11610 . . . . 5 (𝑥 ∈ ℤ → (¬ 2 ∥ 𝑥 ↔ 2 ∥ (𝑥 + 1)))
119, 10syl 14 . . . 4 (𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} → (¬ 2 ∥ 𝑥 ↔ 2 ∥ (𝑥 + 1)))
128, 11mpbid 146 . . 3 (𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} → 2 ∥ (𝑥 + 1))
13 nnehalf 11638 . . 3 (((𝑥 + 1) ∈ ℕ ∧ 2 ∥ (𝑥 + 1)) → ((𝑥 + 1) / 2) ∈ ℕ)
144, 12, 13syl2anc 409 . 2 (𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} → ((𝑥 + 1) / 2) ∈ ℕ)
15 nnz 9098 . . . . . 6 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
16 2z 9107 . . . . . . 7 2 ∈ ℤ
1716a1i 9 . . . . . 6 (𝑦 ∈ ℕ → 2 ∈ ℤ)
1815, 17zmulcld 9204 . . . . 5 (𝑦 ∈ ℕ → (𝑦 · 2) ∈ ℤ)
19 peano2zm 9117 . . . . 5 ((𝑦 · 2) ∈ ℤ → ((𝑦 · 2) − 1) ∈ ℤ)
2018, 19syl 14 . . . 4 (𝑦 ∈ ℕ → ((𝑦 · 2) − 1) ∈ ℤ)
21 1e2m1 8864 . . . . 5 1 = (2 − 1)
2217zred 9198 . . . . . 6 (𝑦 ∈ ℕ → 2 ∈ ℝ)
23 nnre 8752 . . . . . . 7 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
2423, 22remulcld 7821 . . . . . 6 (𝑦 ∈ ℕ → (𝑦 · 2) ∈ ℝ)
25 1red 7806 . . . . . 6 (𝑦 ∈ ℕ → 1 ∈ ℝ)
26 0le2 8835 . . . . . . . 8 0 ≤ 2
2726a1i 9 . . . . . . 7 (𝑦 ∈ ℕ → 0 ≤ 2)
28 nnge1 8768 . . . . . . 7 (𝑦 ∈ ℕ → 1 ≤ 𝑦)
2922, 23, 27, 28lemulge12d 8721 . . . . . 6 (𝑦 ∈ ℕ → 2 ≤ (𝑦 · 2))
3022, 24, 25, 29lesub1dd 8348 . . . . 5 (𝑦 ∈ ℕ → (2 − 1) ≤ ((𝑦 · 2) − 1))
3121, 30eqbrtrid 3971 . . . 4 (𝑦 ∈ ℕ → 1 ≤ ((𝑦 · 2) − 1))
32 elnnz1 9102 . . . 4 (((𝑦 · 2) − 1) ∈ ℕ ↔ (((𝑦 · 2) − 1) ∈ ℤ ∧ 1 ≤ ((𝑦 · 2) − 1)))
3320, 31, 32sylanbrc 414 . . 3 (𝑦 ∈ ℕ → ((𝑦 · 2) − 1) ∈ ℕ)
34 dvdsmul2 11553 . . . . 5 ((𝑦 ∈ ℤ ∧ 2 ∈ ℤ) → 2 ∥ (𝑦 · 2))
3515, 16, 34sylancl 410 . . . 4 (𝑦 ∈ ℕ → 2 ∥ (𝑦 · 2))
36 oddm1even 11609 . . . . . 6 ((𝑦 · 2) ∈ ℤ → (¬ 2 ∥ (𝑦 · 2) ↔ 2 ∥ ((𝑦 · 2) − 1)))
3718, 36syl 14 . . . . 5 (𝑦 ∈ ℕ → (¬ 2 ∥ (𝑦 · 2) ↔ 2 ∥ ((𝑦 · 2) − 1)))
3837biimprd 157 . . . 4 (𝑦 ∈ ℕ → (2 ∥ ((𝑦 · 2) − 1) → ¬ 2 ∥ (𝑦 · 2)))
3935, 38mt2d 615 . . 3 (𝑦 ∈ ℕ → ¬ 2 ∥ ((𝑦 · 2) − 1))
40 breq2 3941 . . . . 5 (𝑧 = ((𝑦 · 2) − 1) → (2 ∥ 𝑧 ↔ 2 ∥ ((𝑦 · 2) − 1)))
4140notbid 657 . . . 4 (𝑧 = ((𝑦 · 2) − 1) → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ ((𝑦 · 2) − 1)))
4241elrab 2844 . . 3 (((𝑦 · 2) − 1) ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ↔ (((𝑦 · 2) − 1) ∈ ℕ ∧ ¬ 2 ∥ ((𝑦 · 2) − 1)))
4333, 39, 42sylanbrc 414 . 2 (𝑦 ∈ ℕ → ((𝑦 · 2) − 1) ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧})
443adantr 274 . . . . . . 7 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ ℕ)
4544nncnd 8759 . . . . . 6 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ ℂ)
46 1cnd 7807 . . . . . 6 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → 1 ∈ ℂ)
4745, 46addcld 7810 . . . . 5 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → (𝑥 + 1) ∈ ℂ)
48 simpr 109 . . . . . 6 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
4948nncnd 8759 . . . . 5 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℂ)
50 2cnd 8818 . . . . 5 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → 2 ∈ ℂ)
51 2ap0 8838 . . . . . 6 2 # 0
5251a1i 9 . . . . 5 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → 2 # 0)
5347, 49, 50, 52divmulap3d 8610 . . . 4 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → (((𝑥 + 1) / 2) = 𝑦 ↔ (𝑥 + 1) = (𝑦 · 2)))
5449, 50mulcld 7811 . . . . 5 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → (𝑦 · 2) ∈ ℂ)
5545, 46, 54addlsub 8157 . . . 4 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → ((𝑥 + 1) = (𝑦 · 2) ↔ 𝑥 = ((𝑦 · 2) − 1)))
5653, 55bitrd 187 . . 3 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → (((𝑥 + 1) / 2) = 𝑦𝑥 = ((𝑦 · 2) − 1)))
57 eqcom 2142 . . 3 (((𝑥 + 1) / 2) = 𝑦𝑦 = ((𝑥 + 1) / 2))
5856, 57bitr3di 194 . 2 ((𝑥 ∈ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ∧ 𝑦 ∈ ℕ) → (𝑥 = ((𝑦 · 2) − 1) ↔ 𝑦 = ((𝑥 + 1) / 2)))
592, 1, 14, 43, 58en3i 6673 1 {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ≈ ℕ
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 1481  {crab 2421   class class class wbr 3937  (class class class)co 5782   ≈ cen 6640  0cc0 7645  1c1 7646   + caddc 7648   · cmul 7650   ≤ cle 7826   − cmin 7958   # cap 8368   / cdiv 8457  ℕcn 8745  2c2 8796  ℤcz 9079   ∥ cdvds 11530 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-cnex 7736  ax-resscn 7737  ax-1cn 7738  ax-1re 7739  ax-icn 7740  ax-addcl 7741  ax-addrcl 7742  ax-mulcl 7743  ax-mulrcl 7744  ax-addcom 7745  ax-mulcom 7746  ax-addass 7747  ax-mulass 7748  ax-distr 7749  ax-i2m1 7750  ax-0lt1 7751  ax-1rid 7752  ax-0id 7753  ax-rnegex 7754  ax-precex 7755  ax-cnre 7756  ax-pre-ltirr 7757  ax-pre-ltwlin 7758  ax-pre-lttrn 7759  ax-pre-apti 7760  ax-pre-ltadd 7761  ax-pre-mulgt0 7762  ax-pre-mulext 7763 This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-xor 1355  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2691  df-sbc 2914  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-br 3938  df-opab 3998  df-mpt 3999  df-id 4223  df-po 4226  df-iso 4227  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-fv 5139  df-riota 5738  df-ov 5785  df-oprab 5786  df-mpo 5787  df-en 6643  df-pnf 7827  df-mnf 7828  df-xr 7829  df-ltxr 7830  df-le 7831  df-sub 7960  df-neg 7961  df-reap 8362  df-ap 8369  df-div 8458  df-inn 8746  df-2 8804  df-n0 9003  df-z 9080  df-dvds 11531 This theorem is referenced by:  xpnnen  11944  unennn  11947
 Copyright terms: Public domain W3C validator