Metamath Proof Explorer

Theorem fmtno4prm

Description: The 4-th Fermat number (65537) is a prime (thefifth Fermat prime). (Contributed by AV, 28-Jul-2021)

Ref Expression
Assertion fmtno4prm 
|- ( FermatNo ` 4 ) e. Prime

Proof

Step Hyp Ref Expression
1 4nn0 
 |-  4 e. NN0
2 fmtno 
 |-  ( 4 e. NN0 -> ( FermatNo ` 4 ) = ( ( 2 ^ ( 2 ^ 4 ) ) + 1 ) )
3 1 2 ax-mp 
 |-  ( FermatNo ` 4 ) = ( ( 2 ^ ( 2 ^ 4 ) ) + 1 )
4 2nn 
 |-  2 e. NN
5 2nn0 
 |-  2 e. NN0
6 5 1 nn0expcli 
 |-  ( 2 ^ 4 ) e. NN0
7 nnexpcl 
 |-  ( ( 2 e. NN /\ ( 2 ^ 4 ) e. NN0 ) -> ( 2 ^ ( 2 ^ 4 ) ) e. NN )
8 4 6 7 mp2an 
 |-  ( 2 ^ ( 2 ^ 4 ) ) e. NN
9 2re 
 |-  2 e. RR
10 nnexpcl 
 |-  ( ( 2 e. NN /\ 4 e. NN0 ) -> ( 2 ^ 4 ) e. NN )
11 4 1 10 mp2an 
 |-  ( 2 ^ 4 ) e. NN
12 1lt2 
 |-  1 < 2
13 expgt1 
 |-  ( ( 2 e. RR /\ ( 2 ^ 4 ) e. NN /\ 1 < 2 ) -> 1 < ( 2 ^ ( 2 ^ 4 ) ) )
14 9 11 12 13 mp3an 
 |-  1 < ( 2 ^ ( 2 ^ 4 ) )
15 eluz2b2 
 |-  ( ( 2 ^ ( 2 ^ 4 ) ) e. ( ZZ>= ` 2 ) <-> ( ( 2 ^ ( 2 ^ 4 ) ) e. NN /\ 1 < ( 2 ^ ( 2 ^ 4 ) ) ) )
16 8 14 15 mpbir2an 
 |-  ( 2 ^ ( 2 ^ 4 ) ) e. ( ZZ>= ` 2 )
17 peano2uz 
 |-  ( ( 2 ^ ( 2 ^ 4 ) ) e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( 2 ^ 4 ) ) + 1 ) e. ( ZZ>= ` 2 ) )
18 16 17 ax-mp 
 |-  ( ( 2 ^ ( 2 ^ 4 ) ) + 1 ) e. ( ZZ>= ` 2 )
19 3 18 eqeltri 
 |-  ( FermatNo ` 4 ) e. ( ZZ>= ` 2 )
20 elinel2 
 |-  ( p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) -> p e. Prime )
21 20 adantr 
 |-  ( ( p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) /\ p || ( FermatNo ` 4 ) ) -> p e. Prime )
22 simpr 
 |-  ( ( p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) /\ p || ( FermatNo ` 4 ) ) -> p || ( FermatNo ` 4 ) )
23 elinel1 
 |-  ( p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) -> p e. ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) )
24 elfzle2 
 |-  ( p e. ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) -> p <_ ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) )
25 23 24 syl 
 |-  ( p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) -> p <_ ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) )
26 25 adantr 
 |-  ( ( p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) /\ p || ( FermatNo ` 4 ) ) -> p <_ ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) )
27 fmtno4prmfac193 
 |-  ( ( p e. Prime /\ p || ( FermatNo ` 4 ) /\ p <_ ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) -> p = ; ; 1 9 3 )
28 21 22 26 27 syl3anc 
 |-  ( ( p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) /\ p || ( FermatNo ` 4 ) ) -> p = ; ; 1 9 3 )
29 fmtno4nprmfac193 
 |-  -. ; ; 1 9 3 || ( FermatNo ` 4 )
30 breq1 
 |-  ( p = ; ; 1 9 3 -> ( p || ( FermatNo ` 4 ) <-> ; ; 1 9 3 || ( FermatNo ` 4 ) ) )
31 29 30 mtbiri 
 |-  ( p = ; ; 1 9 3 -> -. p || ( FermatNo ` 4 ) )
32 28 31 syl 
 |-  ( ( p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) /\ p || ( FermatNo ` 4 ) ) -> -. p || ( FermatNo ` 4 ) )
33 32 pm2.01da 
 |-  ( p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) -> -. p || ( FermatNo ` 4 ) )
34 33 rgen 
 |-  A. p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) -. p || ( FermatNo ` 4 )
35 isprm7 
 |-  ( ( FermatNo ` 4 ) e. Prime <-> ( ( FermatNo ` 4 ) e. ( ZZ>= ` 2 ) /\ A. p e. ( ( 2 ... ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) i^i Prime ) -. p || ( FermatNo ` 4 ) ) )
36 19 34 35 mpbir2an 
 |-  ( FermatNo ` 4 ) e. Prime