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

Theorem isprm5lem 12309
Description: Lemma for isprm5 12310. The interesting direction (showing that one only needs to check prime divisors up to the square root of 𝑃). (Contributed by Jim Kingdon, 20-Oct-2024.)
Hypotheses
Ref Expression
isprm5lem.p (𝜑𝑃 ∈ (ℤ‘2))
isprm5lem.z (𝜑 → ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃))
isprm5lem.x (𝜑𝑋 ∈ (2...(𝑃 − 1)))
Assertion
Ref Expression
isprm5lem (𝜑 → ¬ 𝑋𝑃)
Distinct variable groups:   𝑧,𝑃   𝑧,𝑋
Allowed substitution hint:   𝜑(𝑧)

Proof of Theorem isprm5lem
Dummy variables 𝑤 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isprm5lem.x . . 3 (𝜑𝑋 ∈ (2...(𝑃 − 1)))
2 elfzuz 10096 . . 3 (𝑋 ∈ (2...(𝑃 − 1)) → 𝑋 ∈ (ℤ‘2))
3 exprmfct 12306 . . 3 (𝑋 ∈ (ℤ‘2) → ∃𝑦 ∈ ℙ 𝑦𝑋)
41, 2, 33syl 17 . 2 (𝜑 → ∃𝑦 ∈ ℙ 𝑦𝑋)
5 simpr 110 . . . . 5 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) → (𝑦↑2) ≤ 𝑃)
6 oveq1 5929 . . . . . . . 8 (𝑧 = 𝑦 → (𝑧↑2) = (𝑦↑2))
76breq1d 4043 . . . . . . 7 (𝑧 = 𝑦 → ((𝑧↑2) ≤ 𝑃 ↔ (𝑦↑2) ≤ 𝑃))
8 breq1 4036 . . . . . . . 8 (𝑧 = 𝑦 → (𝑧𝑃𝑦𝑃))
98notbid 668 . . . . . . 7 (𝑧 = 𝑦 → (¬ 𝑧𝑃 ↔ ¬ 𝑦𝑃))
107, 9imbi12d 234 . . . . . 6 (𝑧 = 𝑦 → (((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃) ↔ ((𝑦↑2) ≤ 𝑃 → ¬ 𝑦𝑃)))
11 isprm5lem.z . . . . . . 7 (𝜑 → ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃))
1211ad2antrr 488 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) → ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃))
13 simplrl 535 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) → 𝑦 ∈ ℙ)
1410, 12, 13rspcdva 2873 . . . . 5 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) → ((𝑦↑2) ≤ 𝑃 → ¬ 𝑦𝑃))
155, 14mpd 13 . . . 4 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) → ¬ 𝑦𝑃)
16 prmz 12279 . . . . . . 7 (𝑦 ∈ ℙ → 𝑦 ∈ ℤ)
1716ad2antrl 490 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) → 𝑦 ∈ ℤ)
1817ad2antrr 488 . . . . 5 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) ∧ 𝑋𝑃) → 𝑦 ∈ ℤ)
19 elfzelz 10100 . . . . . . . 8 (𝑋 ∈ (2...(𝑃 − 1)) → 𝑋 ∈ ℤ)
201, 19syl 14 . . . . . . 7 (𝜑𝑋 ∈ ℤ)
2120ad2antrr 488 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑋𝑃) → 𝑋 ∈ ℤ)
2221adantlr 477 . . . . 5 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) ∧ 𝑋𝑃) → 𝑋 ∈ ℤ)
23 isprm5lem.p . . . . . . . 8 (𝜑𝑃 ∈ (ℤ‘2))
24 eluzelz 9610 . . . . . . . 8 (𝑃 ∈ (ℤ‘2) → 𝑃 ∈ ℤ)
2523, 24syl 14 . . . . . . 7 (𝜑𝑃 ∈ ℤ)
2625ad2antrr 488 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑋𝑃) → 𝑃 ∈ ℤ)
2726adantlr 477 . . . . 5 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) ∧ 𝑋𝑃) → 𝑃 ∈ ℤ)
28 simplrr 536 . . . . . 6 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑋𝑃) → 𝑦𝑋)
2928adantlr 477 . . . . 5 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) ∧ 𝑋𝑃) → 𝑦𝑋)
30 simpr 110 . . . . 5 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) ∧ 𝑋𝑃) → 𝑋𝑃)
3118, 22, 27, 29, 30dvdstrd 11995 . . . 4 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) ∧ 𝑋𝑃) → 𝑦𝑃)
3215, 31mtand 666 . . 3 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ (𝑦↑2) ≤ 𝑃) → ¬ 𝑋𝑃)
3317ad2antrr 488 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → 𝑦 ∈ ℤ)
3421adantlr 477 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → 𝑋 ∈ ℤ)
3525adantr 276 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) → 𝑃 ∈ ℤ)
3635ad2antrr 488 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → 𝑃 ∈ ℤ)
3728adantlr 477 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → 𝑦𝑋)
38 simpr 110 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → 𝑋𝑃)
3933, 34, 36, 37, 38dvdstrd 11995 . . . . . . . 8 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → 𝑦𝑃)
4017adantr 276 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑦 ∈ ℤ)
41 prmnn 12278 . . . . . . . . . . . . 13 (𝑦 ∈ ℙ → 𝑦 ∈ ℕ)
4241nnne0d 9035 . . . . . . . . . . . 12 (𝑦 ∈ ℙ → 𝑦 ≠ 0)
4342ad2antrl 490 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) → 𝑦 ≠ 0)
4443adantr 276 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑦 ≠ 0)
4525ad2antrr 488 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑃 ∈ ℤ)
46 dvdsval2 11955 . . . . . . . . . 10 ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ 𝑃 ∈ ℤ) → (𝑦𝑃 ↔ (𝑃 / 𝑦) ∈ ℤ))
4740, 44, 45, 46syl3anc 1249 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (𝑦𝑃 ↔ (𝑃 / 𝑦) ∈ ℤ))
4847adantr 276 . . . . . . . 8 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → (𝑦𝑃 ↔ (𝑃 / 𝑦) ∈ ℤ))
4939, 48mpbid 147 . . . . . . 7 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → (𝑃 / 𝑦) ∈ ℤ)
5040zred 9448 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑦 ∈ ℝ)
5150recnd 8055 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑦 ∈ ℂ)
5251mulid2d 8045 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (1 · 𝑦) = 𝑦)
53 2nn 9152 . . . . . . . . . . . . . . 15 2 ∈ ℕ
54 fzssnn 10143 . . . . . . . . . . . . . . 15 (2 ∈ ℕ → (2...(𝑃 − 1)) ⊆ ℕ)
5553, 54ax-mp 5 . . . . . . . . . . . . . 14 (2...(𝑃 − 1)) ⊆ ℕ
5655, 1sselid 3181 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ ℕ)
5756ad2antrr 488 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑋 ∈ ℕ)
5857nnred 9003 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑋 ∈ ℝ)
5925zred 9448 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℝ)
6059ad2antrr 488 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑃 ∈ ℝ)
61 simplrr 536 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑦𝑋)
62 dvdsle 12009 . . . . . . . . . . . . 13 ((𝑦 ∈ ℤ ∧ 𝑋 ∈ ℕ) → (𝑦𝑋𝑦𝑋))
6340, 57, 62syl2anc 411 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (𝑦𝑋𝑦𝑋))
6461, 63mpd 13 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑦𝑋)
65 elfzle2 10103 . . . . . . . . . . . . . 14 (𝑋 ∈ (2...(𝑃 − 1)) → 𝑋 ≤ (𝑃 − 1))
661, 65syl 14 . . . . . . . . . . . . 13 (𝜑𝑋 ≤ (𝑃 − 1))
67 zltlem1 9383 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑋 < 𝑃𝑋 ≤ (𝑃 − 1)))
6820, 25, 67syl2anc 411 . . . . . . . . . . . . 13 (𝜑 → (𝑋 < 𝑃𝑋 ≤ (𝑃 − 1)))
6966, 68mpbird 167 . . . . . . . . . . . 12 (𝜑𝑋 < 𝑃)
7069ad2antrr 488 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑋 < 𝑃)
7150, 58, 60, 64, 70lelttrd 8151 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑦 < 𝑃)
7252, 71eqbrtrd 4055 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (1 · 𝑦) < 𝑃)
73 1red 8041 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 1 ∈ ℝ)
7441nnrpd 9769 . . . . . . . . . . . 12 (𝑦 ∈ ℙ → 𝑦 ∈ ℝ+)
7574ad2antrl 490 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) → 𝑦 ∈ ℝ+)
7675adantr 276 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑦 ∈ ℝ+)
7773, 60, 76ltmuldivd 9819 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → ((1 · 𝑦) < 𝑃 ↔ 1 < (𝑃 / 𝑦)))
7872, 77mpbid 147 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 1 < (𝑃 / 𝑦))
7978adantr 276 . . . . . . 7 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → 1 < (𝑃 / 𝑦))
80 eluz2b1 9675 . . . . . . 7 ((𝑃 / 𝑦) ∈ (ℤ‘2) ↔ ((𝑃 / 𝑦) ∈ ℤ ∧ 1 < (𝑃 / 𝑦)))
8149, 79, 80sylanbrc 417 . . . . . 6 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → (𝑃 / 𝑦) ∈ (ℤ‘2))
82 exprmfct 12306 . . . . . 6 ((𝑃 / 𝑦) ∈ (ℤ‘2) → ∃𝑤 ∈ ℙ 𝑤 ∥ (𝑃 / 𝑦))
8381, 82syl 14 . . . . 5 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → ∃𝑤 ∈ ℙ 𝑤 ∥ (𝑃 / 𝑦))
84 prmz 12279 . . . . . . . 8 (𝑤 ∈ ℙ → 𝑤 ∈ ℤ)
8584ad2antrl 490 . . . . . . 7 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 𝑤 ∈ ℤ)
8649adantr 276 . . . . . . 7 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑃 / 𝑦) ∈ ℤ)
8745ad2antrr 488 . . . . . . 7 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 𝑃 ∈ ℤ)
88 simprr 531 . . . . . . 7 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 𝑤 ∥ (𝑃 / 𝑦))
8939adantr 276 . . . . . . . 8 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 𝑦𝑃)
9044ad2antrr 488 . . . . . . . 8 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 𝑦 ≠ 0)
91 divconjdvds 12014 . . . . . . . 8 ((𝑦𝑃𝑦 ≠ 0) → (𝑃 / 𝑦) ∥ 𝑃)
9289, 90, 91syl2anc 411 . . . . . . 7 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑃 / 𝑦) ∥ 𝑃)
9385, 86, 87, 88, 92dvdstrd 11995 . . . . . 6 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 𝑤𝑃)
9485zred 9448 . . . . . . . . 9 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 𝑤 ∈ ℝ)
9594resqcld 10791 . . . . . . . 8 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑤↑2) ∈ ℝ)
9660ad2antrr 488 . . . . . . . 8 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 𝑃 ∈ ℝ)
9781adantr 276 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑃 / 𝑦) ∈ (ℤ‘2))
98 eluz2nn 9640 . . . . . . . . . . . 12 ((𝑃 / 𝑦) ∈ (ℤ‘2) → (𝑃 / 𝑦) ∈ ℕ)
9997, 98syl 14 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑃 / 𝑦) ∈ ℕ)
10099nnred 9003 . . . . . . . . . 10 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑃 / 𝑦) ∈ ℝ)
101100resqcld 10791 . . . . . . . . 9 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → ((𝑃 / 𝑦)↑2) ∈ ℝ)
102 dvdsle 12009 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ (𝑃 / 𝑦) ∈ ℕ) → (𝑤 ∥ (𝑃 / 𝑦) → 𝑤 ≤ (𝑃 / 𝑦)))
10385, 99, 102syl2anc 411 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑤 ∥ (𝑃 / 𝑦) → 𝑤 ≤ (𝑃 / 𝑦)))
10488, 103mpd 13 . . . . . . . . . 10 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 𝑤 ≤ (𝑃 / 𝑦))
105 prmnn 12278 . . . . . . . . . . . . . 14 (𝑤 ∈ ℙ → 𝑤 ∈ ℕ)
106105nnnn0d 9302 . . . . . . . . . . . . 13 (𝑤 ∈ ℙ → 𝑤 ∈ ℕ0)
107106nn0ge0d 9305 . . . . . . . . . . . 12 (𝑤 ∈ ℙ → 0 ≤ 𝑤)
108107ad2antrl 490 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 0 ≤ 𝑤)
109 0red 8027 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 0 ∈ ℝ)
110 1red 8041 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 1 ∈ ℝ)
111 0le1 8508 . . . . . . . . . . . . 13 0 ≤ 1
112111a1i 9 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 0 ≤ 1)
11399nnge1d 9033 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 1 ≤ (𝑃 / 𝑦))
114109, 110, 100, 112, 113letrd 8150 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 0 ≤ (𝑃 / 𝑦))
11594, 100, 108, 114le2sqd 10797 . . . . . . . . . 10 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑤 ≤ (𝑃 / 𝑦) ↔ (𝑤↑2) ≤ ((𝑃 / 𝑦)↑2)))
116104, 115mpbid 147 . . . . . . . . 9 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑤↑2) ≤ ((𝑃 / 𝑦)↑2))
11760recnd 8055 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑃 ∈ ℂ)
11841ad2antrl 490 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) → 𝑦 ∈ ℕ)
119118adantr 276 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑦 ∈ ℕ)
120119nnap0d 9036 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑦 # 0)
121117, 51, 120sqdivapd 10778 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → ((𝑃 / 𝑦)↑2) = ((𝑃↑2) / (𝑦↑2)))
122117sqvald 10762 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (𝑃↑2) = (𝑃 · 𝑃))
12350resqcld 10791 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (𝑦↑2) ∈ ℝ)
124 eluz2nn 9640 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (ℤ‘2) → 𝑃 ∈ ℕ)
12523, 124syl 14 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ ℕ)
126125nnrpd 9769 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ ℝ+)
127126ad2antrr 488 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑃 ∈ ℝ+)
128 simpr 110 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → 𝑃 < (𝑦↑2))
12960, 123, 127, 128ltmul2dd 9828 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (𝑃 · 𝑃) < (𝑃 · (𝑦↑2)))
130122, 129eqbrtrd 4055 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (𝑃↑2) < (𝑃 · (𝑦↑2)))
13160resqcld 10791 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (𝑃↑2) ∈ ℝ)
132119nnsqcld 10786 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (𝑦↑2) ∈ ℕ)
133132nnrpd 9769 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (𝑦↑2) ∈ ℝ+)
134131, 60, 133ltdivmul2d 9824 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → (((𝑃↑2) / (𝑦↑2)) < 𝑃 ↔ (𝑃↑2) < (𝑃 · (𝑦↑2))))
135130, 134mpbird 167 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → ((𝑃↑2) / (𝑦↑2)) < 𝑃)
136121, 135eqbrtrd 4055 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → ((𝑃 / 𝑦)↑2) < 𝑃)
137136ad2antrr 488 . . . . . . . . 9 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → ((𝑃 / 𝑦)↑2) < 𝑃)
13895, 101, 96, 116, 137lelttrd 8151 . . . . . . . 8 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑤↑2) < 𝑃)
13995, 96, 138ltled 8145 . . . . . . 7 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → (𝑤↑2) ≤ 𝑃)
140 oveq1 5929 . . . . . . . . . 10 (𝑧 = 𝑤 → (𝑧↑2) = (𝑤↑2))
141140breq1d 4043 . . . . . . . . 9 (𝑧 = 𝑤 → ((𝑧↑2) ≤ 𝑃 ↔ (𝑤↑2) ≤ 𝑃))
142 breq1 4036 . . . . . . . . . 10 (𝑧 = 𝑤 → (𝑧𝑃𝑤𝑃))
143142notbid 668 . . . . . . . . 9 (𝑧 = 𝑤 → (¬ 𝑧𝑃 ↔ ¬ 𝑤𝑃))
144141, 143imbi12d 234 . . . . . . . 8 (𝑧 = 𝑤 → (((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃) ↔ ((𝑤↑2) ≤ 𝑃 → ¬ 𝑤𝑃)))
14511ad4antr 494 . . . . . . . 8 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧𝑃))
146 simprl 529 . . . . . . . 8 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → 𝑤 ∈ ℙ)
147144, 145, 146rspcdva 2873 . . . . . . 7 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → ((𝑤↑2) ≤ 𝑃 → ¬ 𝑤𝑃))
148139, 147mpd 13 . . . . . 6 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → ¬ 𝑤𝑃)
14993, 148pm2.21fal 1384 . . . . 5 (((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) ∧ (𝑤 ∈ ℙ ∧ 𝑤 ∥ (𝑃 / 𝑦))) → ⊥)
15083, 149rexlimddv 2619 . . . 4 ((((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) ∧ 𝑋𝑃) → ⊥)
151150inegd 1383 . . 3 (((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) ∧ 𝑃 < (𝑦↑2)) → ¬ 𝑋𝑃)
152 zsqcl 10702 . . . . 5 (𝑦 ∈ ℤ → (𝑦↑2) ∈ ℤ)
15317, 152syl 14 . . . 4 ((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) → (𝑦↑2) ∈ ℤ)
154 zlelttric 9371 . . . 4 (((𝑦↑2) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑦↑2) ≤ 𝑃𝑃 < (𝑦↑2)))
155153, 35, 154syl2anc 411 . . 3 ((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) → ((𝑦↑2) ≤ 𝑃𝑃 < (𝑦↑2)))
15632, 151, 155mpjaodan 799 . 2 ((𝜑 ∧ (𝑦 ∈ ℙ ∧ 𝑦𝑋)) → ¬ 𝑋𝑃)
1574, 156rexlimddv 2619 1 (𝜑 → ¬ 𝑋𝑃)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  wfal 1369  wcel 2167  wne 2367  wral 2475  wrex 2476  wss 3157   class class class wbr 4033  cfv 5258  (class class class)co 5922  cr 7878  0cc0 7879  1c1 7880   · cmul 7884   < clt 8061  cle 8062  cmin 8197   / cdiv 8699  cn 8990  2c2 9041  cz 9326  cuz 9601  +crp 9728  ...cfz 10083  cexp 10630  cdvds 11952  cprime 12275
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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-mulrcl 7978  ax-addcom 7979  ax-mulcom 7980  ax-addass 7981  ax-mulass 7982  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-1rid 7986  ax-0id 7987  ax-rnegex 7988  ax-precex 7989  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-apti 7994  ax-pre-ltadd 7995  ax-pre-mulgt0 7996  ax-pre-mulext 7997  ax-arch 7998  ax-caucvg 7999
This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-if 3562  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-id 4328  df-po 4331  df-iso 4332  df-iord 4401  df-on 4403  df-ilim 4404  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-1st 6198  df-2nd 6199  df-recs 6363  df-frec 6449  df-1o 6474  df-2o 6475  df-er 6592  df-en 6800  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-reap 8602  df-ap 8609  df-div 8700  df-inn 8991  df-2 9049  df-3 9050  df-4 9051  df-n0 9250  df-z 9327  df-uz 9602  df-q 9694  df-rp 9729  df-fz 10084  df-fzo 10218  df-fl 10360  df-mod 10415  df-seqfrec 10540  df-exp 10631  df-cj 11007  df-re 11008  df-im 11009  df-rsqrt 11163  df-abs 11164  df-dvds 11953  df-prm 12276
This theorem is referenced by:  isprm5  12310
  Copyright terms: Public domain W3C validator