Metamath Proof Explorer

Theorem dvdsflip

Description: An involution of the divisors of a number. (Contributed by Stefan O'Rear, 12-Sep-2015) (Proof shortened by Mario Carneiro, 13-May-2016)

Ref Expression
Hypotheses dvdsflip.a ⊢ 𝐴 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
dvdsflip.f ⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑁 / 𝑦 ) )
Assertion dvdsflip ( 𝑁 ∈ ℕ → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )

Proof

Step Hyp Ref Expression
1 dvdsflip.a ⊢ 𝐴 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
2 dvdsflip.f ⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑁 / 𝑦 ) )
3 1 eleq2i ⊢ ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
4 dvdsdivcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑦 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
5 3 4 sylan2b ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) → ( 𝑁 / 𝑦 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
6 5 1 eleqtrrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) → ( 𝑁 / 𝑦 ) ∈ 𝐴 )
7 1 eleq2i ⊢ ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
8 dvdsdivcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑧 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
9 7 8 sylan2b ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → ( 𝑁 / 𝑧 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
10 9 1 eleqtrrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → ( 𝑁 / 𝑧 ) ∈ 𝐴 )
11 1 ssrab3 ⊢ 𝐴 ⊆ ℕ
12 11 sseli ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℕ )
13 11 sseli ⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ℕ )
14 12 13 anim12i ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) )
15 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) → 𝑁 ∈ ℂ )
17 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
18 17 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) → 𝑦 ∈ ℂ )
19 nncn ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℂ )
20 19 ad2antll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) → 𝑧 ∈ ℂ )
21 nnne0 ⊢ ( 𝑧 ∈ ℕ → 𝑧 ≠ 0 )
22 21 ad2antll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) → 𝑧 ≠ 0 )
23 16 18 20 22 divmul3d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) → ( ( 𝑁 / 𝑧 ) = 𝑦 ↔ 𝑁 = ( 𝑦 · 𝑧 ) ) )
24 nnne0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
25 24 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) → 𝑦 ≠ 0 )
26 16 20 18 25 divmul2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) → ( ( 𝑁 / 𝑦 ) = 𝑧 ↔ 𝑁 = ( 𝑦 · 𝑧 ) ) )
27 23 26 bitr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) → ( ( 𝑁 / 𝑧 ) = 𝑦 ↔ ( 𝑁 / 𝑦 ) = 𝑧 ) )
28 14 27 sylan2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑁 / 𝑧 ) = 𝑦 ↔ ( 𝑁 / 𝑦 ) = 𝑧 ) )
29 eqcom ⊢ ( 𝑦 = ( 𝑁 / 𝑧 ) ↔ ( 𝑁 / 𝑧 ) = 𝑦 )
30 eqcom ⊢ ( 𝑧 = ( 𝑁 / 𝑦 ) ↔ ( 𝑁 / 𝑦 ) = 𝑧 )
31 28 29 30 3bitr4g ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 = ( 𝑁 / 𝑧 ) ↔ 𝑧 = ( 𝑁 / 𝑦 ) ) )
32 2 6 10 31 f1o2d ⊢ ( 𝑁 ∈ ℕ → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )