# Metamath Proof Explorer

## Theorem inductionexd

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

Ref Expression
Assertion inductionexd ${⊢}{N}\in ℕ\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)↔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)↔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)↔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)↔3\parallel \left({4}^{{N}}+5\right)\right)$
13 3z ${⊢}3\in ℤ$
14 4z ${⊢}4\in ℤ$
15 1nn0 ${⊢}1\in {ℕ}_{0}$
16 zexpcl ${⊢}\left(4\in ℤ\wedge 1\in {ℕ}_{0}\right)\to {4}^{1}\in ℤ$
17 14 15 16 mp2an ${⊢}{4}^{1}\in ℤ$
18 5nn ${⊢}5\in ℕ$
19 18 nnzi ${⊢}5\in ℤ$
20 zaddcl ${⊢}\left({4}^{1}\in ℤ\wedge 5\in ℤ\right)\to {4}^{1}+5\in ℤ$
21 17 19 20 mp2an ${⊢}{4}^{1}+5\in ℤ$
22 13 13 21 3pm3.2i ${⊢}\left(3\in ℤ\wedge 3\in ℤ\wedge {4}^{1}+5\in ℤ\right)$
23 3t3e9 ${⊢}3\cdot 3=9$
24 4nn0 ${⊢}4\in {ℕ}_{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 ℤ\wedge 3\in ℤ\wedge {4}^{1}+5\in ℤ\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 ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to 3\in ℤ$
36 4nn ${⊢}4\in ℕ$
37 36 a1i ${⊢}{n}\in ℕ\to 4\in ℕ$
38 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
39 37 38 nnexpcld ${⊢}{n}\in ℕ\to {4}^{{n}}\in ℕ$
40 39 nnzd ${⊢}{n}\in ℕ\to {4}^{{n}}\in ℤ$
41 40 adantr ${⊢}\left({n}\in ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to {4}^{{n}}\in ℤ$
42 19 a1i ${⊢}\left({n}\in ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to 5\in ℤ$
43 41 42 zaddcld ${⊢}\left({n}\in ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to {4}^{{n}}+5\in ℤ$
44 14 a1i ${⊢}\left({n}\in ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to 4\in ℤ$
45 simpr ${⊢}\left({n}\in ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to 3\parallel \left({4}^{{n}}+5\right)$
46 35 43 44 45 dvdsmultr1d ${⊢}\left({n}\in ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to 3\parallel \left({4}^{{n}}+5\right)\cdot 4$
47 dvdsmul1 ${⊢}\left(3\in ℤ\wedge 5\in ℤ\right)\to 3\parallel 3\cdot 5$
48 13 19 47 mp2an ${⊢}3\parallel 3\cdot 5$
49 48 a1i ${⊢}\left({n}\in ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to 3\parallel 3\cdot 5$
50 43 44 zmulcld ${⊢}\left({n}\in ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to \left({4}^{{n}}+5\right)\cdot 4\in ℤ$
51 35 42 zmulcld ${⊢}\left({n}\in ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to 3\cdot 5\in ℤ$
52 35 46 49 50 51 dvds2subd ${⊢}\left({n}\in ℕ\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 ℕ\to {4}^{{n}}\in ℂ$
54 27 a1i ${⊢}{n}\in ℕ\to 5\in ℂ$
55 28 a1i ${⊢}{n}\in ℕ\to 4\in ℂ$
56 53 54 55 adddird ${⊢}{n}\in ℕ\to \left({4}^{{n}}+5\right)\cdot 4={4}^{{n}}\cdot 4+5\cdot 4$
57 56 oveq1d ${⊢}{n}\in ℕ\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 ℕ\to 3\cdot 5=15$
62 61 oveq2d ${⊢}{n}\in ℕ\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 ℕ\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 mulid1i ${⊢}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 ℕ\to 5=5\cdot 4-15$
79 63 78 oveq12d ${⊢}{n}\in ℕ\to {4}^{{n}+1}+5={4}^{{n}}\cdot 4+5\cdot 4-15$
80 53 55 mulcld ${⊢}{n}\in ℕ\to {4}^{{n}}\cdot 4\in ℂ$
81 54 55 mulcld ${⊢}{n}\in ℕ\to 5\cdot 4\in ℂ$
82 5nn0 ${⊢}5\in {ℕ}_{0}$
83 15 82 deccl ${⊢}15\in {ℕ}_{0}$
84 83 nn0cni ${⊢}15\in ℂ$
85 84 a1i ${⊢}{n}\in ℕ\to 15\in ℂ$
86 80 81 85 addsubassd ${⊢}{n}\in ℕ\to {4}^{{n}}\cdot 4+5\cdot 4-15={4}^{{n}}\cdot 4+5\cdot 4-15$
87 79 86 eqtr4d ${⊢}{n}\in ℕ\to {4}^{{n}+1}+5={4}^{{n}}\cdot 4+5\cdot 4-15$
88 57 62 87 3eqtr4rd ${⊢}{n}\in ℕ\to {4}^{{n}+1}+5=\left({4}^{{n}}+5\right)\cdot 4-3\cdot 5$
89 88 adantr ${⊢}\left({n}\in ℕ\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 ℕ\wedge 3\parallel \left({4}^{{n}}+5\right)\right)\to 3\parallel \left({4}^{{n}+1}+5\right)$
91 90 ex ${⊢}{n}\in ℕ\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 ℕ\to 3\parallel \left({4}^{{N}}+5\right)$