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 ⊢ A = x ∈ ℕ | x ∥ N
dvdsflip.f ⊢ F = y ∈ A ⟼ N y
Assertion dvdsflip ⊢ N ∈ ℕ → F : A ⟶ 1-1 onto A

Proof

Step Hyp Ref Expression
1 dvdsflip.a ⊢ A = x ∈ ℕ | x ∥ N
2 dvdsflip.f ⊢ F = y ∈ A ⟼ N y
3 1 eleq2i ⊢ y ∈ A ↔ y ∈ x ∈ ℕ | x ∥ N
4 dvdsdivcl ⊢ N ∈ ℕ ∧ y ∈ x ∈ ℕ | x ∥ N → N y ∈ x ∈ ℕ | x ∥ N
5 3 4 sylan2b ⊢ N ∈ ℕ ∧ y ∈ A → N y ∈ x ∈ ℕ | x ∥ N
6 5 1 eleqtrrdi ⊢ N ∈ ℕ ∧ y ∈ A → N y ∈ A
7 1 eleq2i ⊢ z ∈ A ↔ z ∈ x ∈ ℕ | x ∥ N
8 dvdsdivcl ⊢ N ∈ ℕ ∧ z ∈ x ∈ ℕ | x ∥ N → N z ∈ x ∈ ℕ | x ∥ N
9 7 8 sylan2b ⊢ N ∈ ℕ ∧ z ∈ A → N z ∈ x ∈ ℕ | x ∥ N
10 9 1 eleqtrrdi ⊢ N ∈ ℕ ∧ z ∈ A → N z ∈ A
11 1 ssrab3 ⊢ A ⊆ ℕ
12 11 sseli ⊢ y ∈ A → y ∈ ℕ
13 11 sseli ⊢ z ∈ A → z ∈ ℕ
14 12 13 anim12i ⊢ y ∈ A ∧ z ∈ A → y ∈ ℕ ∧ z ∈ ℕ
15 nncn ⊢ N ∈ ℕ → N ∈ ℂ
16 15 adantr ⊢ N ∈ ℕ ∧ y ∈ ℕ ∧ z ∈ ℕ → N ∈ ℂ
17 nncn ⊢ y ∈ ℕ → y ∈ ℂ
18 17 ad2antrl ⊢ N ∈ ℕ ∧ y ∈ ℕ ∧ z ∈ ℕ → y ∈ ℂ
19 nncn ⊢ z ∈ ℕ → z ∈ ℂ
20 19 ad2antll ⊢ N ∈ ℕ ∧ y ∈ ℕ ∧ z ∈ ℕ → z ∈ ℂ
21 nnne0 ⊢ z ∈ ℕ → z ≠ 0
22 21 ad2antll ⊢ N ∈ ℕ ∧ y ∈ ℕ ∧ z ∈ ℕ → z ≠ 0
23 16 18 20 22 divmul3d ⊢ N ∈ ℕ ∧ y ∈ ℕ ∧ z ∈ ℕ → N z = y ↔ N = y ⁢ z
24 nnne0 ⊢ y ∈ ℕ → y ≠ 0
25 24 ad2antrl ⊢ N ∈ ℕ ∧ y ∈ ℕ ∧ z ∈ ℕ → y ≠ 0
26 16 20 18 25 divmul2d ⊢ N ∈ ℕ ∧ y ∈ ℕ ∧ z ∈ ℕ → N y = z ↔ N = y ⁢ z
27 23 26 bitr4d ⊢ N ∈ ℕ ∧ y ∈ ℕ ∧ z ∈ ℕ → N z = y ↔ N y = z
28 14 27 sylan2 ⊢ N ∈ ℕ ∧ y ∈ A ∧ z ∈ A → N z = y ↔ N y = z
29 eqcom ⊢ y = N z ↔ N z = y
30 eqcom ⊢ z = N y ↔ N y = z
31 28 29 30 3bitr4g ⊢ N ∈ ℕ ∧ y ∈ A ∧ z ∈ A → y = N z ↔ z = N y
32 2 6 10 31 f1o2d ⊢ N ∈ ℕ → F : A ⟶ 1-1 onto A