rpexp - Intuitionistic Logic Explorer

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

Theorem rpexp 12914

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 10994	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0)
2	1	oveq1d 6094	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((0↑𝑁) gcd 0) = (0 gcd 0))
3	2	eqeq1d 2247	. . . 4 ⊢ (𝑁 ∈ ℕ → (((0↑𝑁) gcd 0) = 1 ↔ (0 gcd 0) = 1))
4		oveq1 6086	. . . . . . 7 ⊢ (𝐴 = 0 → (𝐴↑𝑁) = (0↑𝑁))
5		oveq12 6088	. . . . . . 7 ⊢ (((𝐴↑𝑁) = (0↑𝑁) ∧ 𝐵 = 0) → ((𝐴↑𝑁) gcd 𝐵) = ((0↑𝑁) gcd 0))
6	4, 5	sylan 283	. . . . . 6 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → ((𝐴↑𝑁) gcd 𝐵) = ((0↑𝑁) gcd 0))
7	6	eqeq1d 2247	. . . . 5 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ ((0↑𝑁) gcd 0) = 1))
8		oveq12 6088	. . . . . 6 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐴 gcd 𝐵) = (0 gcd 0))
9	8	eqeq1d 2247	. . . . 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 1051	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 = 0 ∧ 𝐵 = 0) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1)))
13		exprmfct 12899	. . . . . . 7 ⊢ (((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵))
14		simpl1 1031	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝐴 ∈ ℤ)
15		simpl3 1033	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝑁 ∈ ℕ)
16	15	nnnn0d 9603	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝑁 ∈ ℕ₀)
17		zexpcl 10974	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ₀) → (𝐴↑𝑁) ∈ ℤ)
18	14, 16, 17	syl2anc 415	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴↑𝑁) ∈ ℤ)
19	18	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴↑𝑁) ∈ ℤ)
20		simpl2 1032	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝐵 ∈ ℤ)
21	20	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℤ)
22		gcddvds 12723	. . . . . . . . . . . . . . 15 ⊢ (((𝐴↑𝑁) ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵))
23	19, 21, 22	syl2anc 415	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵))
24	23	simpld 112	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁))
25		prmz 12872	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
26	25	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
27		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
28	14	zcnd 9752	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → 𝐴 ∈ ℂ)
29		expeq0 10990	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0))
30	28, 15, 29	syl2anc 415	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0))
31	30	anbi1d 469	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (((𝐴↑𝑁) = 0 ∧ 𝐵 = 0) ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
32	27, 31	mtbird 684	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ¬ ((𝐴↑𝑁) = 0 ∧ 𝐵 = 0))
33		gcdn0cl 12722	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴↑𝑁) ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ ((𝐴↑𝑁) = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℕ)
34	18, 20, 32, 33	syl21anc 1277	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℕ)
35	34	nnzd 9750	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ)
36	35	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ)
37		dvdstr 12578	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℤ ∧ ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
38	26, 36, 19, 37	syl3anc 1278	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
39	24, 38	mpan2d 432	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → 𝑝 ∥ (𝐴↑𝑁)))
40		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
41		simpll1 1067	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℤ)
42	15	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ)
43		prmdvdsexp 12909	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑝 ∥ (𝐴↑𝑁) ↔ 𝑝 ∥ 𝐴))
44	40, 41, 42, 43	syl3anc 1278	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴↑𝑁) ↔ 𝑝 ∥ 𝐴))
45	39, 44	sylibd 149	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → 𝑝 ∥ 𝐴))
46	23	simprd 114	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵)
47		dvdstr 12578	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℤ ∧ ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵) → 𝑝 ∥ 𝐵))
48	26, 36, 21, 47	syl3anc 1278	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ∧ ((𝐴↑𝑁) gcd 𝐵) ∥ 𝐵) → 𝑝 ∥ 𝐵))
49	46, 48	mpan2d 432	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → 𝑝 ∥ 𝐵))
50	45, 49	jcad 307	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)))
51		dvdsgcd 12772	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ (𝐴 gcd 𝐵)))
52	26, 41, 21, 51	syl3anc 1278	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ (𝐴 gcd 𝐵)))
53		nprmdvds1 12901	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1)
54		breq2 4132	. . . . . . . . . . . . . 14 ⊢ ((𝐴 gcd 𝐵) = 1 → (𝑝 ∥ (𝐴 gcd 𝐵) ↔ 𝑝 ∥ 1))
55	54	notbid 677	. . . . . . . . . . . . 13 ⊢ ((𝐴 gcd 𝐵) = 1 → (¬ 𝑝 ∥ (𝐴 gcd 𝐵) ↔ ¬ 𝑝 ∥ 1))
56	53, 55	syl5ibrcom 157	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → ((𝐴 gcd 𝐵) = 1 → ¬ 𝑝 ∥ (𝐴 gcd 𝐵)))
57	56	necon2ad 2477	. . . . . . . . . . 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 2668	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) → (𝐴 gcd 𝐵) ≠ 1))
61		gcdn0cl 12722	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
62	61	3adantl3 1186	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
63		eluz2b3 9987	. . . . . . . . . 10 ⊢ ((𝐴 gcd 𝐵) ∈ (ℤ_≥‘2) ↔ ((𝐴 gcd 𝐵) ∈ ℕ ∧ (𝐴 gcd 𝐵) ≠ 1))
64	63	baib 931	. . . . . . . . 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 12899	. . . . . . 7 ⊢ ((𝐴 gcd 𝐵) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝐵))
69		gcddvds 12723	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
70	41, 21, 69	syl2anc 415	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
71	70	simpld 112	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∥ 𝐴)
72		iddvdsexp 12565	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐴 ∥ (𝐴↑𝑁))
73	41, 42, 72	syl2anc 415	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → 𝐴 ∥ (𝐴↑𝑁))
74	62	nnzd 9750	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℤ)
75	74	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∈ ℤ)
76		dvdstr 12578	. . . . . . . . . . . . . 14 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ) → (((𝐴 gcd 𝐵) ∥ 𝐴 ∧ 𝐴 ∥ (𝐴↑𝑁)) → (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)))
77	75, 41, 19, 76	syl3anc 1278	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (((𝐴 gcd 𝐵) ∥ 𝐴 ∧ 𝐴 ∥ (𝐴↑𝑁)) → (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)))
78	71, 73, 77	mp2and 437	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁))
79		dvdstr 12578	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
80	26, 75, 19, 79	syl3anc 1278	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ (𝐴↑𝑁)) → 𝑝 ∥ (𝐴↑𝑁)))
81	78, 80	mpan2d 432	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 gcd 𝐵) → 𝑝 ∥ (𝐴↑𝑁)))
82	70	simprd 114	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) ∥ 𝐵)
83		dvdstr 12578	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ 𝐵) → 𝑝 ∥ 𝐵))
84	26, 75, 21, 83	syl3anc 1278	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝐴 gcd 𝐵) ∧ (𝐴 gcd 𝐵) ∥ 𝐵) → 𝑝 ∥ 𝐵))
85	82, 84	mpan2d 432	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 gcd 𝐵) → 𝑝 ∥ 𝐵))
86	81, 85	jcad 307	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 gcd 𝐵) → (𝑝 ∥ (𝐴↑𝑁) ∧ 𝑝 ∥ 𝐵)))
87		dvdsgcd 12772	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ (𝐴↑𝑁) ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵)))
88	26, 19, 21, 87	syl3anc 1278	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝐴↑𝑁) ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵)))
89		breq2 4132	. . . . . . . . . . . . . 14 ⊢ (((𝐴↑𝑁) gcd 𝐵) = 1 → (𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ↔ 𝑝 ∥ 1))
90	89	notbid 677	. . . . . . . . . . . . 13 ⊢ (((𝐴↑𝑁) gcd 𝐵) = 1 → (¬ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵) ↔ ¬ 𝑝 ∥ 1))
91	53, 90	syl5ibrcom 157	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → (((𝐴↑𝑁) gcd 𝐵) = 1 → ¬ 𝑝 ∥ ((𝐴↑𝑁) gcd 𝐵)))
92	91	necon2ad 2477	. . . . . . . . . . 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 2668	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (∃𝑝 ∈ ℙ 𝑝 ∥ (𝐴 gcd 𝐵) → ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
96		eluz2b3 9987	. . . . . . . . . 10 ⊢ (((𝐴↑𝑁) gcd 𝐵) ∈ (ℤ_≥‘2) ↔ (((𝐴↑𝑁) gcd 𝐵) ∈ ℕ ∧ ((𝐴↑𝑁) gcd 𝐵) ≠ 1))
97	96	baib 931	. . . . . . . . 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 1028	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ ℤ)
104		simp3 1030	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ)
105	104	nnnn0d 9603	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ₀)
106	103, 105, 17	syl2anc 415	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) ∈ ℤ)
107		simp2 1029	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐵 ∈ ℤ)
108	106, 107	gcdcld 12728	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℕ₀)
109	108	nn0zd 9749	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) gcd 𝐵) ∈ ℤ)
110		1zzd 9654	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℤ)
111		zdceq 9703	. . . . . . 7 ⊢ ((((𝐴↑𝑁) gcd 𝐵) ∈ ℤ ∧ 1 ∈ ℤ) → DECID ((𝐴↑𝑁) gcd 𝐵) = 1)
112	109, 110, 111	syl2anc 415	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → DECID ((𝐴↑𝑁) gcd 𝐵) = 1)
113	103, 107	gcdcld 12728	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
114	113	nn0zd 9749	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℤ)
115		zdceq 9703	. . . . . . 7 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 gcd 𝐵) = 1)
116	114, 110, 115	syl2anc 415	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → DECID (𝐴 gcd 𝐵) = 1)
117		nebidc 2500	. . . . . 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 12715	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID (𝐴 = 0 ∧ 𝐵 = 0))
123		exmiddc 848	. . . 4 ⊢ (DECID (𝐴 = 0 ∧ 𝐵 = 0) → ((𝐴 = 0 ∧ 𝐵 = 0) ∨ ¬ (𝐴 = 0 ∧ 𝐵 = 0)))
124	122, 123	syl 14	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 = 0 ∧ 𝐵 = 0) ∨ ¬ (𝐴 = 0 ∧ 𝐵 = 0)))
125	124	3adant3 1048	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 = 0 ∧ 𝐵 = 0) ∨ ¬ (𝐴 = 0 ∧ 𝐵 = 0)))
126	12, 121, 125	mpjaod 730	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 ≠ wne 2420 ∃wrex 2529 class class class wbr 4128 ‘cfv 5375 (class class class)co 6079 ℂcc 8171 0cc0 8173 1c1 8174 ℕcn 9287 2c2 9338 ℕ₀cn0 9546 ℤcz 9627 ℤ_≥cuz 9904 ↑cexp 10958 ∥ cdvds 12537 gcd cgcd 12713 ℙcprime 12868

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 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4244 ax-sep 4247 ax-nul 4257 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-setind 4682 ax-iinf 4733 ax-cnex 8264 ax-resscn 8265 ax-1cn 8266 ax-1re 8267 ax-icn 8268 ax-addcl 8269 ax-addrcl 8270 ax-mulcl 8271 ax-mulrcl 8272 ax-addcom 8273 ax-mulcom 8274 ax-addass 8275 ax-mulass 8276 ax-distr 8277 ax-i2m1 8278 ax-0lt1 8279 ax-1rid 8280 ax-0id 8281 ax-rnegex 8282 ax-precex 8283 ax-cnre 8284 ax-pre-ltirr 8285 ax-pre-ltwlin 8286 ax-pre-lttrn 8287 ax-pre-apti 8288 ax-pre-ltadd 8289 ax-pre-mulgt0 8290 ax-pre-mulext 8291 ax-arch 8292 ax-caucvg 8293

This theorem depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3714 df-pr 3715 df-op 3717 df-uni 3934 df-int 3969 df-iun 4012 df-br 4129 df-opab 4191 df-mpt 4192 df-tr 4228 df-id 4436 df-po 4439 df-iso 4440 df-iord 4509 df-on 4511 df-ilim 4512 df-suc 4514 df-iom 4736 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-ima 4785 df-iota 5335 df-fun 5377 df-fn 5378 df-f 5379 df-f1 5380 df-fo 5381 df-f1o 5382 df-fv 5383 df-riota 6032 df-ov 6082 df-oprab 6083 df-mpo 6084 df-1st 6368 df-2nd 6369 df-recs 6570 df-frec 6656 df-1o 6681 df-2o 6682 df-er 6801 df-en 7017 df-sup 7318 df-pnf 8356 df-mnf 8357 df-xr 8358 df-ltxr 8359 df-le 8360 df-sub 8493 df-neg 8494 df-reap 8897 df-ap 8904 df-div 8997 df-inn 9288 df-2 9346 df-3 9347 df-4 9348 df-n0 9547 df-z 9628 df-uz 9905 df-q 10003 df-rp 10038 df-fz 10395 df-fzo 10533 df-fl 10688 df-mod 10743 df-seqfrec 10868 df-exp 10959 df-cj 11590 df-re 11591 df-im 11592 df-rsqrt 11747 df-abs 11748 df-dvds 12538 df-gcd 12714 df-prm 12869

This theorem is referenced by: rpexp1i 12915 phiprmpw 12983 pockthlem 13118 logbgcd1irr 16052 logbgcd1irraplemexp 16053

W3C validator