Theorem ex-ind-dvds

Description: Example of a proof by induction (divisibility result). (Contributed by Stanislas Polu, 9-Mar-2020) (Revised by BJ, 24-Mar-2020)

	Ref	Expression
Assertion	ex-ind-dvds	$$⊢N\in {\mathbb{N}}_0\to 3\parallel \left(4^N+2\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢k=0\to 4^k=4^0$$
2	1	oveq1d	$$⊢k=0\to 4^k+2=4^0+2$$
3	2	breq2d	$$⊢k=0\to \left(3\parallel \left(4^k+2\right)\leftrightarrow 3\parallel \left(4^0+2\right)\right)$$
4		oveq2	$$⊢k=n\to 4^k=4^n$$
5	4	oveq1d	$$⊢k=n\to 4^k+2=4^n+2$$
6	5	breq2d	$$⊢k=n\to \left(3\parallel \left(4^k+2\right)\leftrightarrow 3\parallel \left(4^n+2\right)\right)$$
7		oveq2	$$⊢k=n+1\to 4^k=4^{n+1}$$
8	7	oveq1d	$$⊢k=n+1\to 4^k+2=4^{n+1}+2$$
9	8	breq2d	$$⊢k=n+1\to \left(3\parallel \left(4^k+2\right)\leftrightarrow 3\parallel \left(4^{n+1}+2\right)\right)$$
10		oveq2	$$⊢k=N\to 4^k=4^N$$
11	10	oveq1d	$$⊢k=N\to 4^k+2=4^N+2$$
12	11	breq2d	$$⊢k=N\to \left(3\parallel \left(4^k+2\right)\leftrightarrow 3\parallel \left(4^N+2\right)\right)$$
13		3z	$$⊢3\in \mathbb{Z}$$
14		iddvds	$$⊢3\in \mathbb{Z}\to 3\parallel 3$$
15	13 14	ax-mp	$$⊢3\parallel 3$$
16		4nn0	$$⊢4\in {\mathbb{N}}_0$$
17	16	numexp0	$$⊢4^0=1$$
18	17	oveq1i	$$⊢4^0+2=1+2$$
19		1p2e3	$$⊢1+2=3$$
20	18 19	eqtri	$$⊢4^0+2=3$$
21	15 20	breqtrri	$$⊢3\parallel \left(4^0+2\right)$$
22	13	a1i	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 3\in \mathbb{Z}$$
23	16	a1i	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 4\in {\mathbb{N}}_0$$
24		simpl	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to n\in {\mathbb{N}}_0$$
25	23 24	nn0expcld	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 4^n\in {\mathbb{N}}_0$$
26	25	nn0zd	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 4^n\in \mathbb{Z}$$
27		2z	$$⊢2\in \mathbb{Z}$$
28	27	a1i	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 2\in \mathbb{Z}$$
29	26 28	zaddcld	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 4^n+2\in \mathbb{Z}$$
30		4z	$$⊢4\in \mathbb{Z}$$
31	30	a1i	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 4\in \mathbb{Z}$$
32	29 31	zmulcld	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to \left(4^n+2\right)\cdot 4\in \mathbb{Z}$$
33	22 28	zmulcld	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 3\cdot 2\in \mathbb{Z}$$
34	16	a1i	$$⊢n\in {\mathbb{N}}_0\to 4\in {\mathbb{N}}_0$$
35		id	$$⊢n\in {\mathbb{N}}_0\to n\in {\mathbb{N}}_0$$
36	34 35	nn0expcld	$$⊢n\in {\mathbb{N}}_0\to 4^n\in {\mathbb{N}}_0$$
37	36	nn0zd	$$⊢n\in {\mathbb{N}}_0\to 4^n\in \mathbb{Z}$$
38	37	adantr	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 4^n\in \mathbb{Z}$$
39	38 28	zaddcld	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 4^n+2\in \mathbb{Z}$$
40		simpr	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 3\parallel \left(4^n+2\right)$$
41	22 39 31 40	dvdsmultr1d	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 3\parallel \left(4^n+2\right)\cdot 4$$
42		dvdsmul1	$$⊢\left(3\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to 3\parallel 3\cdot 2$$
43	13 27 42	mp2an	$$⊢3\parallel 3\cdot 2$$
44	43	a1i	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 3\parallel 3\cdot 2$$
45	22 32 33 41 44	dvds2subd	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 3\parallel \left(\left(4^n+2\right)\cdot 4-3\cdot 2\right)$$
46	36	nn0cnd	$$⊢n\in {\mathbb{N}}_0\to 4^n\in ℂ$$
47		2cnd	$$⊢n\in {\mathbb{N}}_0\to 2\in ℂ$$
48		4cn	$$⊢4\in ℂ$$
49	48	a1i	$$⊢n\in {\mathbb{N}}_0\to 4\in ℂ$$
50	46 47 49	adddird	$$⊢n\in {\mathbb{N}}_0\to \left(4^n+2\right)\cdot 4=4^n\cdot 4+2\cdot 4$$
51	50	oveq1d	$$⊢n\in {\mathbb{N}}_0\to \left(4^n+2\right)\cdot 4-2\cdot 3=4^n\cdot 4+2\cdot 4-2\cdot 3$$
52		3cn	$$⊢3\in ℂ$$
53		2cn	$$⊢2\in ℂ$$
54	52 53	mulcomi	$$⊢3\cdot 2=2\cdot 3$$
55	54	a1i	$$⊢n\in {\mathbb{N}}_0\to 3\cdot 2=2\cdot 3$$
56	55	oveq2d	$$⊢n\in {\mathbb{N}}_0\to \left(4^n+2\right)\cdot 4-3\cdot 2=\left(4^n+2\right)\cdot 4-2\cdot 3$$
57	49 35	expp1d	$$⊢n\in {\mathbb{N}}_0\to 4^{n+1}=4^n\cdot 4$$
58		ax-1cn	$$⊢1\in ℂ$$
59		3p1e4	$$⊢3+1=4$$
60	52 58 59	addcomli	$$⊢1+3=4$$
61	60	eqcomi	$$⊢4=1+3$$
62	58 52 61	mvrraddi	$$⊢4-3=1$$
63	62	oveq2i	$$⊢2\left(4-3\right)=2\cdot 1$$
64	53 48 52	subdii	$$⊢2\left(4-3\right)=2\cdot 4-2\cdot 3$$
65		2t1e2	$$⊢2\cdot 1=2$$
66	63 64 65	3eqtr3ri	$$⊢2=2\cdot 4-2\cdot 3$$
67	66	a1i	$$⊢n\in {\mathbb{N}}_0\to 2=2\cdot 4-2\cdot 3$$
68	57 67	oveq12d	$$⊢n\in {\mathbb{N}}_0\to 4^{n+1}+2=4^n\cdot 4+2\cdot 4-2\cdot 3$$
69	46 49	mulcld	$$⊢n\in {\mathbb{N}}_0\to 4^n\cdot 4\in ℂ$$
70	47 49	mulcld	$$⊢n\in {\mathbb{N}}_0\to 2\cdot 4\in ℂ$$
71	52	a1i	$$⊢n\in {\mathbb{N}}_0\to 3\in ℂ$$
72	47 71	mulcld	$$⊢n\in {\mathbb{N}}_0\to 2\cdot 3\in ℂ$$
73	69 70 72	addsubassd	$$⊢n\in {\mathbb{N}}_0\to 4^n\cdot 4+2\cdot 4-2\cdot 3=4^n\cdot 4+2\cdot 4-2\cdot 3$$
74	68 73	eqtr4d	$$⊢n\in {\mathbb{N}}_0\to 4^{n+1}+2=4^n\cdot 4+2\cdot 4-2\cdot 3$$
75	51 56 74	3eqtr4rd	$$⊢n\in {\mathbb{N}}_0\to 4^{n+1}+2=\left(4^n+2\right)\cdot 4-3\cdot 2$$
76	75	adantr	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 4^{n+1}+2=\left(4^n+2\right)\cdot 4-3\cdot 2$$
77	45 76	breqtrrd	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel \left(4^n+2\right)\right)\to 3\parallel \left(4^{n+1}+2\right)$$
78	77	ex	$$⊢n\in {\mathbb{N}}_0\to \left(3\parallel \left(4^n+2\right)\to 3\parallel \left(4^{n+1}+2\right)\right)$$
79	3 6 9 12 21 78	nn0ind	$$⊢N\in {\mathbb{N}}_0\to 3\parallel \left(4^N+2\right)$$