Metamath Proof Explorer


Theorem fmtnodvds

Description: Any Fermat number divides a greater Fermat number minus 2. Corollary 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 ) )