Metamath Proof Explorer

Theorem inductionexd

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

Ref Expression
Assertion inductionexd ⊢ N ∈ ℕ → 3 ∥ 4 N + 5

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ k = 1 → 4 k = 4 1
2 1 oveq1d ⊢ k = 1 → 4 k + 5 = 4 1 + 5
3 2 breq2d ⊢ k = 1 → 3 ∥ 4 k + 5 ↔ 3 ∥ 4 1 + 5
4 oveq2 ⊢ k = n → 4 k = 4 n
5 4 oveq1d ⊢ k = n → 4 k + 5 = 4 n + 5
6 5 breq2d ⊢ k = n → 3 ∥ 4 k + 5 ↔ 3 ∥ 4 n + 5
7 oveq2 ⊢ k = n + 1 → 4 k = 4 n + 1
8 7 oveq1d ⊢ k = n + 1 → 4 k + 5 = 4 n + 1 + 5
9 8 breq2d ⊢ k = n + 1 → 3 ∥ 4 k + 5 ↔ 3 ∥ 4 n + 1 + 5
10 oveq2 ⊢ k = N → 4 k = 4 N
11 10 oveq1d ⊢ k = N → 4 k + 5 = 4 N + 5
12 11 breq2d ⊢ k = N → 3 ∥ 4 k + 5 ↔ 3 ∥ 4 N + 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 ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 3 ∈ ℤ
36 4nn ⊢ 4 ∈ ℕ
37 36 a1i ⊢ n ∈ ℕ → 4 ∈ ℕ
38 nnnn0 ⊢ n ∈ ℕ → n ∈ ℕ 0
39 37 38 nnexpcld ⊢ n ∈ ℕ → 4 n ∈ ℕ
40 39 nnzd ⊢ n ∈ ℕ → 4 n ∈ ℤ
41 40 adantr ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 4 n ∈ ℤ
42 19 a1i ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 5 ∈ ℤ
43 41 42 zaddcld ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 4 n + 5 ∈ ℤ
44 14 a1i ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 4 ∈ ℤ
45 43 44 zmulcld ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 4 n + 5 ⋅ 4 ∈ ℤ
46 35 42 zmulcld ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 3 ⋅ 5 ∈ ℤ
47 simpr ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 3 ∥ 4 n + 5
48 35 43 44 47 dvdsmultr1d ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 3 ∥ 4 n + 5 ⋅ 4
49 dvdsmul1 ⊢ 3 ∈ ℤ ∧ 5 ∈ ℤ → 3 ∥ 3 ⋅ 5
50 13 19 49 mp2an ⊢ 3 ∥ 3 ⋅ 5
51 50 a1i ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 3 ∥ 3 ⋅ 5
52 35 45 46 48 51 dvds2subd ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 3 ∥ 4 n + 5 ⋅ 4 − 3 ⋅ 5
53 39 nncnd ⊢ n ∈ ℕ → 4 n ∈ ℂ
54 27 a1i ⊢ n ∈ ℕ → 5 ∈ ℂ
55 28 a1i ⊢ n ∈ ℕ → 4 ∈ ℂ
56 53 54 55 adddird ⊢ n ∈ ℕ → 4 n + 5 ⋅ 4 = 4 n ⋅ 4 + 5 ⋅ 4
57 56 oveq1d ⊢ n ∈ ℕ → 4 n + 5 ⋅ 4 − 15 = 4 n ⋅ 4 + 5 ⋅ 4 - 15
58 3cn ⊢ 3 ∈ ℂ
59 5t3e15 ⊢ 5 ⋅ 3 = 15
60 27 58 59 mulcomli ⊢ 3 ⋅ 5 = 15
61 60 a1i ⊢ n ∈ ℕ → 3 ⋅ 5 = 15
62 61 oveq2d ⊢ n ∈ ℕ → 4 n + 5 ⋅ 4 − 3 ⋅ 5 = 4 n + 5 ⋅ 4 − 15
63 55 38 expp1d ⊢ n ∈ ℕ → 4 n + 1 = 4 n ⋅ 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 ⊢ 15 = 5 ⋅ 3
76 75 oveq2i ⊢ 5 ⋅ 4 − 15 = 5 ⋅ 4 − 5 ⋅ 3
77 74 76 eqtr4i ⊢ 5 = 5 ⋅ 4 − 15
78 77 a1i ⊢ n ∈ ℕ → 5 = 5 ⋅ 4 − 15
79 63 78 oveq12d ⊢ n ∈ ℕ → 4 n + 1 + 5 = 4 n ⋅ 4 + 5 ⋅ 4 - 15
80 53 55 mulcld ⊢ n ∈ ℕ → 4 n ⋅ 4 ∈ ℂ
81 54 55 mulcld ⊢ n ∈ ℕ → 5 ⋅ 4 ∈ ℂ
82 5nn0 ⊢ 5 ∈ ℕ 0
83 15 82 deccl ⊢ 15 ∈ ℕ 0
84 83 nn0cni ⊢ 15 ∈ ℂ
85 84 a1i ⊢ n ∈ ℕ → 15 ∈ ℂ
86 80 81 85 addsubassd ⊢ n ∈ ℕ → 4 n ⋅ 4 + 5 ⋅ 4 - 15 = 4 n ⋅ 4 + 5 ⋅ 4 - 15
87 79 86 eqtr4d ⊢ n ∈ ℕ → 4 n + 1 + 5 = 4 n ⋅ 4 + 5 ⋅ 4 - 15
88 57 62 87 3eqtr4rd ⊢ n ∈ ℕ → 4 n + 1 + 5 = 4 n + 5 ⋅ 4 − 3 ⋅ 5
89 88 adantr ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 4 n + 1 + 5 = 4 n + 5 ⋅ 4 − 3 ⋅ 5
90 52 89 breqtrrd ⊢ n ∈ ℕ ∧ 3 ∥ 4 n + 5 → 3 ∥ 4 n + 1 + 5
91 90 ex ⊢ n ∈ ℕ → 3 ∥ 4 n + 5 → 3 ∥ 4 n + 1 + 5
92 3 6 9 12 34 91 nnind ⊢ N ∈ ℕ → 3 ∥ 4 N + 5