Metamath Proof Explorer

Theorem inductionexd

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

Ref Expression
Assertion inductionexd 
|- ( N e. NN -> 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 e. ZZ
14 4z 
 |-  4 e. ZZ
15 1nn0 
 |-  1 e. NN0
16 zexpcl 
 |-  ( ( 4 e. ZZ /\ 1 e. NN0 ) -> ( 4 ^ 1 ) e. ZZ )
17 14 15 16 mp2an 
 |-  ( 4 ^ 1 ) e. ZZ
18 5nn 
 |-  5 e. NN
19 18 nnzi 
 |-  5 e. ZZ
20 zaddcl 
 |-  ( ( ( 4 ^ 1 ) e. ZZ /\ 5 e. ZZ ) -> ( ( 4 ^ 1 ) + 5 ) e. ZZ )
21 17 19 20 mp2an 
 |-  ( ( 4 ^ 1 ) + 5 ) e. ZZ
22 13 13 21 3pm3.2i 
 |-  ( 3 e. ZZ /\ 3 e. ZZ /\ ( ( 4 ^ 1 ) + 5 ) e. ZZ )
23 3t3e9 
 |-  ( 3 x. 3 ) = 9
24 4nn0 
 |-  4 e. NN0
25 24 numexp1 
 |-  ( 4 ^ 1 ) = 4
26 25 oveq1i 
 |-  ( ( 4 ^ 1 ) + 5 ) = ( 4 + 5 )
27 5cn 
 |-  5 e. CC
28 4cn 
 |-  4 e. CC
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 x. 3 ) = ( ( 4 ^ 1 ) + 5 )
33 dvds0lem 
 |-  ( ( ( 3 e. ZZ /\ 3 e. ZZ /\ ( ( 4 ^ 1 ) + 5 ) e. ZZ ) /\ ( 3 x. 3 ) = ( ( 4 ^ 1 ) + 5 ) ) -> 3 || ( ( 4 ^ 1 ) + 5 ) )
34 22 32 33 mp2an 
 |-  3 || ( ( 4 ^ 1 ) + 5 )
35 13 a1i 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> 3 e. ZZ )
36 4nn 
 |-  4 e. NN
37 36 a1i 
 |-  ( n e. NN -> 4 e. NN )
38 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
39 37 38 nnexpcld 
 |-  ( n e. NN -> ( 4 ^ n ) e. NN )
40 39 nnzd 
 |-  ( n e. NN -> ( 4 ^ n ) e. ZZ )
41 40 adantr 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> ( 4 ^ n ) e. ZZ )
42 19 a1i 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> 5 e. ZZ )
43 41 42 zaddcld 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> ( ( 4 ^ n ) + 5 ) e. ZZ )
44 14 a1i 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> 4 e. ZZ )
45 43 44 zmulcld 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> ( ( ( 4 ^ n ) + 5 ) x. 4 ) e. ZZ )
46 35 42 zmulcld 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> ( 3 x. 5 ) e. ZZ )
47 simpr 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> 3 || ( ( 4 ^ n ) + 5 ) )
48 35 43 44 47 dvdsmultr1d 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> 3 || ( ( ( 4 ^ n ) + 5 ) x. 4 ) )
49 dvdsmul1 
 |-  ( ( 3 e. ZZ /\ 5 e. ZZ ) -> 3 || ( 3 x. 5 ) )
50 13 19 49 mp2an 
 |-  3 || ( 3 x. 5 )
51 50 a1i 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> 3 || ( 3 x. 5 ) )
52 35 45 46 48 51 dvds2subd 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> 3 || ( ( ( ( 4 ^ n ) + 5 ) x. 4 ) - ( 3 x. 5 ) ) )
53 39 nncnd 
 |-  ( n e. NN -> ( 4 ^ n ) e. CC )
54 27 a1i 
 |-  ( n e. NN -> 5 e. CC )
55 28 a1i 
 |-  ( n e. NN -> 4 e. CC )
56 53 54 55 adddird 
 |-  ( n e. NN -> ( ( ( 4 ^ n ) + 5 ) x. 4 ) = ( ( ( 4 ^ n ) x. 4 ) + ( 5 x. 4 ) ) )
