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

Theorem prime 9101
Description: Two ways to express "𝐴 is a prime number (or 1)." (Contributed by NM, 4-May-2005.)
Assertion
Ref Expression
prime (𝐴 ∈ ℕ → (∀𝑥 ∈ ℕ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ∀𝑥 ∈ ℕ ((1 < 𝑥𝑥𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴)))
Distinct variable group:   𝑥,𝐴

Proof of Theorem prime
StepHypRef Expression
1 nnz 9024 . . . . . . 7 (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
2 1z 9031 . . . . . . . 8 1 ∈ ℤ
3 zdceq 9077 . . . . . . . 8 ((𝑥 ∈ ℤ ∧ 1 ∈ ℤ) → DECID 𝑥 = 1)
42, 3mpan2 419 . . . . . . 7 (𝑥 ∈ ℤ → DECID 𝑥 = 1)
5 dfordc 860 . . . . . . . 8 (DECID 𝑥 = 1 → ((𝑥 = 1 ∨ 𝑥 = 𝐴) ↔ (¬ 𝑥 = 1 → 𝑥 = 𝐴)))
6 df-ne 2284 . . . . . . . . 9 (𝑥 ≠ 1 ↔ ¬ 𝑥 = 1)
76imbi1i 237 . . . . . . . 8 ((𝑥 ≠ 1 → 𝑥 = 𝐴) ↔ (¬ 𝑥 = 1 → 𝑥 = 𝐴))
85, 7syl6bbr 197 . . . . . . 7 (DECID 𝑥 = 1 → ((𝑥 = 1 ∨ 𝑥 = 𝐴) ↔ (𝑥 ≠ 1 → 𝑥 = 𝐴)))
91, 4, 83syl 17 . . . . . 6 (𝑥 ∈ ℕ → ((𝑥 = 1 ∨ 𝑥 = 𝐴) ↔ (𝑥 ≠ 1 → 𝑥 = 𝐴)))
109imbi2d 229 . . . . 5 (𝑥 ∈ ℕ → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 ≠ 1 → 𝑥 = 𝐴))))
11 impexp 261 . . . . . 6 (((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴) ↔ (𝑥 ≠ 1 → ((𝐴 / 𝑥) ∈ ℕ → 𝑥 = 𝐴)))
12 bi2.04 247 . . . . . 6 ((𝑥 ≠ 1 → ((𝐴 / 𝑥) ∈ ℕ → 𝑥 = 𝐴)) ↔ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 ≠ 1 → 𝑥 = 𝐴)))
1311, 12bitri 183 . . . . 5 (((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴) ↔ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 ≠ 1 → 𝑥 = 𝐴)))
1410, 13syl6bbr 197 . . . 4 (𝑥 ∈ ℕ → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴)))
1514adantl 273 . . 3 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴)))
16 nngt1ne1 8712 . . . . . . 7 (𝑥 ∈ ℕ → (1 < 𝑥𝑥 ≠ 1))
1716adantl 273 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (1 < 𝑥𝑥 ≠ 1))
1817anbi1d 458 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((1 < 𝑥 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ)))
19 nnz 9024 . . . . . . . . 9 ((𝐴 / 𝑥) ∈ ℕ → (𝐴 / 𝑥) ∈ ℤ)
20 nnre 8684 . . . . . . . . . . . . 13 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
21 gtndiv 9097 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℕ ∧ 𝐴 < 𝑥) → ¬ (𝐴 / 𝑥) ∈ ℤ)
22213expia 1166 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℕ) → (𝐴 < 𝑥 → ¬ (𝐴 / 𝑥) ∈ ℤ))
2320, 22sylan 279 . . . . . . . . . . . 12 ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → (𝐴 < 𝑥 → ¬ (𝐴 / 𝑥) ∈ ℤ))
2423con2d 596 . . . . . . . . . . 11 ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℤ → ¬ 𝐴 < 𝑥))
25 nnre 8684 . . . . . . . . . . . 12 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
26 lenlt 7804 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥𝐴 ↔ ¬ 𝐴 < 𝑥))
2720, 25, 26syl2an 285 . . . . . . . . . . 11 ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → (𝑥𝐴 ↔ ¬ 𝐴 < 𝑥))
2824, 27sylibrd 168 . . . . . . . . . 10 ((𝑥 ∈ ℕ ∧ 𝐴 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℤ → 𝑥𝐴))
2928ancoms 266 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℤ → 𝑥𝐴))
3019, 29syl5 32 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℕ → 𝑥𝐴))
3130pm4.71rd 389 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝐴 / 𝑥) ∈ ℕ ↔ (𝑥𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ)))
3231anbi2d 457 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((1 < 𝑥 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥 ∧ (𝑥𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ))))
33 3anass 949 . . . . . 6 ((1 < 𝑥𝑥𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥 ∧ (𝑥𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ)))
3432, 33syl6bbr 197 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((1 < 𝑥 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥𝑥𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ)))
3518, 34bitr3d 189 . . . 4 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → ((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) ↔ (1 < 𝑥𝑥𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ)))
3635imbi1d 230 . . 3 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (((𝑥 ≠ 1 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴) ↔ ((1 < 𝑥𝑥𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴)))
3715, 36bitrd 187 . 2 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ((1 < 𝑥𝑥𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴)))
3837ralbidva 2408 1 (𝐴 ∈ ℕ → (∀𝑥 ∈ ℕ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ∀𝑥 ∈ ℕ ((1 < 𝑥𝑥𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 680  DECID wdc 802  w3a 945   = wceq 1314  wcel 1463  wne 2283  wral 2391   class class class wbr 3897  (class class class)co 5740  cr 7583  1c1 7585   < clt 7764  cle 7765   / cdiv 8392  cn 8677  cz 9005
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 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-mulrcl 7683  ax-addcom 7684  ax-mulcom 7685  ax-addass 7686  ax-mulass 7687  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-1rid 7691  ax-0id 7692  ax-rnegex 7693  ax-precex 7694  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700  ax-pre-mulgt0 7701  ax-pre-mulext 7702
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-br 3898  df-opab 3958  df-id 4183  df-po 4186  df-iso 4187  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-iota 5056  df-fun 5093  df-fv 5099  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-reap 8300  df-ap 8307  df-div 8393  df-inn 8678  df-n0 8929  df-z 9006
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator