rpexp - Intuitionistic Logic Explorer

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

Theorem rpexp 12321

Description: If two numbers 𝐴 and 𝐵 are relatively prime, then they are still relatively prime if raised to a power. (Contributed by Mario Carneiro, 24-Feb-2014.)

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

Proof of Theorem rpexp Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0exp 10666	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0)
2	1	oveq1d 5937	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((0↑𝑁) gcd 0) = (0 gcd 0))
3	2	eqeq1d 2205	. . . 4 ⊢ (𝑁 ∈ ℕ → (((0↑𝑁) gcd 0) = 1 ↔ (0 gcd 0) = 1))
4		oveq1 5929	. . . . . . 7 ⊢ (𝐴 = 0 → (𝐴↑𝑁) = (0↑𝑁))
5		oveq12 5931	. . . . . . 7 ⊢ (((𝐴↑𝑁) = (0↑𝑁) ∧ 𝐵 = 0) → ((𝐴↑𝑁) gcd 𝐵) = ((0↑𝑁) gcd 0))
6	4, 5	sylan 283	. . . . . 6 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → ((𝐴↑𝑁) gcd 𝐵) = ((0↑𝑁) gcd 0))
7	6	eqeq1d 2205	. . . . 5 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ ((0↑𝑁) gcd 0) = 1))
8		oveq12 5931	. . . . . 6 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐴 gcd 𝐵) = (0 gcd 0))
9	8	eqeq1d 2205	. . . . 5 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → ((𝐴 gcd 𝐵) = 1 ↔ (0 gcd 0) = 1))
10	7, 9	bibi12d 235	. . . 4 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → ((((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1) ↔ (((0↑𝑁) gcd 0) = 1 ↔ (0 gcd 0) = 1)))
11	3, 10	syl5ibrcom 157	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝐴 = 0 ∧ 𝐵 = 0) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1)))
12	11	3ad2ant3 1022	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 = 0 ∧ 𝐵 = 0) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1)))
13		exprmfct 12306	. . . . . . 7 ⊢ (((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵))
14		simpl1 1002	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝐴 ∈ ℤ)
15		simpl3 1004	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝑁 ∈ ℕ)
16	15	nnnn0d 9302	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝑁 ∈ ℕ₀)
17		zexpcl 10646	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ₀) → (𝐴↑𝑁) ∈ ℤ)
18	14, 16, 17	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴↑𝑁) ∈ ℤ)
19	18	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴↑𝑁) ∈ ℤ)
20		simpl2 1003	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝐵 ∈ ℤ)
21	20	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℤ)
22		gcddvds 12130	. . . . . . . . . . . . . . 15 ⊢ (((𝐴↑𝑁) ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵))
23	19, 21, 22	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵))
24	23	simpld 112	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁))
25		prmz 12279	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
26	25	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
27		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
28	14	zcnd 9449	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝐴 ∈ ℂ)
29		expeq0 10662	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0))
30	28, 15, 29	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0))
31	30	anbi1d 465	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (((𝐴↑𝑁) = 0 ∧ 𝐵 = 0) ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
32	27, 31	mtbird 674	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ¬ ((𝐴↑𝑁) = 0 ∧ 𝐵 = 0))
33		gcdn0cl 12129	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴↑𝑁) ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ ((𝐴↑𝑁) = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℕ)
34	18, 20, 32, 33	syl21anc 1248	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℕ)
35	34	nnzd 9447	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ)
36	35	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ)
37		dvdstr 11993	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℤ ∧ ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
38	26, 36, 19, 37	syl3anc 1249	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
39	24, 38	mpan2d 428	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → 𝑝 ∥ (𝐴↑𝑁)))
40		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
41		simpll1 1038	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℤ)
42	15	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ)
43		prmdvdsexp 12316	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑝 ∥ (𝐴↑𝑁) ↔ 𝑝 ∥ 𝐴))
44	40, 41, 42, 43	syl3anc 1249	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴↑𝑁) ↔ 𝑝 ∥ 𝐴))
45	39, 44	sylibd 149	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → 𝑝 ∥ 𝐴))
46	23	simprd 114	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵)
47		dvdstr 11993	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℤ ∧ ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵) → 𝑝 ∥ 𝐵))
48	26, 36, 21, 47	syl3anc 1249	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵) → 𝑝 ∥ 𝐵))
49	46, 48	mpan2d 428	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → 𝑝 ∥ 𝐵))
50	45, 49	jcad 307	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)))
51		dvdsgcd 12179	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ (𝐴 gcd 𝐵)))
52	26, 41, 21, 51	syl3anc 1249	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ (𝐴 gcd 𝐵)))
53		nprmdvds1 12308	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1)
54		breq2 4037	. . . . . . . . . . . . . 14 ⊢ ((𝐴 gcd 𝐵) = 1 → (𝑝 ∥ (𝐴 gcd 𝐵) ↔ 𝑝 ∥ 1))
55	54	notbid 668	. . . . . . . . . . . . 13 ⊢ ((𝐴 gcd 𝐵) = 1 → (¬ 𝑝 ∥ (𝐴 gcd 𝐵) ↔ ¬ 𝑝 ∥ 1))
56	53, 55	syl5ibrcom 157	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → ((𝐴 gcd 𝐵) = 1 → ¬ 𝑝 ∥ (𝐴 gcd 𝐵)))
57	56	necon2ad 2424	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (𝑝 ∥ (𝐴 gcd 𝐵) → (𝐴 gcd 𝐵) ≠ 1))
58	57	adantl 277	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 gcd 𝐵) → (𝐴 gcd 𝐵) ≠ 1))
59	50, 52, 58	3syld 57	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → (𝐴 gcd 𝐵) ≠ 1))
60	59	rexlimdva 2614	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → (𝐴 gcd 𝐵) ≠ 1))
61		gcdn0cl 12129	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
62	61	3adantl3 1157	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
63		eluz2b3 9678	. . . . . . . . . 10 ⊢ ((𝐴 gcd 𝐵) ∈ (ℤ_≥‘2) ↔ ((𝐴 gcd 𝐵) ∈ ℕ ∧ (𝐴 gcd 𝐵) ≠ 1))
64	63	baib 920	. . . . . . . . 9 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → ((𝐴 gcd 𝐵) ∈ (ℤ_≥‘2) ↔ (𝐴 gcd 𝐵) ≠ 1))
65	62, 64	syl 14	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐴 gcd 𝐵) ∈ (ℤ_≥‘2) ↔ (𝐴 gcd 𝐵) ≠ 1))
66	60, 65	sylibrd 169	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → (𝐴 gcd 𝐵) ∈ (ℤ_≥‘2)))
67	13, 66	syl5 32	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2) → (𝐴 gcd 𝐵) ∈ (ℤ_≥‘2)))
68		exprmfct 12306	. . . . . . 7 ⊢ ((𝐴 gcd 𝐵) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝐵))
69		gcddvds 12130	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
70	41, 21, 69	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
71	70	simpld 112	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∥ 𝐴)
72		iddvdsexp 11980	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐴 ∥ (𝐴↑𝑁))
73	41, 42, 72	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝐴 ∥ (𝐴↑𝑁))
74	62	nnzd 9447	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℤ)
75	74	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∈ ℤ)
76		dvdstr 11993	. . . . . . . . . . . . . 14 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ) → (((𝐴 gcd 𝐵) ∥ 𝐴 ∧ 𝐴 ∥ (𝐴↑𝑁)) → (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)))
77	75, 41, 19, 76	syl3anc 1249	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (((𝐴 gcd 𝐵) ∥ 𝐴 ∧ 𝐴 ∥ (𝐴↑𝑁)) → (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)))
78	71, 73, 77	mp2and 433	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁))
79		dvdstr 11993	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
80	26, 75, 19, 79	syl3anc 1249	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
81	78, 80	mpan2d 428	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 gcd 𝐵) → 𝑝 ∥ (𝐴↑𝑁)))
82	70	simprd 114	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∥ 𝐵)
83		dvdstr 11993	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ 𝐵) → 𝑝 ∥ 𝐵))
84	26, 75, 21, 83	syl3anc 1249	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ 𝐵) → 𝑝 ∥ 𝐵))
85	82, 84	mpan2d 428	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 gcd 𝐵) → 𝑝 ∥ 𝐵))
86	81, 85	jcad 307	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 gcd 𝐵) → (𝑝 ∥ (𝐴↑𝑁) ∧ 𝑝 ∥ 𝐵)))
87		dvdsgcd 12179	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ (𝐴↑𝑁) ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵)))
88	26, 19, 21, 87	syl3anc 1249	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝐴↑𝑁) ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵)))
89		breq2 4037	. . . . . . . . . . . . . 14 ⊢ (((𝐴↑𝑁) gcd 𝐵) = 1 → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ↔ 𝑝 ∥ 1))
90	89	notbid 668	. . . . . . . . . . . . 13 ⊢ (((𝐴↑𝑁) gcd 𝐵) = 1 → (¬ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ↔ ¬ 𝑝 ∥ 1))
91	53, 90	syl5ibrcom 157	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → (((𝐴↑𝑁) gcd 𝐵) = 1 → ¬ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵)))
92	91	necon2ad 2424	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
93	92	adantl 277	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
94	86, 88, 93	3syld 57	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 gcd 𝐵) → ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
95	94	rexlimdva 2614	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝐵) → ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
96		eluz2b3 9678	. . . . . . . . . 10 ⊢ (((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2) ↔ (((𝐴↑𝑁) gcd 𝐵) ∈ ℕ ∧ ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
97	96	baib 920	. . . . . . . . 9 ⊢ (((𝐴↑𝑁) gcd 𝐵) ∈ ℕ → (((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2) ↔ ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
98	34, 97	syl 14	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2) ↔ ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
99	95, 98	sylibrd 169	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝐵) → ((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2)))
100	68, 99	syl5 32	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐴 gcd 𝐵) ∈ (ℤ_≥‘2) → ((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2)))
101	67, 100	impbid 129	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2) ↔ (𝐴 gcd 𝐵) ∈ (ℤ_≥‘2)))
102	101, 98, 65	3bitr3d 218	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (((𝐴↑𝑁) gcd 𝐵) ≠ 1 ↔ (𝐴 gcd 𝐵) ≠ 1))
103		simp1 999	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ ℤ)
104		simp3 1001	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ)
105	104	nnnn0d 9302	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ₀)
106	103, 105, 17	syl2anc 411	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) ∈ ℤ)
107		simp2 1000	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐵 ∈ ℤ)
108	106, 107	gcdcld 12135	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℕ₀)
109	108	nn0zd 9446	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ)
110		1zzd 9353	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℤ)
111		zdceq 9401	. . . . . . 7 ⊢ ((((𝐴↑𝑁) gcd 𝐵) ∈ ℤ ∧ 1 ∈ ℤ) → DECID ((𝐴↑𝑁) gcd 𝐵) = 1)
112	109, 110, 111	syl2anc 411	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → DECID ((𝐴↑𝑁) gcd 𝐵) = 1)
113	103, 107	gcdcld 12135	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
114	113	nn0zd 9446	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℤ)
115		zdceq 9401	. . . . . . 7 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 gcd 𝐵) = 1)
116	114, 110, 115	syl2anc 411	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → DECID (𝐴 gcd 𝐵) = 1)
117		nebidc 2447	. . . . . 6 ⊢ (DECID ((𝐴↑𝑁) gcd 𝐵) = 1 → (DECID (𝐴 gcd 𝐵) = 1 → ((((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1) ↔ (((𝐴↑𝑁) gcd 𝐵) ≠ 1 ↔ (𝐴 gcd 𝐵) ≠ 1))))
118	112, 116, 117	sylc 62	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1) ↔ (((𝐴↑𝑁) gcd 𝐵) ≠ 1 ↔ (𝐴 gcd 𝐵) ≠ 1)))
119	118	adantr 276	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1) ↔ (((𝐴↑𝑁) gcd 𝐵) ≠ 1 ↔ (𝐴 gcd 𝐵) ≠ 1)))
120	102, 119	mpbird 167	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1))
121	120	ex 115	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬ (𝐴 = 0 ∧ 𝐵 = 0) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1)))
122		gcdmndc 12122	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID (𝐴 = 0 ∧ 𝐵 = 0))
123		exmiddc 837	. . . 4 ⊢ (DECID (𝐴 = 0 ∧ 𝐵 = 0) → ((𝐴 = 0 ∧ 𝐵 = 0) ∨ ¬ (𝐴 = 0 ∧ 𝐵 = 0)))
124	122, 123	syl 14	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 = 0 ∧ 𝐵 = 0) ∨ ¬ (𝐴 = 0 ∧ 𝐵 = 0)))
125	124	3adant3 1019	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 = 0 ∧ 𝐵 = 0) ∨ ¬ (𝐴 = 0 ∧ 𝐵 = 0)))
126	12, 121, 125	mpjaod 719	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 DECID wdc 835 ∧ w3a 980 = wceq 1364 ∈ wcel 2167 ≠ wne 2367 ∃wrex 2476 class class class wbr 4033 ‘cfv 5258 (class class class)co 5922 ℂcc 7877 0cc0 7879 1c1 7880 ℕcn 8990 2c2 9041 ℕ₀cn0 9249 ℤcz 9326 ℤ_≥cuz 9601 ↑cexp 10630 ∥ cdvds 11952 gcd cgcd 12120 ℙcprime 12275

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-frec 6449 df-1o 6474 df-2o 6475 df-er 6592 df-en 6800 df-sup 7050 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-n0 9250 df-z 9327 df-uz 9602 df-q 9694 df-rp 9729 df-fz 10084 df-fzo 10218 df-fl 10360 df-mod 10415 df-seqfrec 10540 df-exp 10631 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-dvds 11953 df-gcd 12121 df-prm 12276

This theorem is referenced by: rpexp1i 12322 phiprmpw 12390 pockthlem 12525 logbgcd1irr 15203 logbgcd1irraplemexp 15204

W3C validator