Theorem inductionexd

Description: Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Assertion	inductionexd	$$⊢N\in \mathbb{N}\to 3\parallel \left(4^N+5\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢k=1\to 4^k=4^1$$
2	1	oveq1d	$$⊢k=1\to 4^k+5=4^1+5$$
3	2	breq2d	$$⊢k=1\to \left(3\parallel \left(4^k+5\right)\leftrightarrow 3\parallel \left(4^1+5\right)\right)$$
4		oveq2	$$⊢k=n\to 4^k=4^n$$
5	4	oveq1d	$$⊢k=n\to 4^k+5=4^n+5$$
6	5	breq2d	$$⊢k=n\to \left(3\parallel \left(4^k+5\right)\leftrightarrow 3\parallel \left(4^n+5\right)\right)$$
7		oveq2	$$⊢k=n+1\to 4^k=4^{n+1}$$
8	7	oveq1d	$$⊢k=n+1\to 4^k+5=4^{n+1}+5$$
9	8	breq2d	$$⊢k=n+1\to \left(3\parallel \left(4^k+5\right)\leftrightarrow 3\parallel \left(4^{n+1}+5\right)\right)$$
10		oveq2	$$⊢k=N\to 4^k=4^N$$
11	10	oveq1d	$$⊢k=N\to 4^k+5=4^N+5$$
12	11	breq2d	$$⊢k=N\to \left(3\parallel \left(4^k+5\right)\leftrightarrow 3\parallel \left(4^N+5\right)\right)$$
13		3z	$$⊢3\in \mathbb{Z}$$
14		4z	$$⊢4\in \mathbb{Z}$$
15		1nn0	$$⊢1\in {\mathbb{N}}_0$$
16		zexpcl	$$⊢\left(4\in \mathbb{Z}\wedge 1\in {\mathbb{N}}_0\right)\to 4^1\in \mathbb{Z}$$
17	14 15 16	mp2an	$$⊢4^1\in \mathbb{Z}$$
18		5nn	$$⊢5\in \mathbb{N}$$
19	18	nnzi	$$⊢5\in \mathbb{Z}$$
20		zaddcl	$$⊢\left(4^1\in \mathbb{Z}\wedge 5\in \mathbb{Z}\right)\to 4^1+5\in \mathbb{Z}$$
21	17 19 20	mp2an	$$⊢4^1+5\in \mathbb{Z}$$
22	13 13 21	3pm3.2i	$$⊢\left(3\in \mathbb{Z}\wedge 3\in \mathbb{Z}\wedge 4^1+5\in \mathbb{Z}\right)$$
23		3t3e9	$$⊢3\cdot 3=9$$
24		4nn0	$$⊢4\in {\mathbb{N}}_0$$
25	24	numexp1	$$⊢4^1=4$$
26	25	oveq1i	$$⊢4^1+5=4+5$$
27		5cn	$$⊢5\in ℂ$$
28		4cn	$$⊢4\in ℂ$$
29		5p4e9	$$⊢5+4=9$$
30	27 28 29	addcomli	$$⊢4+5=9$$
31	26 30	eqtri	$$⊢4^1+5=9$$
32	23 31	eqtr4i	$$⊢3\cdot 3=4^1+5$$
33		dvds0lem	$$⊢\left(\left(3\in \mathbb{Z}\wedge 3\in \mathbb{Z}\wedge 4^1+5\in \mathbb{Z}\right)\wedge 3\cdot 3=4^1+5\right)\to 3\parallel \left(4^1+5\right)$$
34	22 32 33	mp2an	$$⊢3\parallel \left(4^1+5\right)$$
35	13	a1i	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 3\in \mathbb{Z}$$
36		4nn	$$⊢4\in \mathbb{N}$$
37	36	a1i	$$⊢n\in \mathbb{N}\to 4\in \mathbb{N}$$
38		nnnn0	$$⊢n\in \mathbb{N}\to n\in {\mathbb{N}}_0$$
39	37 38	nnexpcld	$$⊢n\in \mathbb{N}\to 4^n\in \mathbb{N}$$
40	39	nnzd	$$⊢n\in \mathbb{N}\to 4^n\in \mathbb{Z}$$
41	40	adantr	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 4^n\in \mathbb{Z}$$
42	19	a1i	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 5\in \mathbb{Z}$$
43	41 42	zaddcld	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 4^n+5\in \mathbb{Z}$$
44	14	a1i	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 4\in \mathbb{Z}$$
45	43 44	zmulcld	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to \left(4^n+5\right)\cdot 4\in \mathbb{Z}$$
46	35 42	zmulcld	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 3\cdot 5\in \mathbb{Z}$$
47		simpr	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 3\parallel \left(4^n+5\right)$$
48	35 43 44 47	dvdsmultr1d	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 3\parallel \left(4^n+5\right)\cdot 4$$
49		dvdsmul1	$$⊢\left(3\in \mathbb{Z}\wedge 5\in \mathbb{Z}\right)\to 3\parallel 3\cdot 5$$
50	13 19 49	mp2an	$$⊢3\parallel 3\cdot 5$$
51	50	a1i	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 3\parallel 3\cdot 5$$
52	35 45 46 48 51	dvds2subd	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 3\parallel \left(\left(4^n+5\right)\cdot 4-3\cdot 5\right)$$
53	39	nncnd	$$⊢n\in \mathbb{N}\to 4^n\in ℂ$$
54	27	a1i	$$⊢n\in \mathbb{N}\to 5\in ℂ$$
55	28	a1i	$$⊢n\in \mathbb{N}\to 4\in ℂ$$
56	53 54 55	adddird	$$⊢n\in \mathbb{N}\to \left(4^n+5\right)\cdot 4=4^n\cdot 4+5\cdot 4$$
57	56	oveq1d	$$⊢n\in \mathbb{N}\to \left(4^n+5\right)\cdot 4-15=4^n\cdot 4+5\cdot 4-15$$
58		3cn	$$⊢3\in ℂ$$
59		5t3e15	$$⊢5\cdot 3=15$$
60	27 58 59	mulcomli	$$⊢3\cdot 5=15$$
61	60	a1i	$$⊢n\in \mathbb{N}\to 3\cdot 5=15$$
62	61	oveq2d	$$⊢n\in \mathbb{N}\to \left(4^n+5\right)\cdot 4-3\cdot 5=\left(4^n+5\right)\cdot 4-15$$
63	55 38	expp1d	$$⊢n\in \mathbb{N}\to 4^{n+1}=4^n\cdot 4$$
64		ax-1cn	$$⊢1\in ℂ$$
65		3p1e4	$$⊢3+1=4$$
66	58 64 65	addcomli	$$⊢1+3=4$$
67	66	eqcomi	$$⊢4=1+3$$
68	67	oveq1i	$$⊢4-3=1+3-3$$
69	64 58	pncan3oi	$$⊢1+3-3=1$$
70	68 69	eqtri	$$⊢4-3=1$$
71	70	oveq2i	$$⊢5\left(4-3\right)=5\cdot 1$$
72	27 28 58	subdii	$$⊢5\left(4-3\right)=5\cdot 4-5\cdot 3$$
73	27	mulridi	$$⊢5\cdot 1=5$$
74	71 72 73	3eqtr3ri	$$⊢5=5\cdot 4-5\cdot 3$$
75	59	eqcomi	$$⊢15=5\cdot 3$$
76	75	oveq2i	$$⊢5\cdot 4-15=5\cdot 4-5\cdot 3$$
77	74 76	eqtr4i	$$⊢5=5\cdot 4-15$$
78	77	a1i	$$⊢n\in \mathbb{N}\to 5=5\cdot 4-15$$
79	63 78	oveq12d	$$⊢n\in \mathbb{N}\to 4^{n+1}+5=4^n\cdot 4+5\cdot 4-15$$
80	53 55	mulcld	$$⊢n\in \mathbb{N}\to 4^n\cdot 4\in ℂ$$
81	54 55	mulcld	$$⊢n\in \mathbb{N}\to 5\cdot 4\in ℂ$$
82		5nn0	$$⊢5\in {\mathbb{N}}_0$$
83	15 82	deccl	$$⊢15\in {\mathbb{N}}_0$$
84	83	nn0cni	$$⊢15\in ℂ$$
85	84	a1i	$$⊢n\in \mathbb{N}\to 15\in ℂ$$
86	80 81 85	addsubassd	$$⊢n\in \mathbb{N}\to 4^n\cdot 4+5\cdot 4-15=4^n\cdot 4+5\cdot 4-15$$
87	79 86	eqtr4d	$$⊢n\in \mathbb{N}\to 4^{n+1}+5=4^n\cdot 4+5\cdot 4-15$$
88	57 62 87	3eqtr4rd	$$⊢n\in \mathbb{N}\to 4^{n+1}+5=\left(4^n+5\right)\cdot 4-3\cdot 5$$
89	88	adantr	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 4^{n+1}+5=\left(4^n+5\right)\cdot 4-3\cdot 5$$
90	52 89	breqtrrd	$$⊢\left(n\in \mathbb{N}\wedge 3\parallel \left(4^n+5\right)\right)\to 3\parallel \left(4^{n+1}+5\right)$$
91	90	ex	$$⊢n\in \mathbb{N}\to \left(3\parallel \left(4^n+5\right)\to 3\parallel \left(4^{n+1}+5\right)\right)$$
92	3 6 9 12 34 91	nnind	$$⊢N\in \mathbb{N}\to 3\parallel \left(4^N+5\right)$$