Metamath Proof Explorer

Theorem fmtnodvds

Description: Any Fermat number divides a greater Fermat number minus 2. Corrolary of fmtnorec2 , see ProofWiki "Product of Sequence of Fermat Numbers plus 2/Corollary", 31-Jul-2021. (Contributed by AV, 1-Aug-2021)

Ref Expression
Assertion fmtnodvds 
|- ( ( N e. NN0 /\ M e. NN ) -> ( FermatNo ` N ) || ( ( FermatNo ` ( N + M ) ) - 2 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. NN0 /\ M e. NN ) -> N e. NN0 )
2 nn0nnaddcl 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( N + M ) e. NN )
3 nnm1nn0 
 |-  ( ( N + M ) e. NN -> ( ( N + M ) - 1 ) e. NN0 )
4 2 3 syl 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( ( N + M ) - 1 ) e. NN0 )
5 1red 
 |-  ( ( N e. NN0 /\ M e. NN ) -> 1 e. RR )
6 nnre 
 |-  ( M e. NN -> M e. RR )
7 6 adantl 
 |-  ( ( N e. NN0 /\ M e. NN ) -> M e. RR )
8 nn0re 
 |-  ( N e. NN0 -> N e. RR )
9 8 adantr 
 |-  ( ( N e. NN0 /\ M e. NN ) -> N e. RR )
10 nnge1 
 |-  ( M e. NN -> 1 <_ M )
11 10 adantl 
 |-  ( ( N e. NN0 /\ M e. NN ) -> 1 <_ M )
12 5 7 9 11 leadd2dd 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( N + 1 ) <_ ( N + M ) )
13 readdcl 
 |-  ( ( N e. RR /\ M e. RR ) -> ( N + M ) e. RR )
14 8 6 13 syl2an 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( N + M ) e. RR )
15 leaddsub 
 |-  ( ( N e. RR /\ 1 e. RR /\ ( N + M ) e. RR ) -> ( ( N + 1 ) <_ ( N + M ) <-> N <_ ( ( N + M ) - 1 ) ) )
16 9 5 14 15 syl3anc 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( ( N + 1 ) <_ ( N + M ) <-> N <_ ( ( N + M ) - 1 ) ) )
17 12 16 mpbid 
 |-  ( ( N e. NN0 /\ M e. NN ) -> N <_ ( ( N + M ) - 1 ) )
18 elfz2nn0 
 |-  ( N e. ( 0 ... ( ( N + M ) - 1 ) ) <-> ( N e. NN0 /\ ( ( N + M ) - 1 ) e. NN0 /\ N <_ ( ( N + M ) - 1 ) ) )
19 1 4 17 18 syl3anbrc 
 |-  ( ( N e. NN0 /\ M e. NN ) -> N e. ( 0 ... ( ( N + M ) - 1 ) ) )
20 fzfid 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( 0 ... ( ( N + M ) - 1 ) ) e. Fin )
21 fz0ssnn0 
 |-  ( 0 ... ( ( N + M ) - 1 ) ) C_ NN0
22 21 a1i 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( 0 ... ( ( N + M ) - 1 ) ) C_ NN0 )
23 2nn0 
 |-  2 e. NN0
24 23 a1i 
 |-  ( n e. NN0 -> 2 e. NN0 )
25 id 
 |-  ( n e. NN0 -> n e. NN0 )
26 24 25 nn0expcld 
 |-  ( n e. NN0 -> ( 2 ^ n ) e. NN0 )
27 24 26 nn0expcld 
 |-  ( n e. NN0 -> ( 2 ^ ( 2 ^ n ) ) e. NN0 )
28 27 nn0zd 
 |-  ( n e. NN0 -> ( 2 ^ ( 2 ^ n ) ) e. ZZ )
29 28 peano2zd 
 |-  ( n e. NN0 -> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) e. ZZ )
30 29 adantl 
 |-  ( ( ( N e. NN0 /\ M e. NN ) /\ n e. NN0 ) -> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) e. ZZ )
31 df-fmtno 
 |-  FermatNo = ( n e. NN0 |-> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
32 30 31 fmptd 
 |-  ( ( N e. NN0 /\ M e. NN ) -> FermatNo : NN0 --> ZZ )
33 20 22 32 fprodfvdvdsd 
 |-  ( ( N e. NN0 /\ M e. NN ) -> A. n e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` n ) || prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) )
34 fveq2 
 |-  ( n = N -> ( FermatNo ` n ) = ( FermatNo ` N ) )
35 34 breq1d 
 |-  ( n = N -> ( ( FermatNo ` n ) || prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) <-> ( FermatNo ` N ) || prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) ) )
36 35 rspcv 
 |-  ( N e. ( 0 ... ( ( N + M ) - 1 ) ) -> ( A. n e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` n ) || prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) -> ( FermatNo ` N ) || prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) ) )
37 19 33 36 sylc 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( FermatNo ` N ) || prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) )
38 elfznn0 
 |-  ( k e. ( 0 ... ( ( N + M ) - 1 ) ) -> k e. NN0 )
39 38 adantl 
 |-  ( ( ( N e. NN0 /\ M e. NN ) /\ k e. ( 0 ... ( ( N + M ) - 1 ) ) ) -> k e. NN0 )
40 fmtnonn 
 |-  ( k e. NN0 -> ( FermatNo ` k ) e. NN )
41 39 40 syl 
 |-  ( ( ( N e. NN0 /\ M e. NN ) /\ k e. ( 0 ... ( ( N + M ) - 1 ) ) ) -> ( FermatNo ` k ) e. NN )
42 41 nncnd 
 |-  ( ( ( N e. NN0 /\ M e. NN ) /\ k e. ( 0 ... ( ( N + M ) - 1 ) ) ) -> ( FermatNo ` k ) e. CC )
43 20 42 fprodcl 
 |-  ( ( N e. NN0 /\ M e. NN ) -> prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) e. CC )
44 2cnd 
 |-  ( ( N e. NN0 /\ M e. NN ) -> 2 e. CC )
45 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
46 nncn 
 |-  ( M e. NN -> M e. CC )
47 addcl 
 |-  ( ( N e. CC /\ M e. CC ) -> ( N + M ) e. CC )
48 45 46 47 syl2an 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( N + M ) e. CC )
49 npcan1 
 |-  ( ( N + M ) e. CC -> ( ( ( N + M ) - 1 ) + 1 ) = ( N + M ) )
50 48 49 syl 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( ( ( N + M ) - 1 ) + 1 ) = ( N + M ) )
51 50 eqcomd 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( N + M ) = ( ( ( N + M ) - 1 ) + 1 ) )
52 51 fveq2d 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( FermatNo ` ( N + M ) ) = ( FermatNo ` ( ( ( N + M ) - 1 ) + 1 ) ) )
53 fmtnorec2 
 |-  ( ( ( N + M ) - 1 ) e. NN0 -> ( FermatNo ` ( ( ( N + M ) - 1 ) + 1 ) ) = ( prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) + 2 ) )
54 4 53 syl 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( FermatNo ` ( ( ( N + M ) - 1 ) + 1 ) ) = ( prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) + 2 ) )
55 52 54 eqtrd 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( FermatNo ` ( N + M ) ) = ( prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) + 2 ) )
56 43 44 55 mvrraddd 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( ( FermatNo ` ( N + M ) ) - 2 ) = prod_ k e. ( 0 ... ( ( N + M ) - 1 ) ) ( FermatNo ` k ) )
57 37 56 breqtrrd 
 |-  ( ( N e. NN0 /\ M e. NN ) -> ( FermatNo ` N ) || ( ( FermatNo ` ( N + M ) ) - 2 ) )