Step | Hyp | Ref
| Expression |
1 | | fmtnorn 45800 |
. 2
โข (๐น โ ran FermatNo โ
โ๐ โ
โ0 (FermatNoโ๐) = ๐น) |
2 | | fmtnorn 45800 |
. 2
โข (๐บ โ ran FermatNo โ
โ๐ โ
โ0 (FermatNoโ๐) = ๐บ) |
3 | | 2a1 28 |
. . . . . . . 8
โข (๐น = ๐บ โ ((FermatNoโ๐) = ๐น โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ))) |
4 | 3 | 2a1d 26 |
. . . . . . 7
โข (๐น = ๐บ โ ((๐ โ โ0 โง ๐ โ โ0)
โ ((FermatNoโ๐)
= ๐บ โ
((FermatNoโ๐) = ๐น โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ))))) |
5 | | fmtnonn 45797 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (FermatNoโ๐)
โ โ) |
6 | 5 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โ (FermatNoโ๐)
โ โ) |
7 | 6 | adantr 482 |
. . . . . . . . . 10
โข (((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โง ((FermatNoโ๐) =
๐บ โง
(FermatNoโ๐) = ๐น)) โ (FermatNoโ๐) โ
โ) |
8 | | eleq1 2826 |
. . . . . . . . . . 11
โข
((FermatNoโ๐)
= ๐น โ
((FermatNoโ๐) โ
โ โ ๐น โ
โ)) |
9 | 8 | ad2antll 728 |
. . . . . . . . . 10
โข (((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โง ((FermatNoโ๐) =
๐บ โง
(FermatNoโ๐) = ๐น)) โ ((FermatNoโ๐) โ โ โ ๐น โ
โ)) |
10 | 7, 9 | mpbid 231 |
. . . . . . . . 9
โข (((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โง ((FermatNoโ๐) =
๐บ โง
(FermatNoโ๐) = ๐น)) โ ๐น โ โ) |
11 | | fmtnonn 45797 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (FermatNoโ๐)
โ โ) |
12 | 11 | ad2antll 728 |
. . . . . . . . . . 11
โข ((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โ (FermatNoโ๐)
โ โ) |
13 | 12 | adantr 482 |
. . . . . . . . . 10
โข (((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โง ((FermatNoโ๐) =
๐บ โง
(FermatNoโ๐) = ๐น)) โ (FermatNoโ๐) โ
โ) |
14 | | eleq1 2826 |
. . . . . . . . . . 11
โข
((FermatNoโ๐)
= ๐บ โ
((FermatNoโ๐) โ
โ โ ๐บ โ
โ)) |
15 | 14 | ad2antrl 727 |
. . . . . . . . . 10
โข (((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โง ((FermatNoโ๐) =
๐บ โง
(FermatNoโ๐) = ๐น)) โ ((FermatNoโ๐) โ โ โ ๐บ โ
โ)) |
16 | 13, 15 | mpbid 231 |
. . . . . . . . 9
โข (((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โง ((FermatNoโ๐) =
๐บ โง
(FermatNoโ๐) = ๐น)) โ ๐บ โ โ) |
17 | | simpll 766 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ยฌ (FermatNoโ๐) = (FermatNoโ๐)) โ ๐ โ โ0) |
18 | | simplr 768 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ยฌ (FermatNoโ๐) = (FermatNoโ๐)) โ ๐ โ โ0) |
19 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (FermatNoโ๐) = (FermatNoโ๐)) |
20 | 19 | con3i 154 |
. . . . . . . . . . . . . . . . 17
โข (ยฌ
(FermatNoโ๐) =
(FermatNoโ๐) โ
ยฌ ๐ = ๐) |
21 | 20 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ยฌ (FermatNoโ๐) = (FermatNoโ๐)) โ ยฌ ๐ = ๐) |
22 | 21 | neqned 2951 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ยฌ (FermatNoโ๐) = (FermatNoโ๐)) โ ๐ โ ๐) |
23 | | goldbachth 45813 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ0
โง ๐ โ
โ0 โง ๐
โ ๐) โ
((FermatNoโ๐) gcd
(FermatNoโ๐)) =
1) |
24 | 17, 18, 22, 23 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ยฌ (FermatNoโ๐) = (FermatNoโ๐)) โ ((FermatNoโ๐) gcd (FermatNoโ๐)) = 1) |
25 | 24 | ex 414 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (ยฌ (FermatNoโ๐) = (FermatNoโ๐) โ ((FermatNoโ๐) gcd (FermatNoโ๐)) = 1)) |
26 | | eqeq12 2754 |
. . . . . . . . . . . . . . . 16
โข
(((FermatNoโ๐)
= ๐น โง
(FermatNoโ๐) = ๐บ) โ ((FermatNoโ๐) = (FermatNoโ๐) โ ๐น = ๐บ)) |
27 | 26 | notbid 318 |
. . . . . . . . . . . . . . 15
โข
(((FermatNoโ๐)
= ๐น โง
(FermatNoโ๐) = ๐บ) โ (ยฌ
(FermatNoโ๐) =
(FermatNoโ๐) โ
ยฌ ๐น = ๐บ)) |
28 | | oveq12 7371 |
. . . . . . . . . . . . . . . 16
โข
(((FermatNoโ๐)
= ๐น โง
(FermatNoโ๐) = ๐บ) โ ((FermatNoโ๐) gcd (FermatNoโ๐)) = (๐น gcd ๐บ)) |
29 | 28 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
โข
(((FermatNoโ๐)
= ๐น โง
(FermatNoโ๐) = ๐บ) โ (((FermatNoโ๐) gcd (FermatNoโ๐)) = 1 โ (๐น gcd ๐บ) = 1)) |
30 | 27, 29 | imbi12d 345 |
. . . . . . . . . . . . . 14
โข
(((FermatNoโ๐)
= ๐น โง
(FermatNoโ๐) = ๐บ) โ ((ยฌ
(FermatNoโ๐) =
(FermatNoโ๐) โ
((FermatNoโ๐) gcd
(FermatNoโ๐)) = 1)
โ (ยฌ ๐น = ๐บ โ (๐น gcd ๐บ) = 1))) |
31 | 30 | ancoms 460 |
. . . . . . . . . . . . 13
โข
(((FermatNoโ๐)
= ๐บ โง
(FermatNoโ๐) = ๐น) โ ((ยฌ
(FermatNoโ๐) =
(FermatNoโ๐) โ
((FermatNoโ๐) gcd
(FermatNoโ๐)) = 1)
โ (ยฌ ๐น = ๐บ โ (๐น gcd ๐บ) = 1))) |
32 | 25, 31 | syl5ibcom 244 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((FermatNoโ๐) = ๐บ โง (FermatNoโ๐) = ๐น) โ (ยฌ ๐น = ๐บ โ (๐น gcd ๐บ) = 1))) |
33 | 32 | com23 86 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (ยฌ ๐น = ๐บ โ (((FermatNoโ๐) = ๐บ โง (FermatNoโ๐) = ๐น) โ (๐น gcd ๐บ) = 1))) |
34 | 33 | impcom 409 |
. . . . . . . . . 10
โข ((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โ (((FermatNoโ๐)
= ๐บ โง
(FermatNoโ๐) = ๐น) โ (๐น gcd ๐บ) = 1)) |
35 | 34 | imp 408 |
. . . . . . . . 9
โข (((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โง ((FermatNoโ๐) =
๐บ โง
(FermatNoโ๐) = ๐น)) โ (๐น gcd ๐บ) = 1) |
36 | | prmnn 16557 |
. . . . . . . . . . . 12
โข (๐ผ โ โ โ ๐ผ โ
โ) |
37 | | coprmdvds1 16535 |
. . . . . . . . . . . . 13
โข ((๐น โ โ โง ๐บ โ โ โง (๐น gcd ๐บ) = 1) โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐ผ = 1)) |
38 | 37 | imp 408 |
. . . . . . . . . . . 12
โข (((๐น โ โ โง ๐บ โ โ โง (๐น gcd ๐บ) = 1) โง (๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ)) โ ๐ผ = 1) |
39 | 36, 38 | syl3anr1 1417 |
. . . . . . . . . . 11
โข (((๐น โ โ โง ๐บ โ โ โง (๐น gcd ๐บ) = 1) โง (๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ)) โ ๐ผ = 1) |
40 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
โข (๐ผ = 1 โ (๐ผ โ โ โ 1 โ
โ)) |
41 | | 1nprm 16562 |
. . . . . . . . . . . . . . . . 17
โข ยฌ 1
โ โ |
42 | 41 | pm2.21i 119 |
. . . . . . . . . . . . . . . 16
โข (1 โ
โ โ ๐น = ๐บ) |
43 | 40, 42 | syl6bi 253 |
. . . . . . . . . . . . . . 15
โข (๐ผ = 1 โ (๐ผ โ โ โ ๐น = ๐บ)) |
44 | 43 | com12 32 |
. . . . . . . . . . . . . 14
โข (๐ผ โ โ โ (๐ผ = 1 โ ๐น = ๐บ)) |
45 | 44 | a1d 25 |
. . . . . . . . . . . . 13
โข (๐ผ โ โ โ ((๐น โ โ โง ๐บ โ โ โง (๐น gcd ๐บ) = 1) โ (๐ผ = 1 โ ๐น = ๐บ))) |
46 | 45 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
โข ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ((๐น โ โ โง ๐บ โ โ โง (๐น gcd ๐บ) = 1) โ (๐ผ = 1 โ ๐น = ๐บ))) |
47 | 46 | impcom 409 |
. . . . . . . . . . 11
โข (((๐น โ โ โง ๐บ โ โ โง (๐น gcd ๐บ) = 1) โง (๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ)) โ (๐ผ = 1 โ ๐น = ๐บ)) |
48 | 39, 47 | mpd 15 |
. . . . . . . . . 10
โข (((๐น โ โ โง ๐บ โ โ โง (๐น gcd ๐บ) = 1) โง (๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ)) โ ๐น = ๐บ) |
49 | 48 | ex 414 |
. . . . . . . . 9
โข ((๐น โ โ โง ๐บ โ โ โง (๐น gcd ๐บ) = 1) โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ)) |
50 | 10, 16, 35, 49 | syl3anc 1372 |
. . . . . . . 8
โข (((ยฌ
๐น = ๐บ โง (๐ โ โ0 โง ๐ โ โ0))
โง ((FermatNoโ๐) =
๐บ โง
(FermatNoโ๐) = ๐น)) โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ)) |
51 | 50 | exp43 438 |
. . . . . . 7
โข (ยฌ
๐น = ๐บ โ ((๐ โ โ0 โง ๐ โ โ0)
โ ((FermatNoโ๐)
= ๐บ โ
((FermatNoโ๐) = ๐น โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ))))) |
52 | 4, 51 | pm2.61i 182 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((FermatNoโ๐) = ๐บ โ ((FermatNoโ๐) = ๐น โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ)))) |
53 | 52 | rexlimdva 3153 |
. . . . 5
โข (๐ โ โ0
โ (โ๐ โ
โ0 (FermatNoโ๐) = ๐บ โ ((FermatNoโ๐) = ๐น โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ)))) |
54 | 53 | com23 86 |
. . . 4
โข (๐ โ โ0
โ ((FermatNoโ๐)
= ๐น โ (โ๐ โ โ0
(FermatNoโ๐) = ๐บ โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ)))) |
55 | 54 | rexlimiv 3146 |
. . 3
โข
(โ๐ โ
โ0 (FermatNoโ๐) = ๐น โ (โ๐ โ โ0
(FermatNoโ๐) = ๐บ โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ))) |
56 | 55 | imp 408 |
. 2
โข
((โ๐ โ
โ0 (FermatNoโ๐) = ๐น โง โ๐ โ โ0
(FermatNoโ๐) = ๐บ) โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ)) |
57 | 1, 2, 56 | syl2anb 599 |
1
โข ((๐น โ ran FermatNo โง ๐บ โ ran FermatNo) โ
((๐ผ โ โ โง
๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐น = ๐บ)) |