qdenval - Intuitionistic Logic Explorer

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

Theorem qdenval 12781

Description: Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)

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

Distinct variable group: 𝑥,𝐴

Proof of Theorem qdenval Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2237	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 = ((1^st ‘𝑥) / (2^nd ‘𝑥)) ↔ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))
2	1	anbi2d 464	. . . 4 ⊢ (𝑎 = 𝐴 → ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝑎 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ↔ (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)))))
3	2	riotabidv 5978	. . 3 ⊢ (𝑎 = 𝐴 → (℩𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝑎 = ((1^st ‘𝑥) / (2^nd ‘𝑥)))) = (℩𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)))))
4	3	fveq2d 5646	. 2 ⊢ (𝑎 = 𝐴 → (2^nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝑎 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))) = (2^nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))))
5		df-denom 12779	. 2 ⊢ denom = (𝑎 ∈ ℚ ↦ (2^nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝑎 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))))
6		zex 9493	. . . 4 ⊢ ℤ ∈ V
7		nnex 9154	. . . 4 ⊢ ℕ ∈ V
8	6, 7	xpex 4844	. . 3 ⊢ (ℤ × ℕ) ∈ V
9		riotaexg 5980	. . 3 ⊢ ((ℤ × ℕ) ∈ V → (℩𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)))) ∈ V)
10		2ndexg 6336	. . 3 ⊢ ((℩𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)))) ∈ V → (2^nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))) ∈ V)
11	8, 9, 10	mp2b 8	. 2 ⊢ (2^nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))) ∈ V
12	4, 5, 11	fvmpt 5726	1 ⊢ (𝐴 ∈ ℚ → (denom‘𝐴) = (2^nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1397 ∈ wcel 2201 Vcvv 2801 × cxp 4725 ‘cfv 5328 ℩crio 5975 (class class class)co 6023 1^st c1st 6306 2^nd c2nd 6307 1c1 8038 / cdiv 8857 ℕcn 9148 ℤcz 9484 ℚcq 9858 gcd cgcd 12547 denomcdenom 12777

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-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2203 ax-14 2204 ax-ext 2212 ax-sep 4208 ax-pow 4266 ax-pr 4301 ax-un 4532 ax-cnex 8128 ax-resscn 8129 ax-1re 8131 ax-addrcl 8134

This theorem depends on definitions: df-bi 117 df-3or 1005 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1810 df-eu 2081 df-mo 2082 df-clab 2217 df-cleq 2223 df-clel 2226 df-nfc 2362 df-ral 2514 df-rex 2515 df-rab 2518 df-v 2803 df-sbc 3031 df-un 3203 df-in 3205 df-ss 3212 df-pw 3655 df-sn 3676 df-pr 3677 df-op 3679 df-uni 3895 df-int 3930 df-br 4090 df-opab 4152 df-mpt 4153 df-id 4392 df-xp 4733 df-rel 4734 df-cnv 4735 df-co 4736 df-dm 4737 df-rn 4738 df-iota 5288 df-fun 5330 df-fn 5331 df-f 5332 df-fo 5334 df-fv 5336 df-riota 5976 df-ov 6026 df-2nd 6309 df-neg 8358 df-inn 9149 df-z 9485 df-denom 12779

This theorem is referenced by: qnumdencl 12782 fden 12786 qnumdenbi 12787

W3C validator