Metamath Proof Explorer

Theorem fmtno4prmfac193

Description: If P was a (prime) factor of the fourth Fermat number, it would be 193. (Contributed by AV, 28-Jul-2021)

Ref Expression
Assertion fmtno4prmfac193 
|- ( ( P e. Prime /\ P || ( FermatNo ` 4 ) /\ P <_ ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) -> P = ; ; 1 9 3 )

Proof

Step Hyp Ref Expression
1 fmtno4prmfac 
 |-  ( ( P e. Prime /\ P || ( FermatNo ` 4 ) /\ P <_ ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) -> ( P = ; 6 5 \/ P = ; ; 1 2 9 \/ P = ; ; 1 9 3 ) )
2 5nn 
 |-  5 e. NN
3 1nn0 
 |-  1 e. NN0
4 3nn 
 |-  3 e. NN
5 3 4 decnncl 
 |-  ; 1 3 e. NN
6 1lt5 
 |-  1 < 5
7 1nn 
 |-  1 e. NN
8 3nn0 
 |-  3 e. NN0
9 1lt10 
 |-  1 < ; 1 0
10 7 8 3 9 declti 
 |-  1 < ; 1 3
11 eqid 
 |-  ( 5 x. ; 1 3 ) = ( 5 x. ; 1 3 )
12 2 5 6 10 11 nprmi 
 |-  -. ( 5 x. ; 1 3 ) e. Prime
13 id 
 |-  ( P = ; 6 5 -> P = ; 6 5 )
14 5nn0 
 |-  5 e. NN0
15 eqid 
 |-  ; 1 3 = ; 1 3
16 5cn 
 |-  5 e. CC
17 16 mulid1i 
 |-  ( 5 x. 1 ) = 5
18 17 oveq1i 
 |-  ( ( 5 x. 1 ) + 1 ) = ( 5 + 1 )
19 5p1e6 
 |-  ( 5 + 1 ) = 6
20 18 19 eqtri 
 |-  ( ( 5 x. 1 ) + 1 ) = 6
21 5t3e15 
 |-  ( 5 x. 3 ) = ; 1 5
22 14 3 8 15 14 3 20 21 decmul2c 
 |-  ( 5 x. ; 1 3 ) = ; 6 5
23 13 22 eqtr4di 
 |-  ( P = ; 6 5 -> P = ( 5 x. ; 1 3 ) )
24 23 eleq1d 
 |-  ( P = ; 6 5 -> ( P e. Prime <-> ( 5 x. ; 1 3 ) e. Prime ) )
25 12 24 mtbiri 
 |-  ( P = ; 6 5 -> -. P e. Prime )
26 25 pm2.21d 
 |-  ( P = ; 6 5 -> ( P e. Prime -> P = ; ; 1 9 3 ) )
27 4nn0 
 |-  4 e. NN0
28 27 4 decnncl 
 |-  ; 4 3 e. NN
29 4nn 
 |-  4 e. NN
30 29 8 3 9 declti 
 |-  1 < ; 4 3
31 1lt3 
 |-  1 < 3
32 eqid 
 |-  ( ; 4 3 x. 3 ) = ( ; 4 3 x. 3 )
33 28 4 30 31 32 nprmi 
 |-  -. ( ; 4 3 x. 3 ) e. Prime
34 id 
 |-  ( P = ; ; 1 2 9 -> P = ; ; 1 2 9 )
35 eqid 
 |-  ; 4 3 = ; 4 3
36 4t3e12 
 |-  ( 4 x. 3 ) = ; 1 2
37 3t3e9 
 |-  ( 3 x. 3 ) = 9
38 8 27 8 35 36 37 decmul1 
 |-  ( ; 4 3 x. 3 ) = ; ; 1 2 9
39 34 38 eqtr4di 
 |-  ( P = ; ; 1 2 9 -> P = ( ; 4 3 x. 3 ) )
40 39 eleq1d 
 |-  ( P = ; ; 1 2 9 -> ( P e. Prime <-> ( ; 4 3 x. 3 ) e. Prime ) )
41 33 40 mtbiri 
 |-  ( P = ; ; 1 2 9 -> -. P e. Prime )
42 41 pm2.21d 
 |-  ( P = ; ; 1 2 9 -> ( P e. Prime -> P = ; ; 1 9 3 ) )
43 ax-1 
 |-  ( P = ; ; 1 9 3 -> ( P e. Prime -> P = ; ; 1 9 3 ) )
44 26 42 43 3jaoi 
 |-  ( ( P = ; 6 5 \/ P = ; ; 1 2 9 \/ P = ; ; 1 9 3 ) -> ( P e. Prime -> P = ; ; 1 9 3 ) )
45 44 com12 
 |-  ( P e. Prime -> ( ( P = ; 6 5 \/ P = ; ; 1 2 9 \/ P = ; ; 1 9 3 ) -> P = ; ; 1 9 3 ) )
46 45 3ad2ant1 
 |-  ( ( P e. Prime /\ P || ( FermatNo ` 4 ) /\ P <_ ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) -> ( ( P = ; 6 5 \/ P = ; ; 1 2 9 \/ P = ; ; 1 9 3 ) -> P = ; ; 1 9 3 ) )
47 1 46 mpd 
 |-  ( ( P e. Prime /\ P || ( FermatNo ` 4 ) /\ P <_ ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) -> P = ; ; 1 9 3 )