57 56 oveq1d 
 |-  ( n e. NN -> ( ( ( ( 4 ^ n ) + 5 ) x. 4 ) - ; 1 5 ) = ( ( ( ( 4 ^ n ) x. 4 ) + ( 5 x. 4 ) ) - ; 1 5 ) )
58 3cn 
 |-  3 e. CC
59 5t3e15 
 |-  ( 5 x. 3 ) = ; 1 5
60 27 58 59 mulcomli 
 |-  ( 3 x. 5 ) = ; 1 5
61 60 a1i 
 |-  ( n e. NN -> ( 3 x. 5 ) = ; 1 5 )
62 61 oveq2d 
 |-  ( n e. NN -> ( ( ( ( 4 ^ n ) + 5 ) x. 4 ) - ( 3 x. 5 ) ) = ( ( ( ( 4 ^ n ) + 5 ) x. 4 ) - ; 1 5 ) )
63 55 38 expp1d 
 |-  ( n e. NN -> ( 4 ^ ( n + 1 ) ) = ( ( 4 ^ n ) x. 4 ) )
64 ax-1cn 
 |-  1 e. CC
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 x. ( 4 - 3 ) ) = ( 5 x. 1 )
72 27 28 58 subdii 
 |-  ( 5 x. ( 4 - 3 ) ) = ( ( 5 x. 4 ) - ( 5 x. 3 ) )
73 27 mulid1i 
 |-  ( 5 x. 1 ) = 5
74 71 72 73 3eqtr3ri 
 |-  5 = ( ( 5 x. 4 ) - ( 5 x. 3 ) )
75 59 eqcomi 
 |-  ; 1 5 = ( 5 x. 3 )
76 75 oveq2i 
 |-  ( ( 5 x. 4 ) - ; 1 5 ) = ( ( 5 x. 4 ) - ( 5 x. 3 ) )
77 74 76 eqtr4i 
 |-  5 = ( ( 5 x. 4 ) - ; 1 5 )
78 77 a1i 
 |-  ( n e. NN -> 5 = ( ( 5 x. 4 ) - ; 1 5 ) )
79 63 78 oveq12d 
 |-  ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) + 5 ) = ( ( ( 4 ^ n ) x. 4 ) + ( ( 5 x. 4 ) - ; 1 5 ) ) )
80 53 55 mulcld 
 |-  ( n e. NN -> ( ( 4 ^ n ) x. 4 ) e. CC )
81 54 55 mulcld 
 |-  ( n e. NN -> ( 5 x. 4 ) e. CC )
82 5nn0 
 |-  5 e. NN0
83 15 82 deccl 
 |-  ; 1 5 e. NN0
84 83 nn0cni 
 |-  ; 1 5 e. CC
85 84 a1i 
 |-  ( n e. NN -> ; 1 5 e. CC )
86 80 81 85 addsubassd 
 |-  ( n e. NN -> ( ( ( ( 4 ^ n ) x. 4 ) + ( 5 x. 4 ) ) - ; 1 5 ) = ( ( ( 4 ^ n ) x. 4 ) + ( ( 5 x. 4 ) - ; 1 5 ) ) )
87 79 86 eqtr4d 
 |-  ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) + 5 ) = ( ( ( ( 4 ^ n ) x. 4 ) + ( 5 x. 4 ) ) - ; 1 5 ) )
88 57 62 87 3eqtr4rd 
 |-  ( n e. NN -> ( ( 4 ^ ( n + 1 ) ) + 5 ) = ( ( ( ( 4 ^ n ) + 5 ) x. 4 ) - ( 3 x. 5 ) ) )
89 88 adantr 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> ( ( 4 ^ ( n + 1 ) ) + 5 ) = ( ( ( ( 4 ^ n ) + 5 ) x. 4 ) - ( 3 x. 5 ) ) )
90 52 89 breqtrrd 
 |-  ( ( n e. NN /\ 3 || ( ( 4 ^ n ) + 5 ) ) -> 3 || ( ( 4 ^ ( n + 1 ) ) + 5 ) )
91 90 ex 
 |-  ( n e. NN -> ( 3 || ( ( 4 ^ n ) + 5 ) -> 3 || ( ( 4 ^ ( n + 1 ) ) + 5 ) ) )
92 3 6 9 12 34 91 nnind 
 |-  ( N e. NN -> 3 || ( ( 4 ^ N ) + 5 ) )