Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lighneallem2 Structured version   Visualization version   GIF version

Theorem lighneallem2 42052
Description: Lemma 2 for lighneal 42057. (Contributed by AV, 13-Aug-2021.)
Assertion
Ref Expression
lighneallem2 (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃𝑀)) → 𝑀 = 1)

Proof of Theorem lighneallem2
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 evennn2n 15298 . . . 4 (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℕ (2 · 𝑘) = 𝑁))
213ad2ant3 1130 . . 3 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℕ (2 · 𝑘) = 𝑁))
3 oveq2 6823 . . . . . . . . . 10 (𝑁 = (2 · 𝑘) → (2↑𝑁) = (2↑(2 · 𝑘)))
43eqcoms 2769 . . . . . . . . 9 ((2 · 𝑘) = 𝑁 → (2↑𝑁) = (2↑(2 · 𝑘)))
5 2cnd 11306 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 2 ∈ ℂ)
6 nncn 11241 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
75, 6mulcomd 10274 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (2 · 𝑘) = (𝑘 · 2))
87oveq2d 6831 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (2↑(2 · 𝑘)) = (2↑(𝑘 · 2)))
9 2nn0 11522 . . . . . . . . . . . . 13 2 ∈ ℕ0
109a1i 11 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 2 ∈ ℕ0)
11 nnnn0 11512 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
125, 10, 11expmuld 13226 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (2↑(𝑘 · 2)) = ((2↑𝑘)↑2))
138, 12eqtrd 2795 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2↑(2 · 𝑘)) = ((2↑𝑘)↑2))
1413adantl 473 . . . . . . . . 9 (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (2↑(2 · 𝑘)) = ((2↑𝑘)↑2))
154, 14sylan9eqr 2817 . . . . . . . 8 ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → (2↑𝑁) = ((2↑𝑘)↑2))
1615oveq1d 6830 . . . . . . 7 ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → ((2↑𝑁) − 1) = (((2↑𝑘)↑2) − 1))
1716eqeq1d 2763 . . . . . 6 ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → (((2↑𝑁) − 1) = (𝑃𝑀) ↔ (((2↑𝑘)↑2) − 1) = (𝑃𝑀)))
18 elnn1uz2 11979 . . . . . . . . 9 (𝑘 ∈ ℕ ↔ (𝑘 = 1 ∨ 𝑘 ∈ (ℤ‘2)))
19 oveq2 6823 . . . . . . . . . . . . . . . . . 18 (𝑘 = 1 → (2↑𝑘) = (2↑1))
20 2cn 11304 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℂ
21 exp1 13081 . . . . . . . . . . . . . . . . . . 19 (2 ∈ ℂ → (2↑1) = 2)
2220, 21ax-mp 5 . . . . . . . . . . . . . . . . . 18 (2↑1) = 2
2319, 22syl6eq 2811 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (2↑𝑘) = 2)
2423oveq1d 6830 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → ((2↑𝑘)↑2) = (2↑2))
2524oveq1d 6830 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (((2↑𝑘)↑2) − 1) = ((2↑2) − 1))
26 sq2 13175 . . . . . . . . . . . . . . . . 17 (2↑2) = 4
2726oveq1i 6825 . . . . . . . . . . . . . . . 16 ((2↑2) − 1) = (4 − 1)
28 4m1e3 11351 . . . . . . . . . . . . . . . 16 (4 − 1) = 3
2927, 28eqtri 2783 . . . . . . . . . . . . . . 15 ((2↑2) − 1) = 3
3025, 29syl6eq 2811 . . . . . . . . . . . . . 14 (𝑘 = 1 → (((2↑𝑘)↑2) − 1) = 3)
3130eqeq1d 2763 . . . . . . . . . . . . 13 (𝑘 = 1 → ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) ↔ 3 = (𝑃𝑀)))
3231adantr 472 . . . . . . . . . . . 12 ((𝑘 = 1 ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) ↔ 3 = (𝑃𝑀)))
33 eqcom 2768 . . . . . . . . . . . . . . 15 (3 = (𝑃𝑀) ↔ (𝑃𝑀) = 3)
34 eldifi 3876 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
35 prmnn 15611 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
36 nnre 11240 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℕ → 𝑃 ∈ ℝ)
3734, 35, 363syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ)
38373ad2ant1 1128 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑃 ∈ ℝ)
39 nnnn0 11512 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
40393ad2ant2 1129 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℕ0)
4138, 40reexpcld 13240 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑃𝑀) ∈ ℝ)
4241adantr 472 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑃𝑀) = 3) → (𝑃𝑀) ∈ ℝ)
43 simpr 479 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑃𝑀) = 3) → (𝑃𝑀) = 3)
4442, 43eqled 10353 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑃𝑀) = 3) → (𝑃𝑀) ≤ 3)
4544ex 449 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑃𝑀) = 3 → (𝑃𝑀) ≤ 3))
4633, 45syl5bi 232 . . . . . . . . . . . . . 14 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (3 = (𝑃𝑀) → (𝑃𝑀) ≤ 3))
4735nnred 11248 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
48 prmgt1 15632 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ ℙ → 1 < 𝑃)
4947, 48jca 555 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ ℙ → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
5034, 49syl 17 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
51503ad2ant1 1128 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
52 nnz 11612 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
53523ad2ant2 1129 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℤ)
54 3rp 12052 . . . . . . . . . . . . . . . . 17 3 ∈ ℝ+
5554a1i 11 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 3 ∈ ℝ+)
56 efexple 25227 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ ℝ ∧ 1 < 𝑃) ∧ 𝑀 ∈ ℤ ∧ 3 ∈ ℝ+) → ((𝑃𝑀) ≤ 3 ↔ 𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃)))))
5751, 53, 55, 56syl3anc 1477 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑃𝑀) ≤ 3 ↔ 𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃)))))
58 oddprmge3 15635 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ‘3))
59 eluzle 11913 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ (ℤ‘3) → 3 ≤ 𝑃)
6058, 59syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ (ℙ ∖ {2}) → 3 ≤ 𝑃)
6154a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ (ℙ ∖ {2}) → 3 ∈ ℝ+)
62 nnrp 12056 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℕ → 𝑃 ∈ ℝ+)
6334, 35, 623syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ+)
6461, 63logled 24594 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ (ℙ ∖ {2}) → (3 ≤ 𝑃 ↔ (log‘3) ≤ (log‘𝑃)))
6560, 64mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (ℙ ∖ {2}) → (log‘3) ≤ (log‘𝑃))
66653ad2ant1 1128 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (log‘3) ≤ (log‘𝑃))
67 relogcl 24543 . . . . . . . . . . . . . . . . . . 19 (3 ∈ ℝ+ → (log‘3) ∈ ℝ)
6854, 67ax-mp 5 . . . . . . . . . . . . . . . . . 18 (log‘3) ∈ ℝ
69 rplogcl 24571 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℝ ∧ 1 < 𝑃) → (log‘𝑃) ∈ ℝ+)
7034, 49, 693syl 18 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ (ℙ ∖ {2}) → (log‘𝑃) ∈ ℝ+)
71703ad2ant1 1128 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (log‘𝑃) ∈ ℝ+)
72 divle1le 12114 . . . . . . . . . . . . . . . . . 18 (((log‘3) ∈ ℝ ∧ (log‘𝑃) ∈ ℝ+) → (((log‘3) / (log‘𝑃)) ≤ 1 ↔ (log‘3) ≤ (log‘𝑃)))
7368, 71, 72sylancr 698 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((log‘3) / (log‘𝑃)) ≤ 1 ↔ (log‘3) ≤ (log‘𝑃)))
7466, 73mpbird 247 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((log‘3) / (log‘𝑃)) ≤ 1)
75 fldivle 12847 . . . . . . . . . . . . . . . . . 18 (((log‘3) ∈ ℝ ∧ (log‘𝑃) ∈ ℝ+) → (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃)))
7668, 71, 75sylancr 698 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃)))
77 nnre 11240 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
78773ad2ant2 1129 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℝ)
7968a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ (ℙ ∖ {2}) → (log‘3) ∈ ℝ)
8062relogcld 24590 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℕ → (log‘𝑃) ∈ ℝ)
8134, 35, 803syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ (ℙ ∖ {2}) → (log‘𝑃) ∈ ℝ)
8235nnrpd 12084 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ ℙ → 𝑃 ∈ ℝ+)
83 1red 10268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℙ → 1 ∈ ℝ)
8483, 48gtned 10385 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ ℙ → 𝑃 ≠ 1)
8582, 84jca 555 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℙ → (𝑃 ∈ ℝ+𝑃 ≠ 1))
86 logne0 24547 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 ∈ ℝ+𝑃 ≠ 1) → (log‘𝑃) ≠ 0)
8734, 85, 863syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ (ℙ ∖ {2}) → (log‘𝑃) ≠ 0)
8879, 81, 87redivcld 11066 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ (ℙ ∖ {2}) → ((log‘3) / (log‘𝑃)) ∈ ℝ)
8988flcld 12814 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ (ℙ ∖ {2}) → (⌊‘((log‘3) / (log‘𝑃))) ∈ ℤ)
9089zred 11695 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ (ℙ ∖ {2}) → (⌊‘((log‘3) / (log‘𝑃))) ∈ ℝ)
91903ad2ant1 1128 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((log‘3) / (log‘𝑃))) ∈ ℝ)
92883ad2ant1 1128 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((log‘3) / (log‘𝑃)) ∈ ℝ)
93 letr 10344 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℝ ∧ (⌊‘((log‘3) / (log‘𝑃))) ∈ ℝ ∧ ((log‘3) / (log‘𝑃)) ∈ ℝ) → ((𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) ∧ (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃))) → 𝑀 ≤ ((log‘3) / (log‘𝑃))))
9478, 91, 92, 93syl3anc 1477 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) ∧ (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃))) → 𝑀 ≤ ((log‘3) / (log‘𝑃))))
95 1red 10268 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℝ)
96 letr 10344 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ ℝ ∧ ((log‘3) / (log‘𝑃)) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑀 ≤ ((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 ≤ 1))
9778, 92, 95, 96syl3anc 1477 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 ≤ ((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 ≤ 1))
98 nnge1 11259 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℕ → 1 ≤ 𝑀)
99 eqcom 2768 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 = 1 ↔ 1 = 𝑀)
100 1red 10268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 1 ∈ ℝ)
101100, 77letri3d 10392 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 ∈ ℕ → (1 = 𝑀 ↔ (1 ≤ 𝑀𝑀 ≤ 1)))
10299, 101syl5rbb 273 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ℕ → ((1 ≤ 𝑀𝑀 ≤ 1) ↔ 𝑀 = 1))
103102biimpd 219 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℕ → ((1 ≤ 𝑀𝑀 ≤ 1) → 𝑀 = 1))
10498, 103mpand 713 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ℕ → (𝑀 ≤ 1 → 𝑀 = 1))
1051043ad2ant2 1129 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ 1 → 𝑀 = 1))
10697, 105syld 47 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 ≤ ((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 = 1))
107106expd 451 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ ((log‘3) / (log‘𝑃)) → (((log‘3) / (log‘𝑃)) ≤ 1 → 𝑀 = 1)))
10894, 107syld 47 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) ∧ (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃))) → (((log‘3) / (log‘𝑃)) ≤ 1 → 𝑀 = 1)))
10976, 108mpan2d 712 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) → (((log‘3) / (log‘𝑃)) ≤ 1 → 𝑀 = 1)))
11074, 109mpid 44 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) → 𝑀 = 1))
11157, 110sylbid 230 . . . . . . . . . . . . . 14 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑃𝑀) ≤ 3 → 𝑀 = 1))
11246, 111syld 47 . . . . . . . . . . . . 13 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (3 = (𝑃𝑀) → 𝑀 = 1))
113112adantl 473 . . . . . . . . . . . 12 ((𝑘 = 1 ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (3 = (𝑃𝑀) → 𝑀 = 1))
11432, 113sylbid 230 . . . . . . . . . . 11 ((𝑘 = 1 ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) → 𝑀 = 1))
115114ex 449 . . . . . . . . . 10 (𝑘 = 1 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) → 𝑀 = 1)))
116 sq1 13173 . . . . . . . . . . . . . . 15 (1↑2) = 1
117116eqcomi 2770 . . . . . . . . . . . . . 14 1 = (1↑2)
118117oveq2i 6826 . . . . . . . . . . . . 13 (((2↑𝑘)↑2) − 1) = (((2↑𝑘)↑2) − (1↑2))
119118eqeq1i 2766 . . . . . . . . . . . 12 ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) ↔ (((2↑𝑘)↑2) − (1↑2)) = (𝑃𝑀))
120 eqcom 2768 . . . . . . . . . . . . 13 ((((2↑𝑘)↑2) − (1↑2)) = (𝑃𝑀) ↔ (𝑃𝑀) = (((2↑𝑘)↑2) − (1↑2)))
1219a1i 11 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ‘2) → 2 ∈ ℕ0)
122 eluzge2nn0 11941 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ‘2) → 𝑘 ∈ ℕ0)
123121, 122nn0expcld 13246 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ‘2) → (2↑𝑘) ∈ ℕ0)
124123adantr 472 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (ℤ‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (2↑𝑘) ∈ ℕ0)
125 1nn0 11521 . . . . . . . . . . . . . . . 16 1 ∈ ℕ0
126125a1i 11 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (ℤ‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → 1 ∈ ℕ0)
127 1p1e2 11347 . . . . . . . . . . . . . . . . . 18 (1 + 1) = 2
12822eqcomi 2770 . . . . . . . . . . . . . . . . . 18 2 = (2↑1)
129127, 128eqtri 2783 . . . . . . . . . . . . . . . . 17 (1 + 1) = (2↑1)
130 eluz2gt1 11974 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (ℤ‘2) → 1 < 𝑘)
131 2re 11303 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
132131a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (ℤ‘2) → 2 ∈ ℝ)
133 1zzd 11621 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (ℤ‘2) → 1 ∈ ℤ)
134 eluzelz 11910 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (ℤ‘2) → 𝑘 ∈ ℤ)
135 1lt2 11407 . . . . . . . . . . . . . . . . . . . 20 1 < 2
136135a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (ℤ‘2) → 1 < 2)
137132, 133, 134, 136ltexp2d 13253 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (ℤ‘2) → (1 < 𝑘 ↔ (2↑1) < (2↑𝑘)))
138130, 137mpbid 222 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ‘2) → (2↑1) < (2↑𝑘))
139129, 138syl5eqbr 4840 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ‘2) → (1 + 1) < (2↑𝑘))
140139adantr 472 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (ℤ‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (1 + 1) < (2↑𝑘))
14134, 39anim12i 591 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ) → (𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ0))
1421413adant3 1127 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ0))
143142adantl 473 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (ℤ‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ0))
144 difsqpwdvds 15814 . . . . . . . . . . . . . . 15 ((((2↑𝑘) ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ (1 + 1) < (2↑𝑘)) ∧ (𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ0)) → ((𝑃𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑃 ∥ (2 · 1)))
145124, 126, 140, 143, 144syl31anc 1480 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑃 ∥ (2 · 1)))
146 2t1e2 11389 . . . . . . . . . . . . . . . . . . 19 (2 · 1) = 2
147146breq2i 4813 . . . . . . . . . . . . . . . . . 18 (𝑃 ∥ (2 · 1) ↔ 𝑃 ∥ 2)
148 prmuz2 15631 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
14934, 148syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ‘2))
150 2prm 15628 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℙ
151 dvdsprm 15638 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ (ℤ‘2) ∧ 2 ∈ ℙ) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
152149, 150, 151sylancl 697 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
153147, 152syl5bb 272 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ (2 · 1) ↔ 𝑃 = 2))
154 eldifsn 4463 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (ℙ ∖ {2}) ↔ (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
155 eqneqall 2944 . . . . . . . . . . . . . . . . . . 19 (𝑃 = 2 → (𝑃 ≠ 2 → 𝑀 = 1))
156155com12 32 . . . . . . . . . . . . . . . . . 18 (𝑃 ≠ 2 → (𝑃 = 2 → 𝑀 = 1))
157154, 156simplbiim 661 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 = 2 → 𝑀 = 1))
158153, 157sylbid 230 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ (2 · 1) → 𝑀 = 1))
1591583ad2ant1 1128 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑃 ∥ (2 · 1) → 𝑀 = 1))
160159adantl 473 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℤ‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃 ∥ (2 · 1) → 𝑀 = 1))
161145, 160syld 47 . . . . . . . . . . . . 13 ((𝑘 ∈ (ℤ‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑀 = 1))
162120, 161syl5bi 232 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((((2↑𝑘)↑2) − (1↑2)) = (𝑃𝑀) → 𝑀 = 1))
163119, 162syl5bi 232 . . . . . . . . . . 11 ((𝑘 ∈ (ℤ‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) → 𝑀 = 1))
164163ex 449 . . . . . . . . . 10 (𝑘 ∈ (ℤ‘2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) → 𝑀 = 1)))
165115, 164jaoi 393 . . . . . . . . 9 ((𝑘 = 1 ∨ 𝑘 ∈ (ℤ‘2)) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) → 𝑀 = 1)))
16618, 165sylbi 207 . . . . . . . 8 (𝑘 ∈ ℕ → ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) → 𝑀 = 1)))
167166impcom 445 . . . . . . 7 (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) → 𝑀 = 1))
168167adantr 472 . . . . . 6 ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → ((((2↑𝑘)↑2) − 1) = (𝑃𝑀) → 𝑀 = 1))
16917, 168sylbid 230 . . . . 5 ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → (((2↑𝑁) − 1) = (𝑃𝑀) → 𝑀 = 1))
170169ex 449 . . . 4 (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) = 𝑁 → (((2↑𝑁) − 1) = (𝑃𝑀) → 𝑀 = 1)))
171170rexlimdva 3170 . . 3 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (∃𝑘 ∈ ℕ (2 · 𝑘) = 𝑁 → (((2↑𝑁) − 1) = (𝑃𝑀) → 𝑀 = 1)))
1722, 171sylbid 230 . 2 ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 ∥ 𝑁 → (((2↑𝑁) − 1) = (𝑃𝑀) → 𝑀 = 1)))
1731723imp 1102 1 (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃𝑀)) → 𝑀 = 1)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1632  wcel 2140  wne 2933  wrex 3052  cdif 3713  {csn 4322   class class class wbr 4805  cfv 6050  (class class class)co 6815  cc 10147  cr 10148  0cc0 10149  1c1 10150   + caddc 10152   · cmul 10154   < clt 10287  cle 10288  cmin 10479   / cdiv 10897  cn 11233  2c2 11283  3c3 11284  4c4 11285  0cn0 11505  cz 11590  cuz 11900  +crp 12046  cfl 12806  cexp 13075  cdvds 15203  cprime 15608  logclog 24522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-inf2 8714  ax-cnex 10205  ax-resscn 10206  ax-1cn 10207  ax-icn 10208  ax-addcl 10209  ax-addrcl 10210  ax-mulcl 10211  ax-mulrcl 10212  ax-mulcom 10213  ax-addass 10214  ax-mulass 10215  ax-distr 10216  ax-i2m1 10217  ax-1ne0 10218  ax-1rid 10219  ax-rnegex 10220  ax-rrecex 10221  ax-cnre 10222  ax-pre-lttri 10223  ax-pre-lttrn 10224  ax-pre-ltadd 10225  ax-pre-mulgt0 10226  ax-pre-sup 10227  ax-addf 10228  ax-mulf 10229
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-int 4629  df-iun 4675  df-iin 4676  df-br 4806  df-opab 4866  df-mpt 4883  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-se 5227  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-pred 5842  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-isom 6059  df-riota 6776  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-of 7064  df-om 7233  df-1st 7335  df-2nd 7336  df-supp 7466  df-wrecs 7578  df-recs 7639  df-rdg 7677  df-1o 7731  df-2o 7732  df-oadd 7735  df-er 7914  df-map 8028  df-pm 8029  df-ixp 8078  df-en 8125  df-dom 8126  df-sdom 8127  df-fin 8128  df-fsupp 8444  df-fi 8485  df-sup 8516  df-inf 8517  df-oi 8583  df-card 8976  df-cda 9203  df-pnf 10289  df-mnf 10290  df-xr 10291  df-ltxr 10292  df-le 10293  df-sub 10481  df-neg 10482  df-div 10898  df-nn 11234  df-2 11292  df-3 11293  df-4 11294  df-5 11295  df-6 11296  df-7 11297  df-8 11298  df-9 11299  df-n0 11506  df-z 11591  df-dec 11707  df-uz 11901  df-q 12003  df-rp 12047  df-xneg 12160  df-xadd 12161  df-xmul 12162  df-ioo 12393  df-ioc 12394  df-ico 12395  df-icc 12396  df-fz 12541  df-fzo 12681  df-fl 12808  df-mod 12884  df-seq 13017  df-exp 13076  df-fac 13276  df-bc 13305  df-hash 13333  df-shft 14027  df-cj 14059  df-re 14060  df-im 14061  df-sqrt 14195  df-abs 14196  df-limsup 14422  df-clim 14439  df-rlim 14440  df-sum 14637  df-ef 15018  df-sin 15020  df-cos 15021  df-pi 15023  df-dvds 15204  df-gcd 15440  df-prm 15609  df-pc 15765  df-struct 16082  df-ndx 16083  df-slot 16084  df-base 16086  df-sets 16087  df-ress 16088  df-plusg 16177  df-mulr 16178  df-starv 16179  df-sca 16180  df-vsca 16181  df-ip 16182  df-tset 16183  df-ple 16184  df-ds 16187  df-unif 16188  df-hom 16189  df-cco 16190  df-rest 16306  df-topn 16307  df-0g 16325  df-gsum 16326  df-topgen 16327  df-pt 16328  df-prds 16331  df-xrs 16385  df-qtop 16390  df-imas 16391  df-xps 16393  df-mre 16469  df-mrc 16470  df-acs 16472  df-mgm 17464  df-sgrp 17506  df-mnd 17517  df-submnd 17558  df-mulg 17763  df-cntz 17971  df-cmn 18416  df-psmet 19961  df-xmet 19962  df-met 19963  df-bl 19964  df-mopn 19965  df-fbas 19966  df-fg 19967  df-cnfld 19970  df-top 20922  df-topon 20939  df-topsp 20960  df-bases 20973  df-cld 21046  df-ntr 21047  df-cls 21048  df-nei 21125  df-lp 21163  df-perf 21164  df-cn 21254  df-cnp 21255  df-haus 21342  df-tx 21588  df-hmeo 21781  df-fil 21872  df-fm 21964  df-flim 21965  df-flf 21966  df-xms 22347  df-ms 22348  df-tms 22349  df-cncf 22903  df-limc 23850  df-dv 23851  df-log 24524
This theorem is referenced by:  lighneal  42057
  Copyright terms: Public domain W3C validator