rplpwr - Metamath Proof Explorer

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

Theorem rplpwr 16641

Description: If 𝐴 and 𝐵 are relatively prime, then so are 𝐴↑𝑁 and 𝐵. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

**Assertion**
Ref	Expression
rplpwr	⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd 𝐵) = 1))

Proof of Theorem rplpwr Dummy variables 𝑛 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7431	. . . . . . . 8 ⊢ (𝑘 = 1 → (𝐴↑𝑘) = (𝐴↑1))
2	1	oveq1d 7438	. . . . . . 7 ⊢ (𝑘 = 1 → ((𝐴↑𝑘) gcd 𝐵) = ((𝐴↑1) gcd 𝐵))
3	2	eqeq1d 2768	. . . . . 6 ⊢ (𝑘 = 1 → (((𝐴↑𝑘) gcd 𝐵) = 1 ↔ ((𝐴↑1) gcd 𝐵) = 1))
4	3	imbi2d 343	. . . . 5 ⊢ (𝑘 = 1 → ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑𝑘) gcd 𝐵) = 1) ↔ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑1) gcd 𝐵) = 1)))
5		oveq2 7431	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → (𝐴↑𝑘) = (𝐴↑𝑛))
6	5	oveq1d 7438	. . . . . . 7 ⊢ (𝑘 = 𝑛 → ((𝐴↑𝑘) gcd 𝐵) = ((𝐴↑𝑛) gcd 𝐵))
7	6	eqeq1d 2768	. . . . . 6 ⊢ (𝑘 = 𝑛 → (((𝐴↑𝑘) gcd 𝐵) = 1 ↔ ((𝐴↑𝑛) gcd 𝐵) = 1))
8	7	imbi2d 343	. . . . 5 ⊢ (𝑘 = 𝑛 → ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑𝑘) gcd 𝐵) = 1) ↔ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑𝑛) gcd 𝐵) = 1)))
9		oveq2 7431	. . . . . . . 8 ⊢ (𝑘 = (𝑛 + 1) → (𝐴↑𝑘) = (𝐴↑(𝑛 + 1)))
10	9	oveq1d 7438	. . . . . . 7 ⊢ (𝑘 = (𝑛 + 1) → ((𝐴↑𝑘) gcd 𝐵) = ((𝐴↑(𝑛 + 1)) gcd 𝐵))
11	10	eqeq1d 2768	. . . . . 6 ⊢ (𝑘 = (𝑛 + 1) → (((𝐴↑𝑘) gcd 𝐵) = 1 ↔ ((𝐴↑(𝑛 + 1)) gcd 𝐵) = 1))
12	11	imbi2d 343	. . . . 5 ⊢ (𝑘 = (𝑛 + 1) → ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑𝑘) gcd 𝐵) = 1) ↔ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑(𝑛 + 1)) gcd 𝐵) = 1)))
13		oveq2 7431	. . . . . . . 8 ⊢ (𝑘 = 𝑁 → (𝐴↑𝑘) = (𝐴↑𝑁))
14	13	oveq1d 7438	. . . . . . 7 ⊢ (𝑘 = 𝑁 → ((𝐴↑𝑘) gcd 𝐵) = ((𝐴↑𝑁) gcd 𝐵))
15	14	eqeq1d 2768	. . . . . 6 ⊢ (𝑘 = 𝑁 → (((𝐴↑𝑘) gcd 𝐵) = 1 ↔ ((𝐴↑𝑁) gcd 𝐵) = 1))
16	15	imbi2d 343	. . . . 5 ⊢ (𝑘 = 𝑁 → ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑𝑘) gcd 𝐵) = 1) ↔ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑𝑁) gcd 𝐵) = 1)))
17		nncn 12259	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
18	17	exp1d 14197	. . . . . . . . 9 ⊢ (𝐴 ∈ ℕ → (𝐴↑1) = 𝐴)
19	18	oveq1d 7438	. . . . . . . 8 ⊢ (𝐴 ∈ ℕ → ((𝐴↑1) gcd 𝐵) = (𝐴 gcd 𝐵))
20	19	adantr 486	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴↑1) gcd 𝐵) = (𝐴 gcd 𝐵))
21	20	eqeq1d 2768	. . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴↑1) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1))
22	21	biimpar 483	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑1) gcd 𝐵) = 1)
23		df-3an 1105	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ↔ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑛 ∈ ℕ))
24		simpl1 1210	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴 ∈ ℕ)
25	24	nncnd 12267	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴 ∈ ℂ)
26		simpl3 1212	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → 𝑛 ∈ ℕ)
27	26	nnnn0d 12583	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → 𝑛 ∈ ℕ₀)
28	25, 27	expp1d 14203	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐴↑(𝑛 + 1)) = ((𝐴↑𝑛) · 𝐴))
29		simp1 1154	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℕ)
30		nnnn0 12529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
31	30	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ₀)
32	29, 31	nnexpcld 14301	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝐴↑𝑛) ∈ ℕ)
33	32	nnzd 12635	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝐴↑𝑛) ∈ ℤ)
34	33	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐴↑𝑛) ∈ ℤ)
35	34	zcnd 12719	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐴↑𝑛) ∈ ℂ)
36	35, 25	mulcomd 11248	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑𝑛) · 𝐴) = (𝐴 · (𝐴↑𝑛)))
37	28, 36	eqtrd 2801	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐴↑(𝑛 + 1)) = (𝐴 · (𝐴↑𝑛)))
38	37	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐵 gcd (𝐴↑(𝑛 + 1))) = (𝐵 gcd (𝐴 · (𝐴↑𝑛))))
39		simpl2 1211	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → 𝐵 ∈ ℕ)
40	32	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐴↑𝑛) ∈ ℕ)
41		nnz 12630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
42	41	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℤ)
43		nnz 12630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℤ)
44	43	3ad2ant2 1152	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℤ)
45	42, 44	gcdcomd 16597	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
46	45	eqeq1d 2768	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → ((𝐴 gcd 𝐵) = 1 ↔ (𝐵 gcd 𝐴) = 1))
47	46	biimpa 482	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐵 gcd 𝐴) = 1)
48		rpmulgcd 16640	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ (𝐴↑𝑛) ∈ ℕ) ∧ (𝐵 gcd 𝐴) = 1) → (𝐵 gcd (𝐴 · (𝐴↑𝑛))) = (𝐵 gcd (𝐴↑𝑛)))
49	39, 24, 40, 47, 48	syl31anc 1400	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐵 gcd (𝐴 · (𝐴↑𝑛))) = (𝐵 gcd (𝐴↑𝑛)))
50	38, 49	eqtrd 2801	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐵 gcd (𝐴↑(𝑛 + 1))) = (𝐵 gcd (𝐴↑𝑛)))
51		peano2nn 12263	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
52	51	3ad2ant3 1153	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
53	52	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝑛 + 1) ∈ ℕ)
54	53	nnnn0d 12583	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝑛 + 1) ∈ ℕ₀)
55	24, 54	nnexpcld 14301	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐴↑(𝑛 + 1)) ∈ ℕ)
56	55	nnzd 12635	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (𝐴↑(𝑛 + 1)) ∈ ℤ)
57	44	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → 𝐵 ∈ ℤ)
58	56, 57	gcdcomd 16597	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑(𝑛 + 1)) gcd 𝐵) = (𝐵 gcd (𝐴↑(𝑛 + 1))))
59	34, 57	gcdcomd 16597	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑𝑛) gcd 𝐵) = (𝐵 gcd (𝐴↑𝑛)))
60	50, 58, 59	3eqtr4d 2811	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑(𝑛 + 1)) gcd 𝐵) = ((𝐴↑𝑛) gcd 𝐵))
61	60	eqeq1d 2768	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (((𝐴↑(𝑛 + 1)) gcd 𝐵) = 1 ↔ ((𝐴↑𝑛) gcd 𝐵) = 1))
62	61	biimprd 251	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (((𝐴↑𝑛) gcd 𝐵) = 1 → ((𝐴↑(𝑛 + 1)) gcd 𝐵) = 1))
63	23, 62	sylanbr 594	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (((𝐴↑𝑛) gcd 𝐵) = 1 → ((𝐴↑(𝑛 + 1)) gcd 𝐵) = 1))
64	63	an32s 665	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑛 ∈ ℕ) → (((𝐴↑𝑛) gcd 𝐵) = 1 → ((𝐴↑(𝑛 + 1)) gcd 𝐵) = 1))
65	64	expcom 419	. . . . . 6 ⊢ (𝑛 ∈ ℕ → (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → (((𝐴↑𝑛) gcd 𝐵) = 1 → ((𝐴↑(𝑛 + 1)) gcd 𝐵) = 1)))
66	65	a2d 30	. . . . 5 ⊢ (𝑛 ∈ ℕ → ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑𝑛) gcd 𝐵) = 1) → (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑(𝑛 + 1)) gcd 𝐵) = 1)))
67	4, 8, 12, 16, 22, 66	nnind 12269	. . . 4 ⊢ (𝑁 ∈ ℕ → (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) = 1) → ((𝐴↑𝑁) gcd 𝐵) = 1))
68	67	expd 421	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd 𝐵) = 1)))
69	68	com12 33	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝑁 ∈ ℕ → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd 𝐵) = 1)))
70	69	3impia 1135	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd 𝐵) = 1))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 (class class class)co 7423 1c1 11119 + caddc 11121 · cmul 11123 ℕcn 12251 ℕ₀cn0 12522 ℤcz 12609 ↑cexp 14117 gcd cgcd 16577

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-sup 9412 df-inf 9413 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-n0 12523 df-z 12610 df-uz 12881 df-rp 13035 df-fl 13845 df-mod 13923 df-seq 14058 df-exp 14118 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-dvds 16336 df-gcd 16578

This theorem is used by: rprpwr 16642 rppwr 16643 logbgcd1irr 26996 lgsne0 27536 2sqlem8 27627 flt4lem5a 43425 flt4lem5b 43426 flt4lem5c 43427 flt4lem5d 43428 flt4lem5e 43429

W3C validator