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

Theorem isprm5 15350
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 15328 . 2 (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ‘2) ∧ ∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃)))
2 prmuz2 15339 . . . . . . . 8 (𝑧 ∈ ℙ → 𝑧 ∈ (ℤ‘2))
32a1i 11 . . . . . . 7 (𝑃 ∈ (ℤ‘2) → (𝑧 ∈ ℙ → 𝑧 ∈ (ℤ‘2)))
4 eluz2b2 11712 . . . . . . . . . . . . 13 (𝑃 ∈ (ℤ‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃))
54simprbi 480 . . . . . . . . . . . 12 (𝑃 ∈ (ℤ‘2) → 1 < 𝑃)
6 eluzelre 11649 . . . . . . . . . . . . 13 (𝑃 ∈ (ℤ‘2) → 𝑃 ∈ ℝ)
7 eluz2nn 11677 . . . . . . . . . . . . . 14 (𝑃 ∈ (ℤ‘2) → 𝑃 ∈ ℕ)
87nngt0d 11015 . . . . . . . . . . . . 13 (𝑃 ∈ (ℤ‘2) → 0 < 𝑃)
9 ltmulgt11 10834 . . . . . . . . . . . . 13 ((𝑃 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 0 < 𝑃) → (1 < 𝑃𝑃 < (𝑃 · 𝑃)))
106, 6, 8, 9syl3anc 1323 . . . . . . . . . . . 12 (𝑃 ∈ (ℤ‘2) → (1 < 𝑃𝑃 < (𝑃 · 𝑃)))
115, 10mpbid 222 . . . . . . . . . . 11 (𝑃 ∈ (ℤ‘2) → 𝑃 < (𝑃 · 𝑃))
126, 6remulcld 10021 . . . . . . . . . . . 12 (𝑃 ∈ (ℤ‘2) → (𝑃 · 𝑃) ∈ ℝ)
136, 12ltnled 10135 . . . . . . . . . . 11 (𝑃 ∈ (ℤ‘2) → (𝑃 < (𝑃 · 𝑃) ↔ ¬ (𝑃 · 𝑃) ≤ 𝑃))
1411, 13mpbid 222 . . . . . . . . . 10 (𝑃 ∈ (ℤ‘2) → ¬ (𝑃 · 𝑃) ≤ 𝑃)
15 oveq12 6619 . . . . . . . . . . . . 13 ((𝑧 = 𝑃𝑧 = 𝑃) → (𝑧 · 𝑧) = (𝑃 · 𝑃))
1615anidms 676 . . . . . . . . . . . 12 (𝑧 = 𝑃 → (𝑧 · 𝑧) = (𝑃 · 𝑃))
1716breq1d 4628 . . . . . . . . . . 11 (𝑧 = 𝑃 → ((𝑧 · 𝑧) ≤ 𝑃 ↔ (𝑃 · 𝑃) ≤ 𝑃))
1817notbid 308 . . . . . . . . . 10 (𝑧 = 𝑃 → (¬ (𝑧 · 𝑧) ≤ 𝑃 ↔ ¬ (𝑃 · 𝑃) ≤ 𝑃))
1914, 18syl5ibrcom 237 . . . . . . . . 9 (𝑃 ∈ (ℤ‘2) → (𝑧 = 𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃))
2019imim2d 57 . . . . . . . 8 (𝑃 ∈ (ℤ‘2) → ((𝑧𝑃𝑧 = 𝑃) → (𝑧𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃)))
21 con2 130 . . . . . . . 8 ((𝑧𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))
2220, 21syl6 35 . . . . . . 7 (𝑃 ∈ (ℤ‘2) → ((𝑧𝑃𝑧 = 𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
233, 22imim12d 81 . . . . . 6 (𝑃 ∈ (ℤ‘2) → ((𝑧 ∈ (ℤ‘2) → (𝑧𝑃𝑧 = 𝑃)) → (𝑧 ∈ ℙ → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))))
2423ralimdv2 2956 . . . . 5 (𝑃 ∈ (ℤ‘2) → (∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃) → ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
25 annim 441 . . . . . . . . 9 ((𝑧𝑃 ∧ ¬ 𝑧 = 𝑃) ↔ ¬ (𝑧𝑃𝑧 = 𝑃))
26 oveq12 6619 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑧𝑥 = 𝑧) → (𝑥 · 𝑥) = (𝑧 · 𝑧))
2726anidms 676 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (𝑥 · 𝑥) = (𝑧 · 𝑧))
2827breq1d 4628 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → ((𝑥 · 𝑥) ≤ 𝑃 ↔ (𝑧 · 𝑧) ≤ 𝑃))
29 breq1 4621 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (𝑥𝑃𝑧𝑃))
3028, 29anbi12d 746 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃) ↔ ((𝑧 · 𝑧) ≤ 𝑃𝑧𝑃)))
3130rspcev 3298 . . . . . . . . . . . . . 14 ((𝑧 ∈ (ℤ‘2) ∧ ((𝑧 · 𝑧) ≤ 𝑃𝑧𝑃)) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃))
3231ancom2s 843 . . . . . . . . . . . . 13 ((𝑧 ∈ (ℤ‘2) ∧ (𝑧𝑃 ∧ (𝑧 · 𝑧) ≤ 𝑃)) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃))
3332expr 642 . . . . . . . . . . . 12 ((𝑧 ∈ (ℤ‘2) ∧ 𝑧𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
3433ad2ant2lr 783 . . . . . . . . . . 11 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) ≤ 𝑃 → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
35 simprl 793 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧𝑃)
36 eluzelz 11648 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (ℤ‘2) → 𝑧 ∈ ℤ)
3736ad2antlr 762 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℤ)
38 eluz2nn 11677 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (ℤ‘2) → 𝑧 ∈ ℕ)
3938ad2antlr 762 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℕ)
4039nnne0d 11016 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ≠ 0)
41 eluzelz 11648 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (ℤ‘2) → 𝑃 ∈ ℤ)
4241ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℤ)
43 dvdsval2 14917 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ∧ 𝑃 ∈ ℤ) → (𝑧𝑃 ↔ (𝑃 / 𝑧) ∈ ℤ))
4437, 40, 42, 43syl3anc 1323 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧𝑃 ↔ (𝑃 / 𝑧) ∈ ℤ))
4535, 44mpbid 222 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∈ ℤ)
46 eluzelre 11649 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (ℤ‘2) → 𝑧 ∈ ℝ)
4746ad2antlr 762 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℝ)
4847recnd 10019 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℂ)
4948mulid2d 10009 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (1 · 𝑧) = 𝑧)
507ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℕ)
51 dvdsle 14963 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑧𝑃𝑧𝑃))
5251imp 445 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧ 𝑧𝑃) → 𝑧𝑃)
5337, 50, 35, 52syl21anc 1322 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧𝑃)
54 simprr 795 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ¬ 𝑧 = 𝑃)
5554neqned 2797 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧𝑃)
5655necomd 2845 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃𝑧)
576ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℝ)
5847, 57ltlend 10133 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 < 𝑃 ↔ (𝑧𝑃𝑃𝑧)))
5953, 56, 58mpbir2and 956 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 < 𝑃)
6049, 59eqbrtrd 4640 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (1 · 𝑧) < 𝑃)
61 1red 10006 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 1 ∈ ℝ)
6242zred 11433 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℝ)
63 nnre 10978 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
64 nngt0 11000 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℕ → 0 < 𝑧)
6563, 64jca 554 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ → (𝑧 ∈ ℝ ∧ 0 < 𝑧))
6639, 65syl 17 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 ∈ ℝ ∧ 0 < 𝑧))
67 ltmuldiv 10847 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑧 ∈ ℝ ∧ 0 < 𝑧)) → ((1 · 𝑧) < 𝑃 ↔ 1 < (𝑃 / 𝑧)))
6861, 62, 66, 67syl3anc 1323 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((1 · 𝑧) < 𝑃 ↔ 1 < (𝑃 / 𝑧)))
6960, 68mpbid 222 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 1 < (𝑃 / 𝑧))
70 eluz2b1 11710 . . . . . . . . . . . . 13 ((𝑃 / 𝑧) ∈ (ℤ‘2) ↔ ((𝑃 / 𝑧) ∈ ℤ ∧ 1 < (𝑃 / 𝑧)))
7145, 69, 70sylanbrc 697 . . . . . . . . . . . 12 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∈ (ℤ‘2))
7247, 47remulcld 10021 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℝ)
7339, 39nnmulcld 11019 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℕ)
74 nnrp 11793 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ ℕ → 𝑃 ∈ ℝ+)
75 nnrp 11793 . . . . . . . . . . . . . . . . . 18 ((𝑧 · 𝑧) ∈ ℕ → (𝑧 · 𝑧) ∈ ℝ+)
76 rpdivcl 11807 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℝ+ ∧ (𝑧 · 𝑧) ∈ ℝ+) → (𝑃 / (𝑧 · 𝑧)) ∈ ℝ+)
7774, 75, 76syl2an 494 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℕ ∧ (𝑧 · 𝑧) ∈ ℕ) → (𝑃 / (𝑧 · 𝑧)) ∈ ℝ+)
7850, 73, 77syl2anc 692 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / (𝑧 · 𝑧)) ∈ ℝ+)
7957, 72, 78lemul1d 11866 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) ↔ (𝑃 · (𝑃 / (𝑧 · 𝑧))) ≤ ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧)))))
8057recnd 10019 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℂ)
8180, 48, 80, 48, 40, 40divmuldivd 10793 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) = ((𝑃 · 𝑃) / (𝑧 · 𝑧)))
8273nncnd 10987 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℂ)
8373nnne0d 11016 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ≠ 0)
8480, 80, 82, 83divassd 10787 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 · 𝑃) / (𝑧 · 𝑧)) = (𝑃 · (𝑃 / (𝑧 · 𝑧))))
8581, 84eqtrd 2655 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) = (𝑃 · (𝑃 / (𝑧 · 𝑧))))
8680, 82, 83divcan2d 10754 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧))) = 𝑃)
8786eqcomd 2627 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 = ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧))))
8885, 87breq12d 4631 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ↔ (𝑃 · (𝑃 / (𝑧 · 𝑧))) ≤ ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧)))))
8979, 88bitr4d 271 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) ↔ ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃))
9089biimpd 219 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃))
9180, 48, 40divcan2d 10754 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · (𝑃 / 𝑧)) = 𝑃)
92 dvds0lem 14923 . . . . . . . . . . . . . 14 (((𝑧 ∈ ℤ ∧ (𝑃 / 𝑧) ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ (𝑧 · (𝑃 / 𝑧)) = 𝑃) → (𝑃 / 𝑧) ∥ 𝑃)
9337, 45, 42, 91, 92syl31anc 1326 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∥ 𝑃)
9490, 93jctird 566 . . . . . . . . . . . 12 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃)))
95 oveq12 6619 . . . . . . . . . . . . . . . 16 ((𝑥 = (𝑃 / 𝑧) ∧ 𝑥 = (𝑃 / 𝑧)) → (𝑥 · 𝑥) = ((𝑃 / 𝑧) · (𝑃 / 𝑧)))
9695anidms 676 . . . . . . . . . . . . . . 15 (𝑥 = (𝑃 / 𝑧) → (𝑥 · 𝑥) = ((𝑃 / 𝑧) · (𝑃 / 𝑧)))
9796breq1d 4628 . . . . . . . . . . . . . 14 (𝑥 = (𝑃 / 𝑧) → ((𝑥 · 𝑥) ≤ 𝑃 ↔ ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃))
98 breq1 4621 . . . . . . . . . . . . . 14 (𝑥 = (𝑃 / 𝑧) → (𝑥𝑃 ↔ (𝑃 / 𝑧) ∥ 𝑃))
9997, 98anbi12d 746 . . . . . . . . . . . . 13 (𝑥 = (𝑃 / 𝑧) → (((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃) ↔ (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃)))
10099rspcev 3298 . . . . . . . . . . . 12 (((𝑃 / 𝑧) ∈ (ℤ‘2) ∧ (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃)) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃))
10171, 94, 100syl6an 567 . . . . . . . . . . 11 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
10272, 57letrid 10140 . . . . . . . . . . 11 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) ≤ 𝑃𝑃 ≤ (𝑧 · 𝑧)))
10334, 101, 102mpjaod 396 . . . . . . . . . 10 (((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) ∧ (𝑧𝑃 ∧ ¬ 𝑧 = 𝑃)) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃))
104103ex 450 . . . . . . . . 9 ((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) → ((𝑧𝑃 ∧ ¬ 𝑧 = 𝑃) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
10525, 104syl5bir 233 . . . . . . . 8 ((𝑃 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) → (¬ (𝑧𝑃𝑧 = 𝑃) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
106105rexlimdva 3025 . . . . . . 7 (𝑃 ∈ (ℤ‘2) → (∃𝑧 ∈ (ℤ‘2) ¬ (𝑧𝑃𝑧 = 𝑃) → ∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)))
107 prmz 15320 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℙ → 𝑧 ∈ ℤ)
108107ad2antrl 763 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑧 ∈ ℤ)
109108zred 11433 . . . . . . . . . . . . 13 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑧 ∈ ℝ)
110109, 109remulcld 10021 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑧 · 𝑧) ∈ ℝ)
111 eluzelz 11648 . . . . . . . . . . . . . . 15 (𝑥 ∈ (ℤ‘2) → 𝑥 ∈ ℤ)
112111ad3antlr 766 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑥 ∈ ℤ)
113112zred 11433 . . . . . . . . . . . . 13 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑥 ∈ ℝ)
114113, 113remulcld 10021 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑥 · 𝑥) ∈ ℝ)
11541ad3antrrr 765 . . . . . . . . . . . . 13 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑃 ∈ ℤ)
116115zred 11433 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑃 ∈ ℝ)
117 eluz2nn 11677 . . . . . . . . . . . . . . 15 (𝑥 ∈ (ℤ‘2) → 𝑥 ∈ ℕ)
118117ad3antlr 766 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑥 ∈ ℕ)
119 simprr 795 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑧𝑥)
120 dvdsle 14963 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑧𝑥𝑧𝑥))
121120imp 445 . . . . . . . . . . . . . 14 (((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℕ) ∧ 𝑧𝑥) → 𝑧𝑥)
122108, 118, 119, 121syl21anc 1322 . . . . . . . . . . . . 13 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑧𝑥)
123 eluzge2nn0 11678 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (ℤ‘2) → 𝑧 ∈ ℕ0)
124123nn0ge0d 11305 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (ℤ‘2) → 0 ≤ 𝑧)
1252, 124syl 17 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℙ → 0 ≤ 𝑧)
126125ad2antrl 763 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 0 ≤ 𝑧)
127 nnnn0 11250 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ0)
128127nn0ge0d 11305 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℕ → 0 ≤ 𝑥)
129118, 128syl 17 . . . . . . . . . . . . . 14 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 0 ≤ 𝑥)
130 le2msq 10874 . . . . . . . . . . . . . 14 (((𝑧 ∈ ℝ ∧ 0 ≤ 𝑧) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (𝑧𝑥 ↔ (𝑧 · 𝑧) ≤ (𝑥 · 𝑥)))
131109, 126, 113, 129, 130syl22anc 1324 . . . . . . . . . . . . 13 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑧𝑥 ↔ (𝑧 · 𝑧) ≤ (𝑥 · 𝑥)))
132122, 131mpbid 222 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑧 · 𝑧) ≤ (𝑥 · 𝑥))
133 simplrl 799 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑥 · 𝑥) ≤ 𝑃)
134110, 114, 116, 132, 133letrd 10145 . . . . . . . . . . 11 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → (𝑧 · 𝑧) ≤ 𝑃)
135 simplrr 800 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑥𝑃)
136 dvdstr 14949 . . . . . . . . . . . . 13 ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑧𝑥𝑥𝑃) → 𝑧𝑃))
137108, 112, 115, 136syl3anc 1323 . . . . . . . . . . . 12 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → ((𝑧𝑥𝑥𝑃) → 𝑧𝑃))
138119, 135, 137mp2and 714 . . . . . . . . . . 11 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → 𝑧𝑃)
139134, 138jc 159 . . . . . . . . . 10 ((((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧𝑥)) → ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))
140 exprmfct 15347 . . . . . . . . . . 11 (𝑥 ∈ (ℤ‘2) → ∃𝑧 ∈ ℙ 𝑧𝑥)
141140ad2antlr 762 . . . . . . . . . 10 (((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) → ∃𝑧 ∈ ℙ 𝑧𝑥)
142139, 141reximddv 3013 . . . . . . . . 9 (((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) ∧ ((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃)) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))
143142ex 450 . . . . . . . 8 ((𝑃 ∈ (ℤ‘2) ∧ 𝑥 ∈ (ℤ‘2)) → (((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
144143rexlimdva 3025 . . . . . . 7 (𝑃 ∈ (ℤ‘2) → (∃𝑥 ∈ (ℤ‘2)((𝑥 · 𝑥) ≤ 𝑃𝑥𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
145106, 144syld 47 . . . . . 6 (𝑃 ∈ (ℤ‘2) → (∃𝑧 ∈ (ℤ‘2) ¬ (𝑧𝑃𝑧 = 𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
146 rexnal 2990 . . . . . 6 (∃𝑧 ∈ (ℤ‘2) ¬ (𝑧𝑃𝑧 = 𝑃) ↔ ¬ ∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃))
147 rexnal 2990 . . . . . 6 (∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃) ↔ ¬ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))
148145, 146, 1473imtr3g 284 . . . . 5 (𝑃 ∈ (ℤ‘2) → (¬ ∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃) → ¬ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
14924, 148impcon4bid 217 . . . 4 (𝑃 ∈ (ℤ‘2) → (∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
150 prmnn 15319 . . . . . . . . 9 (𝑧 ∈ ℙ → 𝑧 ∈ ℕ)
151150nncnd 10987 . . . . . . . 8 (𝑧 ∈ ℙ → 𝑧 ∈ ℂ)
152151sqvald 12952 . . . . . . 7 (𝑧 ∈ ℙ → (𝑧↑2) = (𝑧 · 𝑧))
153152breq1d 4628 . . . . . 6 (𝑧 ∈ ℙ → ((𝑧↑2) ≤ 𝑃 ↔ (𝑧 · 𝑧) ≤ 𝑃))
154153imbi1d 331 . . . . 5 (𝑧 ∈ ℙ → (((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃) ↔ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃)))
155154ralbiia 2974 . . . 4 (∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧𝑃))
156149, 155syl6bbr 278 . . 3 (𝑃 ∈ (ℤ‘2) → (∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃)))
157156pm5.32i 668 . 2 ((𝑃 ∈ (ℤ‘2) ∧ ∀𝑧 ∈ (ℤ‘2)(𝑧𝑃𝑧 = 𝑃)) ↔ (𝑃 ∈ (ℤ‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃)))
1581, 157bitri 264 1 (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908   class class class wbr 4618  cfv 5852  (class class class)co 6610  cr 9886  0cc0 9887  1c1 9888   · cmul 9892   < clt 10025  cle 10026   / cdiv 10635  cn 10971  2c2 11021  cz 11328  cuz 11638  +crp 11783  cexp 12807  cdvds 14914  cprime 15316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-sup 8299  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-n0 11244  df-z 11329  df-uz 11639  df-rp 11784  df-fz 12276  df-seq 12749  df-exp 12808  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-dvds 14915  df-prm 15317
This theorem is referenced by:  isprm7  15351  pockthg  15541  prmlem1a  15744
  Copyright terms: Public domain W3C validator