Step | Hyp | Ref
| Expression |
1 | | prmdvdsfmtnof.1 |
. . 3
β’ πΉ = (π β ran FermatNo β¦ inf({π β β β£ π β₯ π}, β, < )) |
2 | 1 | prmdvdsfmtnof 45852 |
. 2
β’ πΉ:ran
FermatNoβΆβ |
3 | | breq2 5114 |
. . . . . . . 8
β’ (π = π β (π β₯ π β π β₯ π)) |
4 | 3 | rabbidv 3418 |
. . . . . . 7
β’ (π = π β {π β β β£ π β₯ π} = {π β β β£ π β₯ π}) |
5 | 4 | infeq1d 9420 |
. . . . . 6
β’ (π = π β inf({π β β β£ π β₯ π}, β, < ) = inf({π β β β£ π β₯ π}, β, < )) |
6 | | id 22 |
. . . . . 6
β’ (π β ran FermatNo β
π β ran
FermatNo) |
7 | | ltso 11242 |
. . . . . . . 8
β’ < Or
β |
8 | 7 | a1i 11 |
. . . . . . 7
β’ (π β ran FermatNo β <
Or β) |
9 | 8 | infexd 9426 |
. . . . . 6
β’ (π β ran FermatNo β
inf({π β β
β£ π β₯ π}, β, < ) β
V) |
10 | 1, 5, 6, 9 | fvmptd3 6976 |
. . . . 5
β’ (π β ran FermatNo β
(πΉβπ) = inf({π β β β£ π β₯ π}, β, < )) |
11 | | breq2 5114 |
. . . . . . . 8
β’ (π = β β (π β₯ π β π β₯ β)) |
12 | 11 | rabbidv 3418 |
. . . . . . 7
β’ (π = β β {π β β β£ π β₯ π} = {π β β β£ π β₯ β}) |
13 | 12 | infeq1d 9420 |
. . . . . 6
β’ (π = β β inf({π β β β£ π β₯ π}, β, < ) = inf({π β β β£ π β₯ β}, β, < )) |
14 | | id 22 |
. . . . . 6
β’ (β β ran FermatNo β β β ran
FermatNo) |
15 | 7 | a1i 11 |
. . . . . . 7
β’ (β β ran FermatNo β <
Or β) |
16 | 15 | infexd 9426 |
. . . . . 6
β’ (β β ran FermatNo β
inf({π β β
β£ π β₯ β}, β, < ) β
V) |
17 | 1, 13, 14, 16 | fvmptd3 6976 |
. . . . 5
β’ (β β ran FermatNo β
(πΉββ) = inf({π β β β£ π β₯ β}, β, < )) |
18 | 10, 17 | eqeqan12d 2751 |
. . . 4
β’ ((π β ran FermatNo β§ β β ran FermatNo) β
((πΉβπ) = (πΉββ) β inf({π β β β£ π β₯ π}, β, < ) = inf({π β β β£ π β₯ β}, β, < ))) |
19 | | fmtnorn 45800 |
. . . . . . 7
β’ (π β ran FermatNo β
βπ β
β0 (FermatNoβπ) = π) |
20 | | fmtnoge3 45796 |
. . . . . . . . . . 11
β’ (π β β0
β (FermatNoβπ)
β (β€β₯β3)) |
21 | | uzuzle23 12821 |
. . . . . . . . . . 11
β’
((FermatNoβπ)
β (β€β₯β3) β (FermatNoβπ) β
(β€β₯β2)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
β’ (π β β0
β (FermatNoβπ)
β (β€β₯β2)) |
23 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((π β β0
β§ (FermatNoβπ) =
π) β
(FermatNoβπ) β
(β€β₯β2)) |
24 | | eleq1 2826 |
. . . . . . . . . 10
β’
((FermatNoβπ)
= π β
((FermatNoβπ) β
(β€β₯β2) β π β
(β€β₯β2))) |
25 | 24 | adantl 483 |
. . . . . . . . 9
β’ ((π β β0
β§ (FermatNoβπ) =
π) β
((FermatNoβπ) β
(β€β₯β2) β π β
(β€β₯β2))) |
26 | 23, 25 | mpbid 231 |
. . . . . . . 8
β’ ((π β β0
β§ (FermatNoβπ) =
π) β π β
(β€β₯β2)) |
27 | 26 | rexlimiva 3145 |
. . . . . . 7
β’
(βπ β
β0 (FermatNoβπ) = π β π β
(β€β₯β2)) |
28 | 19, 27 | sylbi 216 |
. . . . . 6
β’ (π β ran FermatNo β
π β
(β€β₯β2)) |
29 | | fmtnorn 45800 |
. . . . . . 7
β’ (β β ran FermatNo β
βπ β
β0 (FermatNoβπ) = β) |
30 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((π β β0
β§ (FermatNoβπ) =
β) β
(FermatNoβπ) β
(β€β₯β2)) |
31 | | eleq1 2826 |
. . . . . . . . . 10
β’
((FermatNoβπ)
= β β
((FermatNoβπ) β
(β€β₯β2) β β β
(β€β₯β2))) |
32 | 31 | adantl 483 |
. . . . . . . . 9
β’ ((π β β0
β§ (FermatNoβπ) =
β) β
((FermatNoβπ) β
(β€β₯β2) β β β
(β€β₯β2))) |
33 | 30, 32 | mpbid 231 |
. . . . . . . 8
β’ ((π β β0
β§ (FermatNoβπ) =
β) β β β
(β€β₯β2)) |
34 | 33 | rexlimiva 3145 |
. . . . . . 7
β’
(βπ β
β0 (FermatNoβπ) = β β β β
(β€β₯β2)) |
35 | 29, 34 | sylbi 216 |
. . . . . 6
β’ (β β ran FermatNo β β β
(β€β₯β2)) |
36 | | eqid 2737 |
. . . . . . 7
β’
inf({π β
β β£ π β₯
π}, β, < ) =
inf({π β β
β£ π β₯ π}, β, <
) |
37 | | eqid 2737 |
. . . . . . 7
β’
inf({π β
β β£ π β₯
β}, β, < ) =
inf({π β β
β£ π β₯ β}, β, <
) |
38 | 36, 37 | prmdvdsfmtnof1lem1 45850 |
. . . . . 6
β’ ((π β
(β€β₯β2) β§ β β (β€β₯β2))
β (inf({π β
β β£ π β₯
π}, β, < ) =
inf({π β β
β£ π β₯ β}, β, < ) β
(inf({π β β
β£ π β₯ π}, β, < ) β
β β§ inf({π β
β β£ π β₯
π}, β, < ) β₯
π β§ inf({π β β β£ π β₯ π}, β, < ) β₯ β))) |
39 | 28, 35, 38 | syl2an 597 |
. . . . 5
β’ ((π β ran FermatNo β§ β β ran FermatNo) β
(inf({π β β
β£ π β₯ π}, β, < ) = inf({π β β β£ π β₯ β}, β, < ) β (inf({π β β β£ π β₯ π}, β, < ) β β β§
inf({π β β
β£ π β₯ π}, β, < ) β₯ π β§ inf({π β β β£ π β₯ π}, β, < ) β₯ β))) |
40 | | prmdvdsfmtnof1lem2 45851 |
. . . . 5
β’ ((π β ran FermatNo β§ β β ran FermatNo) β
((inf({π β β
β£ π β₯ π}, β, < ) β
β β§ inf({π β
β β£ π β₯
π}, β, < ) β₯
π β§ inf({π β β β£ π β₯ π}, β, < ) β₯ β) β π = β)) |
41 | 39, 40 | syld 47 |
. . . 4
β’ ((π β ran FermatNo β§ β β ran FermatNo) β
(inf({π β β
β£ π β₯ π}, β, < ) = inf({π β β β£ π β₯ β}, β, < ) β π = β)) |
42 | 18, 41 | sylbid 239 |
. . 3
β’ ((π β ran FermatNo β§ β β ran FermatNo) β
((πΉβπ) = (πΉββ) β π = β)) |
43 | 42 | rgen2 3195 |
. 2
β’
βπ β ran
FermatNoββ β ran
FermatNo((πΉβπ) = (πΉββ) β π = β) |
44 | | dff13 7207 |
. 2
β’ (πΉ:ran FermatNoβ1-1ββ β (πΉ:ran FermatNoβΆβ β§
βπ β ran
FermatNoββ β ran
FermatNo((πΉβπ) = (πΉββ) β π = β))) |
45 | 2, 43, 44 | mpbir2an 710 |
1
β’ πΉ:ran FermatNoβ1-1ββ |