qredeu - Metamath Proof Explorer

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

Theorem qredeu 16571

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

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

Distinct variable group: 𝑥,𝐴

Proof of Theorem qredeu Dummy variables 𝑛 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnz 12496	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
2		gcddvds 16416	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ∧ (𝑧 gcd 𝑛) ∥ 𝑛))
3	2	simpld 494	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑧)
4	1, 3	sylan2 593	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑧)
5		gcdcl 16419	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∈ ℕ₀)
6	1, 5	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ₀)
7	6	nn0zd 12500	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℤ)
8		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℤ)
9	1	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
10		nnne0 12166	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
11	10	neneqd 2934	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ¬ 𝑛 = 0)
12	11	intnand 488	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ¬ (𝑧 = 0 ∧ 𝑛 = 0))
13	12	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ¬ (𝑧 = 0 ∧ 𝑛 = 0))
14		gcdn0cl 16415	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ¬ (𝑧 = 0 ∧ 𝑛 = 0)) → (𝑧 gcd 𝑛) ∈ ℕ)
15	8, 9, 13, 14	syl21anc 837	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ)
16		nnne0 12166	. . . . . . . . . . 11 ⊢ ((𝑧 gcd 𝑛) ∈ ℕ → (𝑧 gcd 𝑛) ≠ 0)
17	15, 16	syl 17	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ≠ 0)
18		dvdsval2 16168	. . . . . . . . . 10 ⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑧 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ))
19	7, 17, 8, 18	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ))
20	4, 19	mpbid 232	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)
21	20	3adant3 1132	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)
22	2	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑛)
23	1, 22	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑛)
24		dvdsval2 16168	. . . . . . . . . . . 12 ⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ))
25	7, 17, 9, 24	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ))
26	23, 25	mpbid 232	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ)
27		nnre 12139	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
28	27	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
29	6	nn0red 12450	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℝ)
30		nngt0 12163	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 0 < 𝑛)
31	30	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < 𝑛)
32		nngt0 12163	. . . . . . . . . . . 12 ⊢ ((𝑧 gcd 𝑛) ∈ ℕ → 0 < (𝑧 gcd 𝑛))
33	15, 32	syl 17	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < (𝑧 gcd 𝑛))
34	28, 29, 31, 33	divgt0d 12064	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < (𝑛 / (𝑧 gcd 𝑛)))
35	26, 34	jca 511	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
36	35	3adant3 1132	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
37		elnnz 12485	. . . . . . . 8 ⊢ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ ↔ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
38	36, 37	sylibr 234	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ)
39	21, 38	opelxpd 5658	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ ∈ (ℤ × ℕ))
40	20, 26	gcdcld 16421	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℕ₀)
41	40	nn0cnd 12451	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℂ)
42		1cnd 11114	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℂ)
43	6	nn0cnd 12451	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℂ)
44	43	mulridd 11136	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · 1) = (𝑧 gcd 𝑛))
45		zcn 12480	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℂ)
46	45	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℂ)
47	46, 43, 17	divcan2d 11906	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) = 𝑧)
48		nncn 12140	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
49	48	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
50	49, 43, 17	divcan2d 11906	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛))) = 𝑛)
51	47, 50	oveq12d 7370	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = (𝑧 gcd 𝑛))
52		mulgcd 16461	. . . . . . . . . 10 ⊢ (((𝑧 gcd 𝑛) ∈ ℕ₀ ∧ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))))
53	6, 20, 26, 52	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))))
54	44, 51, 53	3eqtr2rd 2775	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · 1))
55	41, 42, 43, 17, 54	mulcanad 11759	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)
56	55	3adant3 1132	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)
57	10	adantl 481	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
58	46, 49, 43, 57, 17	divcan7d 11932	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) = (𝑧 / 𝑛))
59	58	eqeq2d 2744	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) ↔ 𝐴 = (𝑧 / 𝑛)))
60	59	biimp3ar 1472	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))
61		ovex 7385	. . . . . . . . . . 11 ⊢ (𝑧 / (𝑧 gcd 𝑛)) ∈ V
62		ovex 7385	. . . . . . . . . . 11 ⊢ (𝑛 / (𝑧 gcd 𝑛)) ∈ V
63	61, 62	op1std 7937	. . . . . . . . . 10 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (1^st ‘𝑥) = (𝑧 / (𝑧 gcd 𝑛)))
64	61, 62	op2ndd 7938	. . . . . . . . . 10 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (2^nd ‘𝑥) = (𝑛 / (𝑧 gcd 𝑛)))
65	63, 64	oveq12d 7370	. . . . . . . . 9 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))))
66	65	eqeq1d 2735	. . . . . . . 8 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ↔ ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1))
67	63, 64	oveq12d 7370	. . . . . . . . 9 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))
68	67	eqeq2d 2744	. . . . . . . 8 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)) ↔ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))))
69	66, 68	anbi12d 632	. . . . . . 7 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ↔ (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))))
70	69	rspcev 3573	. . . . . 6 ⊢ ((⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ ∈ (ℤ × ℕ) ∧ (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))) → ∃𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))
71	39, 56, 60, 70	syl12anc 836	. . . . 5 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ∃𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))
72		elxp6 7961	. . . . . . 7 ⊢ (𝑥 ∈ (ℤ × ℕ) ↔ (𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)))
73		elxp6 7961	. . . . . . 7 ⊢ (𝑦 ∈ (ℤ × ℕ) ↔ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)))
74		simprl 770	. . . . . . . . . . . 12 ⊢ ((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) → (1^st ‘𝑥) ∈ ℤ)
75	74	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(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 772	. . . . . . . . . . . 12 ⊢ ((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) → (2^nd ‘𝑥) ∈ ℕ)
77	76	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(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 778	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(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 770	. . . . . . . . . . . 12 ⊢ ((𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)) → (1^st ‘𝑦) ∈ ℤ)
80	79	ad2antlr 727	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(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 772	. . . . . . . . . . . 12 ⊢ ((𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)) → (2^nd ‘𝑦) ∈ ℕ)
82	81	ad2antlr 727	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(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 780	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(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 779	. . . . . . . . . . . 12 ⊢ ((((𝑥 = ⟨(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 781	. . . . . . . . . . . 12 ⊢ ((((𝑥 = ⟨(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 2770	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(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 16570	. . . . . . . . . . 11 ⊢ ((((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 1397	. . . . . . . . . 10 ⊢ ((((𝑥 = ⟨(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 6841	. . . . . . . . . . 11 ⊢ (1^st ‘𝑥) ∈ V
90		fvex 6841	. . . . . . . . . . 11 ⊢ (2^nd ‘𝑥) ∈ V
91	89, 90	opth 5419	. . . . . . . . . 10 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ↔ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
92	88, 91	sylibr 234	. . . . . . . . 9 ⊢ ((((𝑥 = ⟨(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 774	. . . . . . . . 9 ⊢ ((((𝑥 = ⟨(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 776	. . . . . . . . 9 ⊢ ((((𝑥 = ⟨(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 2778	. . . . . . . 8 ⊢ ((((𝑥 = ⟨(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 412	. . . . . . 7 ⊢ (((𝑥 = ⟨(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 598	. . . . . 6 ⊢ ((𝑥 ∈ (ℤ × ℕ) ∧ 𝑦 ∈ (ℤ × ℕ)) → (((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))) → 𝑥 = 𝑦))
98	97	rgen2 3173	. . . . 5 ⊢ ∀𝑥 ∈ (ℤ × ℕ)∀𝑦 ∈ (ℤ × ℕ)(((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))) → 𝑥 = 𝑦)
99	71, 98	jctir 520	. . . 4 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (∃𝑥 ∈ (ℤ × ℕ)(((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 1121	. . 3 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝐴 = (𝑧 / 𝑛) → (∃𝑥 ∈ (ℤ × ℕ)(((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 3175	. 2 ⊢ (∃𝑧 ∈ ℤ ∃𝑛 ∈ ℕ 𝐴 = (𝑧 / 𝑛) → (∃𝑥 ∈ (ℤ × ℕ)(((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 12850	. 2 ⊢ (𝐴 ∈ ℚ ↔ ∃𝑧 ∈ ℤ ∃𝑛 ∈ ℕ 𝐴 = (𝑧 / 𝑛))
103		fveq2 6828	. . . . . 6 ⊢ (𝑥 = 𝑦 → (1^st ‘𝑥) = (1^st ‘𝑦))
104		fveq2 6828	. . . . . 6 ⊢ (𝑥 = 𝑦 → (2^nd ‘𝑥) = (2^nd ‘𝑦))
105	103, 104	oveq12d 7370	. . . . 5 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = ((1^st ‘𝑦) gcd (2^nd ‘𝑦)))
106	105	eqeq1d 2735	. . . 4 ⊢ (𝑥 = 𝑦 → (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ↔ ((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1))
107	103, 104	oveq12d 7370	. . . . 5 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((1^st ‘𝑦) / (2^nd ‘𝑦)))
108	107	eqeq2d 2744	. . . 4 ⊢ (𝑥 = 𝑦 → (𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)) ↔ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))
109	106, 108	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ↔ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))))
110	109	reu4 3686	. 2 ⊢ (∃!𝑥 ∈ (ℤ × ℕ)(((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 292	1 ⊢ (𝐴 ∈ ℚ → ∃!𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 ∀wral 3048 ∃wrex 3057 ∃!wreu 3345 ⟨cop 4581 class class class wbr 5093 × cxp 5617 ‘cfv 6486 (class class class)co 7352 1^st c1st 7925 2^nd c2nd 7926 ℂcc 11011 ℝcr 11012 0cc0 11013 1c1 11014 · cmul 11018 < clt 11153 / cdiv 11781 ℕcn 12132 ℕ₀cn0 12388 ℤcz 12475 ℚcq 12848 ∥ cdvds 16165 gcd cgcd 16407

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090 ax-pre-sup 11091

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-1st 7927 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-sup 9333 df-inf 9334 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-div 11782 df-nn 12133 df-2 12195 df-3 12196 df-n0 12389 df-z 12476 df-uz 12739 df-q 12849 df-rp 12893 df-fl 13698 df-mod 13776 df-seq 13911 df-exp 13971 df-cj 15008 df-re 15009 df-im 15010 df-sqrt 15144 df-abs 15145 df-dvds 16166 df-gcd 16408

This theorem is referenced by: qnumdencl 16652 qnumdenbi 16657

W3C validator