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 \in ℕ_{0} \land M \in ℕ) \to FermatNo (N) ∥ (FermatNo (N + M) - 2)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to N \in ℕ_{0}$
2		nn0nnaddcl	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to N + M \in ℕ$
3		nnm1nn0	$⊢ N + M \in ℕ \to N + M - 1 \in ℕ_{0}$
4	2 3	syl	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to N + M - 1 \in ℕ_{0}$
5		1red	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to 1 \in ℝ$
6		nnre	$⊢ M \in ℕ \to M \in ℝ$
7	6	adantl	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to M \in ℝ$
8		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
9	8	adantr	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to N \in ℝ$
10		nnge1	$⊢ M \in ℕ \to 1 \leq M$
11	10	adantl	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to 1 \leq M$
12	5 7 9 11	leadd2dd	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to N + 1 \leq N + M$
13		readdcl	$⊢ (N \in ℝ \land M \in ℝ) \to N + M \in ℝ$
14	8 6 13	syl2an	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to N + M \in ℝ$
15		leaddsub	$⊢ (N \in ℝ \land 1 \in ℝ \land N + M \in ℝ) \to (N + 1 \leq N + M \leftrightarrow N \leq N + M - 1)$
16	9 5 14 15	syl3anc	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to (N + 1 \leq N + M \leftrightarrow N \leq N + M - 1)$
17	12 16	mpbid	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to N \leq N + M - 1$
18		elfz2nn0	$⊢ N \in (0 \dots N + M - 1) \leftrightarrow (N \in ℕ_{0} \land N + M - 1 \in ℕ_{0} \land N \leq N + M - 1)$
19	1 4 17 18	syl3anbrc	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to N \in (0 \dots N + M - 1)$
20		fzfid	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to (0 \dots N + M - 1) \in Fin$
21		fz0ssnn0	$⊢ (0 \dots N + M - 1) \subseteq ℕ_{0}$
22	21	a1i	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to (0 \dots N + M - 1) \subseteq ℕ_{0}$
23		2nn0	$⊢ 2 \in ℕ_{0}$
24	23	a1i	$⊢ n \in ℕ_{0} \to 2 \in ℕ_{0}$
25		id	$⊢ n \in ℕ_{0} \to n \in ℕ_{0}$
26	24 25	nn0expcld	$⊢ n \in ℕ_{0} \to 2^{n} \in ℕ_{0}$
27	24 26	nn0expcld	$⊢ n \in ℕ_{0} \to 2^{2^{n}} \in ℕ_{0}$
28	27	nn0zd	$⊢ n \in ℕ_{0} \to 2^{2^{n}} \in ℤ$
29	28	peano2zd	$⊢ n \in ℕ_{0} \to 2^{2^{n}} + 1 \in ℤ$
30	29	adantl	$⊢ ((N \in ℕ_{0} \land M \in ℕ) \land n \in ℕ_{0}) \to 2^{2^{n}} + 1 \in ℤ$
31		df-fmtno	$⊢ FermatNo = (n \in ℕ_{0} ⟼ 2^{2^{n}} + 1)$
32	30 31	fmptd	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to FermatNo : ℕ_{0} ⟶ ℤ$
33	20 22 32	fprodfvdvdsd	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to \forall n \in (0 \dots N + M - 1) FermatNo (n) ∥ \prod_{k = 0}^{N + M - 1} FermatNo (k)$
34		fveq2	$⊢ n = N \to FermatNo (n) = FermatNo (N)$
35	34	breq1d	$⊢ n = N \to (FermatNo (n) ∥ \prod_{k = 0}^{N + M - 1} FermatNo (k) \leftrightarrow FermatNo (N) ∥ \prod_{k = 0}^{N + M - 1} FermatNo (k))$
36	35	rspcv	$⊢ N \in (0 \dots N + M - 1) \to (\forall n \in (0 \dots N + M - 1) FermatNo (n) ∥ \prod_{k = 0}^{N + M - 1} FermatNo (k) \to FermatNo (N) ∥ \prod_{k = 0}^{N + M - 1} FermatNo (k))$
37	19 33 36	sylc	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to FermatNo (N) ∥ \prod_{k = 0}^{N + M - 1} FermatNo (k)$
38		elfznn0	$⊢ k \in (0 \dots N + M - 1) \to k \in ℕ_{0}$
39	38	adantl	$⊢ ((N \in ℕ_{0} \land M \in ℕ) \land k \in (0 \dots N + M - 1)) \to k \in ℕ_{0}$
40		fmtnonn	$⊢ k \in ℕ_{0} \to FermatNo (k) \in ℕ$
41	39 40	syl	$⊢ ((N \in ℕ_{0} \land M \in ℕ) \land k \in (0 \dots N + M - 1)) \to FermatNo (k) \in ℕ$
42	41	nncnd	$⊢ ((N \in ℕ_{0} \land M \in ℕ) \land k \in (0 \dots N + M - 1)) \to FermatNo (k) \in ℂ$
43	20 42	fprodcl	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to \prod_{k = 0}^{N + M - 1} FermatNo (k) \in ℂ$
44		2cnd	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to 2 \in ℂ$
45		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
46		nncn	$⊢ M \in ℕ \to M \in ℂ$
47		addcl	$⊢ (N \in ℂ \land M \in ℂ) \to N + M \in ℂ$
48	45 46 47	syl2an	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to N + M \in ℂ$
49		npcan1	$⊢ N + M \in ℂ \to (N + M) - 1 + 1 = N + M$
50	48 49	syl	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to (N + M) - 1 + 1 = N + M$
51	50	eqcomd	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to N + M = (N + M) - 1 + 1$
52	51	fveq2d	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to FermatNo (N + M) = FermatNo ((N + M) - 1 + 1)$
53		fmtnorec2	$⊢ N + M - 1 \in ℕ_{0} \to FermatNo ((N + M) - 1 + 1) = \prod_{k = 0}^{N + M - 1} FermatNo (k) + 2$
54	4 53	syl	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to FermatNo ((N + M) - 1 + 1) = \prod_{k = 0}^{N + M - 1} FermatNo (k) + 2$
55	52 54	eqtrd	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to FermatNo (N + M) = \prod_{k = 0}^{N + M - 1} FermatNo (k) + 2$
56	43 44 55	mvrraddd	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to FermatNo (N + M) - 2 = \prod_{k = 0}^{N + M - 1} FermatNo (k)$
57	37 56	breqtrrd	$⊢ (N \in ℕ_{0} \land M \in ℕ) \to FermatNo (N) ∥ (FermatNo (N + M) - 2)$

Metamath Proof Explorer

Theorem fmtnodvds

Proof