Metamath Proof Explorer

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 mulid1i ⊢ ( 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 ) )