Step |
Hyp |
Ref |
Expression |
1 |
|
prmdvdsfmtnof.1 |
⊢ 𝐹 = ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ) |
2 |
1
|
prmdvdsfmtnof |
⊢ 𝐹 : ran FermatNo ⟶ ℙ |
3 |
|
breq2 |
⊢ ( 𝑓 = 𝑔 → ( 𝑝 ∥ 𝑓 ↔ 𝑝 ∥ 𝑔 ) ) |
4 |
3
|
rabbidv |
⊢ ( 𝑓 = 𝑔 → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } ) |
5 |
4
|
infeq1d |
⊢ ( 𝑓 = 𝑔 → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ) |
6 |
|
id |
⊢ ( 𝑔 ∈ ran FermatNo → 𝑔 ∈ ran FermatNo ) |
7 |
|
ltso |
⊢ < Or ℝ |
8 |
7
|
a1i |
⊢ ( 𝑔 ∈ ran FermatNo → < Or ℝ ) |
9 |
8
|
infexd |
⊢ ( 𝑔 ∈ ran FermatNo → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ∈ V ) |
10 |
1 5 6 9
|
fvmptd3 |
⊢ ( 𝑔 ∈ ran FermatNo → ( 𝐹 ‘ 𝑔 ) = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ) |
11 |
|
breq2 |
⊢ ( 𝑓 = ℎ → ( 𝑝 ∥ 𝑓 ↔ 𝑝 ∥ ℎ ) ) |
12 |
11
|
rabbidv |
⊢ ( 𝑓 = ℎ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ } ) |
13 |
12
|
infeq1d |
⊢ ( 𝑓 = ℎ → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ } , ℝ , < ) ) |
14 |
|
id |
⊢ ( ℎ ∈ ran FermatNo → ℎ ∈ ran FermatNo ) |
15 |
7
|
a1i |
⊢ ( ℎ ∈ ran FermatNo → < Or ℝ ) |
16 |
15
|
infexd |
⊢ ( ℎ ∈ ran FermatNo → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ } , ℝ , < ) ∈ V ) |
17 |
1 13 14 16
|
fvmptd3 |
⊢ ( ℎ ∈ ran FermatNo → ( 𝐹 ‘ ℎ ) = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ } , ℝ , < ) ) |
18 |
10 17
|
eqeqan12d |
⊢ ( ( 𝑔 ∈ ran FermatNo ∧ ℎ ∈ ran FermatNo ) → ( ( 𝐹 ‘ 𝑔 ) = ( 𝐹 ‘ ℎ ) ↔ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ } , ℝ , < ) ) ) |
19 |
|
fmtnorn |
⊢ ( 𝑔 ∈ ran FermatNo ↔ ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = 𝑔 ) |
20 |
|
fmtnoge3 |
⊢ ( 𝑛 ∈ ℕ0 → ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 3 ) ) |
21 |
|
uzuzle23 |
⊢ ( ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 3 ) → ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 2 ) ) |
22 |
20 21
|
syl |
⊢ ( 𝑛 ∈ ℕ0 → ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 2 ) ) |
23 |
22
|
adantr |
⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑔 ) → ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 2 ) ) |
24 |
|
eleq1 |
⊢ ( ( FermatNo ‘ 𝑛 ) = 𝑔 → ( ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 2 ) ↔ 𝑔 ∈ ( ℤ≥ ‘ 2 ) ) ) |
25 |
24
|
adantl |
⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑔 ) → ( ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 2 ) ↔ 𝑔 ∈ ( ℤ≥ ‘ 2 ) ) ) |
26 |
23 25
|
mpbid |
⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑔 ) → 𝑔 ∈ ( ℤ≥ ‘ 2 ) ) |
27 |
26
|
rexlimiva |
⊢ ( ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = 𝑔 → 𝑔 ∈ ( ℤ≥ ‘ 2 ) ) |
28 |
19 27
|
sylbi |
⊢ ( 𝑔 ∈ ran FermatNo → 𝑔 ∈ ( ℤ≥ ‘ 2 ) ) |
29 |
|
fmtnorn |
⊢ ( ℎ ∈ ran FermatNo ↔ ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = ℎ ) |
30 |
22
|
adantr |
⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = ℎ ) → ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 2 ) ) |
31 |
|
eleq1 |
⊢ ( ( FermatNo ‘ 𝑛 ) = ℎ → ( ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ℎ ∈ ( ℤ≥ ‘ 2 ) ) ) |
32 |
31
|
adantl |
⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = ℎ ) → ( ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ℎ ∈ ( ℤ≥ ‘ 2 ) ) ) |
33 |
30 32
|
mpbid |
⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = ℎ ) → ℎ ∈ ( ℤ≥ ‘ 2 ) ) |
34 |
33
|
rexlimiva |
⊢ ( ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = ℎ → ℎ ∈ ( ℤ≥ ‘ 2 ) ) |
35 |
29 34
|
sylbi |
⊢ ( ℎ ∈ ran FermatNo → ℎ ∈ ( ℤ≥ ‘ 2 ) ) |
36 |
|
eqid |
⊢ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) |
37 |
|
eqid |
⊢ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ } , ℝ , < ) = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ } , ℝ , < ) |
38 |
36 37
|
prmdvdsfmtnof1lem1 |
⊢ ( ( 𝑔 ∈ ( ℤ≥ ‘ 2 ) ∧ ℎ ∈ ( ℤ≥ ‘ 2 ) ) → ( inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ } , ℝ , < ) → ( inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ∈ ℙ ∧ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ∥ 𝑔 ∧ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ∥ ℎ ) ) ) |
39 |
28 35 38
|
syl2an |
⊢ ( ( 𝑔 ∈ ran FermatNo ∧ ℎ ∈ ran FermatNo ) → ( inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ } , ℝ , < ) → ( inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ∈ ℙ ∧ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ∥ 𝑔 ∧ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ∥ ℎ ) ) ) |
40 |
|
prmdvdsfmtnof1lem2 |
⊢ ( ( 𝑔 ∈ ran FermatNo ∧ ℎ ∈ ran FermatNo ) → ( ( inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ∈ ℙ ∧ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ∥ 𝑔 ∧ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) ∥ ℎ ) → 𝑔 = ℎ ) ) |
41 |
39 40
|
syld |
⊢ ( ( 𝑔 ∈ ran FermatNo ∧ ℎ ∈ ran FermatNo ) → ( inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑔 } , ℝ , < ) = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ℎ } , ℝ , < ) → 𝑔 = ℎ ) ) |
42 |
18 41
|
sylbid |
⊢ ( ( 𝑔 ∈ ran FermatNo ∧ ℎ ∈ ran FermatNo ) → ( ( 𝐹 ‘ 𝑔 ) = ( 𝐹 ‘ ℎ ) → 𝑔 = ℎ ) ) |
43 |
42
|
rgen2 |
⊢ ∀ 𝑔 ∈ ran FermatNo ∀ ℎ ∈ ran FermatNo ( ( 𝐹 ‘ 𝑔 ) = ( 𝐹 ‘ ℎ ) → 𝑔 = ℎ ) |
44 |
|
dff13 |
⊢ ( 𝐹 : ran FermatNo –1-1→ ℙ ↔ ( 𝐹 : ran FermatNo ⟶ ℙ ∧ ∀ 𝑔 ∈ ran FermatNo ∀ ℎ ∈ ran FermatNo ( ( 𝐹 ‘ 𝑔 ) = ( 𝐹 ‘ ℎ ) → 𝑔 = ℎ ) ) ) |
45 |
2 43 44
|
mpbir2an |
⊢ 𝐹 : ran FermatNo –1-1→ ℙ |