Theorem isprm2 16659

Description: The predicate "is a prime number". A prime number is an integer greater than or equal to 2 whose only positive divisors are 1 and itself. Definition in [ApostolNT] p. 16. (Contributed by Paul Chapman, 26-Oct-2012.)

Assertion

Ref	Expression
isprm2	⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))

Distinct variable group:   𝑧,𝑃

Proof of Theorem isprm2

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1nprm 16656	. . . . 5 ⊢ ¬ 1 ∈ ℙ
2		eleq1 2817	. . . . . 6 ⊢ (𝑃 = 1 → (𝑃 ∈ ℙ ↔ 1 ∈ ℙ))
3	2	biimpcd 249	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑃 = 1 → 1 ∈ ℙ))
4	1, 3	mtoi 199	. . . 4 ⊢ (𝑃 ∈ ℙ → ¬ 𝑃 = 1)
5	4	neqned 2933	. . 3 ⊢ (𝑃 ∈ ℙ → 𝑃 ≠ 1)
6	5	pm4.71i 559	. 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℙ ∧ 𝑃 ≠ 1))
7		isprm 16650	. . . 4 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o))
8		isprm2lem 16658	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o ↔ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃}))
9		eqss 3965	. . . . . . . . . . 11 ⊢ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃} ↔ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃} ∧ {1, 𝑃} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃}))
10	9	imbi2i 336	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℕ → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃}) ↔ (𝑃 ∈ ℕ → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃} ∧ {1, 𝑃} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃})))
11		1idssfct 16657	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℕ → {1, 𝑃} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃})
12		jcab 517	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℕ → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃} ∧ {1, 𝑃} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃})) ↔ ((𝑃 ∈ ℕ → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}) ∧ (𝑃 ∈ ℕ → {1, 𝑃} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃})))
13	11, 12	mpbiran2 710	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℕ → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃} ∧ {1, 𝑃} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃})) ↔ (𝑃 ∈ ℕ → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}))
14	10, 13	bitri 275	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃}) ↔ (𝑃 ∈ ℕ → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}))
15	14	pm5.74ri 272	. . . . . . . 8 ⊢ (𝑃 ∈ ℕ → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃} ↔ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}))
16	15	adantr 480	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃} ↔ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}))
17	8, 16	bitrd 279	. . . . . 6 ⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o ↔ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}))
18	17	expcom 413	. . . . 5 ⊢ (𝑃 ≠ 1 → (𝑃 ∈ ℕ → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o ↔ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃})))
19	18	pm5.32d 577	. . . 4 ⊢ (𝑃 ≠ 1 → ((𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o) ↔ (𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃})))
20	7, 19	bitrid 283	. . 3 ⊢ (𝑃 ≠ 1 → (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃})))
21	20	pm5.32ri 575	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ≠ 1) ↔ ((𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}) ∧ 𝑃 ≠ 1))
22		ancom 460	. . . 4 ⊢ (((𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}) ∧ 𝑃 ≠ 1) ↔ (𝑃 ≠ 1 ∧ (𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃})))
23		anass 468	. . . 4 ⊢ (((𝑃 ≠ 1 ∧ 𝑃 ∈ ℕ) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}) ↔ (𝑃 ≠ 1 ∧ (𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃})))
24	22, 23	bitr4i 278	. . 3 ⊢ (((𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}) ∧ 𝑃 ≠ 1) ↔ ((𝑃 ≠ 1 ∧ 𝑃 ∈ ℕ) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}))
25		ancom 460	. . . . 5 ⊢ ((𝑃 ≠ 1 ∧ 𝑃 ∈ ℕ) ↔ (𝑃 ∈ ℕ ∧ 𝑃 ≠ 1))
26		eluz2b3 12888	. . . . 5 ⊢ (𝑃 ∈ (ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 𝑃 ≠ 1))
27	25, 26	bitr4i 278	. . . 4 ⊢ ((𝑃 ≠ 1 ∧ 𝑃 ∈ ℕ) ↔ 𝑃 ∈ (ℤ≥‘2))
28	27	anbi1i 624	. . 3 ⊢ (((𝑃 ≠ 1 ∧ 𝑃 ∈ ℕ) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}) ↔ (𝑃 ∈ (ℤ≥‘2) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}))
29		df-ss 3934	. . . . 5 ⊢ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃} ↔ ∀𝑧(𝑧 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} → 𝑧 ∈ {1, 𝑃}))
30		breq1 5113	. . . . . . . . . 10 ⊢ (𝑛 = 𝑧 → (𝑛 ∥ 𝑃 ↔ 𝑧 ∥ 𝑃))
31	30	elrab 3662	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ↔ (𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃))
32		vex 3454	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
33	32	elpr 4617	. . . . . . . . 9 ⊢ (𝑧 ∈ {1, 𝑃} ↔ (𝑧 = 1 ∨ 𝑧 = 𝑃))
34	31, 33	imbi12i 350	. . . . . . . 8 ⊢ ((𝑧 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} → 𝑧 ∈ {1, 𝑃}) ↔ ((𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃) → (𝑧 = 1 ∨ 𝑧 = 𝑃)))
35		impexp 450	. . . . . . . 8 ⊢ (((𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃) → (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ (𝑧 ∈ ℕ → (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))
36	34, 35	bitri 275	. . . . . . 7 ⊢ ((𝑧 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} → 𝑧 ∈ {1, 𝑃}) ↔ (𝑧 ∈ ℕ → (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))
37	36	albii 1819	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} → 𝑧 ∈ {1, 𝑃}) ↔ ∀𝑧(𝑧 ∈ ℕ → (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))
38		df-ral 3046	. . . . . 6 ⊢ (∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ∀𝑧(𝑧 ∈ ℕ → (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))
39	37, 38	bitr4i 278	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} → 𝑧 ∈ {1, 𝑃}) ↔ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)))
40	29, 39	bitri 275	. . . 4 ⊢ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃} ↔ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)))
41	40	anbi2i 623	. . 3 ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}) ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))
42	24, 28, 41	3bitri 297	. 2 ⊢ (((𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ⊆ {1, 𝑃}) ∧ 𝑃 ≠ 1) ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))
43	6, 21, 42	3bitri 297	1 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  {crab 3408   ⊆ wss 3917  {cpr 4594   class class class wbr 5110  ‘cfv 6514  2_oc2o 8431   ≈ cen 8918  1c1 11076  ℕcn 12193  2c2 12248  ℤ_≥cuz 12800   ∥ cdvds 16229  ℙcprime 16648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-2o 8438  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-sup 9400  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-3 12257  df-n0 12450  df-z 12537  df-uz 12801  df-rp 12959  df-seq 13974  df-exp 14034  df-cj 15072  df-re 15073  df-im 15074  df-sqrt 15208  df-abs 15209  df-dvds 16230  df-prm 16649

This theorem is referenced by:  isprm3  16660  isprm4  16661  dvdsprime  16664  coprm  16688  isprm6  16691  ablsimpgprmd  20054  prmirredlem  21389  znidomb  21478  perfectlem2  27148  perfectALTVlem2  47727