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 PP2xyPxyPxPy

Proof

Step Hyp Ref Expression
1 prmuz2 PP2
2 euclemma PxyPxyPxPy
3 2 3expb PxyPxyPxPy
4 3 biimpd PxyPxyPxPy
5 4 ralrimivva PxyPxyPxPy
6 1 5 jca PP2xyPxyPxPy
7 simpl P2xyPxyPxPyP2
8 eluz2nn P2P
9 8 adantr P2zzPP
10 9 nnzd P2zzPP
11 iddvds PPP
12 10 11 syl P2zzPPP
13 nncn PP
14 9 13 syl P2zzPP
15 nncn zz
16 15 ad2antrl P2zzPz
17 nnne0 zz0
18 17 ad2antrl P2zzPz0
19 14 16 18 divcan1d P2zzPPzz=P
20 12 19 breqtrrd P2zzPPPzz
21 20 adantr P2zzPxyPxyPxPyPPzz
22 simprr P2zzPzP
23 simprl P2zzPz
24 nndivdvds PzzPPz
25 9 23 24 syl2anc P2zzPzPPz
26 22 25 mpbid P2zzPPz
27 26 nnzd P2zzPPz
28 nnz zz
29 28 ad2antrl P2zzPz
30 27 29 jca P2zzPPzz
31 oveq1 x=Pzxy=Pzy
32 31 breq2d x=PzPxyPPzy
33 breq2 x=PzPxPPz
34 33 orbi1d x=PzPxPyPPzPy
35 32 34 imbi12d x=PzPxyPxPyPPzyPPzPy
36 oveq2 y=zPzy=Pzz
37 36 breq2d y=zPPzyPPzz
38 breq2 y=zPyPz
39 38 orbi2d y=zPPzPyPPzPz
40 37 39 imbi12d y=zPPzyPPzPyPPzzPPzPz
41 35 40 rspc2va PzzxyPxyPxPyPPzzPPzPz
42 30 41 sylan P2zzPxyPxyPxPyPPzzPPzPz
43 21 42 mpd P2zzPxyPxyPxPyPPzPz
44 dvdsle PPzPPzPPz
45 10 26 44 syl2anc P2zzPPPzPPz
46 14 div1d P2zzPP1=P
47 46 breq1d P2zzPP1PzPPz
48 45 47 sylibrd P2zzPPPzP1Pz
49 nnrp zz+
50 49 rpregt0d zz0<z
51 50 ad2antrl P2zzPz0<z
52 1rp 1+
53 rpregt0 1+10<1
54 52 53 mp1i P2zzP10<1
55 nnrp PP+
56 9 55 syl P2zzPP+
57 56 rpregt0d P2zzPP0<P
58 lediv2 z0<z10<1P0<Pz1P1Pz
59 51 54 57 58 syl3anc P2zzPz1P1Pz
60 48 59 sylibrd P2zzPPPzz1
61 nnle1eq1 zz1z=1
62 61 ad2antrl P2zzPz1z=1
63 60 62 sylibd P2zzPPPzz=1
64 nnnn0 zz0
65 64 ad2antrl P2zzPz0
66 65 adantr P2zzPPzz0
67 nnnn0 PP0
68 9 67 syl P2zzPP0
69 68 adantr P2zzPPzP0
70 simplrr P2zzPPzzP
71 simpr P2zzPPzPz
72 dvdseq z0P0zPPzz=P
73 66 69 70 71 72 syl22anc P2zzPPzz=P
74 73 ex P2zzPPzz=P
75 63 74 orim12d P2zzPPPzPzz=1z=P
76 75 imp P2zzPPPzPzz=1z=P
77 43 76 syldan P2zzPxyPxyPxPyz=1z=P
78 77 an32s P2xyPxyPxPyzzPz=1z=P
79 78 expr P2xyPxyPxPyzzPz=1z=P
80 79 ralrimiva P2xyPxyPxPyzzPz=1z=P
81 isprm2 PP2zzPz=1z=P
82 7 80 81 sylanbrc P2xyPxyPxPyP
83 6 82 impbii PP2xyPxyPxPy