Step | Hyp | Ref
| Expression |
1 | | 9nn 12256 |
. . . 4
โข 9 โ
โ |
2 | 1 | elexi 3463 |
. . 3
โข 9 โ
V |
3 | | eleq1 2822 |
. . . 4
โข (๐ = 9 โ (๐ โ (โคโฅโ3)
โ 9 โ (โคโฅโ3))) |
4 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = 9 โ (8โ๐) = (8โ9)) |
5 | | id 22 |
. . . . . . . 8
โข (๐ = 9 โ ๐ = 9) |
6 | 4, 5 | oveq12d 7376 |
. . . . . . 7
โข (๐ = 9 โ ((8โ๐) mod ๐) = ((8โ9) mod 9)) |
7 | | oveq2 7366 |
. . . . . . 7
โข (๐ = 9 โ (8 mod ๐) = (8 mod 9)) |
8 | 6, 7 | eqeq12d 2749 |
. . . . . 6
โข (๐ = 9 โ (((8โ๐) mod ๐) = (8 mod ๐) โ ((8โ9) mod 9) = (8 mod
9))) |
9 | | eleq1 2822 |
. . . . . 6
โข (๐ = 9 โ (๐ โ โ โ 9 โ
โ)) |
10 | 8, 9 | imbi12d 345 |
. . . . 5
โข (๐ = 9 โ ((((8โ๐) mod ๐) = (8 mod ๐) โ ๐ โ โ) โ (((8โ9) mod 9) =
(8 mod 9) โ 9 โ โ))) |
11 | 10 | notbid 318 |
. . . 4
โข (๐ = 9 โ (ยฌ
(((8โ๐) mod ๐) = (8 mod ๐) โ ๐ โ โ) โ ยฌ (((8โ9)
mod 9) = (8 mod 9) โ 9 โ โ))) |
12 | 3, 11 | anbi12d 632 |
. . 3
โข (๐ = 9 โ ((๐ โ (โคโฅโ3)
โง ยฌ (((8โ๐)
mod ๐) = (8 mod ๐) โ ๐ โ โ)) โ (9 โ
(โคโฅโ3) โง ยฌ (((8โ9) mod 9) = (8 mod 9)
โ 9 โ โ)))) |
13 | | 3z 12541 |
. . . . 5
โข 3 โ
โค |
14 | 1 | nnzi 12532 |
. . . . 5
โข 9 โ
โค |
15 | | 3re 12238 |
. . . . . 6
โข 3 โ
โ |
16 | | 9re 12257 |
. . . . . 6
โข 9 โ
โ |
17 | | 3lt9 12362 |
. . . . . 6
โข 3 <
9 |
18 | 15, 16, 17 | ltleii 11283 |
. . . . 5
โข 3 โค
9 |
19 | | eluz2 12774 |
. . . . 5
โข (9 โ
(โคโฅโ3) โ (3 โ โค โง 9 โ
โค โง 3 โค 9)) |
20 | 13, 14, 18, 19 | mpbir3an 1342 |
. . . 4
โข 9 โ
(โคโฅโ3) |
21 | | 8nn 12253 |
. . . . . . 7
โข 8 โ
โ |
22 | | 8nn0 12441 |
. . . . . . 7
โข 8 โ
โ0 |
23 | | 0z 12515 |
. . . . . . 7
โข 0 โ
โค |
24 | | 1nn0 12434 |
. . . . . . 7
โข 1 โ
โ0 |
25 | | 8exp8mod9 46014 |
. . . . . . . 8
โข
((8โ8) mod 9) = 1 |
26 | | 1re 11160 |
. . . . . . . . 9
โข 1 โ
โ |
27 | | nnrp 12931 |
. . . . . . . . . 10
โข (9 โ
โ โ 9 โ โ+) |
28 | 1, 27 | ax-mp 5 |
. . . . . . . . 9
โข 9 โ
โ+ |
29 | | 0le1 11683 |
. . . . . . . . 9
โข 0 โค
1 |
30 | | 1lt9 12364 |
. . . . . . . . 9
โข 1 <
9 |
31 | | modid 13807 |
. . . . . . . . 9
โข (((1
โ โ โง 9 โ โ+) โง (0 โค 1 โง 1 <
9)) โ (1 mod 9) = 1) |
32 | 26, 28, 29, 30, 31 | mp4an 692 |
. . . . . . . 8
โข (1 mod 9)
= 1 |
33 | 25, 32 | eqtr4i 2764 |
. . . . . . 7
โข
((8โ8) mod 9) = (1 mod 9) |
34 | | 8p1e9 12308 |
. . . . . . 7
โข (8 + 1) =
9 |
35 | | 8cn 12255 |
. . . . . . . . 9
โข 8 โ
โ |
36 | 35 | addid2i 11348 |
. . . . . . . 8
โข (0 + 8) =
8 |
37 | | 9cn 12258 |
. . . . . . . . . 10
โข 9 โ
โ |
38 | 37 | mul02i 11349 |
. . . . . . . . 9
โข (0
ยท 9) = 0 |
39 | 38 | oveq1i 7368 |
. . . . . . . 8
โข ((0
ยท 9) + 8) = (0 + 8) |
40 | 35 | mulid2i 11165 |
. . . . . . . 8
โข (1
ยท 8) = 8 |
41 | 36, 39, 40 | 3eqtr4i 2771 |
. . . . . . 7
โข ((0
ยท 9) + 8) = (1 ยท 8) |
42 | 1, 21, 22, 23, 24, 22, 33, 34, 41 | modxp1i 16947 |
. . . . . 6
โข
((8โ9) mod 9) = (8 mod 9) |
43 | | 9nprm 16990 |
. . . . . 6
โข ยฌ 9
โ โ |
44 | 42, 43 | pm3.2i 472 |
. . . . 5
โข
(((8โ9) mod 9) = (8 mod 9) โง ยฌ 9 โ
โ) |
45 | | annim 405 |
. . . . 5
โข
((((8โ9) mod 9) = (8 mod 9) โง ยฌ 9 โ โ) โ
ยฌ (((8โ9) mod 9) = (8 mod 9) โ 9 โ
โ)) |
46 | 44, 45 | mpbi 229 |
. . . 4
โข ยฌ
(((8โ9) mod 9) = (8 mod 9) โ 9 โ โ) |
47 | 20, 46 | pm3.2i 472 |
. . 3
โข (9 โ
(โคโฅโ3) โง ยฌ (((8โ9) mod 9) = (8 mod 9)
โ 9 โ โ)) |
48 | 2, 12, 47 | ceqsexv2d 3496 |
. 2
โข
โ๐(๐ โ
(โคโฅโ3) โง ยฌ (((8โ๐) mod ๐) = (8 mod ๐) โ ๐ โ โ)) |
49 | | df-rex 3071 |
. 2
โข
(โ๐ โ
(โคโฅโ3) ยฌ (((8โ๐) mod ๐) = (8 mod ๐) โ ๐ โ โ) โ โ๐(๐ โ (โคโฅโ3)
โง ยฌ (((8โ๐)
mod ๐) = (8 mod ๐) โ ๐ โ โ))) |
50 | 48, 49 | mpbir 230 |
1
โข
โ๐ โ
(โคโฅโ3) ยฌ (((8โ๐) mod ๐) = (8 mod ๐) โ ๐ โ โ) |