Metamath Proof Explorer

Theorem isprm6

Description: A number is prime iff it satisfies Euclid's lemma euclemma . (Contributed by Mario Carneiro, 6-Sep-2015)

Ref Expression
Assertion isprm6 ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
2 euclemma ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑥 · 𝑦 ) ↔ ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) )
3 2 3expb ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑃 ∥ ( 𝑥 · 𝑦 ) ↔ ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) )
4 3 biimpd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) )
5 4 ralrimivva ⊢ ( 𝑃 ∈ ℙ → ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) )
6 1 5 jca ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) )
7 simpl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
8 eluz2nn ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℕ )
9 8 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑃 ∈ ℕ )
10 9 nnzd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑃 ∈ ℤ )
11 iddvds ⊢ ( 𝑃 ∈ ℤ → 𝑃 ∥ 𝑃 )
12 10 11 syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑃 ∥ 𝑃 )
13 nncn ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℂ )
14 9 13 syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑃 ∈ ℂ )
15 nncn ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℂ )
16 15 ad2antrl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑧 ∈ ℂ )
17 nnne0 ⊢ ( 𝑧 ∈ ℕ → 𝑧 ≠ 0 )
18 17 ad2antrl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑧 ≠ 0 )
19 14 16 18 divcan1d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( ( 𝑃 / 𝑧 ) · 𝑧 ) = 𝑃 )
20 12 19 breqtrrd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑃 ∥ ( ( 𝑃 / 𝑧 ) · 𝑧 ) )
21 20 adantr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) → 𝑃 ∥ ( ( 𝑃 / 𝑧 ) · 𝑧 ) )
22 simprr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑧 ∥ 𝑃 )
23 simprl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑧 ∈ ℕ )
24 nndivdvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( 𝑧 ∥ 𝑃 ↔ ( 𝑃 / 𝑧 ) ∈ ℕ ) )
25 9 23 24 syl2anc ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑧 ∥ 𝑃 ↔ ( 𝑃 / 𝑧 ) ∈ ℕ ) )
26 22 25 mpbid ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑃 / 𝑧 ) ∈ ℕ )
27 26 nnzd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑃 / 𝑧 ) ∈ ℤ )
28 nnz ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℤ )
29 28 ad2antrl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑧 ∈ ℤ )
30 27 29 jca ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( ( 𝑃 / 𝑧 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) )
31 oveq1 ⊢ ( 𝑥 = ( 𝑃 / 𝑧 ) → ( 𝑥 · 𝑦 ) = ( ( 𝑃 / 𝑧 ) · 𝑦 ) )
32 31 breq2d ⊢ ( 𝑥 = ( 𝑃 / 𝑧 ) → ( 𝑃 ∥ ( 𝑥 · 𝑦 ) ↔ 𝑃 ∥ ( ( 𝑃 / 𝑧 ) · 𝑦 ) ) )
33 breq2 ⊢ ( 𝑥 = ( 𝑃 / 𝑧 ) → ( 𝑃 ∥ 𝑥 ↔ 𝑃 ∥ ( 𝑃 / 𝑧 ) ) )
34 33 orbi1d ⊢ ( 𝑥 = ( 𝑃 / 𝑧 ) → ( ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ↔ ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑦 ) ) )
35 32 34 imbi12d ⊢ ( 𝑥 = ( 𝑃 / 𝑧 ) → ( ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ↔ ( 𝑃 ∥ ( ( 𝑃 / 𝑧 ) · 𝑦 ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑦 ) ) ) )
36 oveq2 ⊢ ( 𝑦 = 𝑧 → ( ( 𝑃 / 𝑧 ) · 𝑦 ) = ( ( 𝑃 / 𝑧 ) · 𝑧 ) )
37 36 breq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑃 ∥ ( ( 𝑃 / 𝑧 ) · 𝑦 ) ↔ 𝑃 ∥ ( ( 𝑃 / 𝑧 ) · 𝑧 ) ) )
38 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑃 ∥ 𝑦 ↔ 𝑃 ∥ 𝑧 ) )
39 38 orbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑦 ) ↔ ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑧 ) ) )
40 37 39 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑃 ∥ ( ( 𝑃 / 𝑧 ) · 𝑦 ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑦 ) ) ↔ ( 𝑃 ∥ ( ( 𝑃 / 𝑧 ) · 𝑧 ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑧 ) ) ) )
41 35 40 rspc2va ⊢ ( ( ( ( 𝑃 / 𝑧 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) → ( 𝑃 ∥ ( ( 𝑃 / 𝑧 ) · 𝑧 ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑧 ) ) )
42 30 41 sylan ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) → ( 𝑃 ∥ ( ( 𝑃 / 𝑧 ) · 𝑧 ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑧 ) ) )
43 21 42 mpd ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑧 ) )
44 dvdsle ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑃 / 𝑧 ) ∈ ℕ ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) → 𝑃 ≤ ( 𝑃 / 𝑧 ) ) )
45 10 26 44 syl2anc ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) → 𝑃 ≤ ( 𝑃 / 𝑧 ) ) )
46 14 div1d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑃 / 1 ) = 𝑃 )
47 46 breq1d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( ( 𝑃 / 1 ) ≤ ( 𝑃 / 𝑧 ) ↔ 𝑃 ≤ ( 𝑃 / 𝑧 ) ) )
48 45 47 sylibrd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) → ( 𝑃 / 1 ) ≤ ( 𝑃 / 𝑧 ) ) )
49 nnrp ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℝ+ )
50 49 rpregt0d ⊢ ( 𝑧 ∈ ℕ → ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) )
51 50 ad2antrl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) )
52 1rp ⊢ 1 ∈ ℝ+
53 rpregt0 ⊢ ( 1 ∈ ℝ+ → ( 1 ∈ ℝ ∧ 0 < 1 ) )
54 52 53 mp1i ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 1 ∈ ℝ ∧ 0 < 1 ) )
55 nnrp ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ+ )
56 9 55 syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑃 ∈ ℝ+ )
57 56 rpregt0d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) )
58 lediv2 ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) ∧ ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) ) → ( 𝑧 ≤ 1 ↔ ( 𝑃 / 1 ) ≤ ( 𝑃 / 𝑧 ) ) )
59 51 54 57 58 syl3anc ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑧 ≤ 1 ↔ ( 𝑃 / 1 ) ≤ ( 𝑃 / 𝑧 ) ) )
60 48 59 sylibrd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) → 𝑧 ≤ 1 ) )
61 nnle1eq1 ⊢ ( 𝑧 ∈ ℕ → ( 𝑧 ≤ 1 ↔ 𝑧 = 1 ) )
62 61 ad2antrl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑧 ≤ 1 ↔ 𝑧 = 1 ) )
63 60 62 sylibd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑃 ∥ ( 𝑃 / 𝑧 ) → 𝑧 = 1 ) )
64 nnnn0 ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℕ0 )
65 64 ad2antrl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑧 ∈ ℕ0 )
66 65 adantr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) ∧ 𝑃 ∥ 𝑧 ) → 𝑧 ∈ ℕ0 )
67 nnnn0 ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
68 9 67 syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → 𝑃 ∈ ℕ0 )
69 68 adantr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) ∧ 𝑃 ∥ 𝑧 ) → 𝑃 ∈ ℕ0 )
70 simplrr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) ∧ 𝑃 ∥ 𝑧 ) → 𝑧 ∥ 𝑃 )
71 simpr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) ∧ 𝑃 ∥ 𝑧 ) → 𝑃 ∥ 𝑧 )
72 dvdseq ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑃 ∈ ℕ0 ) ∧ ( 𝑧 ∥ 𝑃 ∧ 𝑃 ∥ 𝑧 ) ) → 𝑧 = 𝑃 )
73 66 69 70 71 72 syl22anc ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) ∧ 𝑃 ∥ 𝑧 ) → 𝑧 = 𝑃 )
74 73 ex ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑃 ∥ 𝑧 → 𝑧 = 𝑃 ) )
75 63 74 orim12d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑧 ) → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) )
76 75 imp ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) ∧ ( 𝑃 ∥ ( 𝑃 / 𝑧 ) ∨ 𝑃 ∥ 𝑧 ) ) → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) )
77 43 76 syldan ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) )
78 77 an32s ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) ∧ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) ) → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) )
79 78 expr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) ∧ 𝑧 ∈ ℕ ) → ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) )
80 79 ralrimiva ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) → ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) )
81 isprm2 ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
82 7 80 81 sylanbrc ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) → 𝑃 ∈ ℙ )
83 6 82 impbii ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) )