Theorem isprm5

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

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

Proof

Step	Hyp	Ref	Expression
1		isprm4	⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) ) )
2		prmuz2	⊢ ( 𝑧 ∈ ℙ → 𝑧 ∈ ( ℤ≥ ‘ 2 ) )
3	2	a1i	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑧 ∈ ℙ → 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) )
4		eluz2gt1	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑃 )
5		eluzelre	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℝ )
6		eluz2nn	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℕ )
7	6	nngt0d	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 0 < 𝑃 )
8		ltmulgt11	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) → ( 1 < 𝑃 ↔ 𝑃 < ( 𝑃 · 𝑃 ) ) )
9	5 5 7 8	syl3anc	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 1 < 𝑃 ↔ 𝑃 < ( 𝑃 · 𝑃 ) ) )
10	4 9	mpbid	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 < ( 𝑃 · 𝑃 ) )
11	5 5	remulcld	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 · 𝑃 ) ∈ ℝ )
12	5 11	ltnled	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 < ( 𝑃 · 𝑃 ) ↔ ¬ ( 𝑃 · 𝑃 ) ≤ 𝑃 ) )
13	10 12	mpbid	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝑃 · 𝑃 ) ≤ 𝑃 )
14		oveq12	⊢ ( ( 𝑧 = 𝑃 ∧ 𝑧 = 𝑃 ) → ( 𝑧 · 𝑧 ) = ( 𝑃 · 𝑃 ) )
15	14	anidms	⊢ ( 𝑧 = 𝑃 → ( 𝑧 · 𝑧 ) = ( 𝑃 · 𝑃 ) )
16	15	breq1d	⊢ ( 𝑧 = 𝑃 → ( ( 𝑧 · 𝑧 ) ≤ 𝑃 ↔ ( 𝑃 · 𝑃 ) ≤ 𝑃 ) )
17	16	notbid	⊢ ( 𝑧 = 𝑃 → ( ¬ ( 𝑧 · 𝑧 ) ≤ 𝑃 ↔ ¬ ( 𝑃 · 𝑃 ) ≤ 𝑃 ) )
18	13 17	syl5ibrcom	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑧 = 𝑃 → ¬ ( 𝑧 · 𝑧 ) ≤ 𝑃 ) )
19	18	imim2d	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) → ( 𝑧 ∥ 𝑃 → ¬ ( 𝑧 · 𝑧 ) ≤ 𝑃 ) ) )
20		con2	⊢ ( ( 𝑧 ∥ 𝑃 → ¬ ( 𝑧 · 𝑧 ) ≤ 𝑃 ) → ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) )
21	19 20	syl6	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) → ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
22	3 21	imim12d	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) ) → ( 𝑧 ∈ ℙ → ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) ) )
23	22	ralimdv2	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) → ∀ 𝑧 ∈ ℙ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
24		annim	⊢ ( ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ↔ ¬ ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) )
25		oveq12	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑧 ) → ( 𝑥 · 𝑥 ) = ( 𝑧 · 𝑧 ) )
26	25	anidms	⊢ ( 𝑥 = 𝑧 → ( 𝑥 · 𝑥 ) = ( 𝑧 · 𝑧 ) )
27	26	breq1d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ↔ ( 𝑧 · 𝑧 ) ≤ 𝑃 ) )
28		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∥ 𝑃 ↔ 𝑧 ∥ 𝑃 ) )
29	27 28	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ↔ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 ∧ 𝑧 ∥ 𝑃 ) ) )
30	29	rspcev	⊢ ( ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 ∧ 𝑧 ∥ 𝑃 ) ) → ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) )
31	30	ancom2s	⊢ ( ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑧 ∥ 𝑃 ∧ ( 𝑧 · 𝑧 ) ≤ 𝑃 ) ) → ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) )
32	31	expr	⊢ ( ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ 𝑃 ) → ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) )
33	32	ad2ant2lr	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) )
34		simprl	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑧 ∥ 𝑃 )
35		eluzelz	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 𝑧 ∈ ℤ )
36	35	ad2antlr	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑧 ∈ ℤ )
37		eluz2nn	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 𝑧 ∈ ℕ )
38	37	ad2antlr	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑧 ∈ ℕ )
39	38	nnne0d	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑧 ≠ 0 )
40		eluzelz	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℤ )
41	40	ad2antrr	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑃 ∈ ℤ )
42		dvdsval2	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ∧ 𝑃 ∈ ℤ ) → ( 𝑧 ∥ 𝑃 ↔ ( 𝑃 / 𝑧 ) ∈ ℤ ) )
43	36 39 41 42	syl3anc	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑧 ∥ 𝑃 ↔ ( 𝑃 / 𝑧 ) ∈ ℤ ) )
44	34 43	mpbid	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑃 / 𝑧 ) ∈ ℤ )
45		eluzelre	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 𝑧 ∈ ℝ )
46	45	ad2antlr	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑧 ∈ ℝ )
47	46	recnd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑧 ∈ ℂ )
48	47	mullidd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 1 · 𝑧 ) = 𝑧 )
49	5	ad2antrr	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑃 ∈ ℝ )
50	6	ad2antrr	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑃 ∈ ℕ )
51		dvdsle	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( 𝑧 ∥ 𝑃 → 𝑧 ≤ 𝑃 ) )
52	51	imp	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ ) ∧ 𝑧 ∥ 𝑃 ) → 𝑧 ≤ 𝑃 )
53	36 50 34 52	syl21anc	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑧 ≤ 𝑃 )
54		simprr	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ¬ 𝑧 = 𝑃 )
55	54	neqned	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑧 ≠ 𝑃 )
56	55	necomd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑃 ≠ 𝑧 )
57	46 49 53 56	leneltd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑧 < 𝑃 )
58	48 57	eqbrtrd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 1 · 𝑧 ) < 𝑃 )
59		1red	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 1 ∈ ℝ )
60	41	zred	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑃 ∈ ℝ )
61		nnre	⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℝ )
62		nngt0	⊢ ( 𝑧 ∈ ℕ → 0 < 𝑧 )
63	61 62	jca	⊢ ( 𝑧 ∈ ℕ → ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) )
64	38 63	syl	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) )
65		ltmuldiv	⊢ ( ( 1 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) ) → ( ( 1 · 𝑧 ) < 𝑃 ↔ 1 < ( 𝑃 / 𝑧 ) ) )
66	59 60 64 65	syl3anc	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( ( 1 · 𝑧 ) < 𝑃 ↔ 1 < ( 𝑃 / 𝑧 ) ) )
67	58 66	mpbid	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 1 < ( 𝑃 / 𝑧 ) )
68		eluz2b1	⊢ ( ( 𝑃 / 𝑧 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( 𝑃 / 𝑧 ) ∈ ℤ ∧ 1 < ( 𝑃 / 𝑧 ) ) )
69	44 67 68	sylanbrc	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑃 / 𝑧 ) ∈ ( ℤ≥ ‘ 2 ) )
70	46 46	remulcld	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑧 · 𝑧 ) ∈ ℝ )
71	38 38	nnmulcld	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑧 · 𝑧 ) ∈ ℕ )
72		nnrp	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ+ )
73		nnrp	⊢ ( ( 𝑧 · 𝑧 ) ∈ ℕ → ( 𝑧 · 𝑧 ) ∈ ℝ+ )
74		rpdivcl	⊢ ( ( 𝑃 ∈ ℝ+ ∧ ( 𝑧 · 𝑧 ) ∈ ℝ+ ) → ( 𝑃 / ( 𝑧 · 𝑧 ) ) ∈ ℝ+ )
75	72 73 74	syl2an	⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑧 · 𝑧 ) ∈ ℕ ) → ( 𝑃 / ( 𝑧 · 𝑧 ) ) ∈ ℝ+ )
76	50 71 75	syl2anc	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑃 / ( 𝑧 · 𝑧 ) ) ∈ ℝ+ )
77	49 70 76	lemul1d	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑃 ≤ ( 𝑧 · 𝑧 ) ↔ ( 𝑃 · ( 𝑃 / ( 𝑧 · 𝑧 ) ) ) ≤ ( ( 𝑧 · 𝑧 ) · ( 𝑃 / ( 𝑧 · 𝑧 ) ) ) ) )
78	49	recnd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑃 ∈ ℂ )
79	78 47 78 47 39 39	divmuldivd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) = ( ( 𝑃 · 𝑃 ) / ( 𝑧 · 𝑧 ) ) )
80	71	nncnd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑧 · 𝑧 ) ∈ ℂ )
81	71	nnne0d	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑧 · 𝑧 ) ≠ 0 )
82	78 78 80 81	divassd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( ( 𝑃 · 𝑃 ) / ( 𝑧 · 𝑧 ) ) = ( 𝑃 · ( 𝑃 / ( 𝑧 · 𝑧 ) ) ) )
83	79 82	eqtrd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) = ( 𝑃 · ( 𝑃 / ( 𝑧 · 𝑧 ) ) ) )
84	78 80 81	divcan2d	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( ( 𝑧 · 𝑧 ) · ( 𝑃 / ( 𝑧 · 𝑧 ) ) ) = 𝑃 )
85	84	eqcomd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → 𝑃 = ( ( 𝑧 · 𝑧 ) · ( 𝑃 / ( 𝑧 · 𝑧 ) ) ) )
86	83 85	breq12d	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) ≤ 𝑃 ↔ ( 𝑃 · ( 𝑃 / ( 𝑧 · 𝑧 ) ) ) ≤ ( ( 𝑧 · 𝑧 ) · ( 𝑃 / ( 𝑧 · 𝑧 ) ) ) ) )
87	77 86	bitr4d	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑃 ≤ ( 𝑧 · 𝑧 ) ↔ ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) ≤ 𝑃 ) )
88	87	biimpd	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑃 ≤ ( 𝑧 · 𝑧 ) → ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) ≤ 𝑃 ) )
89	78 47 39	divcan2d	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑧 · ( 𝑃 / 𝑧 ) ) = 𝑃 )
90		dvds0lem	⊢ ( ( ( 𝑧 ∈ ℤ ∧ ( 𝑃 / 𝑧 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ ( 𝑧 · ( 𝑃 / 𝑧 ) ) = 𝑃 ) → ( 𝑃 / 𝑧 ) ∥ 𝑃 )
91	36 44 41 89 90	syl31anc	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑃 / 𝑧 ) ∥ 𝑃 )
92	88 91	jctird	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑃 ≤ ( 𝑧 · 𝑧 ) → ( ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) ≤ 𝑃 ∧ ( 𝑃 / 𝑧 ) ∥ 𝑃 ) ) )
93		oveq12	⊢ ( ( 𝑥 = ( 𝑃 / 𝑧 ) ∧ 𝑥 = ( 𝑃 / 𝑧 ) ) → ( 𝑥 · 𝑥 ) = ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) )
94	93	anidms	⊢ ( 𝑥 = ( 𝑃 / 𝑧 ) → ( 𝑥 · 𝑥 ) = ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) )
95	94	breq1d	⊢ ( 𝑥 = ( 𝑃 / 𝑧 ) → ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ↔ ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) ≤ 𝑃 ) )
96		breq1	⊢ ( 𝑥 = ( 𝑃 / 𝑧 ) → ( 𝑥 ∥ 𝑃 ↔ ( 𝑃 / 𝑧 ) ∥ 𝑃 ) )
97	95 96	anbi12d	⊢ ( 𝑥 = ( 𝑃 / 𝑧 ) → ( ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ↔ ( ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) ≤ 𝑃 ∧ ( 𝑃 / 𝑧 ) ∥ 𝑃 ) ) )
98	97	rspcev	⊢ ( ( ( 𝑃 / 𝑧 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 𝑃 / 𝑧 ) · ( 𝑃 / 𝑧 ) ) ≤ 𝑃 ∧ ( 𝑃 / 𝑧 ) ∥ 𝑃 ) ) → ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) )
99	69 92 98	syl6an	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( 𝑃 ≤ ( 𝑧 · 𝑧 ) → ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) )
100	70 49	letrid	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ( ( 𝑧 · 𝑧 ) ≤ 𝑃 ∨ 𝑃 ≤ ( 𝑧 · 𝑧 ) ) )
101	33 99 100	mpjaod	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) ) → ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) )
102	101	ex	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃 ) → ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) )
103	24 102	biimtrrid	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ¬ ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) → ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) )
104	103	rexlimdva	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ∃ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ¬ ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) → ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) )
105		prmz	⊢ ( 𝑧 ∈ ℙ → 𝑧 ∈ ℤ )
106	105	ad2antrl	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑧 ∈ ℤ )
107	106	zred	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑧 ∈ ℝ )
108	107 107	remulcld	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → ( 𝑧 · 𝑧 ) ∈ ℝ )
109		eluzelz	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → 𝑥 ∈ ℤ )
110	109	ad3antlr	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑥 ∈ ℤ )
111	110	zred	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑥 ∈ ℝ )
112	111 111	remulcld	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → ( 𝑥 · 𝑥 ) ∈ ℝ )
113	40	ad3antrrr	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑃 ∈ ℤ )
114	113	zred	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑃 ∈ ℝ )
115		eluz2nn	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → 𝑥 ∈ ℕ )
116	115	ad3antlr	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑥 ∈ ℕ )
117		simprr	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑧 ∥ 𝑥 )
118		dvdsle	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℕ ) → ( 𝑧 ∥ 𝑥 → 𝑧 ≤ 𝑥 ) )
119	118	imp	⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑥 ∈ ℕ ) ∧ 𝑧 ∥ 𝑥 ) → 𝑧 ≤ 𝑥 )
120	106 116 117 119	syl21anc	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑧 ≤ 𝑥 )
121		eluzge2nn0	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 𝑧 ∈ ℕ0 )
122	121	nn0ge0d	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 𝑧 )
123	2 122	syl	⊢ ( 𝑧 ∈ ℙ → 0 ≤ 𝑧 )
124	123	ad2antrl	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 0 ≤ 𝑧 )
125		nnnn0	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ0 )
126	125	nn0ge0d	⊢ ( 𝑥 ∈ ℕ → 0 ≤ 𝑥 )
127	116 126	syl	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 0 ≤ 𝑥 )
128		le2msq	⊢ ( ( ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝑧 · 𝑧 ) ≤ ( 𝑥 · 𝑥 ) ) )
129	107 124 111 127 128	syl22anc	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝑧 · 𝑧 ) ≤ ( 𝑥 · 𝑥 ) ) )
130	120 129	mpbid	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → ( 𝑧 · 𝑧 ) ≤ ( 𝑥 · 𝑥 ) )
131		simplrl	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → ( 𝑥 · 𝑥 ) ≤ 𝑃 )
132	108 112 114 130 131	letrd	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → ( 𝑧 · 𝑧 ) ≤ 𝑃 )
133		simplrr	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑥 ∥ 𝑃 )
134	106 110 113 117 133	dvdstrd	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → 𝑧 ∥ 𝑃 )
135	132 134	jc	⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) ∧ ( 𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥 ) ) → ¬ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) )
136		exprmfct	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑧 ∈ ℙ 𝑧 ∥ 𝑥 )
137	136	ad2antlr	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) → ∃ 𝑧 ∈ ℙ 𝑧 ∥ 𝑥 )
138	135 137	reximddv	⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) ) → ∃ 𝑧 ∈ ℙ ¬ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) )
139	138	ex	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) → ∃ 𝑧 ∈ ℙ ¬ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
140	139	rexlimdva	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ∃ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑥 · 𝑥 ) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃 ) → ∃ 𝑧 ∈ ℙ ¬ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
141	104 140	syld	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ∃ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ¬ ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) → ∃ 𝑧 ∈ ℙ ¬ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
142		rexnal	⊢ ( ∃ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ¬ ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) ↔ ¬ ∀ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) )
143		rexnal	⊢ ( ∃ 𝑧 ∈ ℙ ¬ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ↔ ¬ ∀ 𝑧 ∈ ℙ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) )
144	141 142 143	3imtr3g	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ¬ ∀ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) → ¬ ∀ 𝑧 ∈ ℙ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
145	23 144	impcon4bid	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) ↔ ∀ 𝑧 ∈ ℙ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
146		prmnn	⊢ ( 𝑧 ∈ ℙ → 𝑧 ∈ ℕ )
147	146	nncnd	⊢ ( 𝑧 ∈ ℙ → 𝑧 ∈ ℂ )
148	147	sqvald	⊢ ( 𝑧 ∈ ℙ → ( 𝑧 ↑ 2 ) = ( 𝑧 · 𝑧 ) )
149	148	breq1d	⊢ ( 𝑧 ∈ ℙ → ( ( 𝑧 ↑ 2 ) ≤ 𝑃 ↔ ( 𝑧 · 𝑧 ) ≤ 𝑃 ) )
150	149	imbi1d	⊢ ( 𝑧 ∈ ℙ → ( ( ( 𝑧 ↑ 2 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ↔ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
151	150	ralbiia	⊢ ( ∀ 𝑧 ∈ ℙ ( ( 𝑧 ↑ 2 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ↔ ∀ 𝑧 ∈ ℙ ( ( 𝑧 · 𝑧 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) )
152	145 151	bitr4di	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) ↔ ∀ 𝑧 ∈ ℙ ( ( 𝑧 ↑ 2 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
153	152	pm5.32i	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) ) ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℙ ( ( 𝑧 ↑ 2 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )
154	1 153	bitri	⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℙ ( ( 𝑧 ↑ 2 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )