Step | Hyp | Ref
| Expression |
1 | | decex 12681 |
. . 3
โข ;;341 โ V |
2 | | eleq1 2822 |
. . . 4
โข (๐ = ;;341
โ (๐ โ
(โคโฅโ3) โ ;;341
โ (โคโฅโ3))) |
3 | | oveq2 7417 |
. . . . . . . 8
โข (๐ = ;;341
โ (2โ๐) =
(2โ;;341)) |
4 | | id 22 |
. . . . . . . 8
โข (๐ = ;;341
โ ๐ = ;;341) |
5 | 3, 4 | oveq12d 7427 |
. . . . . . 7
โข (๐ = ;;341
โ ((2โ๐) mod
๐) = ((2โ;;341) mod ;;341)) |
6 | | oveq2 7417 |
. . . . . . 7
โข (๐ = ;;341
โ (2 mod ๐) = (2 mod
;;341)) |
7 | 5, 6 | eqeq12d 2749 |
. . . . . 6
โข (๐ = ;;341
โ (((2โ๐) mod
๐) = (2 mod ๐) โ ((2โ;;341) mod ;;341) =
(2 mod ;;341))) |
8 | | eleq1 2822 |
. . . . . 6
โข (๐ = ;;341
โ (๐ โ โ
โ ;;341 โ โ)) |
9 | 7, 8 | imbi12d 345 |
. . . . 5
โข (๐ = ;;341
โ ((((2โ๐) mod
๐) = (2 mod ๐) โ ๐ โ โ) โ (((2โ;;341) mod ;;341) =
(2 mod ;;341) โ ;;341
โ โ))) |
10 | 9 | notbid 318 |
. . . 4
โข (๐ = ;;341
โ (ยฌ (((2โ๐)
mod ๐) = (2 mod ๐) โ ๐ โ โ) โ ยฌ (((2โ;;341) mod ;;341) =
(2 mod ;;341) โ ;;341
โ โ))) |
11 | 2, 10 | anbi12d 632 |
. . 3
โข (๐ = ;;341
โ ((๐ โ
(โคโฅโ3) โง ยฌ (((2โ๐) mod ๐) = (2 mod ๐) โ ๐ โ โ)) โ (;;341
โ (โคโฅโ3) โง ยฌ (((2โ;;341) mod ;;341) =
(2 mod ;;341) โ ;;341
โ โ)))) |
12 | | 3z 12595 |
. . . . 5
โข 3 โ
โค |
13 | | 3nn0 12490 |
. . . . . . . 8
โข 3 โ
โ0 |
14 | | 4nn0 12491 |
. . . . . . . 8
โข 4 โ
โ0 |
15 | 13, 14 | deccl 12692 |
. . . . . . 7
โข ;34 โ
โ0 |
16 | | 1nn0 12488 |
. . . . . . 7
โข 1 โ
โ0 |
17 | 15, 16 | deccl 12692 |
. . . . . 6
โข ;;341 โ โ0 |
18 | 17 | nn0zi 12587 |
. . . . 5
โข ;;341 โ โค |
19 | 13 | dec0h 12699 |
. . . . . 6
โข 3 = ;03 |
20 | | 0nn0 12487 |
. . . . . . 7
โข 0 โ
โ0 |
21 | | 3re 12292 |
. . . . . . . 8
โข 3 โ
โ |
22 | | 9re 12311 |
. . . . . . . 8
โข 9 โ
โ |
23 | | 3lt9 12416 |
. . . . . . . 8
โข 3 <
9 |
24 | 21, 22, 23 | ltleii 11337 |
. . . . . . 7
โข 3 โค
9 |
25 | | 3nn 12291 |
. . . . . . . 8
โข 3 โ
โ |
26 | | 0re 11216 |
. . . . . . . . 9
โข 0 โ
โ |
27 | | 9pos 12325 |
. . . . . . . . 9
โข 0 <
9 |
28 | 26, 22, 27 | ltleii 11337 |
. . . . . . . 8
โข 0 โค
9 |
29 | 25, 14, 20, 28 | decltdi 12716 |
. . . . . . 7
โข 0 <
;34 |
30 | 20, 15, 13, 16, 24, 29 | decleh 12712 |
. . . . . 6
โข ;03 โค ;;341 |
31 | 19, 30 | eqbrtri 5170 |
. . . . 5
โข 3 โค
;;341 |
32 | | eluz2 12828 |
. . . . 5
โข (;;341 โ (โคโฅโ3) โ
(3 โ โค โง ;;341 โ โค โง 3 โค ;;341)) |
33 | 12, 18, 31, 32 | mpbir3an 1342 |
. . . 4
โข ;;341 โ
(โคโฅโ3) |
34 | | 341fppr2 46402 |
. . . . . . 7
โข ;;341 โ ( FPPr โ2) |
35 | | fpprwppr 46407 |
. . . . . . 7
โข (;;341 โ ( FPPr โ2) โ ((2โ;;341) mod ;;341) =
(2 mod ;;341)) |
36 | 34, 35 | ax-mp 5 |
. . . . . 6
โข
((2โ;;341) mod ;;341) =
(2 mod ;;341) |
37 | | 11t31e341 46400 |
. . . . . . . 8
โข (;11 ยท ;31) = ;;341 |
38 | 37 | eqcomi 2742 |
. . . . . . 7
โข ;;341 = (;11 ยท ;31) |
39 | | 2z 12594 |
. . . . . . . . 9
โข 2 โ
โค |
40 | 16, 16 | deccl 12692 |
. . . . . . . . . 10
โข ;11 โ
โ0 |
41 | 40 | nn0zi 12587 |
. . . . . . . . 9
โข ;11 โ โค |
42 | | 2nn0 12489 |
. . . . . . . . . . 11
โข 2 โ
โ0 |
43 | 42 | dec0h 12699 |
. . . . . . . . . 10
โข 2 = ;02 |
44 | | 2re 12286 |
. . . . . . . . . . . 12
โข 2 โ
โ |
45 | | 2lt9 12417 |
. . . . . . . . . . . 12
โข 2 <
9 |
46 | 44, 22, 45 | ltleii 11337 |
. . . . . . . . . . 11
โข 2 โค
9 |
47 | | 0lt1 11736 |
. . . . . . . . . . 11
โข 0 <
1 |
48 | 20, 16, 42, 16, 46, 47 | decleh 12712 |
. . . . . . . . . 10
โข ;02 โค ;11 |
49 | 43, 48 | eqbrtri 5170 |
. . . . . . . . 9
โข 2 โค
;11 |
50 | | eluz2 12828 |
. . . . . . . . 9
โข (;11 โ
(โคโฅโ2) โ (2 โ โค โง ;11 โ โค โง 2 โค ;11)) |
51 | 39, 41, 49, 50 | mpbir3an 1342 |
. . . . . . . 8
โข ;11 โ
(โคโฅโ2) |
52 | 13, 16 | deccl 12692 |
. . . . . . . . . 10
โข ;31 โ
โ0 |
53 | 52 | nn0zi 12587 |
. . . . . . . . 9
โข ;31 โ โค |
54 | | 3pos 12317 |
. . . . . . . . . . 11
โข 0 <
3 |
55 | 20, 13, 42, 16, 46, 54 | decleh 12712 |
. . . . . . . . . 10
โข ;02 โค ;31 |
56 | 43, 55 | eqbrtri 5170 |
. . . . . . . . 9
โข 2 โค
;31 |
57 | | eluz2 12828 |
. . . . . . . . 9
โข (;31 โ
(โคโฅโ2) โ (2 โ โค โง ;31 โ โค โง 2 โค ;31)) |
58 | 39, 53, 56, 57 | mpbir3an 1342 |
. . . . . . . 8
โข ;31 โ
(โคโฅโ2) |
59 | | nprm 16625 |
. . . . . . . 8
โข ((;11 โ
(โคโฅโ2) โง ;31 โ (โคโฅโ2)) โ
ยฌ (;11 ยท ;31) โ โ) |
60 | 51, 58, 59 | mp2an 691 |
. . . . . . 7
โข ยฌ
(;11 ยท ;31) โ โ |
61 | 38, 60 | eqneltri 2853 |
. . . . . 6
โข ยฌ
;;341 โ โ |
62 | 36, 61 | pm3.2i 472 |
. . . . 5
โข
(((2โ;;341) mod ;;341) =
(2 mod ;;341) โง ยฌ ;;341
โ โ) |
63 | | annim 405 |
. . . . 5
โข
((((2โ;;341) mod ;;341) =
(2 mod ;;341) โง ยฌ ;;341
โ โ) โ ยฌ (((2โ;;341)
mod ;;341) = (2 mod ;;341)
โ ;;341 โ โ)) |
64 | 62, 63 | mpbi 229 |
. . . 4
โข ยฌ
(((2โ;;341) mod ;;341) =
(2 mod ;;341) โ ;;341
โ โ) |
65 | 33, 64 | pm3.2i 472 |
. . 3
โข (;;341 โ (โคโฅโ3) โง
ยฌ (((2โ;;341) mod ;;341) =
(2 mod ;;341) โ ;;341
โ โ)) |
66 | 1, 11, 65 | ceqsexv2d 3529 |
. 2
โข
โ๐(๐ โ
(โคโฅโ3) โง ยฌ (((2โ๐) mod ๐) = (2 mod ๐) โ ๐ โ โ)) |
67 | | df-rex 3072 |
. 2
โข
(โ๐ โ
(โคโฅโ3) ยฌ (((2โ๐) mod ๐) = (2 mod ๐) โ ๐ โ โ) โ โ๐(๐ โ (โคโฅโ3)
โง ยฌ (((2โ๐)
mod ๐) = (2 mod ๐) โ ๐ โ โ))) |
68 | 66, 67 | mpbir 230 |
1
โข
โ๐ โ
(โคโฅโ3) ยฌ (((2โ๐) mod ๐) = (2 mod ๐) โ ๐ โ โ) |