rpexp - Intuitionistic Logic Explorer

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

Theorem rpexp 12641

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 10763	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0)
2	1	oveq1d 5989	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((0↑𝑁) gcd 0) = (0 gcd 0))
3	2	eqeq1d 2218	. . . 4 ⊢ (𝑁 ∈ ℕ → (((0↑𝑁) gcd 0) = 1 ↔ (0 gcd 0) = 1))
4		oveq1 5981	. . . . . . 7 ⊢ (𝐴 = 0 → (𝐴↑𝑁) = (0↑𝑁))
5		oveq12 5983	. . . . . . 7 ⊢ (((𝐴↑𝑁) = (0↑𝑁) ∧ 𝐵 = 0) → ((𝐴↑𝑁) gcd 𝐵) = ((0↑𝑁) gcd 0))
6	4, 5	sylan 283	. . . . . 6 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → ((𝐴↑𝑁) gcd 𝐵) = ((0↑𝑁) gcd 0))
7	6	eqeq1d 2218	. . . . 5 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ ((0↑𝑁) gcd 0) = 1))
8		oveq12 5983	. . . . . 6 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐴 gcd 𝐵) = (0 gcd 0))
9	8	eqeq1d 2218	. . . . 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 1025	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 = 0 ∧ 𝐵 = 0) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1)))
13		exprmfct 12626	. . . . . . 7 ⊢ (((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵))
14		simpl1 1005	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝐴 ∈ ℤ)
15		simpl3 1007	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝑁 ∈ ℕ)
16	15	nnnn0d 9390	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝑁 ∈ ℕ₀)
17		zexpcl 10743	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ₀) → (𝐴↑𝑁) ∈ ℤ)
18	14, 16, 17	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴↑𝑁) ∈ ℤ)
19	18	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴↑𝑁) ∈ ℤ)
20		simpl2 1006	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝐵 ∈ ℤ)
21	20	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℤ)
22		gcddvds 12450	. . . . . . . . . . . . . . 15 ⊢ (((𝐴↑𝑁) ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵))
23	19, 21, 22	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵))
24	23	simpld 112	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁))
25		prmz 12599	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
26	25	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
27		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
28	14	zcnd 9538	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝐴 ∈ ℂ)
29		expeq0 10759	. . . . . . . . . . . . . . . . . . . 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 677	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ¬ ((𝐴↑𝑁) = 0 ∧ 𝐵 = 0))
33		gcdn0cl 12449	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴↑𝑁) ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ ((𝐴↑𝑁) = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℕ)
34	18, 20, 32, 33	syl21anc 1251	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℕ)
35	34	nnzd 9536	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ)
36	35	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ)
37		dvdstr 12305	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℤ ∧ ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
38	26, 36, 19, 37	syl3anc 1252	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
39	24, 38	mpan2d 428	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → 𝑝 ∥ (𝐴↑𝑁)))
40		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
41		simpll1 1041	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℤ)
42	15	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ)
43		prmdvdsexp 12636	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑝 ∥ (𝐴↑𝑁) ↔ 𝑝 ∥ 𝐴))
44	40, 41, 42, 43	syl3anc 1252	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴↑𝑁) ↔ 𝑝 ∥ 𝐴))
45	39, 44	sylibd 149	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → 𝑝 ∥ 𝐴))
46	23	simprd 114	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵)
47		dvdstr 12305	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℤ ∧ ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵) → 𝑝 ∥ 𝐵))
48	26, 36, 21, 47	syl3anc 1252	. . . . . . . . . . . 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 12499	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ (𝐴 gcd 𝐵)))
52	26, 41, 21, 51	syl3anc 1252	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ (𝐴 gcd 𝐵)))
53		nprmdvds1 12628	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1)
54		breq2 4066	. . . . . . . . . . . . . 14 ⊢ ((𝐴 gcd 𝐵) = 1 → (𝑝 ∥ (𝐴 gcd 𝐵) ↔ 𝑝 ∥ 1))
55	54	notbid 671	. . . . . . . . . . . . 13 ⊢ ((𝐴 gcd 𝐵) = 1 → (¬ 𝑝 ∥ (𝐴 gcd 𝐵) ↔ ¬ 𝑝 ∥ 1))
56	53, 55	syl5ibrcom 157	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → ((𝐴 gcd 𝐵) = 1 → ¬ 𝑝 ∥ (𝐴 gcd 𝐵)))
57	56	necon2ad 2437	. . . . . . . . . . 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 2628	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → (𝐴 gcd 𝐵) ≠ 1))
61		gcdn0cl 12449	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
62	61	3adantl3 1160	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
63		eluz2b3 9767	. . . . . . . . . 10 ⊢ ((𝐴 gcd 𝐵) ∈ (ℤ_≥‘2) ↔ ((𝐴 gcd 𝐵) ∈ ℕ ∧ (𝐴 gcd 𝐵) ≠ 1))
64	63	baib 923	. . . . . . . . 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 12626	. . . . . . 7 ⊢ ((𝐴 gcd 𝐵) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝐵))
69		gcddvds 12450	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
70	41, 21, 69	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
71	70	simpld 112	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∥ 𝐴)
72		iddvdsexp 12292	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐴 ∥ (𝐴↑𝑁))
73	41, 42, 72	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝐴 ∥ (𝐴↑𝑁))
74	62	nnzd 9536	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℤ)
75	74	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∈ ℤ)
76		dvdstr 12305	. . . . . . . . . . . . . 14 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ) → (((𝐴 gcd 𝐵) ∥ 𝐴 ∧ 𝐴 ∥ (𝐴↑𝑁)) → (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)))
77	75, 41, 19, 76	syl3anc 1252	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (((𝐴 gcd 𝐵) ∥ 𝐴 ∧ 𝐴 ∥ (𝐴↑𝑁)) → (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)))
78	71, 73, 77	mp2and 433	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁))
79		dvdstr 12305	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
80	26, 75, 19, 79	syl3anc 1252	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
81	78, 80	mpan2d 428	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 gcd 𝐵) → 𝑝 ∥ (𝐴↑𝑁)))
82	70	simprd 114	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∥ 𝐵)
83		dvdstr 12305	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ 𝐵) → 𝑝 ∥ 𝐵))
84	26, 75, 21, 83	syl3anc 1252	. . . . . . . . . . . 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 12499	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ (𝐴↑𝑁) ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵)))
88	26, 19, 21, 87	syl3anc 1252	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝐴↑𝑁) ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵)))
89		breq2 4066	. . . . . . . . . . . . . 14 ⊢ (((𝐴↑𝑁) gcd 𝐵) = 1 → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ↔ 𝑝 ∥ 1))
90	89	notbid 671	. . . . . . . . . . . . 13 ⊢ (((𝐴↑𝑁) gcd 𝐵) = 1 → (¬ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ↔ ¬ 𝑝 ∥ 1))
91	53, 90	syl5ibrcom 157	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → (((𝐴↑𝑁) gcd 𝐵) = 1 → ¬ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵)))
92	91	necon2ad 2437	. . . . . . . . . . 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 2628	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝐵) → ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
96		eluz2b3 9767	. . . . . . . . . 10 ⊢ (((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2) ↔ (((𝐴↑𝑁) gcd 𝐵) ∈ ℕ ∧ ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
97	96	baib 923	. . . . . . . . 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 1002	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ ℤ)
104		simp3 1004	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ)
105	104	nnnn0d 9390	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ₀)
106	103, 105, 17	syl2anc 411	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) ∈ ℤ)
107		simp2 1003	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐵 ∈ ℤ)
108	106, 107	gcdcld 12455	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℕ₀)
109	108	nn0zd 9535	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ)
110		1zzd 9441	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℤ)
111		zdceq 9490	. . . . . . 7 ⊢ ((((𝐴↑𝑁) gcd 𝐵) ∈ ℤ ∧ 1 ∈ ℤ) → DECID ((𝐴↑𝑁) gcd 𝐵) = 1)
112	109, 110, 111	syl2anc 411	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → DECID ((𝐴↑𝑁) gcd 𝐵) = 1)
113	103, 107	gcdcld 12455	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
114	113	nn0zd 9535	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℤ)
115		zdceq 9490	. . . . . . 7 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 gcd 𝐵) = 1)
116	114, 110, 115	syl2anc 411	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → DECID (𝐴 gcd 𝐵) = 1)
117		nebidc 2460	. . . . . 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 12442	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID (𝐴 = 0 ∧ 𝐵 = 0))
123		exmiddc 840	. . . 4 ⊢ (DECID (𝐴 = 0 ∧ 𝐵 = 0) → ((𝐴 = 0 ∧ 𝐵 = 0) ∨ ¬ (𝐴 = 0 ∧ 𝐵 = 0)))
124	122, 123	syl 14	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 = 0 ∧ 𝐵 = 0) ∨ ¬ (𝐴 = 0 ∧ 𝐵 = 0)))
125	124	3adant3 1022	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 = 0 ∧ 𝐵 = 0) ∨ ¬ (𝐴 = 0 ∧ 𝐵 = 0)))
126	12, 121, 125	mpjaod 722	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 712 DECID wdc 838 ∧ w3a 983 = wceq 1375 ∈ wcel 2180 ≠ wne 2380 ∃wrex 2489 class class class wbr 4062 ‘cfv 5294 (class class class)co 5974 ℂcc 7965 0cc0 7967 1c1 7968 ℕcn 9078 2c2 9129 ℕ₀cn0 9337 ℤcz 9414 ℤ_≥cuz 9690 ↑cexp 10727 ∥ cdvds 12264 gcd cgcd 12440 ℙcprime 12595

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 617 ax-in2 618 ax-io 713 ax-5 1473 ax-7 1474 ax-gen 1475 ax-ie1 1519 ax-ie2 1520 ax-8 1530 ax-10 1531 ax-11 1532 ax-i12 1533 ax-bndl 1535 ax-4 1536 ax-17 1552 ax-i9 1556 ax-ial 1560 ax-i5r 1561 ax-13 2182 ax-14 2183 ax-ext 2191 ax-coll 4178 ax-sep 4181 ax-nul 4189 ax-pow 4237 ax-pr 4272 ax-un 4501 ax-setind 4606 ax-iinf 4657 ax-cnex 8058 ax-resscn 8059 ax-1cn 8060 ax-1re 8061 ax-icn 8062 ax-addcl 8063 ax-addrcl 8064 ax-mulcl 8065 ax-mulrcl 8066 ax-addcom 8067 ax-mulcom 8068 ax-addass 8069 ax-mulass 8070 ax-distr 8071 ax-i2m1 8072 ax-0lt1 8073 ax-1rid 8074 ax-0id 8075 ax-rnegex 8076 ax-precex 8077 ax-cnre 8078 ax-pre-ltirr 8079 ax-pre-ltwlin 8080 ax-pre-lttrn 8081 ax-pre-apti 8082 ax-pre-ltadd 8083 ax-pre-mulgt0 8084 ax-pre-mulext 8085 ax-arch 8086 ax-caucvg 8087

This theorem depends on definitions: df-bi 117 df-stab 835 df-dc 839 df-3or 984 df-3an 985 df-tru 1378 df-fal 1381 df-nf 1487 df-sb 1789 df-eu 2060 df-mo 2061 df-clab 2196 df-cleq 2202 df-clel 2205 df-nfc 2341 df-ne 2381 df-nel 2476 df-ral 2493 df-rex 2494 df-reu 2495 df-rmo 2496 df-rab 2497 df-v 2781 df-sbc 3009 df-csb 3105 df-dif 3179 df-un 3181 df-in 3183 df-ss 3190 df-nul 3472 df-if 3583 df-pw 3631 df-sn 3652 df-pr 3653 df-op 3655 df-uni 3868 df-int 3903 df-iun 3946 df-br 4063 df-opab 4125 df-mpt 4126 df-tr 4162 df-id 4361 df-po 4364 df-iso 4365 df-iord 4434 df-on 4436 df-ilim 4437 df-suc 4439 df-iom 4660 df-xp 4702 df-rel 4703 df-cnv 4704 df-co 4705 df-dm 4706 df-rn 4707 df-res 4708 df-ima 4709 df-iota 5254 df-fun 5296 df-fn 5297 df-f 5298 df-f1 5299 df-fo 5300 df-f1o 5301 df-fv 5302 df-riota 5927 df-ov 5977 df-oprab 5978 df-mpo 5979 df-1st 6256 df-2nd 6257 df-recs 6421 df-frec 6507 df-1o 6532 df-2o 6533 df-er 6650 df-en 6858 df-sup 7119 df-pnf 8151 df-mnf 8152 df-xr 8153 df-ltxr 8154 df-le 8155 df-sub 8287 df-neg 8288 df-reap 8690 df-ap 8697 df-div 8788 df-inn 9079 df-2 9137 df-3 9138 df-4 9139 df-n0 9338 df-z 9415 df-uz 9691 df-q 9783 df-rp 9818 df-fz 10173 df-fzo 10307 df-fl 10457 df-mod 10512 df-seqfrec 10637 df-exp 10728 df-cj 11319 df-re 11320 df-im 11321 df-rsqrt 11475 df-abs 11476 df-dvds 12265 df-gcd 12441 df-prm 12596

This theorem is referenced by: rpexp1i 12642 phiprmpw 12710 pockthlem 12845 logbgcd1irr 15606 logbgcd1irraplemexp 15607

W3C validator