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 simpr n 3 4 n + 5 3 4 n + 5
46 35 43 44 45 dvdsmultr1d n 3 4 n + 5 3 4 n + 5 4
47 dvdsmul1 3 5 3 3 5
48 13 19 47 mp2an 3 3 5
49 48 a1i n 3 4 n + 5 3 3 5
50 43 44 zmulcld n 3 4 n + 5 4 n + 5 4
51 35 42 zmulcld n 3 4 n + 5 3 5
52 35 46 49 50 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