Theorem isprm5 15626

Description: One need only check prime divisors of 𝑃 up to √𝑃 in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014.)

Assertion

Ref	Expression
isprm5	⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))

Distinct variable group:   𝑧,𝑃

Proof of Theorem isprm5

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isprm4 15604	. 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ (ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃)))
2		prmuz2 15615	. . . . . . . 8 ⊢ (𝑧 ∈ ℙ → 𝑧 ∈ (ℤ≥‘2))
3	2	a1i 11	. . . . . . 7 ⊢ (𝑃 ∈ (ℤ≥‘2) → (𝑧 ∈ ℙ → 𝑧 ∈ (ℤ≥‘2)))
4		eluz2b2 11964	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃))
5	4	simprbi 484	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℤ≥‘2) → 1 < 𝑃)
6		eluzelre 11899	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℤ≥‘2) → 𝑃 ∈ ℝ)
7		eluz2nn 11928	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ (ℤ≥‘2) → 𝑃 ∈ ℕ)
8	7	nngt0d 11266	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℤ≥‘2) → 0 < 𝑃)
9		ltmulgt11 11085	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 0 < 𝑃) → (1 < 𝑃 ↔ 𝑃 < (𝑃 · 𝑃)))
10	6, 6, 8, 9	syl3anc 1476	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℤ≥‘2) → (1 < 𝑃 ↔ 𝑃 < (𝑃 · 𝑃)))
11	5, 10	mpbid 222	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℤ≥‘2) → 𝑃 < (𝑃 · 𝑃))
12	6, 6	remulcld 10272	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℤ≥‘2) → (𝑃 · 𝑃) ∈ ℝ)
13	6, 12	ltnled 10386	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℤ≥‘2) → (𝑃 < (𝑃 · 𝑃) ↔ ¬ (𝑃 · 𝑃) ≤ 𝑃))
14	11, 13	mpbid 222	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℤ≥‘2) → ¬ (𝑃 · 𝑃) ≤ 𝑃)
15		oveq12 6802	. . . . . . . . . . . . 13 ⊢ ((𝑧 = 𝑃 ∧ 𝑧 = 𝑃) → (𝑧 · 𝑧) = (𝑃 · 𝑃))
16	15	anidms 556	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑃 → (𝑧 · 𝑧) = (𝑃 · 𝑃))
17	16	breq1d 4796	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑃 → ((𝑧 · 𝑧) ≤ 𝑃 ↔ (𝑃 · 𝑃) ≤ 𝑃))
18	17	notbid 307	. . . . . . . . . 10 ⊢ (𝑧 = 𝑃 → (¬ (𝑧 · 𝑧) ≤ 𝑃 ↔ ¬ (𝑃 · 𝑃) ≤ 𝑃))
19	14, 18	syl5ibrcom 237	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℤ≥‘2) → (𝑧 = 𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃))
20	19	imim2d 57	. . . . . . . 8 ⊢ (𝑃 ∈ (ℤ≥‘2) → ((𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → (𝑧 ∥ 𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃)))
21		con2 132	. . . . . . . 8 ⊢ ((𝑧 ∥ 𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))
22	20, 21	syl6 35	. . . . . . 7 ⊢ (𝑃 ∈ (ℤ≥‘2) → ((𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
23	3, 22	imim12d 81	. . . . . 6 ⊢ (𝑃 ∈ (ℤ≥‘2) → ((𝑧 ∈ (ℤ≥‘2) → (𝑧 ∥ 𝑃 → 𝑧 = 𝑃)) → (𝑧 ∈ ℙ → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))))
24	23	ralimdv2 3110	. . . . 5 ⊢ (𝑃 ∈ (ℤ≥‘2) → (∀𝑧 ∈ (ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
25		annim 390	. . . . . . . . 9 ⊢ ((𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃) ↔ ¬ (𝑧 ∥ 𝑃 → 𝑧 = 𝑃))
26		oveq12 6802	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑧) → (𝑥 · 𝑥) = (𝑧 · 𝑧))
27	26	anidms 556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → (𝑥 · 𝑥) = (𝑧 · 𝑧))
28	27	breq1d 4796	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → ((𝑥 · 𝑥) ≤ 𝑃 ↔ (𝑧 · 𝑧) ≤ 𝑃))
29		breq1 4789	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝑥 ∥ 𝑃 ↔ 𝑧 ∥ 𝑃))
30	28, 29	anbi12d 616	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃) ↔ ((𝑧 · 𝑧) ≤ 𝑃 ∧ 𝑧 ∥ 𝑃)))
31	30	rspcev 3460	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (ℤ≥‘2) ∧ ((𝑧 · 𝑧) ≤ 𝑃 ∧ 𝑧 ∥ 𝑃)) → ∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃))
32	31	ancom2s 629	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (ℤ≥‘2) ∧ (𝑧 ∥ 𝑃 ∧ (𝑧 · 𝑧) ≤ 𝑃)) → ∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃))
33	32	expr 444	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)))
34	33	ad2ant2lr 742	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) ≤ 𝑃 → ∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)))
35		simprl 754	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∥ 𝑃)
36		eluzelz 11898	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (ℤ≥‘2) → 𝑧 ∈ ℤ)
37	36	ad2antlr 706	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℤ)
38		eluz2nn 11928	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (ℤ≥‘2) → 𝑧 ∈ ℕ)
39	38	ad2antlr 706	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℕ)
40	39	nnne0d 11267	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ≠ 0)
41		eluzelz 11898	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (ℤ≥‘2) → 𝑃 ∈ ℤ)
42	41	ad2antrr 705	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℤ)
43		dvdsval2 15192	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ∧ 𝑃 ∈ ℤ) → (𝑧 ∥ 𝑃 ↔ (𝑃 / 𝑧) ∈ ℤ))
44	37, 40, 42, 43	syl3anc 1476	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 ∥ 𝑃 ↔ (𝑃 / 𝑧) ∈ ℤ))
45	35, 44	mpbid 222	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∈ ℤ)
46		eluzelre 11899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (ℤ≥‘2) → 𝑧 ∈ ℝ)
47	46	ad2antlr 706	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℝ)
48	47	recnd 10270	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℂ)
49	48	mulid2d 10260	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (1 · 𝑧) = 𝑧)
50	7	ad2antrr 705	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℕ)
51		dvdsle 15241	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑧 ∥ 𝑃 → 𝑧 ≤ 𝑃))
52	51	imp 393	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧ 𝑧 ∥ 𝑃) → 𝑧 ≤ 𝑃)
53	37, 50, 35, 52	syl21anc 1475	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ≤ 𝑃)
54		simprr 756	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ¬ 𝑧 = 𝑃)
55	54	neqned 2950	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ≠ 𝑃)
56	55	necomd 2998	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ≠ 𝑧)
57	6	ad2antrr 705	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℝ)
58	47, 57	ltlend 10384	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 < 𝑃 ↔ (𝑧 ≤ 𝑃 ∧ 𝑃 ≠ 𝑧)))
59	53, 56, 58	mpbir2and 692	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 < 𝑃)
60	49, 59	eqbrtrd 4808	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (1 · 𝑧) < 𝑃)
61		1red 10257	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 1 ∈ ℝ)
62	42	zred 11684	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℝ)
63		nnre 11229	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
64		nngt0 11251	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℕ → 0 < 𝑧)
65	63, 64	jca 501	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ → (𝑧 ∈ ℝ ∧ 0 < 𝑧))
66	39, 65	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 ∈ ℝ ∧ 0 < 𝑧))
67		ltmuldiv 11098	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑧 ∈ ℝ ∧ 0 < 𝑧)) → ((1 · 𝑧) < 𝑃 ↔ 1 < (𝑃 / 𝑧)))
68	61, 62, 66, 67	syl3anc 1476	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((1 · 𝑧) < 𝑃 ↔ 1 < (𝑃 / 𝑧)))
69	60, 68	mpbid 222	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 1 < (𝑃 / 𝑧))
70		eluz2b1 11962	. . . . . . . . . . . . 13 ⊢ ((𝑃 / 𝑧) ∈ (ℤ≥‘2) ↔ ((𝑃 / 𝑧) ∈ ℤ ∧ 1 < (𝑃 / 𝑧)))
71	45, 69, 70	sylanbrc 572	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∈ (ℤ≥‘2))
72	47, 47	remulcld 10272	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℝ)
73	39, 39	nnmulcld 11270	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℕ)
74		nnrp 12045	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℝ+)
75		nnrp 12045	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 · 𝑧) ∈ ℕ → (𝑧 · 𝑧) ∈ ℝ+)
76		rpdivcl 12059	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℝ+ ∧ (𝑧 · 𝑧) ∈ ℝ+) → (𝑃 / (𝑧 · 𝑧)) ∈ ℝ+)
77	74, 75, 76	syl2an 583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℕ ∧ (𝑧 · 𝑧) ∈ ℕ) → (𝑃 / (𝑧 · 𝑧)) ∈ ℝ+)
78	50, 73, 77	syl2anc 573	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / (𝑧 · 𝑧)) ∈ ℝ+)
79	57, 72, 78	lemul1d 12118	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) ↔ (𝑃 · (𝑃 / (𝑧 · 𝑧))) ≤ ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧)))))
80	57	recnd 10270	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℂ)
81	80, 48, 80, 48, 40, 40	divmuldivd 11044	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) = ((𝑃 · 𝑃) / (𝑧 · 𝑧)))
82	73	nncnd 11238	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℂ)
83	73	nnne0d 11267	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ≠ 0)
84	80, 80, 82, 83	divassd 11038	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 · 𝑃) / (𝑧 · 𝑧)) = (𝑃 · (𝑃 / (𝑧 · 𝑧))))
85	81, 84	eqtrd 2805	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) = (𝑃 · (𝑃 / (𝑧 · 𝑧))))
86	80, 82, 83	divcan2d 11005	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧))) = 𝑃)
87	86	eqcomd 2777	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 = ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧))))
88	85, 87	breq12d 4799	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ↔ (𝑃 · (𝑃 / (𝑧 · 𝑧))) ≤ ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧)))))
89	79, 88	bitr4d 271	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) ↔ ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃))
90	89	biimpd 219	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃))
91	80, 48, 40	divcan2d 11005	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · (𝑃 / 𝑧)) = 𝑃)
92		dvds0lem 15201	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ ℤ ∧ (𝑃 / 𝑧) ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ (𝑧 · (𝑃 / 𝑧)) = 𝑃) → (𝑃 / 𝑧) ∥ 𝑃)
93	37, 45, 42, 91, 92	syl31anc 1479	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∥ 𝑃)
94	90, 93	jctird 516	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃)))
95		oveq12 6802	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝑃 / 𝑧) ∧ 𝑥 = (𝑃 / 𝑧)) → (𝑥 · 𝑥) = ((𝑃 / 𝑧) · (𝑃 / 𝑧)))
96	95	anidms 556	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑃 / 𝑧) → (𝑥 · 𝑥) = ((𝑃 / 𝑧) · (𝑃 / 𝑧)))
97	96	breq1d 4796	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑃 / 𝑧) → ((𝑥 · 𝑥) ≤ 𝑃 ↔ ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃))
98		breq1 4789	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑃 / 𝑧) → (𝑥 ∥ 𝑃 ↔ (𝑃 / 𝑧) ∥ 𝑃))
99	97, 98	anbi12d 616	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑃 / 𝑧) → (((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃) ↔ (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃)))
100	99	rspcev 3460	. . . . . . . . . . . 12 ⊢ (((𝑃 / 𝑧) ∈ (ℤ≥‘2) ∧ (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃)) → ∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃))
101	71, 94, 100	syl6an 663	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → ∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)))
102	72, 57	letrid 10391	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) ≤ 𝑃 ∨ 𝑃 ≤ (𝑧 · 𝑧)))
103	34, 101, 102	mpjaod 849	. . . . . . . . . 10 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) ∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃))
104	103	ex 397	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) → ((𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃) → ∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)))
105	25, 104	syl5bir 233	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) → (¬ (𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)))
106	105	rexlimdva 3179	. . . . . . 7 ⊢ (𝑃 ∈ (ℤ≥‘2) → (∃𝑧 ∈ (ℤ≥‘2) ¬ (𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)))
107		prmz 15596	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℙ → 𝑧 ∈ ℤ)
108	107	ad2antrl 707	. . . . . . . . . . . . . 14 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑧 ∈ ℤ)
109	108	zred 11684	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑧 ∈ ℝ)
110	109, 109	remulcld 10272	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑧 · 𝑧) ∈ ℝ)
111		eluzelz 11898	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ℤ≥‘2) → 𝑥 ∈ ℤ)
112	111	ad3antlr 710	. . . . . . . . . . . . . 14 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑥 ∈ ℤ)
113	112	zred 11684	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑥 ∈ ℝ)
114	113, 113	remulcld 10272	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑥 · 𝑥) ∈ ℝ)
115	41	ad3antrrr 709	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑃 ∈ ℤ)
116	115	zred 11684	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑃 ∈ ℝ)
117		eluz2nn 11928	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ℤ≥‘2) → 𝑥 ∈ ℕ)
118	117	ad3antlr 710	. . . . . . . . . . . . . 14 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑥 ∈ ℕ)
119		simprr 756	. . . . . . . . . . . . . 14 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑧 ∥ 𝑥)
120		dvdsle 15241	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑧 ∥ 𝑥 → 𝑧 ≤ 𝑥))
121	120	imp 393	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℕ) ∧ 𝑧 ∥ 𝑥) → 𝑧 ≤ 𝑥)
122	108, 118, 119, 121	syl21anc 1475	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑧 ≤ 𝑥)
123		eluzge2nn0 11929	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (ℤ≥‘2) → 𝑧 ∈ ℕ0)
124	123	nn0ge0d 11556	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (ℤ≥‘2) → 0 ≤ 𝑧)
125	2, 124	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℙ → 0 ≤ 𝑧)
126	125	ad2antrl 707	. . . . . . . . . . . . . 14 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 0 ≤ 𝑧)
127		nnnn0 11501	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℕ0)
128	127	nn0ge0d 11556	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℕ → 0 ≤ 𝑥)
129	118, 128	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 0 ≤ 𝑥)
130		le2msq 11125	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ ℝ ∧ 0 ≤ 𝑧) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (𝑧 ≤ 𝑥 ↔ (𝑧 · 𝑧) ≤ (𝑥 · 𝑥)))
131	109, 126, 113, 129, 130	syl22anc 1477	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑧 ≤ 𝑥 ↔ (𝑧 · 𝑧) ≤ (𝑥 · 𝑥)))
132	122, 131	mpbid 222	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑧 · 𝑧) ≤ (𝑥 · 𝑥))
133		simplrl 762	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑥 · 𝑥) ≤ 𝑃)
134	110, 114, 116, 132, 133	letrd 10396	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑧 · 𝑧) ≤ 𝑃)
135		simplrr 763	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑥 ∥ 𝑃)
136		dvdstr 15227	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑧 ∥ 𝑥 ∧ 𝑥 ∥ 𝑃) → 𝑧 ∥ 𝑃))
137	108, 112, 115, 136	syl3anc 1476	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → ((𝑧 ∥ 𝑥 ∧ 𝑥 ∥ 𝑃) → 𝑧 ∥ 𝑃))
138	119, 135, 137	mp2and 679	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑧 ∥ 𝑃)
139	134, 138	jc 160	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))
140		exprmfct 15623	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ≥‘2) → ∃𝑧 ∈ ℙ 𝑧 ∥ 𝑥)
141	140	ad2antlr 706	. . . . . . . . . 10 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) → ∃𝑧 ∈ ℙ 𝑧 ∥ 𝑥)
142	139, 141	reximddv 3166	. . . . . . . . 9 ⊢ (((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))
143	142	ex 397	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2)) → (((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
144	143	rexlimdva 3179	. . . . . . 7 ⊢ (𝑃 ∈ (ℤ≥‘2) → (∃𝑥 ∈ (ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
145	106, 144	syld 47	. . . . . 6 ⊢ (𝑃 ∈ (ℤ≥‘2) → (∃𝑧 ∈ (ℤ≥‘2) ¬ (𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
146		rexnal 3143	. . . . . 6 ⊢ (∃𝑧 ∈ (ℤ≥‘2) ¬ (𝑧 ∥ 𝑃 → 𝑧 = 𝑃) ↔ ¬ ∀𝑧 ∈ (ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃))
147		rexnal 3143	. . . . . 6 ⊢ (∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃) ↔ ¬ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))
148	145, 146, 147	3imtr3g 284	. . . . 5 ⊢ (𝑃 ∈ (ℤ≥‘2) → (¬ ∀𝑧 ∈ (ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ¬ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
149	24, 148	impcon4bid 217	. . . 4 ⊢ (𝑃 ∈ (ℤ≥‘2) → (∀𝑧 ∈ (ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
150		prmnn 15595	. . . . . . . . 9 ⊢ (𝑧 ∈ ℙ → 𝑧 ∈ ℕ)
151	150	nncnd 11238	. . . . . . . 8 ⊢ (𝑧 ∈ ℙ → 𝑧 ∈ ℂ)
152	151	sqvald 13212	. . . . . . 7 ⊢ (𝑧 ∈ ℙ → (𝑧↑2) = (𝑧 · 𝑧))
153	152	breq1d 4796	. . . . . 6 ⊢ (𝑧 ∈ ℙ → ((𝑧↑2) ≤ 𝑃 ↔ (𝑧 · 𝑧) ≤ 𝑃))
154	153	imbi1d 330	. . . . 5 ⊢ (𝑧 ∈ ℙ → (((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃) ↔ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
155	154	ralbiia 3128	. . . 4 ⊢ (∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))
156	149, 155	syl6bbr 278	. . 3 ⊢ (𝑃 ∈ (ℤ≥‘2) → (∀𝑧 ∈ (ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
157	156	pm5.32i 564	. 2 ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ (ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃)) ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
158	1, 157	bitri 264	1 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  ∃wrex 3062   class class class wbr 4786  ‘cfv 6031  (class class class)co 6793  ℝcr 10137  0cc0 10138  1c1 10139   · cmul 10143   < clt 10276   ≤ cle 10277   / cdiv 10886  ℕcn 11222  2c2 11272  ℤcz 11579  ℤ_≥cuz 11888  ℝ⁺crp 12035  ↑cexp 13067   ∥ cdvds 15189  ℙcprime 15592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-rp 12036  df-fz 12534  df-seq 13009  df-exp 13068  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-dvds 15190  df-prm 15593

This theorem is referenced by:  isprm7  15627  pockthg  15817  prmlem1a  16020