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	⊢ ( 𝑁 ∈ ℕ0 → 3 ∥ ( ( 4 ↑ 𝑁 ) + 2 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑘 = 0 → ( 4 ↑ 𝑘 ) = ( 4 ↑ 0 ) )
2	1	oveq1d	⊢ ( 𝑘 = 0 → ( ( 4 ↑ 𝑘 ) + 2 ) = ( ( 4 ↑ 0 ) + 2 ) )
3	2	breq2d	⊢ ( 𝑘 = 0 → ( 3 ∥ ( ( 4 ↑ 𝑘 ) + 2 ) ↔ 3 ∥ ( ( 4 ↑ 0 ) + 2 ) ) )
4		oveq2	⊢ ( 𝑘 = 𝑛 → ( 4 ↑ 𝑘 ) = ( 4 ↑ 𝑛 ) )
5	4	oveq1d	⊢ ( 𝑘 = 𝑛 → ( ( 4 ↑ 𝑘 ) + 2 ) = ( ( 4 ↑ 𝑛 ) + 2 ) )
6	5	breq2d	⊢ ( 𝑘 = 𝑛 → ( 3 ∥ ( ( 4 ↑ 𝑘 ) + 2 ) ↔ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) )
7		oveq2	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 4 ↑ 𝑘 ) = ( 4 ↑ ( 𝑛 + 1 ) ) )
8	7	oveq1d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 4 ↑ 𝑘 ) + 2 ) = ( ( 4 ↑ ( 𝑛 + 1 ) ) + 2 ) )
9	8	breq2d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 3 ∥ ( ( 4 ↑ 𝑘 ) + 2 ) ↔ 3 ∥ ( ( 4 ↑ ( 𝑛 + 1 ) ) + 2 ) ) )
10		oveq2	⊢ ( 𝑘 = 𝑁 → ( 4 ↑ 𝑘 ) = ( 4 ↑ 𝑁 ) )
11	10	oveq1d	⊢ ( 𝑘 = 𝑁 → ( ( 4 ↑ 𝑘 ) + 2 ) = ( ( 4 ↑ 𝑁 ) + 2 ) )
12	11	breq2d	⊢ ( 𝑘 = 𝑁 → ( 3 ∥ ( ( 4 ↑ 𝑘 ) + 2 ) ↔ 3 ∥ ( ( 4 ↑ 𝑁 ) + 2 ) ) )
13		3z	⊢ 3 ∈ ℤ
14		iddvds	⊢ ( 3 ∈ ℤ → 3 ∥ 3 )
15	13 14	ax-mp	⊢ 3 ∥ 3
16		4nn0	⊢ 4 ∈ ℕ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 ∥ ( ( 4 ↑ 0 ) + 2 )
22	13	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → 3 ∈ ℤ )
23	16	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → 4 ∈ ℕ0 )
24		simpl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → 𝑛 ∈ ℕ0 )
25	23 24	nn0expcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → ( 4 ↑ 𝑛 ) ∈ ℕ0 )
26	25	nn0zd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → ( 4 ↑ 𝑛 ) ∈ ℤ )
27		2z	⊢ 2 ∈ ℤ
28	27	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → 2 ∈ ℤ )
29	26 28	zaddcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → ( ( 4 ↑ 𝑛 ) + 2 ) ∈ ℤ )
30		4z	⊢ 4 ∈ ℤ
31	30	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → 4 ∈ ℤ )
32	29 31	zmulcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → ( ( ( 4 ↑ 𝑛 ) + 2 ) · 4 ) ∈ ℤ )
33	22 28	zmulcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → ( 3 · 2 ) ∈ ℤ )
34	16	a1i	⊢ ( 𝑛 ∈ ℕ0 → 4 ∈ ℕ0 )
35		id	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 )
36	34 35	nn0expcld	⊢ ( 𝑛 ∈ ℕ0 → ( 4 ↑ 𝑛 ) ∈ ℕ0 )
37	36	nn0zd	⊢ ( 𝑛 ∈ ℕ0 → ( 4 ↑ 𝑛 ) ∈ ℤ )
38	37	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → ( 4 ↑ 𝑛 ) ∈ ℤ )
39	38 28	zaddcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → ( ( 4 ↑ 𝑛 ) + 2 ) ∈ ℤ )
40		simpr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) )
41	22 39 31 40	dvdsmultr1d	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → 3 ∥ ( ( ( 4 ↑ 𝑛 ) + 2 ) · 4 ) )
42		dvdsmul1	⊢ ( ( 3 ∈ ℤ ∧ 2 ∈ ℤ ) → 3 ∥ ( 3 · 2 ) )
43	13 27 42	mp2an	⊢ 3 ∥ ( 3 · 2 )
44	43	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → 3 ∥ ( 3 · 2 ) )
45	22 32 33 41 44	dvds2subd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → 3 ∥ ( ( ( ( 4 ↑ 𝑛 ) + 2 ) · 4 ) − ( 3 · 2 ) ) )
46	36	nn0cnd	⊢ ( 𝑛 ∈ ℕ0 → ( 4 ↑ 𝑛 ) ∈ ℂ )
47		2cnd	⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℂ )
48		4cn	⊢ 4 ∈ ℂ
49	48	a1i	⊢ ( 𝑛 ∈ ℕ0 → 4 ∈ ℂ )
50	46 47 49	adddird	⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 4 ↑ 𝑛 ) + 2 ) · 4 ) = ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( 2 · 4 ) ) )
51	50	oveq1d	⊢ ( 𝑛 ∈ ℕ0 → ( ( ( ( 4 ↑ 𝑛 ) + 2 ) · 4 ) − ( 2 · 3 ) ) = ( ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( 2 · 4 ) ) − ( 2 · 3 ) ) )
52		3cn	⊢ 3 ∈ ℂ
53		2cn	⊢ 2 ∈ ℂ
54	52 53	mulcomi	⊢ ( 3 · 2 ) = ( 2 · 3 )
55	54	a1i	⊢ ( 𝑛 ∈ ℕ0 → ( 3 · 2 ) = ( 2 · 3 ) )
56	55	oveq2d	⊢ ( 𝑛 ∈ ℕ0 → ( ( ( ( 4 ↑ 𝑛 ) + 2 ) · 4 ) − ( 3 · 2 ) ) = ( ( ( ( 4 ↑ 𝑛 ) + 2 ) · 4 ) − ( 2 · 3 ) ) )
57	49 35	expp1d	⊢ ( 𝑛 ∈ ℕ0 → ( 4 ↑ ( 𝑛 + 1 ) ) = ( ( 4 ↑ 𝑛 ) · 4 ) )
58		ax-1cn	⊢ 1 ∈ ℂ
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 · ( 4 − 3 ) ) = ( 2 · 1 )
64	53 48 52	subdii	⊢ ( 2 · ( 4 − 3 ) ) = ( ( 2 · 4 ) − ( 2 · 3 ) )
65		2t1e2	⊢ ( 2 · 1 ) = 2
66	63 64 65	3eqtr3ri	⊢ 2 = ( ( 2 · 4 ) − ( 2 · 3 ) )
67	66	a1i	⊢ ( 𝑛 ∈ ℕ0 → 2 = ( ( 2 · 4 ) − ( 2 · 3 ) ) )
68	57 67	oveq12d	⊢ ( 𝑛 ∈ ℕ0 → ( ( 4 ↑ ( 𝑛 + 1 ) ) + 2 ) = ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( ( 2 · 4 ) − ( 2 · 3 ) ) ) )
69	46 49	mulcld	⊢ ( 𝑛 ∈ ℕ0 → ( ( 4 ↑ 𝑛 ) · 4 ) ∈ ℂ )
70	47 49	mulcld	⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 4 ) ∈ ℂ )
71	52	a1i	⊢ ( 𝑛 ∈ ℕ0 → 3 ∈ ℂ )
72	47 71	mulcld	⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 3 ) ∈ ℂ )
73	69 70 72	addsubassd	⊢ ( 𝑛 ∈ ℕ0 → ( ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( 2 · 4 ) ) − ( 2 · 3 ) ) = ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( ( 2 · 4 ) − ( 2 · 3 ) ) ) )
74	68 73	eqtr4d	⊢ ( 𝑛 ∈ ℕ0 → ( ( 4 ↑ ( 𝑛 + 1 ) ) + 2 ) = ( ( ( ( 4 ↑ 𝑛 ) · 4 ) + ( 2 · 4 ) ) − ( 2 · 3 ) ) )
75	51 56 74	3eqtr4rd	⊢ ( 𝑛 ∈ ℕ0 → ( ( 4 ↑ ( 𝑛 + 1 ) ) + 2 ) = ( ( ( ( 4 ↑ 𝑛 ) + 2 ) · 4 ) − ( 3 · 2 ) ) )
76	75	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → ( ( 4 ↑ ( 𝑛 + 1 ) ) + 2 ) = ( ( ( ( 4 ↑ 𝑛 ) + 2 ) · 4 ) − ( 3 · 2 ) ) )
77	45 76	breqtrrd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) ) → 3 ∥ ( ( 4 ↑ ( 𝑛 + 1 ) ) + 2 ) )
78	77	ex	⊢ ( 𝑛 ∈ ℕ0 → ( 3 ∥ ( ( 4 ↑ 𝑛 ) + 2 ) → 3 ∥ ( ( 4 ↑ ( 𝑛 + 1 ) ) + 2 ) ) )
79	3 6 9 12 21 78	nn0ind	⊢ ( 𝑁 ∈ ℕ0 → 3 ∥ ( ( 4 ↑ 𝑁 ) + 2 ) )