Metamath Proof Explorer

Theorem fmtno5nprm

Description: The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021)

Ref Expression
Assertion fmtno5nprm 
|- ( FermatNo ` 5 ) e/ Prime

Proof

Step Hyp Ref Expression
1 6nn0 
 |-  6 e. NN0
2 7nn0 
 |-  7 e. NN0
3 1 2 deccl 
 |-  ; 6 7 e. NN0
4 0nn0 
 |-  0 e. NN0
5 3 4 deccl 
 |-  ; ; 6 7 0 e. NN0
6 5 4 deccl 
 |-  ; ; ; 6 7 0 0 e. NN0
7 4nn0 
 |-  4 e. NN0
8 6 7 deccl 
 |-  ; ; ; ; 6 7 0 0 4 e. NN0
9 1nn0 
 |-  1 e. NN0
10 8 9 deccl 
 |-  ; ; ; ; ; 6 7 0 0 4 1 e. NN0
11 7nn 
 |-  7 e. NN
12 10 11 decnncl 
 |-  ; ; ; ; ; ; 6 7 0 0 4 1 7 e. NN
13 1 7 deccl 
 |-  ; 6 4 e. NN0
14 1nn 
 |-  1 e. NN
15 13 14 decnncl 
 |-  ; ; 6 4 1 e. NN
16 8 14 decnncl 
 |-  ; ; ; ; ; 6 7 0 0 4 1 e. NN
17 1lt10 
 |-  1 < ; 1 0
18 16 2 9 17 declti 
 |-  1 < ; ; ; ; ; ; 6 7 0 0 4 1 7
19 4nn 
 |-  4 e. NN
20 1 19 decnncl 
 |-  ; 6 4 e. NN
21 20 9 9 17 declti 
 |-  1 < ; ; 6 4 1
22 fmtno5fac 
 |-  ( FermatNo ` 5 ) = ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. ; ; 6 4 1 )
23 22 eqcomi 
 |-  ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. ; ; 6 4 1 ) = ( FermatNo ` 5 )
24 12 15 18 21 23 nprmi 
 |-  -. ( FermatNo ` 5 ) e. Prime
25 24 nelir 
 |-  ( FermatNo ` 5 ) e/ Prime