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 
|- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( ( 2 ... ( |_ ` ( sqrt ` P ) ) ) i^i Prime ) -. z || P ) )

Proof

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