Step | Hyp | Ref
| Expression |
1 | | prmdvdsfmtnof.1 |
. . 3
⊢ 𝐹 = (𝑓 ∈ ran FermatNo ↦ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < )) |
2 | 1 | prmdvdsfmtnof 40036 |
. 2
⊢ 𝐹:ran
FermatNo⟶ℙ |
3 | 1 | a1i 11 |
. . . . . 6
⊢ (𝑔 ∈ ran FermatNo →
𝐹 = (𝑓 ∈ ran FermatNo ↦ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < ))) |
4 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑝 ∥ 𝑓 ↔ 𝑝 ∥ 𝑔)) |
5 | 4 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓} = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔}) |
6 | 5 | infeq1d 8266 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < ) = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔}, ℝ, < )) |
7 | 6 | adantl 481 |
. . . . . 6
⊢ ((𝑔 ∈ ran FermatNo ∧ 𝑓 = 𝑔) → inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < ) = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔}, ℝ, < )) |
8 | | id 22 |
. . . . . 6
⊢ (𝑔 ∈ ran FermatNo →
𝑔 ∈ ran
FermatNo) |
9 | | ltso 9997 |
. . . . . . . 8
⊢ < Or
ℝ |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝑔 ∈ ran FermatNo → <
Or ℝ) |
11 | 10 | infexd 8272 |
. . . . . 6
⊢ (𝑔 ∈ ran FermatNo →
inf({𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑔}, ℝ, < ) ∈
V) |
12 | 3, 7, 8, 11 | fvmptd 6197 |
. . . . 5
⊢ (𝑔 ∈ ran FermatNo →
(𝐹‘𝑔) = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔}, ℝ, < )) |
13 | 1 | a1i 11 |
. . . . . 6
⊢ (ℎ ∈ ran FermatNo → 𝐹 = (𝑓 ∈ ran FermatNo ↦ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < ))) |
14 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑓 = ℎ → (𝑝 ∥ 𝑓 ↔ 𝑝 ∥ ℎ)) |
15 | 14 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝑓 = ℎ → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓} = {𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ}) |
16 | 15 | infeq1d 8266 |
. . . . . . 7
⊢ (𝑓 = ℎ → inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < ) = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ}, ℝ, < )) |
17 | 16 | adantl 481 |
. . . . . 6
⊢ ((ℎ ∈ ran FermatNo ∧ 𝑓 = ℎ) → inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < ) = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ}, ℝ, < )) |
18 | | id 22 |
. . . . . 6
⊢ (ℎ ∈ ran FermatNo → ℎ ∈ ran
FermatNo) |
19 | 9 | a1i 11 |
. . . . . . 7
⊢ (ℎ ∈ ran FermatNo → <
Or ℝ) |
20 | 19 | infexd 8272 |
. . . . . 6
⊢ (ℎ ∈ ran FermatNo →
inf({𝑝 ∈ ℙ
∣ 𝑝 ∥ ℎ}, ℝ, < ) ∈
V) |
21 | 13, 17, 18, 20 | fvmptd 6197 |
. . . . 5
⊢ (ℎ ∈ ran FermatNo →
(𝐹‘ℎ) = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ}, ℝ, < )) |
22 | 12, 21 | eqeqan12d 2626 |
. . . 4
⊢ ((𝑔 ∈ ran FermatNo ∧ ℎ ∈ ran FermatNo) →
((𝐹‘𝑔) = (𝐹‘ℎ) ↔ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔}, ℝ, < ) = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ}, ℝ, < ))) |
23 | | fmtnorn 39984 |
. . . . . . 7
⊢ (𝑔 ∈ ran FermatNo ↔
∃𝑛 ∈
ℕ0 (FermatNo‘𝑛) = 𝑔) |
24 | | fmtnoge3 39980 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (FermatNo‘𝑛)
∈ (ℤ≥‘3)) |
25 | | uzuzle23 11605 |
. . . . . . . . . . 11
⊢
((FermatNo‘𝑛)
∈ (ℤ≥‘3) → (FermatNo‘𝑛) ∈
(ℤ≥‘2)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (FermatNo‘𝑛)
∈ (ℤ≥‘2)) |
27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ (FermatNo‘𝑛) =
𝑔) →
(FermatNo‘𝑛) ∈
(ℤ≥‘2)) |
28 | | eleq1 2676 |
. . . . . . . . . 10
⊢
((FermatNo‘𝑛)
= 𝑔 →
((FermatNo‘𝑛) ∈
(ℤ≥‘2) ↔ 𝑔 ∈
(ℤ≥‘2))) |
29 | 28 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ (FermatNo‘𝑛) =
𝑔) →
((FermatNo‘𝑛) ∈
(ℤ≥‘2) ↔ 𝑔 ∈
(ℤ≥‘2))) |
30 | 27, 29 | mpbid 221 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ (FermatNo‘𝑛) =
𝑔) → 𝑔 ∈
(ℤ≥‘2)) |
31 | 30 | rexlimiva 3010 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ0 (FermatNo‘𝑛) = 𝑔 → 𝑔 ∈
(ℤ≥‘2)) |
32 | 23, 31 | sylbi 206 |
. . . . . 6
⊢ (𝑔 ∈ ran FermatNo →
𝑔 ∈
(ℤ≥‘2)) |
33 | | fmtnorn 39984 |
. . . . . . 7
⊢ (ℎ ∈ ran FermatNo ↔
∃𝑛 ∈
ℕ0 (FermatNo‘𝑛) = ℎ) |
34 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ (FermatNo‘𝑛) =
ℎ) →
(FermatNo‘𝑛) ∈
(ℤ≥‘2)) |
35 | | eleq1 2676 |
. . . . . . . . . 10
⊢
((FermatNo‘𝑛)
= ℎ →
((FermatNo‘𝑛) ∈
(ℤ≥‘2) ↔ ℎ ∈
(ℤ≥‘2))) |
36 | 35 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ (FermatNo‘𝑛) =
ℎ) →
((FermatNo‘𝑛) ∈
(ℤ≥‘2) ↔ ℎ ∈
(ℤ≥‘2))) |
37 | 34, 36 | mpbid 221 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ (FermatNo‘𝑛) =
ℎ) → ℎ ∈
(ℤ≥‘2)) |
38 | 37 | rexlimiva 3010 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ0 (FermatNo‘𝑛) = ℎ → ℎ ∈
(ℤ≥‘2)) |
39 | 33, 38 | sylbi 206 |
. . . . . 6
⊢ (ℎ ∈ ran FermatNo → ℎ ∈
(ℤ≥‘2)) |
40 | | eqid 2610 |
. . . . . . 7
⊢
inf({𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑔}, ℝ, < ) =
inf({𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑔}, ℝ, <
) |
41 | | eqid 2610 |
. . . . . . 7
⊢
inf({𝑝 ∈
ℙ ∣ 𝑝 ∥
ℎ}, ℝ, < ) =
inf({𝑝 ∈ ℙ
∣ 𝑝 ∥ ℎ}, ℝ, <
) |
42 | 40, 41 | prmdvdsfmtnof1lem1 40034 |
. . . . . 6
⊢ ((𝑔 ∈
(ℤ≥‘2) ∧ ℎ ∈ (ℤ≥‘2))
→ (inf({𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑔}, ℝ, < ) =
inf({𝑝 ∈ ℙ
∣ 𝑝 ∥ ℎ}, ℝ, < ) →
(inf({𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑔}, ℝ, < ) ∈
ℙ ∧ inf({𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑔}, ℝ, < ) ∥
𝑔 ∧ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔}, ℝ, < ) ∥ ℎ))) |
43 | 32, 39, 42 | syl2an 493 |
. . . . 5
⊢ ((𝑔 ∈ ran FermatNo ∧ ℎ ∈ ran FermatNo) →
(inf({𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑔}, ℝ, < ) = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ}, ℝ, < ) → (inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔}, ℝ, < ) ∈ ℙ ∧
inf({𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑔}, ℝ, < ) ∥ 𝑔 ∧ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔}, ℝ, < ) ∥ ℎ))) |
44 | | prmdvdsfmtnof1lem2 40035 |
. . . . 5
⊢ ((𝑔 ∈ ran FermatNo ∧ ℎ ∈ ran FermatNo) →
((inf({𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑔}, ℝ, < ) ∈
ℙ ∧ inf({𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑔}, ℝ, < ) ∥
𝑔 ∧ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔}, ℝ, < ) ∥ ℎ) → 𝑔 = ℎ)) |
45 | 43, 44 | syld 46 |
. . . 4
⊢ ((𝑔 ∈ ran FermatNo ∧ ℎ ∈ ran FermatNo) →
(inf({𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑔}, ℝ, < ) = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ}, ℝ, < ) → 𝑔 = ℎ)) |
46 | 22, 45 | sylbid 229 |
. . 3
⊢ ((𝑔 ∈ ran FermatNo ∧ ℎ ∈ ran FermatNo) →
((𝐹‘𝑔) = (𝐹‘ℎ) → 𝑔 = ℎ)) |
47 | 46 | rgen2a 2960 |
. 2
⊢
∀𝑔 ∈ ran
FermatNo∀ℎ ∈ ran
FermatNo((𝐹‘𝑔) = (𝐹‘ℎ) → 𝑔 = ℎ) |
48 | | dff13 6416 |
. 2
⊢ (𝐹:ran FermatNo–1-1→ℙ ↔ (𝐹:ran FermatNo⟶ℙ ∧
∀𝑔 ∈ ran
FermatNo∀ℎ ∈ ran
FermatNo((𝐹‘𝑔) = (𝐹‘ℎ) → 𝑔 = ℎ))) |
49 | 2, 47, 48 | mpbir2an 957 |
1
⊢ 𝐹:ran FermatNo–1-1→ℙ |