hashgcdlem - Intuitionistic Logic Explorer

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

Theorem hashgcdlem 12238

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 5882	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 gcd (𝑀 / 𝑁)) = (𝑥 gcd (𝑀 / 𝑁)))
3	2	eqeq1d 2186	. . . 4 ⊢ (𝑦 = 𝑥 → ((𝑦 gcd (𝑀 / 𝑁)) = 1 ↔ (𝑥 gcd (𝑀 / 𝑁)) = 1))
4		hashgcdlem.a	. . . 4 ⊢ 𝐴 = {𝑦 ∈ (0..^(𝑀 / 𝑁)) ∣ (𝑦 gcd (𝑀 / 𝑁)) = 1}
5	3, 4	elrab2 2897	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1))
6		elfzonn0 10186	. . . . . . 7 ⊢ (𝑥 ∈ (0..^(𝑀 / 𝑁)) → 𝑥 ∈ ℕ₀)
7	6	ad2antrl 490	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 ∈ ℕ₀)
8		nnnn0 9183	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
9	8	3ad2ant2 1019	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ∈ ℕ₀)
10	9	adantr 276	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑁 ∈ ℕ₀)
11	7, 10	nn0mulcld 9234	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) ∈ ℕ₀)
12		simpl1 1000	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑀 ∈ ℕ)
13		elfzolt2 10156	. . . . . . 7 ⊢ (𝑥 ∈ (0..^(𝑀 / 𝑁)) → 𝑥 < (𝑀 / 𝑁))
14	13	ad2antrl 490	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 < (𝑀 / 𝑁))
15		elfzoelz 10147	. . . . . . . . 9 ⊢ (𝑥 ∈ (0..^(𝑀 / 𝑁)) → 𝑥 ∈ ℤ)
16	15	ad2antrl 490	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 ∈ ℤ)
17	16	zred 9375	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑥 ∈ ℝ)
18		nnre 8926	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
19	18	3ad2ant1 1018	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑀 ∈ ℝ)
20	19	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑀 ∈ ℝ)
21		nnre 8926	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
22		nngt0 8944	. . . . . . . . . 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 8831	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑥 · 𝑁) < 𝑀 ↔ 𝑥 < (𝑀 / 𝑁)))
27	17, 20, 25, 26	syl3anc 1238	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 · 𝑁) < 𝑀 ↔ 𝑥 < (𝑀 / 𝑁)))
28	14, 27	mpbird 167	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) < 𝑀)
29		elfzo0 10182	. . . . 5 ⊢ ((𝑥 · 𝑁) ∈ (0..^𝑀) ↔ ((𝑥 · 𝑁) ∈ ℕ₀ ∧ 𝑀 ∈ ℕ ∧ (𝑥 · 𝑁) < 𝑀))
30	11, 12, 28, 29	syl3anbrc 1181	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) ∈ (0..^𝑀))
31		nncn 8927	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
32	31	3ad2ant1 1018	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑀 ∈ ℂ)
33		nncn 8927	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
34	33	3ad2ant2 1019	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ∈ ℂ)
35		nnap0 8948	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 # 0)
36	35	3ad2ant2 1019	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 # 0)
37	32, 34, 36	divcanap1d 8748	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → ((𝑀 / 𝑁) · 𝑁) = 𝑀)
38	37	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑀 / 𝑁) · 𝑁) = 𝑀)
39	38	eqcomd 2183	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → 𝑀 = ((𝑀 / 𝑁) · 𝑁))
40	39	oveq2d 5891	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 · 𝑁) gcd 𝑀) = ((𝑥 · 𝑁) gcd ((𝑀 / 𝑁) · 𝑁)))
41		nndivdvds 11803	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ 𝑀 ↔ (𝑀 / 𝑁) ∈ ℕ))
42	41	biimp3a 1345	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑀 / 𝑁) ∈ ℕ)
43	42	nnzd 9374	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑀 / 𝑁) ∈ ℤ)
44	43	adantr 276	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑀 / 𝑁) ∈ ℤ)
45		mulgcdr 12019	. . . . . 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 5890	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → ((𝑥 gcd (𝑀 / 𝑁)) · 𝑁) = (1 · 𝑁))
49	34	mulid2d 7976	. . . . . . 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 5882	. . . . . 6 ⊢ (𝑧 = (𝑥 · 𝑁) → (𝑧 gcd 𝑀) = ((𝑥 · 𝑁) gcd 𝑀))
54	53	eqeq1d 2186	. . . . 5 ⊢ (𝑧 = (𝑥 · 𝑁) → ((𝑧 gcd 𝑀) = 𝑁 ↔ ((𝑥 · 𝑁) gcd 𝑀) = 𝑁))
55		hashgcdlem.b	. . . . 5 ⊢ 𝐵 = {𝑧 ∈ (0..^𝑀) ∣ (𝑧 gcd 𝑀) = 𝑁}
56	54, 55	elrab2 2897	. . . 4 ⊢ ((𝑥 · 𝑁) ∈ 𝐵 ↔ ((𝑥 · 𝑁) ∈ (0..^𝑀) ∧ ((𝑥 · 𝑁) gcd 𝑀) = 𝑁))
57	30, 52, 56	sylanbrc 417	. . 3 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ (𝑥 gcd (𝑀 / 𝑁)) = 1)) → (𝑥 · 𝑁) ∈ 𝐵)
58	5, 57	sylan2b 287	. 2 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ 𝑥 ∈ 𝐴) → (𝑥 · 𝑁) ∈ 𝐵)
59		oveq1 5882	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 gcd 𝑀) = (𝑤 gcd 𝑀))
60	59	eqeq1d 2186	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝑧 gcd 𝑀) = 𝑁 ↔ (𝑤 gcd 𝑀) = 𝑁))
61	60, 55	elrab2 2897	. . 3 ⊢ (𝑤 ∈ 𝐵 ↔ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁))
62		simprr 531	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 gcd 𝑀) = 𝑁)
63		elfzoelz 10147	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ ℤ)
64	63	ad2antrl 490	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 ∈ ℤ)
65		simpl1 1000	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑀 ∈ ℕ)
66	65	nnzd 9374	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑀 ∈ ℤ)
67		gcddvds 11964	. . . . . . . . . 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 4028	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∥ 𝑤)
71		nnz 9272	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
72	71	3ad2ant2 1019	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ∈ ℤ)
73	72	adantr 276	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∈ ℤ)
74		nnne0 8947	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
75	74	3ad2ant2 1019	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝑁 ≠ 0)
76	75	adantr 276	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ≠ 0)
77		dvdsval2 11797	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ 𝑤 ∈ ℤ) → (𝑁 ∥ 𝑤 ↔ (𝑤 / 𝑁) ∈ ℤ))
78	73, 76, 64, 77	syl3anc 1238	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑁 ∥ 𝑤 ↔ (𝑤 / 𝑁) ∈ ℤ))
79	70, 78	mpbid 147	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ ℤ)
80		elfzofz 10162	. . . . . . . . 9 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ (0...𝑀))
81	80	ad2antrl 490	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 ∈ (0...𝑀))
82		elfznn0 10114	. . . . . . . 8 ⊢ (𝑤 ∈ (0...𝑀) → 𝑤 ∈ ℕ₀)
83		nn0re 9185	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ₀ → 𝑤 ∈ ℝ)
84		nn0ge0 9201	. . . . . . . . 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 8830	. . . . . . 7 ⊢ (((𝑤 ∈ ℝ ∧ 0 ≤ 𝑤) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑤 / 𝑁))
89	86, 87, 88	syl2anc 411	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 0 ≤ (𝑤 / 𝑁))
90		elnn0z 9266	. . . . . 6 ⊢ ((𝑤 / 𝑁) ∈ ℕ₀ ↔ ((𝑤 / 𝑁) ∈ ℤ ∧ 0 ≤ (𝑤 / 𝑁)))
91	79, 89, 90	sylanbrc 417	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ ℕ₀)
92	42	adantr 276	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑀 / 𝑁) ∈ ℕ)
93		elfzolt2 10156	. . . . . . 7 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 < 𝑀)
94	93	ad2antrl 490	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 < 𝑀)
95	64	zred 9375	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑤 ∈ ℝ)
96	19	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑀 ∈ ℝ)
97		ltdiv1 8825	. . . . . . 7 ⊢ ((𝑤 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑤 < 𝑀 ↔ (𝑤 / 𝑁) < (𝑀 / 𝑁)))
98	95, 96, 87, 97	syl3anc 1238	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 < 𝑀 ↔ (𝑤 / 𝑁) < (𝑀 / 𝑁)))
99	94, 98	mpbid 147	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) < (𝑀 / 𝑁))
100		elfzo0 10182	. . . . 5 ⊢ ((𝑤 / 𝑁) ∈ (0..^(𝑀 / 𝑁)) ↔ ((𝑤 / 𝑁) ∈ ℕ₀ ∧ (𝑀 / 𝑁) ∈ ℕ ∧ (𝑤 / 𝑁) < (𝑀 / 𝑁)))
101	91, 92, 99, 100	syl3anbrc 1181	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑤 / 𝑁) ∈ (0..^(𝑀 / 𝑁)))
102	62	oveq1d 5890	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 gcd 𝑀) / 𝑁) = (𝑁 / 𝑁))
103		simpl2 1001	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∈ ℕ)
104		simpl3 1002	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → 𝑁 ∥ 𝑀)
105		gcddiv 12020	. . . . . 6 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 ∥ 𝑤 ∧ 𝑁 ∥ 𝑀)) → ((𝑤 gcd 𝑀) / 𝑁) = ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)))
106	64, 66, 103, 70, 104, 105	syl32anc 1246	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 gcd 𝑀) / 𝑁) = ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)))
107	34, 36	dividapd 8743	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → (𝑁 / 𝑁) = 1)
108	107	adantr 276	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → (𝑁 / 𝑁) = 1)
109	102, 106, 108	3eqtr3d 2218	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑤 ∈ (0..^𝑀) ∧ (𝑤 gcd 𝑀) = 𝑁)) → ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)) = 1)
110		oveq1 5882	. . . . . 6 ⊢ (𝑦 = (𝑤 / 𝑁) → (𝑦 gcd (𝑀 / 𝑁)) = ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)))
111	110	eqeq1d 2186	. . . . 5 ⊢ (𝑦 = (𝑤 / 𝑁) → ((𝑦 gcd (𝑀 / 𝑁)) = 1 ↔ ((𝑤 / 𝑁) gcd (𝑀 / 𝑁)) = 1))
112	111, 4	elrab2 2897	. . . 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 9376	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑤 ∈ ℂ)
120	34	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑁 ∈ ℂ)
121	36	adantr 276	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑁 # 0)
122	119, 120, 121	divcanap1d 8748	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → ((𝑤 / 𝑁) · 𝑁) = 𝑤)
123	122	eqcomd 2183	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑤 = ((𝑤 / 𝑁) · 𝑁))
124		oveq1 5882	. . . . . 6 ⊢ (𝑥 = (𝑤 / 𝑁) → (𝑥 · 𝑁) = ((𝑤 / 𝑁) · 𝑁))
125	124	eqeq2d 2189	. . . . 5 ⊢ (𝑥 = (𝑤 / 𝑁) → (𝑤 = (𝑥 · 𝑁) ↔ 𝑤 = ((𝑤 / 𝑁) · 𝑁)))
126	123, 125	syl5ibrcom 157	. . . 4 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → (𝑥 = (𝑤 / 𝑁) → 𝑤 = (𝑥 · 𝑁)))
127	15	ad2antrl 490	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑥 ∈ ℤ)
128	127	zcnd 9376	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑥 ∈ ℂ)
129	128, 120, 121	divcanap4d 8753	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → ((𝑥 · 𝑁) / 𝑁) = 𝑥)
130	129	eqcomd 2183	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) ∧ (𝑥 ∈ (0..^(𝑀 / 𝑁)) ∧ 𝑤 ∈ (0..^𝑀))) → 𝑥 = ((𝑥 · 𝑁) / 𝑁))
131		oveq1 5882	. . . . . 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 6076	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 4004 ↦ cmpt 4065 –1-1-onto→wf1o 5216 (class class class)co 5875 ℂcc 7809 ℝcr 7810 0cc0 7811 1c1 7812 · cmul 7816 < clt 7992 ≤ cle 7993 # cap 8538 / cdiv 8629 ℕcn 8919 ℕ₀cn0 9176 ℤcz 9253 ...cfz 10008 ..^cfzo 10142 ∥ cdvds 11794 gcd cgcd 11943

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 4119 ax-sep 4122 ax-nul 4130 ax-pow 4175 ax-pr 4210 ax-un 4434 ax-setind 4537 ax-iinf 4588 ax-cnex 7902 ax-resscn 7903 ax-1cn 7904 ax-1re 7905 ax-icn 7906 ax-addcl 7907 ax-addrcl 7908 ax-mulcl 7909 ax-mulrcl 7910 ax-addcom 7911 ax-mulcom 7912 ax-addass 7913 ax-mulass 7914 ax-distr 7915 ax-i2m1 7916 ax-0lt1 7917 ax-1rid 7918 ax-0id 7919 ax-rnegex 7920 ax-precex 7921 ax-cnre 7922 ax-pre-ltirr 7923 ax-pre-ltwlin 7924 ax-pre-lttrn 7925 ax-pre-apti 7926 ax-pre-ltadd 7927 ax-pre-mulgt0 7928 ax-pre-mulext 7929 ax-arch 7930 ax-caucvg 7931

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 2740 df-sbc 2964 df-csb 3059 df-dif 3132 df-un 3134 df-in 3136 df-ss 3143 df-nul 3424 df-if 3536 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-int 3846 df-iun 3889 df-br 4005 df-opab 4066 df-mpt 4067 df-tr 4103 df-id 4294 df-po 4297 df-iso 4298 df-iord 4367 df-on 4369 df-ilim 4370 df-suc 4372 df-iom 4591 df-xp 4633 df-rel 4634 df-cnv 4635 df-co 4636 df-dm 4637 df-rn 4638 df-res 4639 df-ima 4640 df-iota 5179 df-fun 5219 df-fn 5220 df-f 5221 df-f1 5222 df-fo 5223 df-f1o 5224 df-fv 5225 df-riota 5831 df-ov 5878 df-oprab 5879 df-mpo 5880 df-1st 6141 df-2nd 6142 df-recs 6306 df-frec 6392 df-sup 6983 df-pnf 7994 df-mnf 7995 df-xr 7996 df-ltxr 7997 df-le 7998 df-sub 8130 df-neg 8131 df-reap 8532 df-ap 8539 df-div 8630 df-inn 8920 df-2 8978 df-3 8979 df-4 8980 df-n0 9177 df-z 9254 df-uz 9529 df-q 9620 df-rp 9654 df-fz 10009 df-fzo 10143 df-fl 10270 df-mod 10323 df-seqfrec 10446 df-exp 10520 df-cj 10851 df-re 10852 df-im 10853 df-rsqrt 11007 df-abs 11008 df-dvds 11795 df-gcd 11944

This theorem is referenced by: hashgcdeq 12239

W3C validator