qredeu

Description: Every rational number has a unique reduced form. (Contributed by Jeff Hankins, 29-Sep-2013)

		Ref	Expression
	Assertion	qredeu	⊢ ( 𝐴 ∈ ℚ → ∃! 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
2		gcddvds	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑧 gcd 𝑛 ) ∥ 𝑧 ∧ ( 𝑧 gcd 𝑛 ) ∥ 𝑛 ) )
3	2	simpld	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑧 gcd 𝑛 ) ∥ 𝑧 )
4	1 3	sylan2	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑧 gcd 𝑛 ) ∥ 𝑧 )
5		gcdcl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑧 gcd 𝑛 ) ∈ ℕ₀ )
6	1 5	sylan2	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑧 gcd 𝑛 ) ∈ ℕ₀ )
7	6	nn0zd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑧 gcd 𝑛 ) ∈ ℤ )
8		simpl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → 𝑧 ∈ ℤ )
9	1	adantl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℤ )
10		nnne0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
11	10	neneqd	⊢ ( 𝑛 ∈ ℕ → ¬ 𝑛 = 0 )
12	11	intnand	⊢ ( 𝑛 ∈ ℕ → ¬ ( 𝑧 = 0 ∧ 𝑛 = 0 ) )
13	12	adantl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ¬ ( 𝑧 = 0 ∧ 𝑛 = 0 ) )
14		gcdn0cl	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ¬ ( 𝑧 = 0 ∧ 𝑛 = 0 ) ) → ( 𝑧 gcd 𝑛 ) ∈ ℕ )
15	8 9 13 14	syl21anc	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑧 gcd 𝑛 ) ∈ ℕ )
16		nnne0	⊢ ( ( 𝑧 gcd 𝑛 ) ∈ ℕ → ( 𝑧 gcd 𝑛 ) ≠ 0 )
17	15 16	syl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑧 gcd 𝑛 ) ≠ 0 )
18		dvdsval2	⊢ ( ( ( 𝑧 gcd 𝑛 ) ∈ ℤ ∧ ( 𝑧 gcd 𝑛 ) ≠ 0 ∧ 𝑧 ∈ ℤ ) → ( ( 𝑧 gcd 𝑛 ) ∥ 𝑧 ↔ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ ) )
19	7 17 8 18	syl3anc	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 gcd 𝑛 ) ∥ 𝑧 ↔ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ ) )
20	4 19	mpbid	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ )
21	20	3adant3	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = ( 𝑧 / 𝑛 ) ) → ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ )
22	2	simprd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑧 gcd 𝑛 ) ∥ 𝑛 )
23	1 22	sylan2	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑧 gcd 𝑛 ) ∥ 𝑛 )
24		dvdsval2	⊢ ( ( ( 𝑧 gcd 𝑛 ) ∈ ℤ ∧ ( 𝑧 gcd 𝑛 ) ≠ 0 ∧ 𝑛 ∈ ℤ ) → ( ( 𝑧 gcd 𝑛 ) ∥ 𝑛 ↔ ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ ) )
25	7 17 9 24	syl3anc	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 gcd 𝑛 ) ∥ 𝑛 ↔ ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ ) )
26	23 25	mpbid	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ )
27		nnre	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
28	27	adantl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ )
29	6	nn0red	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑧 gcd 𝑛 ) ∈ ℝ )
30		nngt0	⊢ ( 𝑛 ∈ ℕ → 0 < 𝑛 )
31	30	adantl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → 0 < 𝑛 )
32		nngt0	⊢ ( ( 𝑧 gcd 𝑛 ) ∈ ℕ → 0 < ( 𝑧 gcd 𝑛 ) )
33	15 32	syl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → 0 < ( 𝑧 gcd 𝑛 ) )
34	28 29 31 33	divgt0d	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → 0 < ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) )
35	26 34	jca	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ ∧ 0 < ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) )
36	35	3adant3	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = ( 𝑧 / 𝑛 ) ) → ( ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ ∧ 0 < ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) )
37		elnnz	⊢ ( ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ∈ ℕ ↔ ( ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ ∧ 0 < ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) )
38	36 37	sylibr	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = ( 𝑧 / 𝑛 ) ) → ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ∈ ℕ )
39	21 38	opelxpd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = ( 𝑧 / 𝑛 ) ) → ⟨ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) , ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ⟩ ∈ ( ℤ × ℕ ) )
40	20 26	gcdcld	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ∈ ℕ₀ )
41	40	nn0cnd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ∈ ℂ )
42		1cnd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℂ )
43	6	nn0cnd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑧 gcd 𝑛 ) ∈ ℂ )
44	43	mulridd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 gcd 𝑛 ) · 1 ) = ( 𝑧 gcd 𝑛 ) )
45		zcn	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ )
46	45	adantr	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → 𝑧 ∈ ℂ )
47	46 43 17	divcan2d	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 gcd 𝑛 ) · ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) ) = 𝑧 )
48		nncn	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
49	48	adantl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
50	49 43 17	divcan2d	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 gcd 𝑛 ) · ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) = 𝑛 )
51	47 50	oveq12d	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑧 gcd 𝑛 ) · ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) ) gcd ( ( 𝑧 gcd 𝑛 ) · ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ) = ( 𝑧 gcd 𝑛 ) )
52		mulgcd	⊢ ( ( ( 𝑧 gcd 𝑛 ) ∈ ℕ₀ ∧ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ ∧ ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ∈ ℤ ) → ( ( ( 𝑧 gcd 𝑛 ) · ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) ) gcd ( ( 𝑧 gcd 𝑛 ) · ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ) = ( ( 𝑧 gcd 𝑛 ) · ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ) )
53	6 20 26 52	syl3anc	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑧 gcd 𝑛 ) · ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) ) gcd ( ( 𝑧 gcd 𝑛 ) · ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ) = ( ( 𝑧 gcd 𝑛 ) · ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ) )
54	44 51 53	3eqtr2rd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 gcd 𝑛 ) · ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ) = ( ( 𝑧 gcd 𝑛 ) · 1 ) )
55	41 42 43 17 54	mulcanad	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) = 1 )
56	55	3adant3	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = ( 𝑧 / 𝑛 ) ) → ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) = 1 )
57	10	adantl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
58	46 49 43 57 17	divcan7d	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) / ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) = ( 𝑧 / 𝑛 ) )
59	58	eqeq2d	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝐴 = ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) / ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ↔ 𝐴 = ( 𝑧 / 𝑛 ) ) )
60	59	biimp3ar	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = ( 𝑧 / 𝑛 ) ) → 𝐴 = ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) / ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) )
61		ovex	⊢ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) ∈ V
62		ovex	⊢ ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ∈ V
63	61 62	op1std	⊢ ( 𝑥 = ⟨ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) , ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ⟩ → ( 1^st ‘ 𝑥 ) = ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) )
64	61 62	op2ndd	⊢ ( 𝑥 = ⟨ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) , ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ⟩ → ( 2^nd ‘ 𝑥 ) = ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) )
65	63 64	oveq12d	⊢ ( 𝑥 = ⟨ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) , ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ⟩ → ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) )
66	65	eqeq1d	⊢ ( 𝑥 = ⟨ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) , ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ⟩ → ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ↔ ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) = 1 ) )
67	63 64	oveq12d	⊢ ( 𝑥 = ⟨ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) , ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ⟩ → ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) = ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) / ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) )
68	67	eqeq2d	⊢ ( 𝑥 = ⟨ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) , ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ⟩ → ( 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ↔ 𝐴 = ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) / ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ) )
69	66 68	anbi12d	⊢ ( 𝑥 = ⟨ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) , ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ⟩ → ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ↔ ( ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) = 1 ∧ 𝐴 = ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) / ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ) ) )
70	69	rspcev	⊢ ( ( ⟨ ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) , ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ⟩ ∈ ( ℤ × ℕ ) ∧ ( ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) gcd ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) = 1 ∧ 𝐴 = ( ( 𝑧 / ( 𝑧 gcd 𝑛 ) ) / ( 𝑛 / ( 𝑧 gcd 𝑛 ) ) ) ) ) → ∃ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) )
71	39 56 60 70	syl12anc	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = ( 𝑧 / 𝑛 ) ) → ∃ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) )
72		elxp6	⊢ ( 𝑥 ∈ ( ℤ × ℕ ) ↔ ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) )
73		elxp6	⊢ ( 𝑦 ∈ ( ℤ × ℕ ) ↔ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) )
74		simprl	⊢ ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) → ( 1^st ‘ 𝑥 ) ∈ ℤ )
75	74	ad2antrr	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → ( 1^st ‘ 𝑥 ) ∈ ℤ )
76		simprr	⊢ ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) → ( 2^nd ‘ 𝑥 ) ∈ ℕ )
77	76	ad2antrr	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → ( 2^nd ‘ 𝑥 ) ∈ ℕ )
78		simprll	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 )
79		simprl	⊢ ( ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) → ( 1^st ‘ 𝑦 ) ∈ ℤ )
80	79	ad2antlr	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → ( 1^st ‘ 𝑦 ) ∈ ℤ )
81		simprr	⊢ ( ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) → ( 2^nd ‘ 𝑦 ) ∈ ℕ )
82	81	ad2antlr	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → ( 2^nd ‘ 𝑦 ) ∈ ℕ )
83		simprrl	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 )
84		simprlr	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) )
85		simprrr	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) )
86	84 85	eqtr3d	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) )
87		qredeq	⊢ ( ( ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ∧ ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ) ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ∧ ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ) ∧ ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) → ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) )
88	75 77 78 80 82 83 86 87	syl331anc	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) )
89		fvex	⊢ ( 1^st ‘ 𝑥 ) ∈ V
90		fvex	⊢ ( 2^nd ‘ 𝑥 ) ∈ V
91	89 90	opth	⊢ ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ↔ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) )
92	88 91	sylibr	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
93		simplll	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
94		simplrl	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
95	92 93 94	3eqtr4d	⊢ ( ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 )
96	95	ex	⊢ ( ( ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ ) ) ∧ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ℤ ∧ ( 2^nd ‘ 𝑦 ) ∈ ℕ ) ) ) → ( ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) )
97	72 73 96	syl2anb	⊢ ( ( 𝑥 ∈ ( ℤ × ℕ ) ∧ 𝑦 ∈ ( ℤ × ℕ ) ) → ( ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) )
98	97	rgen2	⊢ ∀ 𝑥 ∈ ( ℤ × ℕ ) ∀ 𝑦 ∈ ( ℤ × ℕ ) ( ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 )
99	71 98	jctir	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = ( 𝑧 / 𝑛 ) ) → ( ∃ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ∀ 𝑥 ∈ ( ℤ × ℕ ) ∀ 𝑦 ∈ ( ℤ × ℕ ) ( ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) ) )
100	99	3expia	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝐴 = ( 𝑧 / 𝑛 ) → ( ∃ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ∀ 𝑥 ∈ ( ℤ × ℕ ) ∀ 𝑦 ∈ ( ℤ × ℕ ) ( ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) ) ) )
101	100	rexlimivv	⊢ ( ∃ 𝑧 ∈ ℤ ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑧 / 𝑛 ) → ( ∃ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ∀ 𝑥 ∈ ( ℤ × ℕ ) ∀ 𝑦 ∈ ( ℤ × ℕ ) ( ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) ) )
102		elq	⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑧 ∈ ℤ ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑧 / 𝑛 ) )
103		fveq2	⊢ ( 𝑥 = 𝑦 → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) )
104		fveq2	⊢ ( 𝑥 = 𝑦 → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) )
105	103 104	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) )
106	105	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ↔ ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ) )
107	103 104	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) )
108	107	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ↔ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) )
109	106 108	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ↔ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) )
110	109	reu4	⊢ ( ∃! 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ↔ ( ∃ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ∀ 𝑥 ∈ ( ℤ × ℕ ) ∀ 𝑦 ∈ ( ℤ × ℕ ) ( ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( ( 1^st ‘ 𝑦 ) gcd ( 2^nd ‘ 𝑦 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑦 ) / ( 2^nd ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) ) )
111	101 102 110	3imtr4i	⊢ ( 𝐴 ∈ ℚ → ∃! 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem qredeu

Proof