Theorem 2503prm

Description: 2503 is a prime number. (Contributed by Mario Carneiro, 3-Mar-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

	Ref	Expression
Hypothesis	2503prm.1	|- N = ; ; ; 2 5 0 3
Assertion	2503prm	|- N e. Prime

Proof

Step	Hyp	Ref	Expression
1		2503prm.1	|- N = ; ; ; 2 5 0 3
2		139prm	|- ; ; 1 3 9 e. Prime
3		1nn0	|- 1 e. NN0
4		8nn	|- 8 e. NN
5	3 4	decnncl	|- ; 1 8 e. NN
6		2nn0	|- 2 e. NN0
7		5nn0	|- 5 e. NN0
8	6 7	deccl	|- ; 2 5 e. NN0
9		0nn0	|- 0 e. NN0
10	8 9	deccl	|- ; ; 2 5 0 e. NN0
11		2p1e3	|- ( 2 + 1 ) = 3
12		eqid	|- ; ; ; 2 5 0 2 = ; ; ; 2 5 0 2
13	10 6 11 12	decsuc	|- ( ; ; ; 2 5 0 2 + 1 ) = ; ; ; 2 5 0 3
14	1 13	eqtr4i	|- N = ( ; ; ; 2 5 0 2 + 1 )
15	14	oveq1i	|- ( N - 1 ) = ( ( ; ; ; 2 5 0 2 + 1 ) - 1 )
16		8nn0	|- 8 e. NN0
17	3 16	deccl	|- ; 1 8 e. NN0
18		3nn0	|- 3 e. NN0
19	3 18	deccl	|- ; 1 3 e. NN0
20		9nn0	|- 9 e. NN0
21		eqid	|- ; ; 1 3 9 = ; ; 1 3 9
22		6nn0	|- 6 e. NN0
23	3 22	deccl	|- ; 1 6 e. NN0
24		eqid	|- ; 1 3 = ; 1 3
25		eqid	|- ; 1 6 = ; 1 6
26		7nn0	|- 7 e. NN0
27		eqid	|- ; 1 8 = ; 1 8
28		6cn	|- 6 e. CC
29		ax-1cn	|- 1 e. CC
30		6p1e7	|- ( 6 + 1 ) = 7
31	28 29 30	addcomli	|- ( 1 + 6 ) = 7
32	26	dec0h	|- 7 = ; 0 7
33	31 32	eqtri	|- ( 1 + 6 ) = ; 0 7
34	29	mulid1i	|- ( 1 x. 1 ) = 1
35	29	addid2i	|- ( 0 + 1 ) = 1
36	34 35	oveq12i	|- ( ( 1 x. 1 ) + ( 0 + 1 ) ) = ( 1 + 1 )
37		1p1e2	|- ( 1 + 1 ) = 2
38	36 37	eqtri	|- ( ( 1 x. 1 ) + ( 0 + 1 ) ) = 2
39		8cn	|- 8 e. CC
40	39	mulid1i	|- ( 8 x. 1 ) = 8
41	40	oveq1i	|- ( ( 8 x. 1 ) + 7 ) = ( 8 + 7 )
42		8p7e15	|- ( 8 + 7 ) = ; 1 5
43	41 42	eqtri	|- ( ( 8 x. 1 ) + 7 ) = ; 1 5
44	3 16 9 26 27 33 3 7 3 38 43	decmac	|- ( ( ; 1 8 x. 1 ) + ( 1 + 6 ) ) = ; 2 5
45	22	dec0h	|- 6 = ; 0 6
46		3cn	|- 3 e. CC
47	46	mulid2i	|- ( 1 x. 3 ) = 3
48	46	addid2i	|- ( 0 + 3 ) = 3
49	47 48	oveq12i	|- ( ( 1 x. 3 ) + ( 0 + 3 ) ) = ( 3 + 3 )
50		3p3e6	|- ( 3 + 3 ) = 6
51	49 50	eqtri	|- ( ( 1 x. 3 ) + ( 0 + 3 ) ) = 6
52		4nn0	|- 4 e. NN0
53		8t3e24	|- ( 8 x. 3 ) = ; 2 4
54		4cn	|- 4 e. CC
55		6p4e10	|- ( 6 + 4 ) = ; 1 0
56	28 54 55	addcomli	|- ( 4 + 6 ) = ; 1 0
57	6 52 22 53 11 56	decaddci2	|- ( ( 8 x. 3 ) + 6 ) = ; 3 0
58	3 16 9 22 27 45 18 9 18 51 57	decmac	|- ( ( ; 1 8 x. 3 ) + 6 ) = ; 6 0
59	3 18 3 22 24 25 17 9 22 44 58	decma2c	|- ( ( ; 1 8 x. ; 1 3 ) + ; 1 6 ) = ; ; 2 5 0
60		9cn	|- 9 e. CC
61	60	mulid2i	|- ( 1 x. 9 ) = 9
62	61	oveq1i	|- ( ( 1 x. 9 ) + 7 ) = ( 9 + 7 )
63		9p7e16	|- ( 9 + 7 ) = ; 1 6
64	62 63	eqtri	|- ( ( 1 x. 9 ) + 7 ) = ; 1 6
65		9t8e72	|- ( 9 x. 8 ) = ; 7 2
66	60 39 65	mulcomli	|- ( 8 x. 9 ) = ; 7 2
67	20 3 16 27 6 26 64 66	decmul1c	|- ( ; 1 8 x. 9 ) = ; ; 1 6 2
68	17 19 20 21 6 23 59 67	decmul2c	|- ( ; 1 8 x. ; ; 1 3 9 ) = ; ; ; 2 5 0 2
69	10 6	deccl	|- ; ; ; 2 5 0 2 e. NN0
70	69	nn0cni	|- ; ; ; 2 5 0 2 e. CC
71	70 29	pncan3oi	|- ( ( ; ; ; 2 5 0 2 + 1 ) - 1 ) = ; ; ; 2 5 0 2
72	68 71	eqtr4i	|- ( ; 1 8 x. ; ; 1 3 9 ) = ( ( ; ; ; 2 5 0 2 + 1 ) - 1 )
73	15 72	eqtr4i	|- ( N - 1 ) = ( ; 1 8 x. ; ; 1 3 9 )
74	10 18	deccl	|- ; ; ; 2 5 0 3 e. NN0
75	1 74	eqeltri	|- N e. NN0
76	75	nn0cni	|- N e. CC
77		npcan	|- ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
78	76 29 77	mp2an	|- ( ( N - 1 ) + 1 ) = N
79	78	eqcomi	|- N = ( ( N - 1 ) + 1 )
80		1nn	|- 1 e. NN
81		2nn	|- 2 e. NN
82	19 20	deccl	|- ; ; 1 3 9 e. NN0
83	82	numexp1	|- ( ; ; 1 3 9 ^ 1 ) = ; ; 1 3 9
84	83	oveq2i	|- ( ; 1 8 x. ( ; ; 1 3 9 ^ 1 ) ) = ( ; 1 8 x. ; ; 1 3 9 )
85	73 84	eqtr4i	|- ( N - 1 ) = ( ; 1 8 x. ( ; ; 1 3 9 ^ 1 ) )
86		8lt10	|- 8 < ; 1 0
87		1lt10	|- 1 < ; 1 0
88	80 18 3 87	declti	|- 1 < ; 1 3
89	3 19 16 20 86 88	decltc	|- ; 1 8 < ; ; 1 3 9
90	89 83	breqtrri	|- ; 1 8 < ( ; ; 1 3 9 ^ 1 )
91	1	2503lem2	|- ( ( 2 ^ ( N - 1 ) ) mod N ) = ( 1 mod N )
92	1	2503lem3	|- ( ( ( 2 ^ ; 1 8 ) - 1 ) gcd N ) = 1
93	2 5 73 79 5 80 81 85 90 91 92	pockthi	|- N e. Prime