Metamath Proof Explorer

Theorem isprm7

Description: One need only check prime divisors of P up to sqrt P in order to ensure primality. This version of isprm5 combines the primality and bound on z into a finite interval of prime numbers. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion isprm7 ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) ¬ 𝑧 ∥ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 isprm5 ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℙ ( ( 𝑧 ↑ 2 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
2 prmz ⊢ ( 𝑧 ∈ ℙ → 𝑧 ∈ ℤ )
3 2 zred ⊢ ( 𝑧 ∈ ℙ → 𝑧 ∈ ℝ )
4 0red ⊢ ( 𝑧 ∈ ℙ → 0 ∈ ℝ )
5 1red ⊢ ( 𝑧 ∈ ℙ → 1 ∈ ℝ )
6 0lt1 ⊢ 0 < 1
7 6 a1i ⊢ ( 𝑧 ∈ ℙ → 0 < 1 )
8 prmgt1 ⊢ ( 𝑧 ∈ ℙ → 1 < 𝑧 )
9 4 5 3 7 8 lttrd ⊢ ( 𝑧 ∈ ℙ → 0 < 𝑧 )
10 4 3 9 ltled ⊢ ( 𝑧 ∈ ℙ → 0 ≤ 𝑧 )
11 3 10 jca ⊢ ( 𝑧 ∈ ℙ → ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ) )
12 eluzelre ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℝ )
13 0red ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 0 ∈ ℝ )
14 2re ⊢ 2 ∈ ℝ
15 14 a1i ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℝ )
16 0le2 ⊢ 0 ≤ 2
17 16 a1i ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 2 )
18 eluzle ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑃 )
19 13 15 12 17 18 letrd ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 𝑃 )
20 12 19 jca ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 ∈ ℝ ∧ 0 ≤ 𝑃 ) )
21 resqcl ⊢ ( 𝑧 ∈ ℝ → ( 𝑧 ↑ 2 ) ∈ ℝ )
22 sqge0 ⊢ ( 𝑧 ∈ ℝ → 0 ≤ ( 𝑧 ↑ 2 ) )
23 21 22 jca ⊢ ( 𝑧 ∈ ℝ → ( ( 𝑧 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑧 ↑ 2 ) ) )
24 23 adantr ⊢ ( ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ) → ( ( 𝑧 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑧 ↑ 2 ) ) )
25 sqrtle ⊢ ( ( ( ( 𝑧 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑧 ↑ 2 ) ) ∧ ( 𝑃 ∈ ℝ ∧ 0 ≤ 𝑃 ) ) → ( ( 𝑧 ↑ 2 ) ≤ 𝑃 ↔ ( √ ‘ ( 𝑧 ↑ 2 ) ) ≤ ( √ ‘ 𝑃 ) ) )
26 24 25 sylan ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ) ∧ ( 𝑃 ∈ ℝ ∧ 0 ≤ 𝑃 ) ) → ( ( 𝑧 ↑ 2 ) ≤ 𝑃 ↔ ( √ ‘ ( 𝑧 ↑ 2 ) ) ≤ ( √ ‘ 𝑃 ) ) )
27 sqrtsq ⊢ ( ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ) → ( √ ‘ ( 𝑧 ↑ 2 ) ) = 𝑧 )
28 27 breq1d ⊢ ( ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ) → ( ( √ ‘ ( 𝑧 ↑ 2 ) ) ≤ ( √ ‘ 𝑃 ) ↔ 𝑧 ≤ ( √ ‘ 𝑃 ) ) )
29 28 adantr ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ) ∧ ( 𝑃 ∈ ℝ ∧ 0 ≤ 𝑃 ) ) → ( ( √ ‘ ( 𝑧 ↑ 2 ) ) ≤ ( √ ‘ 𝑃 ) ↔ 𝑧 ≤ ( √ ‘ 𝑃 ) ) )
30 26 29 bitrd ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ) ∧ ( 𝑃 ∈ ℝ ∧ 0 ≤ 𝑃 ) ) → ( ( 𝑧 ↑ 2 ) ≤ 𝑃 ↔ 𝑧 ≤ ( √ ‘ 𝑃 ) ) )
31 11 20 30 syl2anr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ℙ ) → ( ( 𝑧 ↑ 2 ) ≤ 𝑃 ↔ 𝑧 ≤ ( √ ‘ 𝑃 ) ) )
32 31 imbi1d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ℙ ) → ( ( ( 𝑧 ↑ 2 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ↔ ( 𝑧 ≤ ( √ ‘ 𝑃 ) → ¬ 𝑧 ∥ 𝑃 ) ) )
33 32 ralbidva ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑧 ∈ ℙ ( ( 𝑧 ↑ 2 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ↔ ∀ 𝑧 ∈ ℙ ( 𝑧 ≤ ( √ ‘ 𝑃 ) → ¬ 𝑧 ∥ 𝑃 ) ) )
34 33 pm5.32i ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℙ ( ( 𝑧 ↑ 2 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℙ ( 𝑧 ≤ ( √ ‘ 𝑃 ) → ¬ 𝑧 ∥ 𝑃 ) ) )
35 impexp ⊢ ( ( ( 𝑧 ∈ ℙ ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) → ¬ 𝑧 ∥ 𝑃 ) ↔ ( 𝑧 ∈ ℙ → ( 𝑧 ≤ ( √ ‘ 𝑃 ) → ¬ 𝑧 ∥ 𝑃 ) ) )
36 12 19 resqrtcld ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ 𝑃 ) ∈ ℝ )
37 36 flcld ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ∈ ℤ )
38 37 2 anim12i ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ℙ ) → ( ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) )
39 38 adantr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ℙ ) ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) → ( ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) )
40 prmuz2 ⊢ ( 𝑧 ∈ ℙ → 𝑧 ∈ ( ℤ≥ ‘ 2 ) )
41 eluzle ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑧 )
42 40 41 syl ⊢ ( 𝑧 ∈ ℙ → 2 ≤ 𝑧 )
43 42 ad2antlr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ℙ ) ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) → 2 ≤ 𝑧 )
44 flge ⊢ ( ( ( √ ‘ 𝑃 ) ∈ ℝ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ≤ ( √ ‘ 𝑃 ) ↔ 𝑧 ≤ ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) )
45 36 2 44 syl2an ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ℙ ) → ( 𝑧 ≤ ( √ ‘ 𝑃 ) ↔ 𝑧 ≤ ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) )
46 45 biimpa ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ℙ ) ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) → 𝑧 ≤ ( ⌊ ‘ ( √ ‘ 𝑃 ) ) )
47 2z ⊢ 2 ∈ ℤ
48 elfz4 ⊢ ( ( ( 2 ∈ ℤ ∧ ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) ∧ ( 2 ≤ 𝑧 ∧ 𝑧 ≤ ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ) → 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) )
49 47 48 mp3anl1 ⊢ ( ( ( ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) ∧ ( 2 ≤ 𝑧 ∧ 𝑧 ≤ ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ) → 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) )
50 39 43 46 49 syl12anc ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ℙ ) ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) → 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) )
51 50 anasss ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) ) → 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) )
52 simprl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) ) → 𝑧 ∈ ℙ )
53 51 52 elind ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) ) → 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) )
54 53 ex ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑧 ∈ ℙ ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) → 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) ) )
55 elin ⊢ ( 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) ↔ ( 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∧ 𝑧 ∈ ℙ ) )
56 elfzelz ⊢ ( 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) → 𝑧 ∈ ℤ )
57 56 zred ⊢ ( 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) → 𝑧 ∈ ℝ )
58 57 adantl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ) → 𝑧 ∈ ℝ )
59 reflcl ⊢ ( ( √ ‘ 𝑃 ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ∈ ℝ )
60 36 59 syl ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ∈ ℝ )
61 60 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ) → ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ∈ ℝ )
62 36 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ) → ( √ ‘ 𝑃 ) ∈ ℝ )
63 elfzle2 ⊢ ( 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) → 𝑧 ≤ ( ⌊ ‘ ( √ ‘ 𝑃 ) ) )
64 63 adantl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ) → 𝑧 ≤ ( ⌊ ‘ ( √ ‘ 𝑃 ) ) )
65 flle ⊢ ( ( √ ‘ 𝑃 ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ≤ ( √ ‘ 𝑃 ) )
66 36 65 syl ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ≤ ( √ ‘ 𝑃 ) )
67 66 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ) → ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ≤ ( √ ‘ 𝑃 ) )
68 58 61 62 64 67 letrd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ) → 𝑧 ≤ ( √ ‘ 𝑃 ) )
69 68 ex ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) → 𝑧 ≤ ( √ ‘ 𝑃 ) ) )
70 69 anim1d ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑧 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∧ 𝑧 ∈ ℙ ) → ( 𝑧 ≤ ( √ ‘ 𝑃 ) ∧ 𝑧 ∈ ℙ ) ) )
71 55 70 syl5bi ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) → ( 𝑧 ≤ ( √ ‘ 𝑃 ) ∧ 𝑧 ∈ ℙ ) ) )
72 ancom ⊢ ( ( 𝑧 ≤ ( √ ‘ 𝑃 ) ∧ 𝑧 ∈ ℙ ) ↔ ( 𝑧 ∈ ℙ ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) )
73 71 72 syl6ib ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) → ( 𝑧 ∈ ℙ ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) ) )
74 54 73 impbid ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑧 ∈ ℙ ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) ↔ 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) ) )
75 74 imbi1d ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝑧 ∈ ℙ ∧ 𝑧 ≤ ( √ ‘ 𝑃 ) ) → ¬ 𝑧 ∥ 𝑃 ) ↔ ( 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) → ¬ 𝑧 ∥ 𝑃 ) ) )
76 35 75 bitr3id ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑧 ∈ ℙ → ( 𝑧 ≤ ( √ ‘ 𝑃 ) → ¬ 𝑧 ∥ 𝑃 ) ) ↔ ( 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) → ¬ 𝑧 ∥ 𝑃 ) ) )
77 76 ralbidv2 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑧 ∈ ℙ ( 𝑧 ≤ ( √ ‘ 𝑃 ) → ¬ 𝑧 ∥ 𝑃 ) ↔ ∀ 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) ¬ 𝑧 ∥ 𝑃 ) )
78 77 pm5.32i ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℙ ( 𝑧 ≤ ( √ ‘ 𝑃 ) → ¬ 𝑧 ∥ 𝑃 ) ) ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) ¬ 𝑧 ∥ 𝑃 ) )
79 1 34 78 3bitri ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝑃 ) ) ) ∩ ℙ ) ¬ 𝑧 ∥ 𝑃 ) )