Metamath Proof Explorer

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 ) )