Metamath Proof Explorer

Theorem 43prm

Description: 43 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 43prm 
|- ; 4 3 e. Prime

Proof

Step Hyp Ref Expression
1 4nn0 
 |-  4 e. NN0
2 3nn 
 |-  3 e. NN
3 1 2 decnncl 
 |-  ; 4 3 e. NN
4 8nn0 
 |-  8 e. NN0
5 4 1 deccl 
 |-  ; 8 4 e. NN0
6 3nn0 
 |-  3 e. NN0
7 1nn0 
 |-  1 e. NN0
8 3lt10 
 |-  3 < ; 1 0
9 8nn 
 |-  8 e. NN
10 4lt10 
 |-  4 < ; 1 0
11 9 1 1 10 declti 
 |-  4 < ; 8 4
12 1 5 6 7 8 11 decltc 
 |-  ; 4 3 < ; ; 8 4 1
13 4nn 
 |-  4 e. NN
14 1lt10 
 |-  1 < ; 1 0
15 13 6 7 14 declti 
 |-  1 < ; 4 3
16 2cn 
 |-  2 e. CC
17 16 mulid2i 
 |-  ( 1 x. 2 ) = 2
18 df-3 
 |-  3 = ( 2 + 1 )
19 1 7 17 18 dec2dvds 
 |-  -. 2 || ; 4 3
20 7 1 deccl 
 |-  ; 1 4 e. NN0
21 1nn 
 |-  1 e. NN
22 0nn0 
 |-  0 e. NN0
23 eqid 
 |-  ; 1 4 = ; 1 4
24 7 dec0h 
 |-  1 = ; 0 1
25 3cn 
 |-  3 e. CC
26 25 mulid1i 
 |-  ( 3 x. 1 ) = 3
27 ax-1cn 
 |-  1 e. CC
28 27 addid2i 
 |-  ( 0 + 1 ) = 1
29 26 28 oveq12i 
 |-  ( ( 3 x. 1 ) + ( 0 + 1 ) ) = ( 3 + 1 )
30 3p1e4 
 |-  ( 3 + 1 ) = 4
31 29 30 eqtri 
 |-  ( ( 3 x. 1 ) + ( 0 + 1 ) ) = 4
32 2nn0 
 |-  2 e. NN0
33 2p1e3 
 |-  ( 2 + 1 ) = 3
34 4cn 
 |-  4 e. CC
35 4t3e12 
 |-  ( 4 x. 3 ) = ; 1 2
36 34 25 35 mulcomli 
 |-  ( 3 x. 4 ) = ; 1 2
37 7 32 33 36 decsuc 
 |-  ( ( 3 x. 4 ) + 1 ) = ; 1 3
38 7 1 22 7 23 24 6 6 7 31 37 decma2c 
 |-  ( ( 3 x. ; 1 4 ) + 1 ) = ; 4 3
39 1lt3 
 |-  1 < 3
40 2 20 21 38 39 ndvdsi 
 |-  -. 3 || ; 4 3
41 3lt5 
 |-  3 < 5
42 1 2 41 dec5dvds 
 |-  -. 5 || ; 4 3
43 7nn 
 |-  7 e. NN
44 6nn0 
 |-  6 e. NN0
45 7t6e42 
 |-  ( 7 x. 6 ) = ; 4 2
46 1 32 33 45 decsuc 
 |-  ( ( 7 x. 6 ) + 1 ) = ; 4 3
47 1lt7 
 |-  1 < 7
48 43 44 21 46 47 ndvdsi 
 |-  -. 7 || ; 4 3
49 7 21 decnncl 
 |-  ; 1 1 e. NN
50 21 decnncl2 
 |-  ; 1 0 e. NN
51 eqid 
 |-  ; 1 1 = ; 1 1
52 eqid 
 |-  ; 1 0 = ; 1 0
53 25 mulid2i 
 |-  ( 1 x. 3 ) = 3
54 27 addid1i 
 |-  ( 1 + 0 ) = 1
55 53 54 oveq12i 
 |-  ( ( 1 x. 3 ) + ( 1 + 0 ) ) = ( 3 + 1 )
56 55 30 eqtri 
 |-  ( ( 1 x. 3 ) + ( 1 + 0 ) ) = 4
57 53 oveq1i 
 |-  ( ( 1 x. 3 ) + 0 ) = ( 3 + 0 )
58 25 addid1i 
 |-  ( 3 + 0 ) = 3
59 6 dec0h 
 |-  3 = ; 0 3
60 57 58 59 3eqtri 
 |-  ( ( 1 x. 3 ) + 0 ) = ; 0 3
61 7 7 7 22 51 52 6 6 22 56 60 decmac 
 |-  ( ( ; 1 1 x. 3 ) + ; 1 0 ) = ; 4 3
62 0lt1 
 |-  0 < 1
