Metamath Proof Explorer

Theorem 1arith

Description: Fundamental theorem of arithmetic, where a prime factorization is represented as a sequence of prime exponents, for which only finitely many primes have nonzero exponent. The function M maps the set of positive integers one-to-one onto the set of prime factorizations R . (Contributed by Paul Chapman, 17-Nov-2012) (Proof shortened by Mario Carneiro, 30-May-2014)

Ref Expression
Hypotheses 1arith.1 ⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
1arith.2 ⊢ 𝑅 = { 𝑒 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑒 “ ℕ ) ∈ Fin }
Assertion 1arith 𝑀 : ℕ –1-1-onto→ 𝑅

Proof

Step Hyp Ref Expression
1 1arith.1 ⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
2 1arith.2 ⊢ 𝑅 = { 𝑒 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑒 “ ℕ ) ∈ Fin }
3 prmex ⊢ ℙ ∈ V
4 3 mptex ⊢ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) ∈ V
5 4 1 fnmpti ⊢ 𝑀 Fn ℕ
6 1 1arithlem3 ⊢ ( 𝑥 ∈ ℕ → ( 𝑀 ‘ 𝑥 ) : ℙ ⟶ ℕ0 )
7 nn0ex ⊢ ℕ0 ∈ V
8 7 3 elmap ⊢ ( ( 𝑀 ‘ 𝑥 ) ∈ ( ℕ0 ↑m ℙ ) ↔ ( 𝑀 ‘ 𝑥 ) : ℙ ⟶ ℕ0 )
9 6 8 sylibr ⊢ ( 𝑥 ∈ ℕ → ( 𝑀 ‘ 𝑥 ) ∈ ( ℕ0 ↑m ℙ ) )
10 fzfi ⊢ ( 1 ... 𝑥 ) ∈ Fin
11 ffn ⊢ ( ( 𝑀 ‘ 𝑥 ) : ℙ ⟶ ℕ0 → ( 𝑀 ‘ 𝑥 ) Fn ℙ )
12 elpreima ⊢ ( ( 𝑀 ‘ 𝑥 ) Fn ℙ → ( 𝑞 ∈ ( ◡ ( 𝑀 ‘ 𝑥 ) “ ℕ ) ↔ ( 𝑞 ∈ ℙ ∧ ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) ∈ ℕ ) ) )
13 6 11 12 3syl ⊢ ( 𝑥 ∈ ℕ → ( 𝑞 ∈ ( ◡ ( 𝑀 ‘ 𝑥 ) “ ℕ ) ↔ ( 𝑞 ∈ ℙ ∧ ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) ∈ ℕ ) ) )
14 1 1arithlem2 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) = ( 𝑞 pCnt 𝑥 ) )
15 14 eleq1d ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) ∈ ℕ ↔ ( 𝑞 pCnt 𝑥 ) ∈ ℕ ) )
16 prmz ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℤ )
17 id ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ )
18 dvdsle ⊢ ( ( 𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ ) → ( 𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥 ) )
19 16 17 18 syl2anr ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥 ) )
20 pcelnn ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑥 ∈ ℕ ) → ( ( 𝑞 pCnt 𝑥 ) ∈ ℕ ↔ 𝑞 ∥ 𝑥 ) )
21 20 ancoms ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑞 pCnt 𝑥 ) ∈ ℕ ↔ 𝑞 ∥ 𝑥 ) )
22 prmnn ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℕ )
23 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
24 22 23 eleqtrdi ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ( ℤ≥ ‘ 1 ) )
25 nnz ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℤ )
26 elfz5 ⊢ ( ( 𝑞 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑞 ∈ ( 1 ... 𝑥 ) ↔ 𝑞 ≤ 𝑥 ) )
27 24 25 26 syl2anr ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∈ ( 1 ... 𝑥 ) ↔ 𝑞 ≤ 𝑥 ) )
28 19 21 27 3imtr4d ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑞 pCnt 𝑥 ) ∈ ℕ → 𝑞 ∈ ( 1 ... 𝑥 ) ) )
29 15 28 sylbid ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) ∈ ℕ → 𝑞 ∈ ( 1 ... 𝑥 ) ) )
30 29 expimpd ⊢ ( 𝑥 ∈ ℕ → ( ( 𝑞 ∈ ℙ ∧ ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) ∈ ℕ ) → 𝑞 ∈ ( 1 ... 𝑥 ) ) )
31 13 30 sylbid ⊢ ( 𝑥 ∈ ℕ → ( 𝑞 ∈ ( ◡ ( 𝑀 ‘ 𝑥 ) “ ℕ ) → 𝑞 ∈ ( 1 ... 𝑥 ) ) )
32 31 ssrdv ⊢ ( 𝑥 ∈ ℕ → ( ◡ ( 𝑀 ‘ 𝑥 ) “ ℕ ) ⊆ ( 1 ... 𝑥 ) )
33 ssfi ⊢ ( ( ( 1 ... 𝑥 ) ∈ Fin ∧ ( ◡ ( 𝑀 ‘ 𝑥 ) “ ℕ ) ⊆ ( 1 ... 𝑥 ) ) → ( ◡ ( 𝑀 ‘ 𝑥 ) “ ℕ ) ∈ Fin )
34 10 32 33 sylancr ⊢ ( 𝑥 ∈ ℕ → ( ◡ ( 𝑀 ‘ 𝑥 ) “ ℕ ) ∈ Fin )
35 cnveq ⊢ ( 𝑒 = ( 𝑀 ‘ 𝑥 ) → ◡ 𝑒 = ◡ ( 𝑀 ‘ 𝑥 ) )
36 35 imaeq1d ⊢ ( 𝑒 = ( 𝑀 ‘ 𝑥 ) → ( ◡ 𝑒 “ ℕ ) = ( ◡ ( 𝑀 ‘ 𝑥 ) “ ℕ ) )
37 36 eleq1d ⊢ ( 𝑒 = ( 𝑀 ‘ 𝑥 ) → ( ( ◡ 𝑒 “ ℕ ) ∈ Fin ↔ ( ◡ ( 𝑀 ‘ 𝑥 ) “ ℕ ) ∈ Fin ) )
38 37 2 elrab2 ⊢ ( ( 𝑀 ‘ 𝑥 ) ∈ 𝑅 ↔ ( ( 𝑀 ‘ 𝑥 ) ∈ ( ℕ0 ↑m ℙ ) ∧ ( ◡ ( 𝑀 ‘ 𝑥 ) “ ℕ ) ∈ Fin ) )
39 9 34 38 sylanbrc ⊢ ( 𝑥 ∈ ℕ → ( 𝑀 ‘ 𝑥 ) ∈ 𝑅 )
40 39 rgen ⊢ ∀ 𝑥 ∈ ℕ ( 𝑀 ‘ 𝑥 ) ∈ 𝑅
41 ffnfv ⊢ ( 𝑀 : ℕ ⟶ 𝑅 ↔ ( 𝑀 Fn ℕ ∧ ∀ 𝑥 ∈ ℕ ( 𝑀 ‘ 𝑥 ) ∈ 𝑅 ) )
42 5 40 41 mpbir2an ⊢ 𝑀 : ℕ ⟶ 𝑅
43 14 adantlr ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) = ( 𝑞 pCnt 𝑥 ) )
44 1 1arithlem2 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑀 ‘ 𝑦 ) ‘ 𝑞 ) = ( 𝑞 pCnt 𝑦 ) )
45 44 adantll ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑀 ‘ 𝑦 ) ‘ 𝑞 ) = ( 𝑞 pCnt 𝑦 ) )
46 43 45 eqeq12d ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) = ( ( 𝑀 ‘ 𝑦 ) ‘ 𝑞 ) ↔ ( 𝑞 pCnt 𝑥 ) = ( 𝑞 pCnt 𝑦 ) ) )
47 46 ralbidva ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑞 ∈ ℙ ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) = ( ( 𝑀 ‘ 𝑦 ) ‘ 𝑞 ) ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑥 ) = ( 𝑞 pCnt 𝑦 ) ) )
48 1 1arithlem3 ⊢ ( 𝑦 ∈ ℕ → ( 𝑀 ‘ 𝑦 ) : ℙ ⟶ ℕ0 )
49 ffn ⊢ ( ( 𝑀 ‘ 𝑦 ) : ℙ ⟶ ℕ0 → ( 𝑀 ‘ 𝑦 ) Fn ℙ )
50 eqfnfv ⊢ ( ( ( 𝑀 ‘ 𝑥 ) Fn ℙ ∧ ( 𝑀 ‘ 𝑦 ) Fn ℙ ) → ( ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑦 ) ↔ ∀ 𝑞 ∈ ℙ ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) = ( ( 𝑀 ‘ 𝑦 ) ‘ 𝑞 ) ) )
51 11 49 50 syl2an ⊢ ( ( ( 𝑀 ‘ 𝑥 ) : ℙ ⟶ ℕ0 ∧ ( 𝑀 ‘ 𝑦 ) : ℙ ⟶ ℕ0 ) → ( ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑦 ) ↔ ∀ 𝑞 ∈ ℙ ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) = ( ( 𝑀 ‘ 𝑦 ) ‘ 𝑞 ) ) )
52 6 48 51 syl2an ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑦 ) ↔ ∀ 𝑞 ∈ ℙ ( ( 𝑀 ‘ 𝑥 ) ‘ 𝑞 ) = ( ( 𝑀 ‘ 𝑦 ) ‘ 𝑞 ) ) )
53 nnnn0 ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ0 )
54 nnnn0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 )
55 pc11 ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑥 ) = ( 𝑞 pCnt 𝑦 ) ) )
56 53 54 55 syl2an ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑥 ) = ( 𝑞 pCnt 𝑦 ) ) )
57 47 52 56 3bitr4d ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
58 57 biimpd ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
59 58 rgen2 ⊢ ∀ 𝑥 ∈ ℕ ∀ 𝑦 ∈ ℕ ( ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑦 ) → 𝑥 = 𝑦 )
60 dff13 ⊢ ( 𝑀 : ℕ –1-1→ 𝑅 ↔ ( 𝑀 : ℕ ⟶ 𝑅 ∧ ∀ 𝑥 ∈ ℕ ∀ 𝑦 ∈ ℕ ( ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
61 42 59 60 mpbir2an ⊢ 𝑀 : ℕ –1-1→ 𝑅
62 eqid ⊢ ( 𝑔 ∈ ℕ ↦ if ( 𝑔 ∈ ℙ , ( 𝑔 ↑ ( 𝑓 ‘ 𝑔 ) ) , 1 ) ) = ( 𝑔 ∈ ℕ ↦ if ( 𝑔 ∈ ℙ , ( 𝑔 ↑ ( 𝑓 ‘ 𝑔 ) ) , 1 ) )
63 cnveq ⊢ ( 𝑒 = 𝑓 → ◡ 𝑒 = ◡ 𝑓 )
64 63 imaeq1d ⊢ ( 𝑒 = 𝑓 → ( ◡ 𝑒 “ ℕ ) = ( ◡ 𝑓 “ ℕ ) )
65 64 eleq1d ⊢ ( 𝑒 = 𝑓 → ( ( ◡ 𝑒 “ ℕ ) ∈ Fin ↔ ( ◡ 𝑓 “ ℕ ) ∈ Fin ) )
66 65 2 elrab2 ⊢ ( 𝑓 ∈ 𝑅 ↔ ( 𝑓 ∈ ( ℕ0 ↑m ℙ ) ∧ ( ◡ 𝑓 “ ℕ ) ∈ Fin ) )
67 66 simplbi ⊢ ( 𝑓 ∈ 𝑅 → 𝑓 ∈ ( ℕ0 ↑m ℙ ) )
68 7 3 elmap ⊢ ( 𝑓 ∈ ( ℕ0 ↑m ℙ ) ↔ 𝑓 : ℙ ⟶ ℕ0 )
69 67 68 sylib ⊢ ( 𝑓 ∈ 𝑅 → 𝑓 : ℙ ⟶ ℕ0 )
70 69 ad2antrr ⊢ ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) → 𝑓 : ℙ ⟶ ℕ0 )
71 simplr ⊢ ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) → 𝑦 ∈ ℝ )
72 0re ⊢ 0 ∈ ℝ
73 ifcl ⊢ ( ( 𝑦 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ )
74 71 72 73 sylancl ⊢ ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ )
75 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
76 72 71 75 sylancr ⊢ ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) → 0 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
77 flge0nn0 ⊢ ( ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) → ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) ∈ ℕ0 )
78 74 76 77 syl2anc ⊢ ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) → ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) ∈ ℕ0 )
79 nn0p1nn ⊢ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) ∈ ℕ0 → ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ∈ ℕ )
80 78 79 syl ⊢ ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) → ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ∈ ℕ )
81 71 adantr ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → 𝑦 ∈ ℝ )
82 80 adantr ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ∈ ℕ )
83 82 nnred ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ∈ ℝ )
84 16 ssriv ⊢ ℙ ⊆ ℤ
85 zssre ⊢ ℤ ⊆ ℝ
86 84 85 sstri ⊢ ℙ ⊆ ℝ
87 simprl ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → 𝑞 ∈ ℙ )
88 86 87 sselid ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → 𝑞 ∈ ℝ )
89 74 adantr ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ )
90 max2 ⊢ ( ( 0 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
91 72 81 90 sylancr ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → 𝑦 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
92 flltp1 ⊢ ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) < ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) )
93 89 92 syl ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) < ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) )
94 81 89 83 91 93 lelttrd ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → 𝑦 < ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) )
95 simprr ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 )
96 81 83 88 94 95 ltletrd ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → 𝑦 < 𝑞 )
97 81 88 ltnled ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( 𝑦 < 𝑞 ↔ ¬ 𝑞 ≤ 𝑦 ) )
98 96 97 mpbid ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ¬ 𝑞 ≤ 𝑦 )
99 87 biantrurd ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( ( 𝑓 ‘ 𝑞 ) ∈ ℕ ↔ ( 𝑞 ∈ ℙ ∧ ( 𝑓 ‘ 𝑞 ) ∈ ℕ ) ) )
100 70 adantr ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → 𝑓 : ℙ ⟶ ℕ0 )
101 ffn ⊢ ( 𝑓 : ℙ ⟶ ℕ0 → 𝑓 Fn ℙ )
102 elpreima ⊢ ( 𝑓 Fn ℙ → ( 𝑞 ∈ ( ◡ 𝑓 “ ℕ ) ↔ ( 𝑞 ∈ ℙ ∧ ( 𝑓 ‘ 𝑞 ) ∈ ℕ ) ) )
103 100 101 102 3syl ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( 𝑞 ∈ ( ◡ 𝑓 “ ℕ ) ↔ ( 𝑞 ∈ ℙ ∧ ( 𝑓 ‘ 𝑞 ) ∈ ℕ ) ) )
104 99 103 bitr4d ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( ( 𝑓 ‘ 𝑞 ) ∈ ℕ ↔ 𝑞 ∈ ( ◡ 𝑓 “ ℕ ) ) )
105 simplr ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 )
106 breq1 ⊢ ( 𝑘 = 𝑞 → ( 𝑘 ≤ 𝑦 ↔ 𝑞 ≤ 𝑦 ) )
107 106 rspccv ⊢ ( ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 → ( 𝑞 ∈ ( ◡ 𝑓 “ ℕ ) → 𝑞 ≤ 𝑦 ) )
108 105 107 syl ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( 𝑞 ∈ ( ◡ 𝑓 “ ℕ ) → 𝑞 ≤ 𝑦 ) )
109 104 108 sylbid ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( ( 𝑓 ‘ 𝑞 ) ∈ ℕ → 𝑞 ≤ 𝑦 ) )
110 98 109 mtod ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ¬ ( 𝑓 ‘ 𝑞 ) ∈ ℕ )
111 100 87 ffvelcdmd ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( 𝑓 ‘ 𝑞 ) ∈ ℕ0 )
112 elnn0 ⊢ ( ( 𝑓 ‘ 𝑞 ) ∈ ℕ0 ↔ ( ( 𝑓 ‘ 𝑞 ) ∈ ℕ ∨ ( 𝑓 ‘ 𝑞 ) = 0 ) )
113 111 112 sylib ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( ( 𝑓 ‘ 𝑞 ) ∈ ℕ ∨ ( 𝑓 ‘ 𝑞 ) = 0 ) )
114 113 ord ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( ¬ ( 𝑓 ‘ 𝑞 ) ∈ ℕ → ( 𝑓 ‘ 𝑞 ) = 0 ) )
115 110 114 mpd ⊢ ( ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) ∧ ( 𝑞 ∈ ℙ ∧ ( ( ⌊ ‘ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) + 1 ) ≤ 𝑞 ) ) → ( 𝑓 ‘ 𝑞 ) = 0 )
116 1 62 70 80 115 1arithlem4 ⊢ ( ( ( 𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℕ 𝑓 = ( 𝑀 ‘ 𝑥 ) )
117 cnvimass ⊢ ( ◡ 𝑓 “ ℕ ) ⊆ dom 𝑓
118 69 fdmd ⊢ ( 𝑓 ∈ 𝑅 → dom 𝑓 = ℙ )
119 118 86 eqsstrdi ⊢ ( 𝑓 ∈ 𝑅 → dom 𝑓 ⊆ ℝ )
120 117 119 sstrid ⊢ ( 𝑓 ∈ 𝑅 → ( ◡ 𝑓 “ ℕ ) ⊆ ℝ )
121 66 simprbi ⊢ ( 𝑓 ∈ 𝑅 → ( ◡ 𝑓 “ ℕ ) ∈ Fin )
122 fimaxre2 ⊢ ( ( ( ◡ 𝑓 “ ℕ ) ⊆ ℝ ∧ ( ◡ 𝑓 “ ℕ ) ∈ Fin ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 )
123 120 121 122 syl2anc ⊢ ( 𝑓 ∈ 𝑅 → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ( ◡ 𝑓 “ ℕ ) 𝑘 ≤ 𝑦 )
124 116 123 r19.29a ⊢ ( 𝑓 ∈ 𝑅 → ∃ 𝑥 ∈ ℕ 𝑓 = ( 𝑀 ‘ 𝑥 ) )
125 124 rgen ⊢ ∀ 𝑓 ∈ 𝑅 ∃ 𝑥 ∈ ℕ 𝑓 = ( 𝑀 ‘ 𝑥 )
126 dffo3 ⊢ ( 𝑀 : ℕ –onto→ 𝑅 ↔ ( 𝑀 : ℕ ⟶ 𝑅 ∧ ∀ 𝑓 ∈ 𝑅 ∃ 𝑥 ∈ ℕ 𝑓 = ( 𝑀 ‘ 𝑥 ) ) )
127 42 125 126 mpbir2an ⊢ 𝑀 : ℕ –onto→ 𝑅
128 df-f1o ⊢ ( 𝑀 : ℕ –1-1-onto→ 𝑅 ↔ ( 𝑀 : ℕ –1-1→ 𝑅 ∧ 𝑀 : ℕ –onto→ 𝑅 ) )
129 61 127 128 mpbir2an ⊢ 𝑀 : ℕ –1-1-onto→ 𝑅