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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( FermatNo ‘ 𝑁 ) ∥ ( ( FermatNo ‘ ( 𝑁 + 𝑀 ) ) − 2 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
2		nn0nnaddcl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( 𝑁 + 𝑀 ) ∈ ℕ )
3		nnm1nn0	⊢ ( ( 𝑁 + 𝑀 ) ∈ ℕ → ( ( 𝑁 + 𝑀 ) − 1 ) ∈ ℕ0 )
4	2 3	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 + 𝑀 ) − 1 ) ∈ ℕ0 )
5		1red	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → 1 ∈ ℝ )
6		nnre	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
7	6	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℝ )
8		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
9	8	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → 𝑁 ∈ ℝ )
10		nnge1	⊢ ( 𝑀 ∈ ℕ → 1 ≤ 𝑀 )
11	10	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → 1 ≤ 𝑀 )
12	5 7 9 11	leadd2dd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( 𝑁 + 1 ) ≤ ( 𝑁 + 𝑀 ) )
13		readdcl	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑁 + 𝑀 ) ∈ ℝ )
14	8 6 13	syl2an	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( 𝑁 + 𝑀 ) ∈ ℝ )
15		leaddsub	⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑁 + 𝑀 ) ∈ ℝ ) → ( ( 𝑁 + 1 ) ≤ ( 𝑁 + 𝑀 ) ↔ 𝑁 ≤ ( ( 𝑁 + 𝑀 ) − 1 ) ) )
16	9 5 14 15	syl3anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 + 1 ) ≤ ( 𝑁 + 𝑀 ) ↔ 𝑁 ≤ ( ( 𝑁 + 𝑀 ) − 1 ) ) )
17	12 16	mpbid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → 𝑁 ≤ ( ( 𝑁 + 𝑀 ) − 1 ) )
18		elfz2nn0	⊢ ( 𝑁 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 𝑀 ) − 1 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ( 𝑁 + 𝑀 ) − 1 ) ) )
19	1 4 17 18	syl3anbrc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → 𝑁 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) )
20		fzfid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ∈ Fin )
21		fz0ssnn0	⊢ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ⊆ ℕ0
22	21	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ⊆ ℕ0 )
23		2nn0	⊢ 2 ∈ ℕ0
24	23	a1i	⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℕ0 )
25		id	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 )
26	24 25	nn0expcld	⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ 𝑛 ) ∈ ℕ0 )
27	24 26	nn0expcld	⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑛 ) ) ∈ ℕ0 )
28	27	nn0zd	⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑛 ) ) ∈ ℤ )
29	28	peano2zd	⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) ∈ ℤ )
30	29	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) ∈ ℤ )
31		df-fmtno	⊢ FermatNo = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )
32	30 31	fmptd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → FermatNo : ℕ0 ⟶ ℤ )
33	20 22 32	fprodfvdvdsd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ∀ 𝑛 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑛 ) ∥ ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) )
34		fveq2	⊢ ( 𝑛 = 𝑁 → ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑁 ) )
35	34	breq1d	⊢ ( 𝑛 = 𝑁 → ( ( FermatNo ‘ 𝑛 ) ∥ ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) ↔ ( FermatNo ‘ 𝑁 ) ∥ ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) ) )
36	35	rspcv	⊢ ( 𝑁 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) → ( ∀ 𝑛 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑛 ) ∥ ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) → ( FermatNo ‘ 𝑁 ) ∥ ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) ) )
37	19 33 36	sylc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( FermatNo ‘ 𝑁 ) ∥ ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) )
38		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) → 𝑘 ∈ ℕ0 )
39	38	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ) → 𝑘 ∈ ℕ0 )
40		fmtnonn	⊢ ( 𝑘 ∈ ℕ0 → ( FermatNo ‘ 𝑘 ) ∈ ℕ )
41	39 40	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ) → ( FermatNo ‘ 𝑘 ) ∈ ℕ )
42	41	nncnd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ) → ( FermatNo ‘ 𝑘 ) ∈ ℂ )
43	20 42	fprodcl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) ∈ ℂ )
44		2cnd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → 2 ∈ ℂ )
45		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
46		nncn	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
47		addcl	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑁 + 𝑀 ) ∈ ℂ )
48	45 46 47	syl2an	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( 𝑁 + 𝑀 ) ∈ ℂ )
49		npcan1	⊢ ( ( 𝑁 + 𝑀 ) ∈ ℂ → ( ( ( 𝑁 + 𝑀 ) − 1 ) + 1 ) = ( 𝑁 + 𝑀 ) )
50	48 49	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( ( 𝑁 + 𝑀 ) − 1 ) + 1 ) = ( 𝑁 + 𝑀 ) )
51	50	eqcomd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( 𝑁 + 𝑀 ) = ( ( ( 𝑁 + 𝑀 ) − 1 ) + 1 ) )
52	51	fveq2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( FermatNo ‘ ( 𝑁 + 𝑀 ) ) = ( FermatNo ‘ ( ( ( 𝑁 + 𝑀 ) − 1 ) + 1 ) ) )
53		fmtnorec2	⊢ ( ( ( 𝑁 + 𝑀 ) − 1 ) ∈ ℕ0 → ( FermatNo ‘ ( ( ( 𝑁 + 𝑀 ) − 1 ) + 1 ) ) = ( ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) + 2 ) )
54	4 53	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( FermatNo ‘ ( ( ( 𝑁 + 𝑀 ) − 1 ) + 1 ) ) = ( ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) + 2 ) )
55	52 54	eqtrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( FermatNo ‘ ( 𝑁 + 𝑀 ) ) = ( ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) + 2 ) )
56	43 44 55	mvrraddd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( FermatNo ‘ ( 𝑁 + 𝑀 ) ) − 2 ) = ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 𝑀 ) − 1 ) ) ( FermatNo ‘ 𝑘 ) )
57	37 56	breqtrrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( FermatNo ‘ 𝑁 ) ∥ ( ( FermatNo ‘ ( 𝑁 + 𝑀 ) ) − 2 ) )