Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . 4
โข (๐ = 0 โ (4โ๐) = (4โ0)) |
2 | 1 | oveq1d 7377 |
. . 3
โข (๐ = 0 โ ((4โ๐) + 2) = ((4โ0) +
2)) |
3 | 2 | breq2d 5122 |
. 2
โข (๐ = 0 โ (3 โฅ
((4โ๐) + 2) โ 3
โฅ ((4โ0) + 2))) |
4 | | oveq2 7370 |
. . . 4
โข (๐ = ๐ โ (4โ๐) = (4โ๐)) |
5 | 4 | oveq1d 7377 |
. . 3
โข (๐ = ๐ โ ((4โ๐) + 2) = ((4โ๐) + 2)) |
6 | 5 | breq2d 5122 |
. 2
โข (๐ = ๐ โ (3 โฅ ((4โ๐) + 2) โ 3 โฅ
((4โ๐) +
2))) |
7 | | oveq2 7370 |
. . . 4
โข (๐ = (๐ + 1) โ (4โ๐) = (4โ(๐ + 1))) |
8 | 7 | oveq1d 7377 |
. . 3
โข (๐ = (๐ + 1) โ ((4โ๐) + 2) = ((4โ(๐ + 1)) + 2)) |
9 | 8 | breq2d 5122 |
. 2
โข (๐ = (๐ + 1) โ (3 โฅ ((4โ๐) + 2) โ 3 โฅ
((4โ(๐ + 1)) +
2))) |
10 | | oveq2 7370 |
. . . 4
โข (๐ = ๐ โ (4โ๐) = (4โ๐)) |
11 | 10 | oveq1d 7377 |
. . 3
โข (๐ = ๐ โ ((4โ๐) + 2) = ((4โ๐) + 2)) |
12 | 11 | breq2d 5122 |
. 2
โข (๐ = ๐ โ (3 โฅ ((4โ๐) + 2) โ 3 โฅ
((4โ๐) +
2))) |
13 | | 3z 12543 |
. . . 4
โข 3 โ
โค |
14 | | iddvds 16159 |
. . . 4
โข (3 โ
โค โ 3 โฅ 3) |
15 | 13, 14 | ax-mp 5 |
. . 3
โข 3 โฅ
3 |
16 | | 4nn0 12439 |
. . . . . 6
โข 4 โ
โ0 |
17 | 16 | numexp0 16955 |
. . . . 5
โข
(4โ0) = 1 |
18 | 17 | oveq1i 7372 |
. . . 4
โข
((4โ0) + 2) = (1 + 2) |
19 | | 1p2e3 12303 |
. . . 4
โข (1 + 2) =
3 |
20 | 18, 19 | eqtri 2765 |
. . 3
โข
((4โ0) + 2) = 3 |
21 | 15, 20 | breqtrri 5137 |
. 2
โข 3 โฅ
((4โ0) + 2) |
22 | 13 | a1i 11 |
. . . . 5
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ 3 โ โค) |
23 | 16 | a1i 11 |
. . . . . . . . 9
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ 4 โ โ0) |
24 | | simpl 484 |
. . . . . . . . 9
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ ๐ โ
โ0) |
25 | 23, 24 | nn0expcld 14156 |
. . . . . . . 8
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ (4โ๐)
โ โ0) |
26 | 25 | nn0zd 12532 |
. . . . . . 7
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ (4โ๐)
โ โค) |
27 | | 2z 12542 |
. . . . . . . 8
โข 2 โ
โค |
28 | 27 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ 2 โ โค) |
29 | 26, 28 | zaddcld 12618 |
. . . . . 6
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ ((4โ๐) +
2) โ โค) |
30 | | 4z 12544 |
. . . . . . 7
โข 4 โ
โค |
31 | 30 | a1i 11 |
. . . . . 6
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ 4 โ โค) |
32 | 29, 31 | zmulcld 12620 |
. . . . 5
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ (((4โ๐) +
2) ยท 4) โ โค) |
33 | 22, 28 | zmulcld 12620 |
. . . . 5
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ (3 ยท 2) โ โค) |
34 | 16 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 4 โ โ0) |
35 | | id 22 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ๐ โ
โ0) |
36 | 34, 35 | nn0expcld 14156 |
. . . . . . . . 9
โข (๐ โ โ0
โ (4โ๐) โ
โ0) |
37 | 36 | nn0zd 12532 |
. . . . . . . 8
โข (๐ โ โ0
โ (4โ๐) โ
โค) |
38 | 37 | adantr 482 |
. . . . . . 7
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ (4โ๐)
โ โค) |
39 | 38, 28 | zaddcld 12618 |
. . . . . 6
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ ((4โ๐) +
2) โ โค) |
40 | | simpr 486 |
. . . . . 6
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ 3 โฅ ((4โ๐) + 2)) |
41 | 22, 39, 31, 40 | dvdsmultr1d 16186 |
. . . . 5
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ 3 โฅ (((4โ๐) + 2) ยท 4)) |
42 | | dvdsmul1 16167 |
. . . . . . 7
โข ((3
โ โค โง 2 โ โค) โ 3 โฅ (3 ยท
2)) |
43 | 13, 27, 42 | mp2an 691 |
. . . . . 6
โข 3 โฅ
(3 ยท 2) |
44 | 43 | a1i 11 |
. . . . 5
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ 3 โฅ (3 ยท 2)) |
45 | 22, 32, 33, 41, 44 | dvds2subd 16182 |
. . . 4
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ 3 โฅ ((((4โ๐) + 2) ยท 4) โ (3 ยท
2))) |
46 | 36 | nn0cnd 12482 |
. . . . . . . 8
โข (๐ โ โ0
โ (4โ๐) โ
โ) |
47 | | 2cnd 12238 |
. . . . . . . 8
โข (๐ โ โ0
โ 2 โ โ) |
48 | | 4cn 12245 |
. . . . . . . . 9
โข 4 โ
โ |
49 | 48 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ0
โ 4 โ โ) |
50 | 46, 47, 49 | adddird 11187 |
. . . . . . 7
โข (๐ โ โ0
โ (((4โ๐) + 2)
ยท 4) = (((4โ๐)
ยท 4) + (2 ยท 4))) |
51 | 50 | oveq1d 7377 |
. . . . . 6
โข (๐ โ โ0
โ ((((4โ๐) + 2)
ยท 4) โ (2 ยท 3)) = ((((4โ๐) ยท 4) + (2 ยท 4)) โ (2
ยท 3))) |
52 | | 3cn 12241 |
. . . . . . . . 9
โข 3 โ
โ |
53 | | 2cn 12235 |
. . . . . . . . 9
โข 2 โ
โ |
54 | 52, 53 | mulcomi 11170 |
. . . . . . . 8
โข (3
ยท 2) = (2 ยท 3) |
55 | 54 | a1i 11 |
. . . . . . 7
โข (๐ โ โ0
โ (3 ยท 2) = (2 ยท 3)) |
56 | 55 | oveq2d 7378 |
. . . . . 6
โข (๐ โ โ0
โ ((((4โ๐) + 2)
ยท 4) โ (3 ยท 2)) = ((((4โ๐) + 2) ยท 4) โ (2 ยท
3))) |
57 | 49, 35 | expp1d 14059 |
. . . . . . . 8
โข (๐ โ โ0
โ (4โ(๐ + 1)) =
((4โ๐) ยท
4)) |
58 | | ax-1cn 11116 |
. . . . . . . . . . . 12
โข 1 โ
โ |
59 | | 3p1e4 12305 |
. . . . . . . . . . . . . 14
โข (3 + 1) =
4 |
60 | 52, 58, 59 | addcomli 11354 |
. . . . . . . . . . . . 13
โข (1 + 3) =
4 |
61 | 60 | eqcomi 2746 |
. . . . . . . . . . . 12
โข 4 = (1 +
3) |
62 | 58, 52, 61 | mvrraddi 11425 |
. . . . . . . . . . 11
โข (4
โ 3) = 1 |
63 | 62 | oveq2i 7373 |
. . . . . . . . . 10
โข (2
ยท (4 โ 3)) = (2 ยท 1) |
64 | 53, 48, 52 | subdii 11611 |
. . . . . . . . . 10
โข (2
ยท (4 โ 3)) = ((2 ยท 4) โ (2 ยท
3)) |
65 | | 2t1e2 12323 |
. . . . . . . . . 10
โข (2
ยท 1) = 2 |
66 | 63, 64, 65 | 3eqtr3ri 2774 |
. . . . . . . . 9
โข 2 = ((2
ยท 4) โ (2 ยท 3)) |
67 | 66 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ0
โ 2 = ((2 ยท 4) โ (2 ยท 3))) |
68 | 57, 67 | oveq12d 7380 |
. . . . . . 7
โข (๐ โ โ0
โ ((4โ(๐ + 1)) +
2) = (((4โ๐) ยท
4) + ((2 ยท 4) โ (2 ยท 3)))) |
69 | 46, 49 | mulcld 11182 |
. . . . . . . 8
โข (๐ โ โ0
โ ((4โ๐) ยท
4) โ โ) |
70 | 47, 49 | mulcld 11182 |
. . . . . . . 8
โข (๐ โ โ0
โ (2 ยท 4) โ โ) |
71 | 52 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ0
โ 3 โ โ) |
72 | 47, 71 | mulcld 11182 |
. . . . . . . 8
โข (๐ โ โ0
โ (2 ยท 3) โ โ) |
73 | 69, 70, 72 | addsubassd 11539 |
. . . . . . 7
โข (๐ โ โ0
โ ((((4โ๐)
ยท 4) + (2 ยท 4)) โ (2 ยท 3)) = (((4โ๐) ยท 4) + ((2 ยท 4)
โ (2 ยท 3)))) |
74 | 68, 73 | eqtr4d 2780 |
. . . . . 6
โข (๐ โ โ0
โ ((4โ(๐ + 1)) +
2) = ((((4โ๐) ยท
4) + (2 ยท 4)) โ (2 ยท 3))) |
75 | 51, 56, 74 | 3eqtr4rd 2788 |
. . . . 5
โข (๐ โ โ0
โ ((4โ(๐ + 1)) +
2) = ((((4โ๐) + 2)
ยท 4) โ (3 ยท 2))) |
76 | 75 | adantr 482 |
. . . 4
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ ((4โ(๐ +
1)) + 2) = ((((4โ๐) +
2) ยท 4) โ (3 ยท 2))) |
77 | 45, 76 | breqtrrd 5138 |
. . 3
โข ((๐ โ โ0
โง 3 โฅ ((4โ๐)
+ 2)) โ 3 โฅ ((4โ(๐ + 1)) + 2)) |
78 | 77 | ex 414 |
. 2
โข (๐ โ โ0
โ (3 โฅ ((4โ๐) + 2) โ 3 โฅ ((4โ(๐ + 1)) + 2))) |
79 | 3, 6, 9, 12, 21, 78 | nn0ind 12605 |
1
โข (๐ โ โ0
โ 3 โฅ ((4โ๐) + 2)) |