Metamath Proof Explorer

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 
|- ; ; 1 2 7 e. Prime

Proof

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