MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isprm5 Structured version   Visualization version   GIF version

Theorem isprm5 15700
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.
StepHypRef Expression
1 isprm4 15679 . 2 (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ‘2) ∧ ∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃)))
2 prmuz2 15690 . . . . . . . 8 (𝑧 ∈ ℙ → 𝑧 ∈ (ℤ‘2))
32a1i 11 . . . . . . 7 (𝑃 ∈ (ℤ‘2) → (𝑧 ∈ ℙ → 𝑧 ∈ (ℤ‘2)))
4 eluz2b2 11962 . . . . . . . . . . . . 13 (𝑃 ∈ (ℤ‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃))
54simprbi 490 . . . . . . . . . . . 12 (𝑃 ∈ (ℤ‘2) → 1 < 𝑃)
6 eluzelre 11897 . . . . . . . . . . . . 13 (𝑃 ∈ (ℤ‘2) → 𝑃 ∈ ℝ)
7 eluz2nn 11926 . . . . . . . . . . . . . 14 (𝑃 ∈ (ℤ‘2) → 𝑃 ∈ ℕ)
87nngt0d 11321 . . . . . . . . . . . . 13 (𝑃 ∈ (ℤ‘2) → 0 < 𝑃)
9 ltmulgt11 11137 . . . . . . . . . . . . 13 ((𝑃 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 0 < 𝑃) → (1 < 𝑃𝑃 < (𝑃 · 𝑃)))
106, 6, 8, 9syl3anc 1490 . . . . . . . . . . . 12 (𝑃 ∈ (ℤ‘2) → (1 < 𝑃𝑃 < (𝑃 · 𝑃)))
115, 10mpbid 223 . . . . . . . . . . 11 (𝑃 ∈ (ℤ‘2) → 𝑃 < (𝑃 · 𝑃))
126, 6remulcld 10324 . . . . . . . . . . . 12 (𝑃 ∈ (ℤ‘2) → (𝑃 · 𝑃) ∈ ℝ)
136, 12ltnled 10438 . . . . . . . . . . 11 (𝑃 ∈ (ℤ‘2) → (𝑃 < (𝑃 · 𝑃) ↔ ¬ (𝑃 · 𝑃) ≤ 𝑃))
1411, 13mpbid 223 . . . . . . . . . 10 (𝑃 ∈ (ℤ‘2) → ¬ (𝑃 · 𝑃) ≤ 𝑃)
15 oveq12 6851 . . . . . . . . . . . . 13 ((𝑧 = 𝑃𝑧 = 𝑃) → (𝑧 · 𝑧) = (𝑃 · 𝑃))
1615anidms 562 . . . . . . . . . . . 12 (𝑧 = 𝑃 → (𝑧 · 𝑧) = (𝑃 · 𝑃))
1716breq1d 4819 . . . . . . . . . . 11 (𝑧 = 𝑃 → ((𝑧 · 𝑧) ≤ 𝑃 ↔ (𝑃 · 𝑃) ≤ 𝑃))
1817notbid 309 . . . . . . . . . 10 (𝑧 = 𝑃 → (¬ (𝑧 · 𝑧) ≤ 𝑃 ↔ ¬ (𝑃 · 𝑃) ≤ 𝑃))
1914, 18syl5ibrcom 238 . . . . . . . . 9 (𝑃 ∈ (ℤ‘2) → (𝑧 = 𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃))
2019imim2d 57 . . . . . . . 8 (𝑃 ∈ (ℤ‘2) → ((𝑧𝑃𝑧 = 𝑃) → (𝑧𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃)))
21 con2 132 . . . . . . . 8 ((𝑧𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))
2220, 21syl6 35 . . . . . . 7 (𝑃 ∈ (ℤ‘2) → ((𝑧𝑃𝑧 = 𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
233, 22imim12d 81 . . . . . 6 (𝑃 ∈ (ℤ‘2) → ((𝑧 ∈ (ℤ‘2) → (𝑧𝑃𝑧 = 𝑃)) → (𝑧 ∈ ℙ → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))))
2423ralimdv2 3108 . . . . 5 (𝑃 ∈ (ℤ‘2) → (∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃) → ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
25 annim 392 . . . . . . . . 9 ((𝑧𝑃 ∧ ¬ 𝑧 = 𝑃) ↔ ¬ (𝑧𝑃𝑧 = 𝑃))
26 oveq12 6851 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑧𝑥 = 𝑧) → (𝑥 · 𝑥) = (𝑧 · 𝑧))
2726anidms 562 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (𝑥 · 𝑥) = (𝑧 · 𝑧))
2827breq1d 4819 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → ((𝑥 · 𝑥) ≤ 𝑃 ↔ (𝑧 · 𝑧) ≤ 𝑃))
29 breq1 4812 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (𝑥𝑃𝑧𝑃))
3028, 29anbi12d 624 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃) ↔ ((𝑧 · 𝑧) ≤ 𝑃𝑧𝑃)))
3130rspcev 3461 . . . . . . . . . . . . . 14 ((𝑧 ∈ (ℤ‘2) ∧ ((𝑧 · 𝑧) ≤ 𝑃𝑧𝑃)) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃))
3231ancom2s 640 . . . . . . . . . . . . 13 ((𝑧 ∈ (ℤ‘2) ∧ (𝑧𝑃 ∧ (𝑧 · 𝑧) ≤ 𝑃)) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃))
3332expr 448 . . . . . . . . . . . 12 ((𝑧 ∈ (ℤ‘2) ∧ 𝑧𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
3433ad2ant2lr 754 . . . . . . . . . . 11 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) ≤ 𝑃 → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
35 simprl 787 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧𝑃)
36 eluzelz 11896 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (ℤ‘2) → 𝑧 ∈ ℤ)
3736ad2antlr 718 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℤ)
38 eluz2nn 11926 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (ℤ‘2) → 𝑧 ∈ ℕ)
3938ad2antlr 718 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℕ)
4039nnne0d 11322 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ≠ 0)
41 eluzelz 11896 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (ℤ‘2) → 𝑃 ∈ ℤ)
4241ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℤ)
43 dvdsval2 15270 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ∧ 𝑃 ∈ ℤ) → (𝑧𝑃 ↔ (𝑃 / 𝑧) ∈ ℤ))
4437, 40, 42, 43syl3anc 1490 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧𝑃 ↔ (𝑃 / 𝑧) ∈ ℤ))
4535, 44mpbid 223 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∈ ℤ)
46 eluzelre 11897 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (ℤ‘2) → 𝑧 ∈ ℝ)
4746ad2antlr 718 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℝ)
4847recnd 10322 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℂ)
4948mulid2d 10312 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (1 · 𝑧) = 𝑧)
507ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℕ)
51 dvdsle 15319 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑧𝑃𝑧𝑃))
5251imp 395 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧ 𝑧𝑃) → 𝑧𝑃)
5337, 50, 35, 52syl21anc 866 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧𝑃)
54 simprr 789 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ¬ 𝑧 = 𝑃)
5554neqned 2944 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧𝑃)
5655necomd 2992 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃𝑧)
576ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℝ)
5847, 57ltlend 10436 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 < 𝑃 ↔ (𝑧𝑃𝑃𝑧)))
5953, 56, 58mpbir2and 704 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 < 𝑃)
6049, 59eqbrtrd 4831 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (1 · 𝑧) < 𝑃)
61 1red 10294 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 1 ∈ ℝ)
6242zred 11729 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℝ)
63 nnre 11282 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
64 nngt0 11306 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℕ → 0 < 𝑧)
6563, 64jca 507 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ → (𝑧 ∈ ℝ ∧ 0 < 𝑧))
6639, 65syl 17 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 ∈ ℝ ∧ 0 < 𝑧))
67 ltmuldiv 11150 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑧 ∈ ℝ ∧ 0 < 𝑧)) → ((1 · 𝑧) < 𝑃 ↔ 1 < (𝑃 / 𝑧)))
6861, 62, 66, 67syl3anc 1490 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((1 · 𝑧) < 𝑃 ↔ 1 < (𝑃 / 𝑧)))
6960, 68mpbid 223 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 1 < (𝑃 / 𝑧))
70 eluz2b1 11960 . . . . . . . . . . . . 13 ((𝑃 / 𝑧) ∈ (ℤ‘2) ↔ ((𝑃 / 𝑧) ∈ ℤ ∧ 1 < (𝑃 / 𝑧)))
7145, 69, 70sylanbrc 578 . . . . . . . . . . . 12 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∈ (ℤ‘2))
7247, 47remulcld 10324 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℝ)
7339, 39nnmulcld 11325 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℕ)
74 nnrp 12041 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ ℕ → 𝑃 ∈ ℝ+)
75 nnrp 12041 . . . . . . . . . . . . . . . . . 18 ((𝑧 · 𝑧) ∈ ℕ → (𝑧 · 𝑧) ∈ ℝ+)
76 rpdivcl 12054 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℝ+ ∧ (𝑧 · 𝑧) ∈ ℝ+) → (𝑃 / (𝑧 · 𝑧)) ∈ ℝ+)
7774, 75, 76syl2an 589 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℕ ∧ (𝑧 · 𝑧) ∈ ℕ) → (𝑃 / (𝑧 · 𝑧)) ∈ ℝ+)
7850, 73, 77syl2anc 579 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / (𝑧 · 𝑧)) ∈ ℝ+)
7957, 72, 78lemul1d 12113 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) ↔ (𝑃 · (𝑃 / (𝑧 · 𝑧))) ≤ ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧)))))
8057recnd 10322 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℂ)
8180, 48, 80, 48, 40, 40divmuldivd 11096 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) = ((𝑃 · 𝑃) / (𝑧 · 𝑧)))
8273nncnd 11292 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℂ)
8373nnne0d 11322 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ≠ 0)
8480, 80, 82, 83divassd 11090 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 · 𝑃) / (𝑧 · 𝑧)) = (𝑃 · (𝑃 / (𝑧 · 𝑧))))
8581, 84eqtrd 2799 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) = (𝑃 · (𝑃 / (𝑧 · 𝑧))))
8680, 82, 83divcan2d 11057 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧))) = 𝑃)
8786eqcomd 2771 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 = ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧))))
8885, 87breq12d 4822 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ↔ (𝑃 · (𝑃 / (𝑧 · 𝑧))) ≤ ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧)))))
8979, 88bitr4d 273 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) ↔ ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃))
9089biimpd 220 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃))
9180, 48, 40divcan2d 11057 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · (𝑃 / 𝑧)) = 𝑃)
92 dvds0lem 15279 . . . . . . . . . . . . . 14 (((𝑧 ∈ ℤ ∧ (𝑃 / 𝑧) ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ (𝑧 · (𝑃 / 𝑧)) = 𝑃) → (𝑃 / 𝑧) ∥ 𝑃)
9337, 45, 42, 91, 92syl31anc 1492 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∥ 𝑃)
9490, 93jctird 522 . . . . . . . . . . . 12 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃)))
95 oveq12 6851 . . . . . . . . . . . . . . . 16 ((𝑥 = (𝑃 / 𝑧) ∧ 𝑥 = (𝑃 / 𝑧)) → (𝑥 · 𝑥) = ((𝑃 / 𝑧) · (𝑃 / 𝑧)))
9695anidms 562 . . . . . . . . . . . . . . 15 (𝑥 = (𝑃 / 𝑧) → (𝑥 · 𝑥) = ((𝑃 / 𝑧) · (𝑃 / 𝑧)))
9796breq1d 4819 . . . . . . . . . . . . . 14 (𝑥 = (𝑃 / 𝑧) → ((𝑥 · 𝑥) ≤ 𝑃 ↔ ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃))
98 breq1 4812 . . . . . . . . . . . . . 14 (𝑥 = (𝑃 / 𝑧) → (𝑥𝑃 ↔ (𝑃 / 𝑧) ∥ 𝑃))
9997, 98anbi12d 624 . . . . . . . . . . . . 13 (𝑥 = (𝑃 / 𝑧) → (((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃) ↔ (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃)))
10099rspcev 3461 . . . . . . . . . . . 12 (((𝑃 / 𝑧) ∈ (ℤ‘2) ∧ (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃)) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃))
10171, 94, 100syl6an 674 . . . . . . . . . . 11 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
10272, 57letrid 10443 . . . . . . . . . . 11 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) ≤ 𝑃𝑃 ≤ (𝑧 · 𝑧)))
10334, 101, 102mpjaod 886 . . . . . . . . . 10 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃))
104103ex 401 . . . . . . . . 9 ((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) → ((𝑧𝑃 ∧ ¬ 𝑧 = 𝑃) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
10525, 104syl5bir 234 . . . . . . . 8 ((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) → (¬ (𝑧𝑃𝑧 = 𝑃) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
106105rexlimdva 3178 . . . . . . 7 (𝑃 ∈ (ℤ‘2) → (∃𝑧 ∈ (ℤ‘2) ¬ (𝑧𝑃𝑧 = 𝑃) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
107 prmz 15671 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℙ → 𝑧 ∈ ℤ)
108107ad2antrl 719 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑧 ∈ ℤ)
109108zred 11729 . . . . . . . . . . . . 13 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑧 ∈ ℝ)
110109, 109remulcld 10324 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑧 · 𝑧) ∈ ℝ)
111 eluzelz 11896 . . . . . . . . . . . . . . 15 (𝑥 ∈ (ℤ‘2) → 𝑥 ∈ ℤ)
112111ad3antlr 722 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑥 ∈ ℤ)
113112zred 11729 . . . . . . . . . . . . 13 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑥 ∈ ℝ)
114113, 113remulcld 10324 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑥 · 𝑥) ∈ ℝ)
11541ad3antrrr 721 . . . . . . . . . . . . 13 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑃 ∈ ℤ)
116115zred 11729 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑃 ∈ ℝ)
117 eluz2nn 11926 . . . . . . . . . . . . . . 15 (𝑥 ∈ (ℤ‘2) → 𝑥 ∈ ℕ)
118117ad3antlr 722 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑥 ∈ ℕ)
119 simprr 789 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑧𝑥)
120 dvdsle 15319 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑧𝑥𝑧𝑥))
121120imp 395 . . . . . . . . . . . . . 14 (((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℕ) ∧ 𝑧𝑥) → 𝑧𝑥)
122108, 118, 119, 121syl21anc 866 . . . . . . . . . . . . 13 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑧𝑥)
123 eluzge2nn0 11927 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (ℤ‘2) → 𝑧 ∈ ℕ0)
124123nn0ge0d 11601 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (ℤ‘2) → 0 ≤ 𝑧)
1252, 124syl 17 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℙ → 0 ≤ 𝑧)
126125ad2antrl 719 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 0 ≤ 𝑧)
127 nnnn0 11546 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ0)
128127nn0ge0d 11601 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℕ → 0 ≤ 𝑥)
129118, 128syl 17 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 0 ≤ 𝑥)
130 le2msq 11177 . . . . . . . . . . . . . 14 (((𝑧 ∈ ℝ ∧ 0 ≤ 𝑧) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (𝑧𝑥 ↔ (𝑧 · 𝑧) ≤ (𝑥 · 𝑥)))
131109, 126, 113, 129, 130syl22anc 867 . . . . . . . . . . . . 13 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑧𝑥 ↔ (𝑧 · 𝑧) ≤ (𝑥 · 𝑥)))
132122, 131mpbid 223 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑧 · 𝑧) ≤ (𝑥 · 𝑥))
133 simplrl 795 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑥 · 𝑥) ≤ 𝑃)
134110, 114, 116, 132, 133letrd 10448 . . . . . . . . . . 11 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑧 · 𝑧) ≤ 𝑃)
135 simplrr 796 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑥𝑃)
136 dvdstr 15305 . . . . . . . . . . . . 13 ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑧𝑥𝑥𝑃) → 𝑧𝑃))
137108, 112, 115, 136syl3anc 1490 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → ((𝑧𝑥𝑥𝑃) → 𝑧𝑃))
138119, 135, 137mp2and 690 . . . . . . . . . . 11 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑧𝑃)
139134, 138jc 160 . . . . . . . . . 10 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))
140 exprmfct 15697 . . . . . . . . . . 11 (𝑥 ∈ (ℤ‘2) → ∃𝑧 ∈ ℙ 𝑧𝑥)
141140ad2antlr 718 . . . . . . . . . 10 (((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) → ∃𝑧 ∈ ℙ 𝑧𝑥)
142139, 141reximddv 3164 . . . . . . . . 9 (((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))
143142ex 401 . . . . . . . 8 ((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) → (((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
144143rexlimdva 3178 . . . . . . 7 (𝑃 ∈ (ℤ‘2) → (∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
145106, 144syld 47 . . . . . 6 (𝑃 ∈ (ℤ‘2) → (∃𝑧 ∈ (ℤ‘2) ¬ (𝑧𝑃𝑧 = 𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
146 rexnal 3141 . . . . . 6 (∃𝑧 ∈ (ℤ‘2) ¬ (𝑧𝑃𝑧 = 𝑃) ↔ ¬ ∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃))
147 rexnal 3141 . . . . . 6 (∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃) ↔ ¬ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))
148145, 146, 1473imtr3g 286 . . . . 5 (𝑃 ∈ (ℤ‘2) → (¬ ∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃) → ¬ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
14924, 148impcon4bid 218 . . . 4 (𝑃 ∈ (ℤ‘2) → (∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
150 prmnn 15670 . . . . . . . . 9 (𝑧 ∈ ℙ → 𝑧 ∈ ℕ)
151150nncnd 11292 . . . . . . . 8 (𝑧 ∈ ℙ → 𝑧 ∈ ℂ)
152151sqvald 13212 . . . . . . 7 (𝑧 ∈ ℙ → (𝑧↑2) = (𝑧 · 𝑧))
153152breq1d 4819 . . . . . 6 (𝑧 ∈ ℙ → ((𝑧↑2) ≤ 𝑃 ↔ (𝑧 · 𝑧) ≤ 𝑃))
154153imbi1d 332 . . . . 5 (𝑧 ∈ ℙ → (((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃) ↔ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
155154ralbiia 3126 . . . 4 (∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))
156149, 155syl6bbr 280 . . 3 (𝑃 ∈ (ℤ‘2) → (∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃)))
157156pm5.32i 570 . 2 ((𝑃 ∈ (ℤ‘2) ∧ ∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃)) ↔ (𝑃 ∈ (ℤ‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃)))
1581, 157bitri 266 1 (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056   class class class wbr 4809  cfv 6068  (class class class)co 6842  cr 10188  0cc0 10189  1c1 10190   · cmul 10194   < clt 10328  cle 10329   / cdiv 10938  cn 11274  2c2 11327  cz 11624  cuz 11886  +crp 12028  cexp 13067  cdvds 15267  cprime 15667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-fz 12534  df-seq 13009  df-exp 13068  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-dvds 15268  df-prm 15668
This theorem is referenced by:  isprm7  15701  pockthg  15891  prmlem1a  16089
  Copyright terms: Public domain W3C validator