63 7 22 21 62 declt 
 |-  ; 1 0 < ; 1 1
64 49 6 50 61 63 ndvdsi 
 |-  -. ; 1 1 || ; 4 3
65 7 2 decnncl 
 |-  ; 1 3 e. NN
66 eqid 
 |-  ; 1 3 = ; 1 3
67 1 dec0h 
 |-  4 = ; 0 4
68 53 28 oveq12i 
 |-  ( ( 1 x. 3 ) + ( 0 + 1 ) ) = ( 3 + 1 )
69 68 30 eqtri 
 |-  ( ( 1 x. 3 ) + ( 0 + 1 ) ) = 4
70 3t3e9 
 |-  ( 3 x. 3 ) = 9
71 70 oveq1i 
 |-  ( ( 3 x. 3 ) + 4 ) = ( 9 + 4 )
72 9p4e13 
 |-  ( 9 + 4 ) = ; 1 3
73 71 72 eqtri 
 |-  ( ( 3 x. 3 ) + 4 ) = ; 1 3
74 7 6 22 1 66 67 6 6 7 69 73 decmac 
 |-  ( ( ; 1 3 x. 3 ) + 4 ) = ; 4 3
75 21 6 1 10 declti 
 |-  4 < ; 1 3
76 65 6 13 74 75 ndvdsi 
 |-  -. ; 1 3 || ; 4 3
77 7 43 decnncl 
 |-  ; 1 7 e. NN
78 9nn 
 |-  9 e. NN
79 43 nnnn0i 
 |-  7 e. NN0
80 78 nnnn0i 
 |-  9 e. NN0
81 eqid 
 |-  ; 1 7 = ; 1 7
82 80 dec0h 
 |-  9 = ; 0 9
83 16 addid2i 
 |-  ( 0 + 2 ) = 2
84 17 83 oveq12i 
 |-  ( ( 1 x. 2 ) + ( 0 + 2 ) ) = ( 2 + 2 )
85 2p2e4 
 |-  ( 2 + 2 ) = 4
86 84 85 eqtri 
 |-  ( ( 1 x. 2 ) + ( 0 + 2 ) ) = 4
87 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
88 1p1e2 
 |-  ( 1 + 1 ) = 2
89 78 nncni 
 |-  9 e. CC
90 89 34 72 addcomli 
 |-  ( 4 + 9 ) = ; 1 3
91 7 1 80 87 88 6 90 decaddci 
 |-  ( ( 7 x. 2 ) + 9 ) = ; 2 3
92 7 79 22 80 81 82 32 6 32 86 91 decmac 
 |-  ( ( ; 1 7 x. 2 ) + 9 ) = ; 4 3
93 9lt10 
 |-  9 < ; 1 0
94 21 79 80 93 declti 
 |-  9 < ; 1 7
95 77 32 78 92 94 ndvdsi 
 |-  -. ; 1 7 || ; 4 3
96 7 78 decnncl 
 |-  ; 1 9 e. NN
97 5nn 
 |-  5 e. NN
98 97 nnnn0i 
 |-  5 e. NN0
99 eqid 
 |-  ; 1 9 = ; 1 9
100 98 dec0h 
 |-  5 = ; 0 5
101 9t2e18 
 |-  ( 9 x. 2 ) = ; 1 8
102 8p5e13 
 |-  ( 8 + 5 ) = ; 1 3
103 7 4 98 101 88 6 102 decaddci 
 |-  ( ( 9 x. 2 ) + 5 ) = ; 2 3
104 7 80 22 98 99 100 32 6 32 86 103 decmac 
 |-  ( ( ; 1 9 x. 2 ) + 5 ) = ; 4 3
105 5lt10 
 |-  5 < ; 1 0
106 21 80 98 105 declti 
 |-  5 < ; 1 9
107 96 32 97 104 106 ndvdsi 
 |-  -. ; 1 9 || ; 4 3
108 32 2 decnncl 
 |-  ; 2 3 e. NN
109 2nn 
 |-  2 e. NN
110 109 decnncl2 
 |-  ; 2 0 e. NN
111 108 nncni 
 |-  ; 2 3 e. CC
112 111 mulid1i 
 |-  ( ; 2 3 x. 1 ) = ; 2 3
113 eqid 
 |-  ; 2 0 = ; 2 0
114 32 6 32 22 112 113 85 58 decadd 
 |-  ( ( ; 2 3 x. 1 ) + ; 2 0 ) = ; 4 3
115 3pos 
 |-  0 < 3
116 32 22 2 115 declt 
 |-  ; 2 0 < ; 2 3
117 108 7 110 114 116 ndvdsi 
 |-  -. ; 2 3 || ; 4 3
118 3 12 15 19 40 42 48 64 76 95 107 117 prmlem2 
 |-  ; 4 3 e. Prime