fmtnorec2

		Ref	Expression
	Assertion	fmtnorec2	$⊢ N \in ℕ_{0} \to FermatNo (N + 1) = \prod_{n = 0}^{N} FermatNo (n) + 2$

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	$⊢ x = 0 \to FermatNo (x + 1) = FermatNo (0 + 1)$
2		oveq2	$⊢ x = 0 \to (0 \dots x) = (0 \dots 0)$
3	2	prodeq1d	$⊢ x = 0 \to \prod_{n = 0}^{x} FermatNo (n) = \prod_{n = 0}^{0} FermatNo (n)$
4	3	oveq1d	$⊢ x = 0 \to \prod_{n = 0}^{x} FermatNo (n) + 2 = \prod_{n = 0}^{0} FermatNo (n) + 2$
5	1 4	eqeq12d	$⊢ x = 0 \to (FermatNo (x + 1) = \prod_{n = 0}^{x} FermatNo (n) + 2 \leftrightarrow FermatNo (0 + 1) = \prod_{n = 0}^{0} FermatNo (n) + 2)$
6		fvoveq1	$⊢ x = y \to FermatNo (x + 1) = FermatNo (y + 1)$
7		oveq2	$⊢ x = y \to (0 \dots x) = (0 \dots y)$
8	7	prodeq1d	$⊢ x = y \to \prod_{n = 0}^{x} FermatNo (n) = \prod_{n = 0}^{y} FermatNo (n)$
9	8	oveq1d	$⊢ x = y \to \prod_{n = 0}^{x} FermatNo (n) + 2 = \prod_{n = 0}^{y} FermatNo (n) + 2$
10	6 9	eqeq12d	$⊢ x = y \to (FermatNo (x + 1) = \prod_{n = 0}^{x} FermatNo (n) + 2 \leftrightarrow FermatNo (y + 1) = \prod_{n = 0}^{y} FermatNo (n) + 2)$
11		fvoveq1	$⊢ x = y + 1 \to FermatNo (x + 1) = FermatNo (y + 1 + 1)$
12		oveq2	$⊢ x = y + 1 \to (0 \dots x) = (0 \dots y + 1)$
13	12	prodeq1d	$⊢ x = y + 1 \to \prod_{n = 0}^{x} FermatNo (n) = \prod_{n = 0}^{y + 1} FermatNo (n)$
14	13	oveq1d	$⊢ x = y + 1 \to \prod_{n = 0}^{x} FermatNo (n) + 2 = \prod_{n = 0}^{y + 1} FermatNo (n) + 2$
15	11 14	eqeq12d	$⊢ x = y + 1 \to (FermatNo (x + 1) = \prod_{n = 0}^{x} FermatNo (n) + 2 \leftrightarrow FermatNo (y + 1 + 1) = \prod_{n = 0}^{y + 1} FermatNo (n) + 2)$
16		fvoveq1	$⊢ x = N \to FermatNo (x + 1) = FermatNo (N + 1)$
17		oveq2	$⊢ x = N \to (0 \dots x) = (0 \dots N)$
18		prodeq1	$⊢ (0 \dots x) = (0 \dots N) \to \prod_{n = 0}^{x} FermatNo (n) = \prod_{n = 0}^{N} FermatNo (n)$
19	18	oveq1d	$⊢ (0 \dots x) = (0 \dots N) \to \prod_{n = 0}^{x} FermatNo (n) + 2 = \prod_{n = 0}^{N} FermatNo (n) + 2$
20	17 19	syl	$⊢ x = N \to \prod_{n = 0}^{x} FermatNo (n) + 2 = \prod_{n = 0}^{N} FermatNo (n) + 2$
21	16 20	eqeq12d	$⊢ x = N \to (FermatNo (x + 1) = \prod_{n = 0}^{x} FermatNo (n) + 2 \leftrightarrow FermatNo (N + 1) = \prod_{n = 0}^{N} FermatNo (n) + 2)$
22		fmtno0	$⊢ FermatNo (0) = 3$
23	22	oveq1i	$⊢ FermatNo (0) + 2 = 3 + 2$
24		3p2e5	$⊢ 3 + 2 = 5$
25	23 24	eqtri	$⊢ FermatNo (0) + 2 = 5$
26		fz0sn	$⊢ (0 \dots 0) = \{0\}$
27	26	prodeq1i	$⊢ \prod_{n = 0}^{0} FermatNo (n) = \prod_{n \in \{0\}} FermatNo (n)$
28		0z	$⊢ 0 \in ℤ$
29		0nn0	$⊢ 0 \in ℕ_{0}$
30		fmtnonn	$⊢ 0 \in ℕ_{0} \to FermatNo (0) \in ℕ$
31	30	nncnd	$⊢ 0 \in ℕ_{0} \to FermatNo (0) \in ℂ$
32	29 31	ax-mp	$⊢ FermatNo (0) \in ℂ$
33		fveq2	$⊢ n = 0 \to FermatNo (n) = FermatNo (0)$
34	33	prodsn	$⊢ (0 \in ℤ \land FermatNo (0) \in ℂ) \to \prod_{n \in \{0\}} FermatNo (n) = FermatNo (0)$
35	28 32 34	mp2an	$⊢ \prod_{n \in \{0\}} FermatNo (n) = FermatNo (0)$
36	27 35	eqtri	$⊢ \prod_{n = 0}^{0} FermatNo (n) = FermatNo (0)$
37	36	oveq1i	$⊢ \prod_{n = 0}^{0} FermatNo (n) + 2 = FermatNo (0) + 2$
38		0p1e1	$⊢ 0 + 1 = 1$
39	38	fveq2i	$⊢ FermatNo (0 + 1) = FermatNo (1)$
40		fmtno1	$⊢ FermatNo (1) = 5$
41	39 40	eqtri	$⊢ FermatNo (0 + 1) = 5$
42	25 37 41	3eqtr4ri	$⊢ FermatNo (0 + 1) = \prod_{n = 0}^{0} FermatNo (n) + 2$
43		fmtnorec2lem	$⊢ y \in ℕ_{0} \to (FermatNo (y + 1) = \prod_{n = 0}^{y} FermatNo (n) + 2 \to FermatNo (y + 1 + 1) = \prod_{n = 0}^{y + 1} FermatNo (n) + 2)$
44	5 10 15 21 42 43	nn0ind	$⊢ N \in ℕ_{0} \to FermatNo (N + 1) = \prod_{n = 0}^{N} FermatNo (n) + 2$

Metamath Proof Explorer

Theorem fmtnorec2

Proof