Theorem 127prm

Description: 127 is a prime number. (Contributed by AV, 16-Aug-2021) (Proof shortened by AV, 16-Sep-2021)

	Ref	Expression
Assertion	127prm	$$⊢127\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢12\in {\mathbb{N}}_0$$
4		7nn	$$⊢7\in \mathbb{N}$$
5	3 4	decnncl	$$⊢127\in \mathbb{N}$$
6		8nn0	$$⊢8\in {\mathbb{N}}_0$$
7		4nn0	$$⊢4\in {\mathbb{N}}_0$$
8		7nn0	$$⊢7\in {\mathbb{N}}_0$$
9		1lt8	$$⊢1<8$$
10		2lt10	$$⊢2<10$$
11		7lt10	$$⊢7<10$$
12	1 6 2 7 8 1 9 10 11	3decltc	$$⊢127<841$$
13		2nn	$$⊢2\in \mathbb{N}$$
14	1 13	decnncl	$$⊢12\in \mathbb{N}$$
15		1lt10	$$⊢1<10$$
16	14 8 1 15	declti	$$⊢1<127$$
17		3nn0	$$⊢3\in {\mathbb{N}}_0$$
18		3t2e6	$$⊢3\cdot 2=6$$
19		df-7	$$⊢7=6+1$$
20	3 17 18 19	dec2dvds	$$⊢\neg 2\parallel 127$$
21		3nn	$$⊢3\in \mathbb{N}$$
22		1nn	$$⊢1\in \mathbb{N}$$
23		3t3e9	$$⊢3\cdot 3=9$$
24	23	oveq1i	$$⊢3\cdot 3+1=9+1$$
25		9p1e10	$$⊢9+1=10$$
26	24 25	eqtri	$$⊢3\cdot 3+1=10$$
27		1lt3	$$⊢1<3$$
28	21 17 22 26 27	ndvdsi	$$⊢\neg 3\parallel 10$$
29	1 2 8	3dvds2dec	$$⊢3\parallel 127\leftrightarrow 3\parallel \left(1+2+7\right)$$
30		1p2e3	$$⊢1+2=3$$
31	30	oveq1i	$$⊢1+2+7=3+7$$
32		7cn	$$⊢7\in ℂ$$
33		3cn	$$⊢3\in ℂ$$
34		7p3e10	$$⊢7+3=10$$
35	32 33 34	addcomli	$$⊢3+7=10$$
36	31 35	eqtri	$$⊢1+2+7=10$$
37	36	breq2i	$$⊢3\parallel \left(1+2+7\right)\leftrightarrow 3\parallel 10$$
38	29 37	bitri	$$⊢3\parallel 127\leftrightarrow 3\parallel 10$$
39	28 38	mtbir	$$⊢\neg 3\parallel 127$$
40		2lt5	$$⊢2<5$$
41		5p2e7	$$⊢5+2=7$$
42	3 13 40 41	dec5dvds2	$$⊢\neg 5\parallel 127$$
43	1 6	deccl	$$⊢18\in {\mathbb{N}}_0$$
44		0nn0	$$⊢0\in {\mathbb{N}}_0$$
45		eqid	$$⊢18=18$$
46	1	dec0h	$$⊢1=01$$
47		5nn0	$$⊢5\in {\mathbb{N}}_0$$
48	32	mulridi	$$⊢7\cdot 1=7$$
49		5cn	$$⊢5\in ℂ$$
50	49	addlidi	$$⊢0+5=5$$
51	48 50	oveq12i	$$⊢7\cdot 1+0+5=7+5$$
52		7p5e12	$$⊢7+5=12$$
53	51 52	eqtri	$$⊢7\cdot 1+0+5=12$$
54		6nn0	$$⊢6\in {\mathbb{N}}_0$$
55		8cn	$$⊢8\in ℂ$$
56		8t7e56	$$⊢8\cdot 7=56$$
57	55 32 56	mulcomli	$$⊢7\cdot 8=56$$
58		6p1e7	$$⊢6+1=7$$
59	47 54 1 57 58	decaddi	$$⊢7\cdot 8+1=57$$
60	1 6 44 1 45 46 8 8 47 53 59	decma2c	$$⊢7\cdot 18+1=127$$
61		1lt7	$$⊢1<7$$
62	4 43 22 60 61	ndvdsi	$$⊢\neg 7\parallel 127$$
63	1 22	decnncl	$$⊢11\in \mathbb{N}$$
64		11nn0	$$⊢11\in {\mathbb{N}}_0$$
65		6nn	$$⊢6\in \mathbb{N}$$
66		eqid	$$⊢11=11$$
67	54	dec0h	$$⊢6=06$$
68	64	nn0cni	$$⊢11\in ℂ$$
69	68	mulridi	$$⊢11\cdot 1=11$$
70		ax-1cn	$$⊢1\in ℂ$$
71	70	addlidi	$$⊢0+1=1$$
72	69 71	oveq12i	$$⊢11\cdot 1+0+1=11+1$$
73		1p1e2	$$⊢1+1=2$$
74	1 1 1 66 73	decaddi	$$⊢11+1=12$$
75	72 74	eqtri	$$⊢11\cdot 1+0+1=12$$
76		6cn	$$⊢6\in ℂ$$
77	76 70 58	addcomli	$$⊢1+6=7$$
78	1 1 54 69 77	decaddi	$$⊢11\cdot 1+6=17$$
79	1 1 44 54 66 67 64 8 1 75 78	decma2c	$$⊢11\cdot 11+6=127$$
80		6lt10	$$⊢6<10$$
81	22 1 54 80	declti	$$⊢6<11$$
82	63 64 65 79 81	ndvdsi	$$⊢\neg 11\parallel 127$$
83	1 21	decnncl	$$⊢13\in \mathbb{N}$$
84		9nn0	$$⊢9\in {\mathbb{N}}_0$$
85		10nn	$$⊢10\in \mathbb{N}$$
86		eqid	$$⊢13=13$$
87		eqid	$$⊢10=10$$
88		9cn	$$⊢9\in ℂ$$
89	88	mullidi	$$⊢1\cdot 9=9$$
90	89 30	oveq12i	$$⊢1\cdot 9+1+2=9+3$$
91		9p3e12	$$⊢9+3=12$$
92	90 91	eqtri	$$⊢1\cdot 9+1+2=12$$
93		9t3e27	$$⊢9\cdot 3=27$$
94	88 33 93	mulcomli	$$⊢3\cdot 9=27$$
95	32	addridi	$$⊢7+0=7$$
96	2 8 44 94 95	decaddi	$$⊢3\cdot 9+0=27$$
97	1 17 1 44 86 87 84 8 2 92 96	decmac	$$⊢13\cdot 9+10=127$$
98		3pos	$$⊢0<3$$
99	1 44 21 98	declt	$$⊢10<13$$
100	83 84 85 97 99	ndvdsi	$$⊢\neg 13\parallel 127$$
101	1 4	decnncl	$$⊢17\in \mathbb{N}$$
102		8nn	$$⊢8\in \mathbb{N}$$
103		eqid	$$⊢17=17$$
104	32	mullidi	$$⊢1\cdot 7=7$$
105	104	oveq1i	$$⊢1\cdot 7+5=7+5$$
106	105 52	eqtri	$$⊢1\cdot 7+5=12$$
107		7t7e49	$$⊢7\cdot 7=49$$
108		4p1e5	$$⊢4+1=5$$
109		9p8e17	$$⊢9+8=17$$
110	7 84 6 107 108 8 109	decaddci	$$⊢7\cdot 7+8=57$$
111	1 8 6 103 8 8 47 106 110	decrmac	$$⊢17\cdot 7+8=127$$
112		8lt10	$$⊢8<10$$
113	22 8 6 112	declti	$$⊢8<17$$
114	101 8 102 111 113	ndvdsi	$$⊢\neg 17\parallel 127$$
115		9nn	$$⊢9\in \mathbb{N}$$
116	1 115	decnncl	$$⊢19\in \mathbb{N}$$
117		eqid	$$⊢19=19$$
118	76	mullidi	$$⊢1\cdot 6=6$$
119		5p1e6	$$⊢5+1=6$$
120	49 70 119	addcomli	$$⊢1+5=6$$
121	118 120	oveq12i	$$⊢1\cdot 6+1+5=6+6$$
122		6p6e12	$$⊢6+6=12$$
123	121 122	eqtri	$$⊢1\cdot 6+1+5=12$$
124		9t6e54	$$⊢9\cdot 6=54$$
125		4p3e7	$$⊢4+3=7$$
126	47 7 17 124 125	decaddi	$$⊢9\cdot 6+3=57$$
127	1 84 1 17 117 86 54 8 47 123 126	decmac	$$⊢19\cdot 6+13=127$$
128		3lt9	$$⊢3<9$$
129	1 17 115 128	declt	$$⊢13<19$$
130	116 54 83 127 129	ndvdsi	$$⊢\neg 19\parallel 127$$
131	2 21	decnncl	$$⊢23\in \mathbb{N}$$
132		eqid	$$⊢23=23$$
133		eqid	$$⊢12=12$$
134		2cn	$$⊢2\in ℂ$$
135		5t2e10	$$⊢5\cdot 2=10$$
136	49 134 135	mulcomli	$$⊢2\cdot 5=10$$
137	136 73	oveq12i	$$⊢2\cdot 5+1+1=10+2$$
138		dec10p	$$⊢10+2=12$$
139	137 138	eqtri	$$⊢2\cdot 5+1+1=12$$
140		5t3e15	$$⊢5\cdot 3=15$$
141	49 33 140	mulcomli	$$⊢3\cdot 5=15$$
142	1 47 2 141 41	decaddi	$$⊢3\cdot 5+2=17$$
143	2 17 1 2 132 133 47 8 1 139 142	decmac	$$⊢23\cdot 5+12=127$$
144		1lt2	$$⊢1<2$$
145	1 2 2 17 10 144	decltc	$$⊢12<23$$
146	131 47 14 143 145	ndvdsi	$$⊢\neg 23\parallel 127$$
147	5 12 16 20 39 42 62 82 100 114 130 146	prmlem2	$$⊢127\in \mathbb{P}$$