hashgcdlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hashgcdlem		Structured version Visualization version GIF version

Theorem hashgcdlem 16848

Description: A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)

**Hypotheses**
Ref	Expression
hashgcdlem.a	⊢ 𝐴 = {𝑦 ∈ (0..^(𝑀 / 𝑁)) ∣ (𝑦 gcd (𝑀 / 𝑁)) = 1}
hashgcdlem.b	⊢ 𝐵 = {𝑧 ∈ (0..^𝑀) ∣ (𝑧 gcd 𝑀) = 𝑁}
hashgcdlem.f	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝑥 · 𝑁))

**Assertion**
Ref	Expression
hashgcdlem	⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝐹:𝐴–1-1-onto→𝐵)

Distinct variable groups: 𝑥,𝑦,𝑀 𝑥,𝑧,𝑀 𝑥,𝐴 𝑥,𝐵 𝑥,𝑁,𝑦 𝑧,𝑁 Allowed substitution hints: 𝐴(𝑦,𝑧) 𝐵(𝑦,𝑧) 𝐹(𝑥,𝑦,𝑧)

Proof of Theorem hashgcdlem Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hashgcdlem.f	. 2 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝑥 · 𝑁))
2		oveq1 7419	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 gcd (𝑀 / 𝑁)) = (𝑥 gcd (𝑀 / 𝑁)))
3	2	eqeq1d 2765	. . . 4 ⊢ (𝑦 = 𝑥 → ((𝑦 gcd (𝑀 / 𝑁)) = 1 ↔ (𝑥 gcd (𝑀 / 𝑁)) = 1))
4		hashgcdlem.a	. . . 4 ⊢ 𝐴 = {𝑦 ∈ (0..^(𝑀 / 𝑁)) ∣ (𝑦 gcd (𝑀 / 𝑁)) = 1}
5	3, 4	elrab2 3655	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1))
6		elfzonn0 13738	. . . . . . 7 ⊢ (𝑥 ∈ (0..^(𝑀 / 𝑁)) → 𝑥 ∈ ℕ₀)
7	6	ad2antrl 740	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 ∈ ℕ₀)
8		nnnn0 12512	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
9	8	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ∈ ℕ₀)
10	9	adantr 485	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑁 ∈ ℕ₀)
11	7, 10	nn0mulcld 12571	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) ∈ ℕ₀)
12		simpl1 1210	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑀 ∈ ℕ)
13		elfzolt2 13699	. . . . . . 7 ⊢ (𝑥 ∈ (0..^(𝑀 / 𝑁)) → 𝑥 < (𝑀 / 𝑁))
14	13	ad2antrl 740	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 < (𝑀 / 𝑁))
15		elfzoelz 13689	. . . . . . . . 9 ⊢ (𝑥 ∈ (0..^(𝑀 / 𝑁)) → 𝑥 ∈ ℤ)
16	15	ad2antrl 740	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 ∈ ℤ)
17	16	zred 12701	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 ∈ ℝ)
18		nnre 12241	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
19	18	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑀 ∈ ℝ)
20	19	adantr 485	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑀 ∈ ℝ)
21		nnre 12241	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
22		nngt0 12268	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
23	21, 22	jca 520	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
24	23	3ad2ant2 1152	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
25	24	adantr 485	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
26		ltmuldiv 12089	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑥 · 𝑁) < 𝑀 ↔ 𝑥 < (𝑀 / 𝑁)))
27	17, 20, 25, 26	syl3anc 1398	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 · 𝑁) < 𝑀 ↔ 𝑥 < (𝑀 / 𝑁)))
28	14, 27	mpbird 260	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) < 𝑀)
29		elfzo0 13731	. . . . 5 ⊢ ((𝑥 · 𝑁) ∈ (0..^𝑀) ↔ ((𝑥 · 𝑁) ∈ ℕ₀ ∧ 𝑀 ∈ ℕ ∧ (𝑥 · 𝑁) < 𝑀))
30	11, 12, 28, 29	syl3anbrc 1362	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) ∈ (0..^𝑀))
31		nncn 12242	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
32	31	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑀 ∈ ℂ)
33		nncn 12242	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
34	33	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ∈ ℂ)
35		nnne0 12271	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
36	35	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ≠ 0)
37	32, 34, 36	divcan1d 11993	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → ((𝑀 / 𝑁) · 𝑁) = 𝑀)
38	37	adantr 485	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑀 / 𝑁) · 𝑁) = 𝑀)
39	38	eqcomd 2769	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑀 = ((𝑀 / 𝑁) · 𝑁))
40	39	oveq2d 7428	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 · 𝑁) gcd 𝑀) = ((𝑥 · 𝑁) gcd ((𝑀 / 𝑁) · 𝑁)))
41		nndivdvds 16320	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ 𝑀 ↔ (𝑀 / 𝑁) ∈ ℕ))
42	41	biimp3a 1498	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑀 / 𝑁) ∈ ℕ)
43	42	nnzd 12618	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑀 / 𝑁) ∈ ℤ)
44	43	adantr 485	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑀 / 𝑁) ∈ ℤ)
45		mulgcdr 16609	. . . . . 6 ⊢ ((𝑥 ∈ ℤ ∧ (𝑀 / 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℕ₀) → ((𝑥 · 𝑁) gcd ((𝑀 / 𝑁) · 𝑁)) = ((𝑥 gcd (𝑀 / 𝑁)) · 𝑁))
46	16, 44, 10, 45	syl3anc 1398	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 · 𝑁) gcd ((𝑀 / 𝑁) · 𝑁)) = ((𝑥 gcd (𝑀 / 𝑁)) · 𝑁))
47		simprr 784	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 gcd (𝑀 / 𝑁)) = 1)
48	47	oveq1d 7427	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 gcd (𝑀 / 𝑁)) · 𝑁) = (1 · 𝑁))
49	34	mullidd 11228	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (1 · 𝑁) = 𝑁)
50	49	adantr 485	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (1 · 𝑁) = 𝑁)
51	48, 50	eqtrd 2798	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 gcd (𝑀 / 𝑁)) · 𝑁) = 𝑁)
52	40, 46, 51	3eqtrd 2802	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 · 𝑁) gcd 𝑀) = 𝑁)
53		oveq1 7419	. . . . . 6 ⊢ (𝑧 = (𝑥 · 𝑁) → (𝑧 gcd 𝑀) = ((𝑥 · 𝑁) gcd 𝑀))
54	53	eqeq1d 2765	. . . . 5 ⊢ (𝑧 = (𝑥 · 𝑁) → ((𝑧 gcd 𝑀) = 𝑁 ↔ ((𝑥 · 𝑁) gcd 𝑀) = 𝑁))
55		hashgcdlem.b	. . . . 5 ⊢ 𝐵 = {𝑧 ∈ (0..^𝑀) ∣ (𝑧 gcd 𝑀) = 𝑁}
56	54, 55	elrab2 3655	. . . 4 ⊢ ((𝑥 · 𝑁) ∈ 𝐵 ↔ ((𝑥 · 𝑁) ∈ (0..^𝑀) ∧ ((𝑥 · 𝑁) gcd 𝑀) = 𝑁))
57	30, 52, 56	sylanbrc 594	. . 3 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) ∈ 𝐵)
58	5, 57	sylan2b 605	. 2 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ 𝑥 ∈ 𝐴) → (𝑥 · 𝑁) ∈ 𝐵)
59		oveq1 7419	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 gcd 𝑀) = (𝑤 gcd 𝑀))
60	59	eqeq1d 2765	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝑧 gcd 𝑀) = 𝑁 ↔ (𝑤 gcd 𝑀) = 𝑁))
61	60, 55	elrab2 3655	. . 3 ⊢ (𝑤 ∈ 𝐵 ↔ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁))
62		simprr 784	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 gcd 𝑀) = 𝑁)
63		elfzoelz 13689	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ ℤ)
64	63	ad2antrl 740	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 ∈ ℤ)
65		simpl1 1210	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑀 ∈ ℕ)
66	65	nnzd 12618	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑀 ∈ ℤ)
67		gcddvds 16562	. . . . . . . . . 10 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
68	64, 66, 67	syl2anc 595	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
69	68	simpld 499	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 gcd 𝑀) ∥ 𝑤)
70	62, 69	eqbrtrrd 5136	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∥ 𝑤)
71		nnz 12613	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
72	71	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ∈ ℤ)
73	72	adantr 485	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∈ ℤ)
74	36	adantr 485	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ≠ 0)
75		dvdsval2 16314	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ 𝑤 ∈ ℤ) → (𝑁 ∥ 𝑤 ↔ (𝑤 / 𝑁) ∈ ℤ))
76	73, 74, 64, 75	syl3anc 1398	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑁 ∥ 𝑤 ↔ (𝑤 / 𝑁) ∈ ℤ))
77	70, 76	mpbid 235	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ ℤ)
78		elfzofz 13706	. . . . . . . . 9 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ (0...𝑀))
79	78	ad2antrl 740	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 ∈ (0...𝑀))
80		elfznn0 13650	. . . . . . . 8 ⊢ (𝑤 ∈ (0...𝑀) → 𝑤 ∈ ℕ₀)
81		nn0re 12514	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ₀ → 𝑤 ∈ ℝ)
82		nn0ge0 12530	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ₀ → 0 ≤ 𝑤)
83	81, 82	jca 520	. . . . . . . 8 ⊢ (𝑤 ∈ ℕ₀ → (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤))
84	79, 80, 83	3syl 19	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤))
85	24	adantr 485	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
86		divge0 12085	. . . . . . 7 ⊢ (((𝑤 ∈ ℝ ∧ 0 ≤ 𝑤) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑤 / 𝑁))
87	84, 85, 86	syl2anc 595	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 0 ≤ (𝑤 / 𝑁))
88		elnn0z 12605	. . . . . 6 ⊢ ((𝑤 / 𝑁) ∈ ℕ₀ ↔ ((𝑤 / 𝑁) ∈ ℤ ∧ 0 ≤ (𝑤 / 𝑁)))
89	77, 87, 88	sylanbrc 594	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ ℕ₀)
90	42	adantr 485	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑀 / 𝑁) ∈ ℕ)
91		elfzolt2 13699	. . . . . . 7 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 < 𝑀)
92	91	ad2antrl 740	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 < 𝑀)
93	64	zred 12701	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 ∈ ℝ)
94	19	adantr 485	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑀 ∈ ℝ)
95		ltdiv1 12080	. . . . . . 7 ⊢ ((𝑤 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑤 < 𝑀 ↔ (𝑤 / 𝑁) < (𝑀 / 𝑁)))
96	93, 94, 85, 95	syl3anc 1398	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 < 𝑀 ↔ (𝑤 / 𝑁) < (𝑀 / 𝑁)))
97	92, 96	mpbid 235	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) < (𝑀 / 𝑁))
98		elfzo0 13731	. . . . 5 ⊢ ((𝑤 / 𝑁) ∈ (0..^(𝑀 / 𝑁)) ↔ ((𝑤 / 𝑁) ∈ ℕ₀ ∧ (𝑀 / 𝑁) ∈ ℕ ∧ (𝑤 / 𝑁) < (𝑀 / 𝑁)))
99	89, 90, 97, 98	syl3anbrc 1362	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ (0..^(𝑀 / 𝑁)))
100	62	oveq1d 7427	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 gcd 𝑀) / 𝑁) = (𝑁 / 𝑁))
101		simpl2 1211	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∈ ℕ)
102		simpl3 1212	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∥ 𝑀)
103		gcddiv 16610	. . . . . 6 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 ∥ 𝑤 ∧ 𝑁 ∥ 𝑀)) → ((𝑤 gcd 𝑀) / 𝑁) = ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)))
104	64, 66, 101, 70, 102, 103	syl32anc 1405	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 gcd 𝑀) / 𝑁) = ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)))
105	34, 36	dividd 11990	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑁 / 𝑁) = 1)
106	105	adantr 485	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑁 / 𝑁) = 1)
107	100, 104, 106	3eqtr3d 2806	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)) = 1)
108		oveq1 7419	. . . . . 6 ⊢ (𝑦 = (𝑤 / 𝑁) → (𝑦 gcd (𝑀 / 𝑁)) = ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)))
109	108	eqeq1d 2765	. . . . 5 ⊢ (𝑦 = (𝑤 / 𝑁) → ((𝑦 gcd (𝑀 / 𝑁)) = 1 ↔ ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)) = 1))
110	109, 4	elrab2 3655	. . . 4 ⊢ ((𝑤 / 𝑁) ∈ 𝐴 ↔ ((𝑤 / 𝑁) ∈ (0..^(𝑀 / 𝑁)) ∧ ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)) = 1))
111	99, 107, 110	sylanbrc 594	. . 3 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ 𝐴)
112	61, 111	sylan2b 605	. 2 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ 𝑤 ∈ 𝐵) → (𝑤 / 𝑁) ∈ 𝐴)
113	5	simplbi 501	. . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (0..^(𝑀 / 𝑁)))
114	61	simplbi 501	. . . 4 ⊢ (𝑤 ∈ 𝐵 → 𝑤 ∈ (0..^𝑀))
115	113, 114	anim12i 624	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀)))
116	63	ad2antll 741	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑤 ∈ ℤ)
117	116	zcnd 12702	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑤 ∈ ℂ)
118	34	adantr 485	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑁 ∈ ℂ)
119	36	adantr 485	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑁 ≠ 0)
120	117, 118, 119	divcan1d 11993	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → ((𝑤 / 𝑁) · 𝑁) = 𝑤)
121	120	eqcomd 2769	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑤 = ((𝑤 / 𝑁) · 𝑁))
122		oveq1 7419	. . . . . 6 ⊢ (𝑥 = (𝑤 / 𝑁) → (𝑥 · 𝑁) = ((𝑤 / 𝑁) · 𝑁))
123	122	eqeq2d 2774	. . . . 5 ⊢ (𝑥 = (𝑤 / 𝑁) → (𝑤 = (𝑥 · 𝑁) ↔ 𝑤 = ((𝑤 / 𝑁) · 𝑁)))
124	121, 123	syl5ibrcom 250	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → (𝑥 = (𝑤 / 𝑁) → 𝑤 = (𝑥 · 𝑁)))
125	15	ad2antrl 740	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑥 ∈ ℤ)
126	125	zcnd 12702	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑥 ∈ ℂ)
127	126, 118, 119	divcan4d 11998	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → ((𝑥 · 𝑁) / 𝑁) = 𝑥)
128	127	eqcomd 2769	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑥 = ((𝑥 · 𝑁) / 𝑁))
129		oveq1 7419	. . . . . 6 ⊢ (𝑤 = (𝑥 · 𝑁) → (𝑤 / 𝑁) = ((𝑥 · 𝑁) / 𝑁))
130	129	eqeq2d 2774	. . . . 5 ⊢ (𝑤 = (𝑥 · 𝑁) → (𝑥 = (𝑤 / 𝑁) ↔ 𝑥 = ((𝑥 · 𝑁) / 𝑁)))
131	128, 130	syl5ibrcom 250	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → (𝑤 = (𝑥 · 𝑁) → 𝑥 = (𝑤 / 𝑁)))
132	124, 131	impbid 215	. . 3 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → (𝑥 = (𝑤 / 𝑁) ↔ 𝑤 = (𝑥 · 𝑁)))
133	115, 132	sylan2 604	. 2 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (𝑥 = (𝑤 / 𝑁) ↔ 𝑤 = (𝑥 · 𝑁)))
134	1, 58, 112, 133	f1o2d 7666	1 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝐹:𝐴–1-1-onto→𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 {crab 3416 class class class wbr 5110 ↦ cmpt 5193 –1-1-onto→wf1o 6537 (class class class)co 7412 ℂcc 11099 ℝcr 11100 0cc0 11101 1c1 11102 · cmul 11106 < clt 11244 ≤ cle 11245 / cdiv 11872 ℕcn 12234 ℕ₀cn0 12505 ℤcz 12592 ...cfz 13536 ..^cfzo 13684 ∥ cdvds 16311 gcd cgcd 16553

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178 ax-pre-sup 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-sup 9403 df-inf 9404 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-div 11873 df-nn 12235 df-2 12304 df-3 12305 df-n0 12506 df-z 12593 df-uz 12864 df-rp 13018 df-fz 13537 df-fzo 13685 df-fl 13827 df-mod 13905 df-seq 14040 df-exp 14100 df-cj 15152 df-re 15153 df-im 15154 df-sqrt 15288 df-abs 15289 df-dvds 16312 df-gcd 16554

This theorem is referenced by: hashgcdeq 16850

W3C validator