Theorem lighneallem2 48734

Description: Lemma 2 for lighneal 48739. (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.

Step	Hyp	Ref	Expression
1		evennn2n 16521	. . . 4 ⊢ (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℕ (2 · 𝑘) = 𝑁))
2	1	3ad2ant3 1153	. . 3 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℕ (2 · 𝑘) = 𝑁))
3		oveq2 7428	. . . . . . . . 9 ⊢ (𝑁 = (2 · 𝑘) → (2↑𝑁) = (2↑(2 · 𝑘)))
4	3	eqcoms 2768	. . . . . . . 8 ⊢ ((2 · 𝑘) = 𝑁 → (2↑𝑁) = (2↑(2 · 𝑘)))
5		2cnd 12421	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℂ)
6		nncn 12343	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
7	5, 6	mulcomd 11330	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) = (𝑘 · 2))
8	7	oveq2d 7436	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (2↑(2 · 𝑘)) = (2↑(𝑘 · 2)))
9		2nn0 12623	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ0
10	9	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℕ0)
11		nnnn0 12613	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
12	5, 10, 11	expmuld 14292	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (2↑(𝑘 · 2)) = ((2↑𝑘)↑2))
13	8, 12	eqtrd 2795	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (2↑(2 · 𝑘)) = ((2↑𝑘)↑2))
14	13	adantl 487	. . . . . . . 8 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (2↑(2 · 𝑘)) = ((2↑𝑘)↑2))
15	4, 14	sylan9eqr 2817	. . . . . . 7 ⊢ ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → (2↑𝑁) = ((2↑𝑘)↑2))
16	15	oveq1d 7435	. . . . . 6 ⊢ ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → ((2↑𝑁) − 1) = (((2↑𝑘)↑2) − 1))
17	16	eqeq1d 2762	. . . . 5 ⊢ ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → (((2↑𝑁) − 1) = (𝑃↑𝑀) ↔ (((2↑𝑘)↑2) − 1) = (𝑃↑𝑀)))
18		elnn1uz2 13052	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↔ (𝑘 = 1 ∨ 𝑘 ∈ (ℤ≥‘2)))
19		oveq2 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (2↑𝑘) = (2↑1))
20		2cn 12418	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
21		exp1 14210	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℂ → (2↑1) = 2)
22	20, 21	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (2↑1) = 2
23	19, 22	eqtrdi 2811	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → (2↑𝑘) = 2)
24	23	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → ((2↑𝑘)↑2) = (2↑2))
25	24	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → (((2↑𝑘)↑2) − 1) = ((2↑2) − 1))
26		sq2 14340	. . . . . . . . . . . . . . . 16 ⊢ (2↑2) = 4
27	26	oveq1i 7430	. . . . . . . . . . . . . . 15 ⊢ ((2↑2) − 1) = (4 − 1)
28		4m1e3 12471	. . . . . . . . . . . . . . 15 ⊢ (4 − 1) = 3
29	27, 28	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ ((2↑2) − 1) = 3
30	25, 29	eqtrdi 2811	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (((2↑𝑘)↑2) − 1) = 3)
31	30	eqeq1d 2762	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) ↔ 3 = (𝑃↑𝑀)))
32	31	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑘 = 1 ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) ↔ 3 = (𝑃↑𝑀)))
33		eqcom 2767	. . . . . . . . . . . . . 14 ⊢ (3 = (𝑃↑𝑀) ↔ (𝑃↑𝑀) = 3)
34		eldifi 4067	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
35		prmnn 16849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
36		nnre 12342	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℝ)
37	34, 35, 36	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ)
38	37	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑃 ∈ ℝ)
39		nnnn0 12613	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
40	39	3ad2ant2 1152	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℕ0)
41	38, 40	reexpcld 14306	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑃↑𝑀) ∈ ℝ)
42	41	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑃↑𝑀) = 3) → (𝑃↑𝑀) ∈ ℝ)
43		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑃↑𝑀) = 3) → (𝑃↑𝑀) = 3)
44	42, 43	eqled 11413	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑃↑𝑀) = 3) → (𝑃↑𝑀) ≤ 3)
45	44	ex 418	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑃↑𝑀) = 3 → (𝑃↑𝑀) ≤ 3))
46	33, 45	biimtrid 245	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (3 = (𝑃↑𝑀) → (𝑃↑𝑀) ≤ 3))
47	35	nnred 12350	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
48		prmgt1 16873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
49	47, 48	jca 521	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
50	34, 49	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
51	50	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
52		nnz 12714	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
53	52	3ad2ant2 1152	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℤ)
54		3rp 13126	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℝ+
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 3 ∈ ℝ+)
56		efexple 27608	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℝ ∧ 1 < 𝑃) ∧ 𝑀 ∈ ℤ ∧ 3 ∈ ℝ+) → ((𝑃↑𝑀) ≤ 3 ↔ 𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃)))))
57	51, 53, 55, 56	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑃↑𝑀) ≤ 3 ↔ 𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃)))))
58		oddprmge3 16876	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ≥‘3))
59		eluzle 12978	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℤ≥‘3) → 3 ≤ 𝑃)
60	58, 59	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 3 ≤ 𝑃)
61	54	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 3 ∈ ℝ+)
62		nnrp 13132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℝ+)
63	34, 35, 62	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ+)
64	61, 63	logled 26955	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (3 ≤ 𝑃 ↔ (log‘3) ≤ (log‘𝑃)))
65	60, 64	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (log‘3) ≤ (log‘𝑃))
66	65	3ad2ant1 1151	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (log‘3) ≤ (log‘𝑃))
67		relogcl 26903	. . . . . . . . . . . . . . . . . 18 ⊢ (3 ∈ ℝ+ → (log‘3) ∈ ℝ)
68	54, 67	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (log‘3) ∈ ℝ
69		rplogcl 26932	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ 1 < 𝑃) → (log‘𝑃) ∈ ℝ+)
70	34, 49, 69	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (log‘𝑃) ∈ ℝ+)
71	70	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (log‘𝑃) ∈ ℝ+)
72		divle1le 13192	. . . . . . . . . . . . . . . . 17 ⊢ (((log‘3) ∈ ℝ ∧ (log‘𝑃) ∈ ℝ+) → (((log‘3) / (log‘𝑃)) ≤ 1 ↔ (log‘3) ≤ (log‘𝑃)))
73	68, 71, 72	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((log‘3) / (log‘𝑃)) ≤ 1 ↔ (log‘3) ≤ (log‘𝑃)))
74	66, 73	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((log‘3) / (log‘𝑃)) ≤ 1)
75		fldivle 13971	. . . . . . . . . . . . . . . . 17 ⊢ (((log‘3) ∈ ℝ ∧ (log‘𝑃) ∈ ℝ+) → (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃)))
76	68, 71, 75	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃)))
77		nnre 12342	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
78	77	3ad2ant2 1152	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℝ)
79	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (log‘3) ∈ ℝ)
80	62	relogcld 26951	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℕ → (log‘𝑃) ∈ ℝ)
81	34, 35, 80	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (log‘𝑃) ∈ ℝ)
82	35	nnrpd 13162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ+)
83		1red 11309	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ ℙ → 1 ∈ ℝ)
84	83, 48	gtned 11445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℙ → 𝑃 ≠ 1)
85	82, 84	jca 521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ℝ+ ∧ 𝑃 ≠ 1))
86		logne0 26907	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ ℝ+ ∧ 𝑃 ≠ 1) → (log‘𝑃) ≠ 0)
87	34, 85, 86	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (log‘𝑃) ≠ 0)
88	79, 81, 87	redivcld 12145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((log‘3) / (log‘𝑃)) ∈ ℝ)
89	88	flcld 13938	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (⌊‘((log‘3) / (log‘𝑃))) ∈ ℤ)
90	89	zred 12803	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (⌊‘((log‘3) / (log‘𝑃))) ∈ ℝ)
91	90	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((log‘3) / (log‘𝑃))) ∈ ℝ)
92	88	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((log‘3) / (log‘𝑃)) ∈ ℝ)
93		letr 11404	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℝ ∧ (⌊‘((log‘3) / (log‘𝑃))) ∈ ℝ ∧ ((log‘3) / (log‘𝑃)) ∈ ℝ) → ((𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) ∧ (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃))) → 𝑀 ≤ ((log‘3) / (log‘𝑃))))
94	78, 91, 92, 93	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) ∧ (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃))) → 𝑀 ≤ ((log‘3) / (log‘𝑃))))
95		1red 11309	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℝ)
96		letr 11404	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℝ ∧ ((log‘3) / (log‘𝑃)) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑀 ≤ ((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 ≤ 1))
97	78, 92, 95, 96	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 ≤ ((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 ≤ 1))
98		nnge1 12366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
99		eqcom 2767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 = 1 ↔ 1 = 𝑀)
100		1red 11309	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 ∈ ℕ → 1 ∈ ℝ)
101	100, 77	letri3d 11452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℕ → (1 = 𝑀 ↔ (1 ≤ 𝑀 ∧ 𝑀 ≤ 1)))
102	99, 101	bitr2id 287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ → ((1 ≤ 𝑀 ∧ 𝑀 ≤ 1) ↔ 𝑀 = 1))
103	102	biimpd 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℕ → ((1 ≤ 𝑀 ∧ 𝑀 ≤ 1) → 𝑀 = 1))
104	98, 103	mpand 708	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ → (𝑀 ≤ 1 → 𝑀 = 1))
105	104	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ 1 → 𝑀 = 1))
106	97, 105	syld 48	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 ≤ ((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 = 1))
107	106	expd 421	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ ((log‘3) / (log‘𝑃)) → (((log‘3) / (log‘𝑃)) ≤ 1 → 𝑀 = 1)))
108	94, 107	syld 48	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) ∧ (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃))) → (((log‘3) / (log‘𝑃)) ≤ 1 → 𝑀 = 1)))
109	76, 108	mpan2d 707	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) → (((log‘3) / (log‘𝑃)) ≤ 1 → 𝑀 = 1)))
110	74, 109	mpid 45	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) → 𝑀 = 1))
111	57, 110	sylbid 243	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑃↑𝑀) ≤ 3 → 𝑀 = 1))
112	46, 111	syld 48	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (3 = (𝑃↑𝑀) → 𝑀 = 1))
113	112	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑘 = 1 ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (3 = (𝑃↑𝑀) → 𝑀 = 1))
114	32, 113	sylbid 243	. . . . . . . . . 10 ⊢ ((𝑘 = 1 ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1))
115	114	ex 418	. . . . . . . . 9 ⊢ (𝑘 = 1 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1)))
116		sq1 14338	. . . . . . . . . . . . . 14 ⊢ (1↑2) = 1
117	116	eqcomi 2769	. . . . . . . . . . . . 13 ⊢ 1 = (1↑2)
118	117	oveq2i 7431	. . . . . . . . . . . 12 ⊢ (((2↑𝑘)↑2) − 1) = (((2↑𝑘)↑2) − (1↑2))
119	118	eqeq1i 2765	. . . . . . . . . . 11 ⊢ ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) ↔ (((2↑𝑘)↑2) − (1↑2)) = (𝑃↑𝑀))
120		eqcom 2767	. . . . . . . . . . . 12 ⊢ ((((2↑𝑘)↑2) − (1↑2)) = (𝑃↑𝑀) ↔ (𝑃↑𝑀) = (((2↑𝑘)↑2) − (1↑2)))
121	9	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ≥‘2) → 2 ∈ ℕ0)
122		eluzge2nn0 13019	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ≥‘2) → 𝑘 ∈ ℕ0)
123	121, 122	nn0expcld 14390	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℤ≥‘2) → (2↑𝑘) ∈ ℕ0)
124	123	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (2↑𝑘) ∈ ℕ0)
125		1nn0 12622	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ0
126	125	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → 1 ∈ ℕ0)
127		1p1e2 12466	. . . . . . . . . . . . . . . . 17 ⊢ (1 + 1) = 2
128	22	eqcomi 2769	. . . . . . . . . . . . . . . . 17 ⊢ 2 = (2↑1)
129	127, 128	eqtri 2783	. . . . . . . . . . . . . . . 16 ⊢ (1 + 1) = (2↑1)
130		eluz2gt1 13047	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (ℤ≥‘2) → 1 < 𝑘)
131		2re 12417	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℝ
132	131	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℤ≥‘2) → 2 ∈ ℝ)
133		1zzd 12727	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℤ≥‘2) → 1 ∈ ℤ)
134		eluzelz 12975	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℤ≥‘2) → 𝑘 ∈ ℤ)
135		1lt2 12515	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 2
136	135	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℤ≥‘2) → 1 < 2)
137	132, 133, 134, 136	ltexp2d 14395	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (ℤ≥‘2) → (1 < 𝑘 ↔ (2↑1) < (2↑𝑘)))
138	130, 137	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ≥‘2) → (2↑1) < (2↑𝑘))
139	129, 138	eqbrtrid 5139	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℤ≥‘2) → (1 + 1) < (2↑𝑘))
140	139	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (1 + 1) < (2↑𝑘))
141	34, 39	anim12i 625	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ) → (𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ0))
142	141	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ0))
143	142	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ0))
144		difsqpwdvds 17065	. . . . . . . . . . . . . 14 ⊢ ((((2↑𝑘) ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ (1 + 1) < (2↑𝑘)) ∧ (𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ0)) → ((𝑃↑𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑃 ∥ (2 · 1)))
145	124, 126, 140, 143, 144	syl31anc 1400	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃↑𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑃 ∥ (2 · 1)))
146		2t1e2 12505	. . . . . . . . . . . . . . . . . 18 ⊢ (2 · 1) = 2
147	146	breq2i 5110	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∥ (2 · 1) ↔ 𝑃 ∥ 2)
148		prmuz2 16871	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ≥‘2))
149	34, 148	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ≥‘2))
150		2prm 16867	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℙ
151		dvdsprm 16879	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 2 ∈ ℙ) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
152	149, 150, 151	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
153	147, 152	bitrid 286	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ (2 · 1) ↔ 𝑃 = 2))
154		eldifsn 4747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℙ ∖ {2}) ↔ (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
155		eqneqall 2966	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 = 2 → (𝑃 ≠ 2 → 𝑀 = 1))
156	155	com12 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ≠ 2 → (𝑃 = 2 → 𝑀 = 1))
157	154, 156	simplbiim 514	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 = 2 → 𝑀 = 1))
158	153, 157	sylbid 243	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ (2 · 1) → 𝑀 = 1))
159	158	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑃 ∥ (2 · 1) → 𝑀 = 1))
160	159	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃 ∥ (2 · 1) → 𝑀 = 1))
161	145, 160	syld 48	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃↑𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑀 = 1))
162	120, 161	biimtrid 245	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((((2↑𝑘)↑2) − (1↑2)) = (𝑃↑𝑀) → 𝑀 = 1))
163	119, 162	biimtrid 245	. . . . . . . . . 10 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1))
164	163	ex 418	. . . . . . . . 9 ⊢ (𝑘 ∈ (ℤ≥‘2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1)))
165	115, 164	jaoi 871	. . . . . . . 8 ⊢ ((𝑘 = 1 ∨ 𝑘 ∈ (ℤ≥‘2)) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1)))
166	18, 165	sylbi 220	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1)))
167	166	impcom 413	. . . . . 6 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1))
168	167	adantr 486	. . . . 5 ⊢ ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1))
169	17, 168	sylbid 243	. . . 4 ⊢ ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1))
170	169	rexlimdva2 3165	. . 3 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (∃𝑘 ∈ ℕ (2 · 𝑘) = 𝑁 → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1)))
171	2, 170	sylbid 243	. 2 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 ∥ 𝑁 → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1)))
172	171	3imp 1128	1 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∃wrex 3086   ∖ cdif 4045  {csn 4583   class class class wbr 5102  ‘cfv 6538  (class class class)co 7420  ℂcc 11198  ℝcr 11199  0cc0 11200  1c1 11201   + caddc 11203   · cmul 11205   < clt 11343   ≤ cle 11344   − cmin 11541   / cdiv 11973  ℕcn 12335  2c2 12397  3c3 12398  4c4 12399  ℕ₀cn0 12606  ℤcz 12693  ℤ_≥cuz 12965  ℝ⁺crp 13120  ⌊cfl 13930  ↑cexp 14204   ∥ cdvds 16422  ℙcprime 16846  logclog 26882

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-inf2 9642  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277  ax-pre-sup 11278  ax-addf 11279

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7693  df-om 7878  df-1st 8001  df-2nd 8002  df-supp 8178  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-2o 8477  df-er 8717  df-map 8849  df-pm 8850  df-ixp 8926  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-fsupp 9354  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9504  df-card 10020  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974  df-nn 12336  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410  df-8 12411  df-9 12412  df-n0 12607  df-z 12694  df-dec 12815  df-uz 12966  df-q 13076  df-rp 13121  df-xneg 13241  df-xadd 13242  df-xmul 13243  df-ioo 13480  df-ioc 13481  df-ico 13482  df-icc 13483  df-fz 13640  df-fzo 13789  df-fl 13932  df-mod 14010  df-seq 14145  df-exp 14205  df-fac 14418  df-bc 14447  df-hash 14475  df-shft 15220  df-cj 15266  df-re 15267  df-im 15268  df-sqrt 15402  df-abs 15403  df-limsup 15638  df-clim 15655  df-rlim 15656  df-sum 15854  df-ef 16233  df-sin 16235  df-cos 16236  df-pi 16238  df-dvds 16423  df-gcd 16665  df-prm 16847  df-pc 17015  df-struct 17325  df-sets 17342  df-slot 17360  df-ndx 17372  df-base 17388  df-ress 17409  df-plusg 17441  df-mulr 17442  df-starv 17443  df-sca 17444  df-vsca 17445  df-ip 17446  df-tset 17447  df-ple 17448  df-ds 17450  df-unif 17451  df-hom 17452  df-cco 17453  df-rest 17593  df-topn 17594  df-0g 17612  df-gsum 17613  df-topgen 17614  df-pt 17615  df-prds 17618  df-xrs 17674  df-qtop 17679  df-imas 17680  df-xps 17682  df-mre 17756  df-mrc 17757  df-acs 17759  df-mgm 18816  df-sgrp 18908  df-mnd 18924  df-submnd 18979  df-mulg 19278  df-cntz 19531  df-cmn 19996  df-psmet 21670  df-xmet 21671  df-met 21672  df-bl 21673  df-mopn 21674  df-fbas 21675  df-fg 21676  df-cnfld 21679  df-top 23212  df-topon 23229  df-topsp 23251  df-bases 23264  df-cld 23337  df-ntr 23338  df-cls 23339  df-nei 23416  df-lp 23454  df-perf 23455  df-cn 23545  df-cnp 23546  df-haus 23633  df-tx 23881  df-hmeo 24074  df-fil 24165  df-fm 24257  df-flim 24258  df-flf 24259  df-xms 24639  df-ms 24640  df-tms 24641  df-cncf 25199  df-limc 26186  df-dv 26187  df-log 26884

This theorem is used by:  lighneal  48739