Theorem inductionexd

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

	Ref	Expression
Assertion	inductionexd	⊢ ( 𝑁 ∈ ℕ → 3 ∥ ( ( 4 ↑ 𝑁 ) + 5 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑘 = 1 → ( 4 ↑ 𝑘 ) = ( 4 ↑ 1 ) )
2	1	oveq1d	⊢ ( 𝑘 = 1 → ( ( 4 ↑ 𝑘 ) + 5 ) = ( ( 4 ↑ 1 ) + 5 ) )
3	2	breq2d	⊢ ( 𝑘 = 1 → ( 3 ∥ ( ( 4 ↑ 𝑘 ) + 5 ) ↔ 3 ∥ ( ( 4 ↑ 1 ) + 5 ) ) )
4		oveq2	⊢ ( 𝑘 = 𝑛 → ( 4 ↑ 𝑘 ) = ( 4 ↑ 𝑛 ) )
5	4	oveq1d	⊢ ( 𝑘 = 𝑛 → ( ( 4 ↑ 𝑘 ) + 5 ) = ( ( 4 ↑ 𝑛 ) + 5 ) )
6	5	breq2d	⊢ ( 𝑘 = 𝑛 → ( 3 ∥ ( ( 4 ↑ 𝑘 ) + 5 ) ↔ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) )
7		oveq2	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 4 ↑ 𝑘 ) = ( 4 ↑ ( 𝑛 + 1 ) ) )
8	7	oveq1d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 4 ↑ 𝑘 ) + 5 ) = ( ( 4 ↑ ( 𝑛 + 1 ) ) + 5 ) )
9	8	breq2d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 3 ∥ ( ( 4 ↑ 𝑘 ) + 5 ) ↔ 3 ∥ ( ( 4 ↑ ( 𝑛 + 1 ) ) + 5 ) ) )
10		oveq2	⊢ ( 𝑘 = 𝑁 → ( 4 ↑ 𝑘 ) = ( 4 ↑ 𝑁 ) )
11	10	oveq1d	⊢ ( 𝑘 = 𝑁 → ( ( 4 ↑ 𝑘 ) + 5 ) = ( ( 4 ↑ 𝑁 ) + 5 ) )
12	11	breq2d	⊢ ( 𝑘 = 𝑁 → ( 3 ∥ ( ( 4 ↑ 𝑘 ) + 5 ) ↔ 3 ∥ ( ( 4 ↑ 𝑁 ) + 5 ) ) )
13		3z	⊢ 3 ∈ ℤ
14		4z	⊢ 4 ∈ ℤ
15		1nn0	⊢ 1 ∈ ℕ0
16		zexpcl	⊢ ( ( 4 ∈ ℤ ∧ 1 ∈ ℕ0 ) → ( 4 ↑ 1 ) ∈ ℤ )
17	14 15 16	mp2an	⊢ ( 4 ↑ 1 ) ∈ ℤ
18		5nn	⊢ 5 ∈ ℕ
19	18	nnzi	⊢ 5 ∈ ℤ
20		zaddcl	⊢ ( ( ( 4 ↑ 1 ) ∈ ℤ ∧ 5 ∈ ℤ ) → ( ( 4 ↑ 1 ) + 5 ) ∈ ℤ )
21	17 19 20	mp2an	⊢ ( ( 4 ↑ 1 ) + 5 ) ∈ ℤ
22	13 13 21	3pm3.2i	⊢ ( 3 ∈ ℤ ∧ 3 ∈ ℤ ∧ ( ( 4 ↑ 1 ) + 5 ) ∈ ℤ )
23		3t3e9	⊢ ( 3 · 3 ) = 9
24		4nn0	⊢ 4 ∈ ℕ0
25	24	numexp1	⊢ ( 4 ↑ 1 ) = 4
26	25	oveq1i	⊢ ( ( 4 ↑ 1 ) + 5 ) = ( 4 + 5 )
27		5cn	⊢ 5 ∈ ℂ
28		4cn	⊢ 4 ∈ ℂ
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 · 3 ) = ( ( 4 ↑ 1 ) + 5 )
33		dvds0lem	⊢ ( ( ( 3 ∈ ℤ ∧ 3 ∈ ℤ ∧ ( ( 4 ↑ 1 ) + 5 ) ∈ ℤ ) ∧ ( 3 · 3 ) = ( ( 4 ↑ 1 ) + 5 ) ) → 3 ∥ ( ( 4 ↑ 1 ) + 5 ) )
34	22 32 33	mp2an	⊢ 3 ∥ ( ( 4 ↑ 1 ) + 5 )
35	13	a1i	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → 3 ∈ ℤ )
36		4nn	⊢ 4 ∈ ℕ
37	36	a1i	⊢ ( 𝑛 ∈ ℕ → 4 ∈ ℕ )
38		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
39	37 38	nnexpcld	⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ 𝑛 ) ∈ ℕ )
40	39	nnzd	⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ 𝑛 ) ∈ ℤ )
41	40	adantr	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → ( 4 ↑ 𝑛 ) ∈ ℤ )
42	19	a1i	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → 5 ∈ ℤ )
43	41 42	zaddcld	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → ( ( 4 ↑ 𝑛 ) + 5 ) ∈ ℤ )
44	14	a1i	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → 4 ∈ ℤ )
45	43 44	zmulcld	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → ( ( ( 4 ↑ 𝑛 ) + 5 ) · 4 ) ∈ ℤ )
46	35 42	zmulcld	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → ( 3 · 5 ) ∈ ℤ )
47		simpr	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) )
48	35 43 44 47	dvdsmultr1d	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → 3 ∥ ( ( ( 4 ↑ 𝑛 ) + 5 ) · 4 ) )
49		dvdsmul1	⊢ ( ( 3 ∈ ℤ ∧ 5 ∈ ℤ ) → 3 ∥ ( 3 · 5 ) )
50	13 19 49	mp2an	⊢ 3 ∥ ( 3 · 5 )
51	50	a1i	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → 3 ∥ ( 3 · 5 ) )
52	35 45 46 48 51	dvds2subd	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → 3 ∥ ( ( ( ( 4 ↑ 𝑛 ) + 5 ) · 4 ) − ( 3 · 5 ) ) )
53	39	nncnd	⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ 𝑛 ) ∈ ℂ )
54	27	a1i	⊢ ( 𝑛 ∈ ℕ → 5 ∈ ℂ )
55	28	a1i	⊢ ( 𝑛 ∈ ℕ → 4 ∈ ℂ )
56	53 54 55	adddird	⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) + 5 ) · 4 ) = ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( 5 · 4 ) ) )
57	56	oveq1d	⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ 𝑛 ) + 5 ) · 4 ) − ; 1 5 ) = ( ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( 5 · 4 ) ) − ; 1 5 ) )
58		3cn	⊢ 3 ∈ ℂ
59		5t3e15	⊢ ( 5 · 3 ) = ; 1 5
60	27 58 59	mulcomli	⊢ ( 3 · 5 ) = ; 1 5
61	60	a1i	⊢ ( 𝑛 ∈ ℕ → ( 3 · 5 ) = ; 1 5 )
62	61	oveq2d	⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ 𝑛 ) + 5 ) · 4 ) − ( 3 · 5 ) ) = ( ( ( ( 4 ↑ 𝑛 ) + 5 ) · 4 ) − ; 1 5 ) )
63	55 38	expp1d	⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ ( 𝑛 + 1 ) ) = ( ( 4 ↑ 𝑛 ) · 4 ) )
64		ax-1cn	⊢ 1 ∈ ℂ
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 · ( 4 − 3 ) ) = ( 5 · 1 )
72	27 28 58	subdii	⊢ ( 5 · ( 4 − 3 ) ) = ( ( 5 · 4 ) − ( 5 · 3 ) )
73	27	mulridi	⊢ ( 5 · 1 ) = 5
74	71 72 73	3eqtr3ri	⊢ 5 = ( ( 5 · 4 ) − ( 5 · 3 ) )
75	59	eqcomi	⊢ ; 1 5 = ( 5 · 3 )
76	75	oveq2i	⊢ ( ( 5 · 4 ) − ; 1 5 ) = ( ( 5 · 4 ) − ( 5 · 3 ) )
77	74 76	eqtr4i	⊢ 5 = ( ( 5 · 4 ) − ; 1 5 )
78	77	a1i	⊢ ( 𝑛 ∈ ℕ → 5 = ( ( 5 · 4 ) − ; 1 5 ) )
79	63 78	oveq12d	⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ ( 𝑛 + 1 ) ) + 5 ) = ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( ( 5 · 4 ) − ; 1 5 ) ) )
80	53 55	mulcld	⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ 𝑛 ) · 4 ) ∈ ℂ )
81	54 55	mulcld	⊢ ( 𝑛 ∈ ℕ → ( 5 · 4 ) ∈ ℂ )
82		5nn0	⊢ 5 ∈ ℕ0
83	15 82	deccl	⊢ ; 1 5 ∈ ℕ0
84	83	nn0cni	⊢ ; 1 5 ∈ ℂ
85	84	a1i	⊢ ( 𝑛 ∈ ℕ → ; 1 5 ∈ ℂ )
86	80 81 85	addsubassd	⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( 5 · 4 ) ) − ; 1 5 ) = ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( ( 5 · 4 ) − ; 1 5 ) ) )
87	79 86	eqtr4d	⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ ( 𝑛 + 1 ) ) + 5 ) = ( ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( 5 · 4 ) ) − ; 1 5 ) )
88	57 62 87	3eqtr4rd	⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ ( 𝑛 + 1 ) ) + 5 ) = ( ( ( ( 4 ↑ 𝑛 ) + 5 ) · 4 ) − ( 3 · 5 ) ) )
89	88	adantr	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → ( ( 4 ↑ ( 𝑛 + 1 ) ) + 5 ) = ( ( ( ( 4 ↑ 𝑛 ) + 5 ) · 4 ) − ( 3 · 5 ) ) )
90	52 89	breqtrrd	⊢ ( ( 𝑛 ∈ ℕ ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) ) → 3 ∥ ( ( 4 ↑ ( 𝑛 + 1 ) ) + 5 ) )
91	90	ex	⊢ ( 𝑛 ∈ ℕ → ( 3 ∥ ( ( 4 ↑ 𝑛 ) + 5 ) → 3 ∥ ( ( 4 ↑ ( 𝑛 + 1 ) ) + 5 ) ) )
92	3 6 9 12 34 91	nnind	⊢ ( 𝑁 ∈ ℕ → 3 ∥ ( ( 4 ↑ 𝑁 ) + 5 ) )