This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( N e. NN0 -> 3 || ( ( 4 ^ N ) + 2 ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( k = 0 -> ( 4 ^ k ) = ( 4 ^ 0 ) )
2 1 oveq1d 
 |-  ( k = 0 -> ( ( 4 ^ k ) + 2 ) = ( ( 4 ^ 0 ) + 2 ) )
3 2 breq2d 
 |-  ( k = 0 -> ( 3 || ( ( 4 ^ k ) + 2 ) <-> 3 || ( ( 4 ^ 0 ) + 2 ) ) )
4 oveq2 
 |-  ( k = n -> ( 4 ^ k ) = ( 4 ^ n ) )
5 4 oveq1d 
 |-  ( k = n -> ( ( 4 ^ k ) + 2 ) = ( ( 4 ^ n ) + 2 ) )
6 5 breq2d 
 |-  ( k = n -> ( 3 || ( ( 4 ^ k ) + 2 ) <-> 3 || ( ( 4 ^ n ) + 2 ) ) )
7 oveq2 
 |-  ( k = ( n + 1 ) -> ( 4 ^ k ) = ( 4 ^ ( n + 1 ) ) )
8 7 oveq1d 
 |-  ( k = ( n + 1 ) -> ( ( 4 ^ k ) + 2 ) = ( ( 4 ^ ( n + 1 ) ) + 2 ) )
9 8 breq2d 
 |-  ( k = ( n + 1 ) -> ( 3 || ( ( 4 ^ k ) + 2 ) <-> 3 || ( ( 4 ^ ( n + 1 ) ) + 2 ) ) )
10 oveq2 
 |-  ( k = N -> ( 4 ^ k ) = ( 4 ^ N ) )
11 10 oveq1d 
 |-  ( k = N -> ( ( 4 ^ k ) + 2 ) = ( ( 4 ^ N ) + 2 ) )
12 11 breq2d 
 |-  ( k = N -> ( 3 || ( ( 4 ^ k ) + 2 ) <-> 3 || ( ( 4 ^ N ) + 2 ) ) )
13 3z 
 |-  3 e. ZZ
14 iddvds 
 |-  ( 3 e. ZZ -> 3 || 3 )
15 13 14 ax-mp 
 |-  3 || 3
16 4nn0 
 |-  4 e. NN0
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 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> 3 e. ZZ )
23 16 a1i 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> 4 e. NN0 )
24 simpl 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> n e. NN0 )
25 23 24 nn0expcld 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> ( 4 ^ n ) e. NN0 )
26 25 nn0zd 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> ( 4 ^ n ) e. ZZ )
27 2z 
 |-  2 e. ZZ
28 27 a1i 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> 2 e. ZZ )
29 26 28 zaddcld 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> ( ( 4 ^ n ) + 2 ) e. ZZ )
30 4z 
 |-  4 e. ZZ
31 30 a1i 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> 4 e. ZZ )
32 29 31 zmulcld 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> ( ( ( 4 ^ n ) + 2 ) x. 4 ) e. ZZ )
33 22 28 zmulcld 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> ( 3 x. 2 ) e. ZZ )
34 16 a1i 
 |-  ( n e. NN0 -> 4 e. NN0 )
35 id 
 |-  ( n e. NN0 -> n e. NN0 )
36 34 35 nn0expcld 
 |-  ( n e. NN0 -> ( 4 ^ n ) e. NN0 )
37 36 nn0zd 
 |-  ( n e. NN0 -> ( 4 ^ n ) e. ZZ )
38 37 adantr 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> ( 4 ^ n ) e. ZZ )
39 38 28 zaddcld 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> ( ( 4 ^ n ) + 2 ) e. ZZ )
40 simpr 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> 3 || ( ( 4 ^ n ) + 2 ) )
41 22 39 31 40 dvdsmultr1d 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> 3 || ( ( ( 4 ^ n ) + 2 ) x. 4 ) )
42 dvdsmul1 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ ) -> 3 || ( 3 x. 2 ) )
43 13 27 42 mp2an 
 |-  3 || ( 3 x. 2 )
44 43 a1i 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> 3 || ( 3 x. 2 ) )
45 22 32 33 41 44 dvds2subd 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> 3 || ( ( ( ( 4 ^ n ) + 2 ) x. 4 ) - ( 3 x. 2 ) ) )
46 36 nn0cnd 
 |-  ( n e. NN0 -> ( 4 ^ n ) e. CC )
47 2cnd 
 |-  ( n e. NN0 -> 2 e. CC )
48 4cn 
 |-  4 e. CC
