hashgcdlem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > hashgcdlem		GIF version

Theorem hashgcdlem 12221

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 5876	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 gcd (𝑀 / 𝑁)) = (𝑥 gcd (𝑀 / 𝑁)))
3	2	eqeq1d 2186	. . . 4 ⊢ (𝑦 = 𝑥 → ((𝑦 gcd (𝑀 / 𝑁)) = 1 ↔ (𝑥 gcd (𝑀 / 𝑁)) = 1))
4		hashgcdlem.a	. . . 4 ⊢ 𝐴 = {𝑦 ∈ (0..^(𝑀 / 𝑁)) ∣ (𝑦 gcd (𝑀 / 𝑁)) = 1}
5	3, 4	elrab2 2896	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1))
6		elfzonn0 10172	. . . . . . 7 ⊢ (𝑥 ∈ (0..^(𝑀 / 𝑁)) → 𝑥 ∈ ℕ₀)
7	6	ad2antrl 490	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 ∈ ℕ₀)
8		nnnn0 9172	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
9	8	3ad2ant2 1019	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ∈ ℕ₀)
10	9	adantr 276	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑁 ∈ ℕ₀)
11	7, 10	nn0mulcld 9223	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) ∈ ℕ₀)
12		simpl1 1000	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑀 ∈ ℕ)
13		elfzolt2 10142	. . . . . . 7 ⊢ (𝑥 ∈ (0..^(𝑀 / 𝑁)) → 𝑥 < (𝑀 / 𝑁))
14	13	ad2antrl 490	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 < (𝑀 / 𝑁))
15		elfzoelz 10133	. . . . . . . . 9 ⊢ (𝑥 ∈ (0..^(𝑀 / 𝑁)) → 𝑥 ∈ ℤ)
16	15	ad2antrl 490	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 ∈ ℤ)
17	16	zred 9364	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 ∈ ℝ)
18		nnre 8915	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
19	18	3ad2ant1 1018	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑀 ∈ ℝ)
20	19	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑀 ∈ ℝ)
21		nnre 8915	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
22		nngt0 8933	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
23	21, 22	jca 306	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
24	23	3ad2ant2 1019	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
25	24	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
26		ltmuldiv 8820	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑥 · 𝑁) < 𝑀 ↔ 𝑥 < (𝑀 / 𝑁)))
27	17, 20, 25, 26	syl3anc 1238	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 · 𝑁) < 𝑀 ↔ 𝑥 < (𝑀 / 𝑁)))
28	14, 27	mpbird 167	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) < 𝑀)
29		elfzo0 10168	. . . . 5 ⊢ ((𝑥 · 𝑁) ∈ (0..^𝑀) ↔ ((𝑥 · 𝑁) ∈ ℕ₀ ∧ 𝑀 ∈ ℕ ∧ (𝑥 · 𝑁) < 𝑀))
30	11, 12, 28, 29	syl3anbrc 1181	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) ∈ (0..^𝑀))
31		nncn 8916	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
32	31	3ad2ant1 1018	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑀 ∈ ℂ)
33		nncn 8916	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
34	33	3ad2ant2 1019	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ∈ ℂ)
35		nnap0 8937	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 # 0)
36	35	3ad2ant2 1019	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 # 0)
37	32, 34, 36	divcanap1d 8737	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → ((𝑀 / 𝑁) · 𝑁) = 𝑀)
38	37	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑀 / 𝑁) · 𝑁) = 𝑀)
39	38	eqcomd 2183	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑀 = ((𝑀 / 𝑁) · 𝑁))
40	39	oveq2d 5885	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 · 𝑁) gcd 𝑀) = ((𝑥 · 𝑁) gcd ((𝑀 / 𝑁) · 𝑁)))
41		nndivdvds 11787	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ 𝑀 ↔ (𝑀 / 𝑁) ∈ ℕ))
42	41	biimp3a 1345	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑀 / 𝑁) ∈ ℕ)
43	42	nnzd 9363	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑀 / 𝑁) ∈ ℤ)
44	43	adantr 276	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑀 / 𝑁) ∈ ℤ)
45		mulgcdr 12002	. . . . . 6 ⊢ ((𝑥 ∈ ℤ ∧ (𝑀 / 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℕ₀) → ((𝑥 · 𝑁) gcd ((𝑀 / 𝑁) · 𝑁)) = ((𝑥 gcd (𝑀 / 𝑁)) · 𝑁))
46	16, 44, 10, 45	syl3anc 1238	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 · 𝑁) gcd ((𝑀 / 𝑁) · 𝑁)) = ((𝑥 gcd (𝑀 / 𝑁)) · 𝑁))
47		simprr 531	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 gcd (𝑀 / 𝑁)) = 1)
48	47	oveq1d 5884	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 gcd (𝑀 / 𝑁)) · 𝑁) = (1 · 𝑁))
49	34	mulid2d 7966	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (1 · 𝑁) = 𝑁)
50	49	adantr 276	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (1 · 𝑁) = 𝑁)
51	48, 50	eqtrd 2210	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 gcd (𝑀 / 𝑁)) · 𝑁) = 𝑁)
52	40, 46, 51	3eqtrd 2214	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 · 𝑁) gcd 𝑀) = 𝑁)
53		oveq1 5876	. . . . . 6 ⊢ (𝑧 = (𝑥 · 𝑁) → (𝑧 gcd 𝑀) = ((𝑥 · 𝑁) gcd 𝑀))
54	53	eqeq1d 2186	. . . . 5 ⊢ (𝑧 = (𝑥 · 𝑁) → ((𝑧 gcd 𝑀) = 𝑁 ↔ ((𝑥 · 𝑁) gcd 𝑀) = 𝑁))
55		hashgcdlem.b	. . . . 5 ⊢ 𝐵 = {𝑧 ∈ (0..^𝑀) ∣ (𝑧 gcd 𝑀) = 𝑁}
56	54, 55	elrab2 2896	. . . 4 ⊢ ((𝑥 · 𝑁) ∈ 𝐵 ↔ ((𝑥 · 𝑁) ∈ (0..^𝑀) ∧ ((𝑥 · 𝑁) gcd 𝑀) = 𝑁))
57	30, 52, 56	sylanbrc 417	. . 3 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) ∈ 𝐵)
58	5, 57	sylan2b 287	. 2 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ 𝑥 ∈ 𝐴) → (𝑥 · 𝑁) ∈ 𝐵)
59		oveq1 5876	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 gcd 𝑀) = (𝑤 gcd 𝑀))
60	59	eqeq1d 2186	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝑧 gcd 𝑀) = 𝑁 ↔ (𝑤 gcd 𝑀) = 𝑁))
61	60, 55	elrab2 2896	. . 3 ⊢ (𝑤 ∈ 𝐵 ↔ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁))
62		simprr 531	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 gcd 𝑀) = 𝑁)
63		elfzoelz 10133	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ ℤ)
64	63	ad2antrl 490	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 ∈ ℤ)
65		simpl1 1000	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑀 ∈ ℕ)
66	65	nnzd 9363	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑀 ∈ ℤ)
67		gcddvds 11947	. . . . . . . . . 10 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
68	64, 66, 67	syl2anc 411	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
69	68	simpld 112	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 gcd 𝑀) ∥ 𝑤)
70	62, 69	eqbrtrrd 4024	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∥ 𝑤)
71		nnz 9261	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
72	71	3ad2ant2 1019	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ∈ ℤ)
73	72	adantr 276	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∈ ℤ)
74		nnne0 8936	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
75	74	3ad2ant2 1019	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ≠ 0)
76	75	adantr 276	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ≠ 0)
77		dvdsval2 11781	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ 𝑤 ∈ ℤ) → (𝑁 ∥ 𝑤 ↔ (𝑤 / 𝑁) ∈ ℤ))
78	73, 76, 64, 77	syl3anc 1238	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑁 ∥ 𝑤 ↔ (𝑤 / 𝑁) ∈ ℤ))
79	70, 78	mpbid 147	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ ℤ)
80		elfzofz 10148	. . . . . . . . 9 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ (0...𝑀))
81	80	ad2antrl 490	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 ∈ (0...𝑀))
82		elfznn0 10100	. . . . . . . 8 ⊢ (𝑤 ∈ (0...𝑀) → 𝑤 ∈ ℕ₀)
83		nn0re 9174	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ₀ → 𝑤 ∈ ℝ)
84		nn0ge0 9190	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ₀ → 0 ≤ 𝑤)
85	83, 84	jca 306	. . . . . . . 8 ⊢ (𝑤 ∈ ℕ₀ → (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤))
86	81, 82, 85	3syl 17	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤))
87	24	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
88		divge0 8819	. . . . . . 7 ⊢ (((𝑤 ∈ ℝ ∧ 0 ≤ 𝑤) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑤 / 𝑁))
89	86, 87, 88	syl2anc 411	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 0 ≤ (𝑤 / 𝑁))
90		elnn0z 9255	. . . . . 6 ⊢ ((𝑤 / 𝑁) ∈ ℕ₀ ↔ ((𝑤 / 𝑁) ∈ ℤ ∧ 0 ≤ (𝑤 / 𝑁)))
91	79, 89, 90	sylanbrc 417	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ ℕ₀)
92	42	adantr 276	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑀 / 𝑁) ∈ ℕ)
93		elfzolt2 10142	. . . . . . 7 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 < 𝑀)
94	93	ad2antrl 490	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 < 𝑀)
95	64	zred 9364	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 ∈ ℝ)
96	19	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑀 ∈ ℝ)
97		ltdiv1 8814	. . . . . . 7 ⊢ ((𝑤 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑤 < 𝑀 ↔ (𝑤 / 𝑁) < (𝑀 / 𝑁)))
98	95, 96, 87, 97	syl3anc 1238	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 < 𝑀 ↔ (𝑤 / 𝑁) < (𝑀 / 𝑁)))
99	94, 98	mpbid 147	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) < (𝑀 / 𝑁))
100		elfzo0 10168	. . . . 5 ⊢ ((𝑤 / 𝑁) ∈ (0..^(𝑀 / 𝑁)) ↔ ((𝑤 / 𝑁) ∈ ℕ₀ ∧ (𝑀 / 𝑁) ∈ ℕ ∧ (𝑤 / 𝑁) < (𝑀 / 𝑁)))
101	91, 92, 99, 100	syl3anbrc 1181	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ (0..^(𝑀 / 𝑁)))
102	62	oveq1d 5884	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 gcd 𝑀) / 𝑁) = (𝑁 / 𝑁))
103		simpl2 1001	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∈ ℕ)
104		simpl3 1002	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∥ 𝑀)
105		gcddiv 12003	. . . . . 6 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 ∥ 𝑤 ∧ 𝑁 ∥ 𝑀)) → ((𝑤 gcd 𝑀) / 𝑁) = ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)))
106	64, 66, 103, 70, 104, 105	syl32anc 1246	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 gcd 𝑀) / 𝑁) = ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)))
107	34, 36	dividapd 8732	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑁 / 𝑁) = 1)
108	107	adantr 276	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑁 / 𝑁) = 1)
109	102, 106, 108	3eqtr3d 2218	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)) = 1)
110		oveq1 5876	. . . . . 6 ⊢ (𝑦 = (𝑤 / 𝑁) → (𝑦 gcd (𝑀 / 𝑁)) = ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)))
111	110	eqeq1d 2186	. . . . 5 ⊢ (𝑦 = (𝑤 / 𝑁) → ((𝑦 gcd (𝑀 / 𝑁)) = 1 ↔ ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)) = 1))
112	111, 4	elrab2 2896	. . . 4 ⊢ ((𝑤 / 𝑁) ∈ 𝐴 ↔ ((𝑤 / 𝑁) ∈ (0..^(𝑀 / 𝑁)) ∧ ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)) = 1))
113	101, 109, 112	sylanbrc 417	. . 3 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ 𝐴)
114	61, 113	sylan2b 287	. 2 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ 𝑤 ∈ 𝐵) → (𝑤 / 𝑁) ∈ 𝐴)
115	5	simplbi 274	. . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (0..^(𝑀 / 𝑁)))
116	61	simplbi 274	. . . 4 ⊢ (𝑤 ∈ 𝐵 → 𝑤 ∈ (0..^𝑀))
117	115, 116	anim12i 338	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀)))
118	63	ad2antll 491	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑤 ∈ ℤ)
119	118	zcnd 9365	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑤 ∈ ℂ)
120	34	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑁 ∈ ℂ)
121	36	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑁 # 0)
122	119, 120, 121	divcanap1d 8737	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → ((𝑤 / 𝑁) · 𝑁) = 𝑤)
123	122	eqcomd 2183	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑤 = ((𝑤 / 𝑁) · 𝑁))
124		oveq1 5876	. . . . . 6 ⊢ (𝑥 = (𝑤 / 𝑁) → (𝑥 · 𝑁) = ((𝑤 / 𝑁) · 𝑁))
125	124	eqeq2d 2189	. . . . 5 ⊢ (𝑥 = (𝑤 / 𝑁) → (𝑤 = (𝑥 · 𝑁) ↔ 𝑤 = ((𝑤 / 𝑁) · 𝑁)))
126	123, 125	syl5ibrcom 157	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → (𝑥 = (𝑤 / 𝑁) → 𝑤 = (𝑥 · 𝑁)))
127	15	ad2antrl 490	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑥 ∈ ℤ)
128	127	zcnd 9365	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑥 ∈ ℂ)
129	128, 120, 121	divcanap4d 8742	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → ((𝑥 · 𝑁) / 𝑁) = 𝑥)
130	129	eqcomd 2183	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑥 = ((𝑥 · 𝑁) / 𝑁))
131		oveq1 5876	. . . . . 6 ⊢ (𝑤 = (𝑥 · 𝑁) → (𝑤 / 𝑁) = ((𝑥 · 𝑁) / 𝑁))
132	131	eqeq2d 2189	. . . . 5 ⊢ (𝑤 = (𝑥 · 𝑁) → (𝑥 = (𝑤 / 𝑁) ↔ 𝑥 = ((𝑥 · 𝑁) / 𝑁)))
133	130, 132	syl5ibrcom 157	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → (𝑤 = (𝑥 · 𝑁) → 𝑥 = (𝑤 / 𝑁)))
134	126, 133	impbid 129	. . 3 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → (𝑥 = (𝑤 / 𝑁) ↔ 𝑤 = (𝑥 · 𝑁)))
135	117, 134	sylan2 286	. 2 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (𝑥 = (𝑤 / 𝑁) ↔ 𝑤 = (𝑥 · 𝑁)))
136	1, 58, 114, 135	f1o2d 6070	1 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝐹:𝐴–1-1-onto→𝐵)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 978 = wceq 1353 ∈ wcel 2148 ≠ wne 2347 {crab 2459 class class class wbr 4000 ↦ cmpt 4061 –1-1-onto→wf1o 5211 (class class class)co 5869 ℂcc 7800 ℝcr 7801 0cc0 7802 1c1 7803 · cmul 7807 < clt 7982 ≤ cle 7983 # cap 8528 / cdiv 8618 ℕcn 8908 ℕ₀cn0 9165 ℤcz 9242 ...cfz 9995 ..^cfzo 10128 ∥ cdvds 11778 gcd cgcd 11926

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-iinf 4584 ax-cnex 7893 ax-resscn 7894 ax-1cn 7895 ax-1re 7896 ax-icn 7897 ax-addcl 7898 ax-addrcl 7899 ax-mulcl 7900 ax-mulrcl 7901 ax-addcom 7902 ax-mulcom 7903 ax-addass 7904 ax-mulass 7905 ax-distr 7906 ax-i2m1 7907 ax-0lt1 7908 ax-1rid 7909 ax-0id 7910 ax-rnegex 7911 ax-precex 7912 ax-cnre 7913 ax-pre-ltirr 7914 ax-pre-ltwlin 7915 ax-pre-lttrn 7916 ax-pre-apti 7917 ax-pre-ltadd 7918 ax-pre-mulgt0 7919 ax-pre-mulext 7920 ax-arch 7921 ax-caucvg 7922

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4290 df-po 4293 df-iso 4294 df-iord 4363 df-on 4365 df-ilim 4366 df-suc 4368 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-f1 5217 df-fo 5218 df-f1o 5219 df-fv 5220 df-riota 5825 df-ov 5872 df-oprab 5873 df-mpo 5874 df-1st 6135 df-2nd 6136 df-recs 6300 df-frec 6386 df-sup 6977 df-pnf 7984 df-mnf 7985 df-xr 7986 df-ltxr 7987 df-le 7988 df-sub 8120 df-neg 8121 df-reap 8522 df-ap 8529 df-div 8619 df-inn 8909 df-2 8967 df-3 8968 df-4 8969 df-n0 9166 df-z 9243 df-uz 9518 df-q 9609 df-rp 9641 df-fz 9996 df-fzo 10129 df-fl 10256 df-mod 10309 df-seqfrec 10432 df-exp 10506 df-cj 10835 df-re 10836 df-im 10837 df-rsqrt 10991 df-abs 10992 df-dvds 11779 df-gcd 11927

This theorem is referenced by: hashgcdeq 12222

W3C validator