49 48 a1i 
 |-  ( n e. NN0 -> 4 e. CC )
50 46 47 49 adddird 
 |-  ( n e. NN0 -> ( ( ( 4 ^ n ) + 2 ) x. 4 ) = ( ( ( 4 ^ n ) x. 4 ) + ( 2 x. 4 ) ) )
51 50 oveq1d 
 |-  ( n e. NN0 -> ( ( ( ( 4 ^ n ) + 2 ) x. 4 ) - ( 2 x. 3 ) ) = ( ( ( ( 4 ^ n ) x. 4 ) + ( 2 x. 4 ) ) - ( 2 x. 3 ) ) )
52 3cn 
 |-  3 e. CC
53 2cn 
 |-  2 e. CC
54 52 53 mulcomi 
 |-  ( 3 x. 2 ) = ( 2 x. 3 )
55 54 a1i 
 |-  ( n e. NN0 -> ( 3 x. 2 ) = ( 2 x. 3 ) )
56 55 oveq2d 
 |-  ( n e. NN0 -> ( ( ( ( 4 ^ n ) + 2 ) x. 4 ) - ( 3 x. 2 ) ) = ( ( ( ( 4 ^ n ) + 2 ) x. 4 ) - ( 2 x. 3 ) ) )
57 49 35 expp1d 
 |-  ( n e. NN0 -> ( 4 ^ ( n + 1 ) ) = ( ( 4 ^ n ) x. 4 ) )
58 ax-1cn 
 |-  1 e. CC
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 x. ( 4 - 3 ) ) = ( 2 x. 1 )
64 53 48 52 subdii 
 |-  ( 2 x. ( 4 - 3 ) ) = ( ( 2 x. 4 ) - ( 2 x. 3 ) )
65 2t1e2 
 |-  ( 2 x. 1 ) = 2
66 63 64 65 3eqtr3ri 
 |-  2 = ( ( 2 x. 4 ) - ( 2 x. 3 ) )
67 66 a1i 
 |-  ( n e. NN0 -> 2 = ( ( 2 x. 4 ) - ( 2 x. 3 ) ) )
68 57 67 oveq12d 
 |-  ( n e. NN0 -> ( ( 4 ^ ( n + 1 ) ) + 2 ) = ( ( ( 4 ^ n ) x. 4 ) + ( ( 2 x. 4 ) - ( 2 x. 3 ) ) ) )
69 46 49 mulcld 
 |-  ( n e. NN0 -> ( ( 4 ^ n ) x. 4 ) e. CC )
70 47 49 mulcld 
 |-  ( n e. NN0 -> ( 2 x. 4 ) e. CC )
71 52 a1i 
 |-  ( n e. NN0 -> 3 e. CC )
72 47 71 mulcld 
 |-  ( n e. NN0 -> ( 2 x. 3 ) e. CC )
73 69 70 72 addsubassd 
 |-  ( n e. NN0 -> ( ( ( ( 4 ^ n ) x. 4 ) + ( 2 x. 4 ) ) - ( 2 x. 3 ) ) = ( ( ( 4 ^ n ) x. 4 ) + ( ( 2 x. 4 ) - ( 2 x. 3 ) ) ) )
74 68 73 eqtr4d 
 |-  ( n e. NN0 -> ( ( 4 ^ ( n + 1 ) ) + 2 ) = ( ( ( ( 4 ^ n ) x. 4 ) + ( 2 x. 4 ) ) - ( 2 x. 3 ) ) )
75 51 56 74 3eqtr4rd 
 |-  ( n e. NN0 -> ( ( 4 ^ ( n + 1 ) ) + 2 ) = ( ( ( ( 4 ^ n ) + 2 ) x. 4 ) - ( 3 x. 2 ) ) )
76 75 adantr 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> ( ( 4 ^ ( n + 1 ) ) + 2 ) = ( ( ( ( 4 ^ n ) + 2 ) x. 4 ) - ( 3 x. 2 ) ) )
77 45 76 breqtrrd 
 |-  ( ( n e. NN0 /\ 3 || ( ( 4 ^ n ) + 2 ) ) -> 3 || ( ( 4 ^ ( n + 1 ) ) + 2 ) )
78 77 ex 
 |-  ( n e. NN0 -> ( 3 || ( ( 4 ^ n ) + 2 ) -> 3 || ( ( 4 ^ ( n + 1 ) ) + 2 ) ) )
79 3 6 9 12 21 78 nn0ind 
 |-  ( N e. NN0 -> 3 || ( ( 4 ^ N ) + 2 ) )