Theorem lighneallem2 48896

Description: Lemma 2 for lighneal 48901. (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 16550	. . . 4 ⊢ (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℕ (2 · 𝑘) = 𝑁))
2	1	3ad2ant3 1153	. . 3 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℕ (2 · 𝑘) = 𝑁))
3		oveq2 7451	. . . . . . . . 9 ⊢ (𝑁 = (2 · 𝑘) → (2↑𝑁) = (2↑(2 · 𝑘)))
4	3	eqcoms 2771	. . . . . . . 8 ⊢ ((2 · 𝑘) = 𝑁 → (2↑𝑁) = (2↑(2 · 𝑘)))
5		2cnd 12448	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℂ)
6		nncn 12370	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
7	5, 6	mulcomd 11357	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) = (𝑘 · 2))
8	7	oveq2d 7459	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (2↑(2 · 𝑘)) = (2↑(𝑘 · 2)))
9		2nn0 12650	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ0
10	9	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℕ0)
11		nnnn0 12640	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
12	5, 10, 11	expmuld 14319	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (2↑(𝑘 · 2)) = ((2↑𝑘)↑2))
13	8, 12	eqtrd 2798	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (2↑(2 · 𝑘)) = ((2↑𝑘)↑2))
14	13	adantl 487	. . . . . . . 8 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (2↑(2 · 𝑘)) = ((2↑𝑘)↑2))
15	4, 14	sylan9eqr 2820	. . . . . . 7 ⊢ ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → (2↑𝑁) = ((2↑𝑘)↑2))
16	15	oveq1d 7458	. . . . . 6 ⊢ ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → ((2↑𝑁) − 1) = (((2↑𝑘)↑2) − 1))
17	16	eqeq1d 2765	. . . . 5 ⊢ ((((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑘 ∈ ℕ) ∧ (2 · 𝑘) = 𝑁) → (((2↑𝑁) − 1) = (𝑃↑𝑀) ↔ (((2↑𝑘)↑2) − 1) = (𝑃↑𝑀)))
18		elnn1uz2 13079	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ ↔ (𝑘 = 1 ∨ 𝑘 ∈ (ℤ≥‘2)))
19		oveq2 7451	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (2↑𝑘) = (2↑1))
20		2cn 12445	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
21		exp1 14237	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℂ → (2↑1) = 2)
22	20, 21	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (2↑1) = 2
23	19, 22	eqtrdi 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → (2↑𝑘) = 2)
24	23	oveq1d 7458	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → ((2↑𝑘)↑2) = (2↑2))
25	24	oveq1d 7458	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → (((2↑𝑘)↑2) − 1) = ((2↑2) − 1))
26		sq2 14367	. . . . . . . . . . . . . . . 16 ⊢ (2↑2) = 4
27	26	oveq1i 7453	. . . . . . . . . . . . . . 15 ⊢ ((2↑2) − 1) = (4 − 1)
28		4m1e3 12498	. . . . . . . . . . . . . . 15 ⊢ (4 − 1) = 3
29	27, 28	eqtri 2786	. . . . . . . . . . . . . 14 ⊢ ((2↑2) − 1) = 3
30	25, 29	eqtrdi 2814	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (((2↑𝑘)↑2) − 1) = 3)
31	30	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) ↔ 3 = (𝑃↑𝑀)))
32	31	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑘 = 1 ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) ↔ 3 = (𝑃↑𝑀)))
33		eqcom 2770	. . . . . . . . . . . . . 14 ⊢ (3 = (𝑃↑𝑀) ↔ (𝑃↑𝑀) = 3)
34		eldifi 4070	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
35		prmnn 16878	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
36		nnre 12369	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℝ)
37	34, 35, 36	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ)
38	37	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑃 ∈ ℝ)
39		nnnn0 12640	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
40	39	3ad2ant2 1152	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℕ0)
41	38, 40	reexpcld 14333	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑃↑𝑀) ∈ ℝ)
42	41	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑃↑𝑀) = 3) → (𝑃↑𝑀) ∈ ℝ)
43		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑃↑𝑀) = 3) → (𝑃↑𝑀) = 3)
44	42, 43	eqled 11440	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑃↑𝑀) = 3) → (𝑃↑𝑀) ≤ 3)
45	44	ex 418	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑃↑𝑀) = 3 → (𝑃↑𝑀) ≤ 3))
46	33, 45	biimtrid 245	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (3 = (𝑃↑𝑀) → (𝑃↑𝑀) ≤ 3))
47	35	nnred 12377	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
48		prmgt1 16902	. . . . . . . . . . . . . . . . . 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 12741	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
53	52	3ad2ant2 1152	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℤ)
54		3rp 13153	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℝ+
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 3 ∈ ℝ+)
56		efexple 27638	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℝ ∧ 1 < 𝑃) ∧ 𝑀 ∈ ℤ ∧ 3 ∈ ℝ+) → ((𝑃↑𝑀) ≤ 3 ↔ 𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃)))))
57	51, 53, 55, 56	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑃↑𝑀) ≤ 3 ↔ 𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃)))))
58		oddprmge3 16905	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ≥‘3))
59		eluzle 13005	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℤ≥‘3) → 3 ≤ 𝑃)
60	58, 59	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 3 ≤ 𝑃)
61	54	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 3 ∈ ℝ+)
62		nnrp 13159	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℝ+)
63	34, 35, 62	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ+)
64	61, 63	logled 26985	. . . . . . . . . . . . . . . . . 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 26933	. . . . . . . . . . . . . . . . . 18 ⊢ (3 ∈ ℝ+ → (log‘3) ∈ ℝ)
68	54, 67	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (log‘3) ∈ ℝ
69		rplogcl 26962	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ 1 < 𝑃) → (log‘𝑃) ∈ ℝ+)
70	34, 49, 69	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (log‘𝑃) ∈ ℝ+)
71	70	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (log‘𝑃) ∈ ℝ+)
72		divle1le 13219	. . . . . . . . . . . . . . . . 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 13998	. . . . . . . . . . . . . . . . 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 12369	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
78	77	3ad2ant2 1152	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℝ)
79	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (log‘3) ∈ ℝ)
80	62	relogcld 26981	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℕ → (log‘𝑃) ∈ ℝ)
81	34, 35, 80	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (log‘𝑃) ∈ ℝ)
82	35	nnrpd 13189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ+)
83		1red 11336	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ ℙ → 1 ∈ ℝ)
84	83, 48	gtned 11472	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℙ → 𝑃 ≠ 1)
85	82, 84	jca 521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ℝ+ ∧ 𝑃 ≠ 1))
86		logne0 26937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ ℝ+ ∧ 𝑃 ≠ 1) → (log‘𝑃) ≠ 0)
87	34, 85, 86	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (log‘𝑃) ≠ 0)
88	79, 81, 87	redivcld 12172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((log‘3) / (log‘𝑃)) ∈ ℝ)
89	88	flcld 13965	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (⌊‘((log‘3) / (log‘𝑃))) ∈ ℤ)
90	89	zred 12830	. . . . . . . . . . . . . . . . . . 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 11431	. . . . . . . . . . . . . . . . . 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 1399	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 ≤ (⌊‘((log‘3) / (log‘𝑃))) ∧ (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃))) → 𝑀 ≤ ((log‘3) / (log‘𝑃))))
95		1red 11336	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℝ)
96		letr 11431	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℝ ∧ ((log‘3) / (log‘𝑃)) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑀 ≤ ((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 ≤ 1))
97	78, 92, 95, 96	syl3anc 1399	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 ≤ ((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 ≤ 1))
98		nnge1 12393	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
99		eqcom 2770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 = 1 ↔ 1 = 𝑀)
100		1red 11336	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 ∈ ℕ → 1 ∈ ℝ)
101	100, 77	letri3d 11479	. . . . . . . . . . . . . . . . . . . . . . 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 14365	. . . . . . . . . . . . . 14 ⊢ (1↑2) = 1
117	116	eqcomi 2772	. . . . . . . . . . . . 13 ⊢ 1 = (1↑2)
118	117	oveq2i 7454	. . . . . . . . . . . 12 ⊢ (((2↑𝑘)↑2) − 1) = (((2↑𝑘)↑2) − (1↑2))
119	118	eqeq1i 2768	. . . . . . . . . . 11 ⊢ ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) ↔ (((2↑𝑘)↑2) − (1↑2)) = (𝑃↑𝑀))
120		eqcom 2770	. . . . . . . . . . . 12 ⊢ ((((2↑𝑘)↑2) − (1↑2)) = (𝑃↑𝑀) ↔ (𝑃↑𝑀) = (((2↑𝑘)↑2) − (1↑2)))
121	9	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ≥‘2) → 2 ∈ ℕ0)
122		eluzge2nn0 13046	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ≥‘2) → 𝑘 ∈ ℕ0)
123	121, 122	nn0expcld 14417	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℤ≥‘2) → (2↑𝑘) ∈ ℕ0)
124	123	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (2↑𝑘) ∈ ℕ0)
125		1nn0 12649	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ0
126	125	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → 1 ∈ ℕ0)
127		1p1e2 12493	. . . . . . . . . . . . . . . . 17 ⊢ (1 + 1) = 2
128	22	eqcomi 2772	. . . . . . . . . . . . . . . . 17 ⊢ 2 = (2↑1)
129	127, 128	eqtri 2786	. . . . . . . . . . . . . . . 16 ⊢ (1 + 1) = (2↑1)
130		eluz2gt1 13074	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (ℤ≥‘2) → 1 < 𝑘)
131		2re 12444	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℝ
132	131	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℤ≥‘2) → 2 ∈ ℝ)
133		1zzd 12754	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℤ≥‘2) → 1 ∈ ℤ)
134		eluzelz 13002	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℤ≥‘2) → 𝑘 ∈ ℤ)
135		1lt2 12542	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 2
136	135	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℤ≥‘2) → 1 < 2)
137	132, 133, 134, 136	ltexp2d 14422	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (ℤ≥‘2) → (1 < 𝑘 ↔ (2↑1) < (2↑𝑘)))
138	130, 137	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ≥‘2) → (2↑1) < (2↑𝑘))
139	129, 138	eqbrtrid 5143	. . . . . . . . . . . . . . 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 17094	. . . . . . . . . . . . . 14 ⊢ ((((2↑𝑘) ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ (1 + 1) < (2↑𝑘)) ∧ (𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ0)) → ((𝑃↑𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑃 ∥ (2 · 1)))
145	124, 126, 140, 143, 144	syl31anc 1401	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃↑𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑃 ∥ (2 · 1)))
146		2t1e2 12532	. . . . . . . . . . . . . . . . . 18 ⊢ (2 · 1) = 2
147	146	breq2i 5114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∥ (2 · 1) ↔ 𝑃 ∥ 2)
148		prmuz2 16900	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ≥‘2))
149	34, 148	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ≥‘2))
150		2prm 16896	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℙ
151		dvdsprm 16908	. . . . . . . . . . . . . . . . . 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 4748	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℙ ∖ {2}) ↔ (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
155		eqneqall 2970	. . . . . . . . . . . . . . . . . 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 3169	. . 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 1570   ∈ wcel 2147   ≠ wne 2959  ∃wrex 3090   ∖ cdif 4048  {csn 4588   class class class wbr 5106  ‘cfv 6558  (class class class)co 7443  ℂcc 11225  ℝcr 11226  0cc0 11227  1c1 11228   + caddc 11230   · cmul 11232   < clt 11370   ≤ cle 11371   − cmin 11568   / cdiv 12000  ℕcn 12362  2c2 12424  3c3 12425  4c4 12426  ℕ₀cn0 12633  ℤcz 12720  ℤ_≥cuz 12992  ℝ⁺crp 13147  ⌊cfl 13957  ↑cexp 14231   ∥ cdvds 16451  ℙcprime 16875  logclog 26912

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-inf2 9669  ax-cnex 11283  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304  ax-pre-sup 11305  ax-addf 11306

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-isom 6567  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-of 7717  df-om 7902  df-1st 8025  df-2nd 8026  df-supp 8205  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-1o 8504  df-2o 8505  df-er 8745  df-map 8877  df-pm 8878  df-ixp 8954  df-en 9002  df-dom 9003  df-sdom 9004  df-fin 9005  df-fsupp 9382  df-fi 9430  df-sup 9461  df-inf 9462  df-oi 9531  df-card 10047  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-div 12001  df-nn 12363  df-2 12432  df-3 12433  df-4 12434  df-5 12435  df-6 12436  df-7 12437  df-8 12438  df-9 12439  df-n0 12634  df-z 12721  df-dec 12842  df-uz 12993  df-q 13103  df-rp 13148  df-xneg 13268  df-xadd 13269  df-xmul 13270  df-ioo 13507  df-ioc 13508  df-ico 13509  df-icc 13510  df-fz 13667  df-fzo 13816  df-fl 13959  df-mod 14037  df-seq 14172  df-exp 14232  df-fac 14445  df-bc 14474  df-hash 14502  df-shft 15249  df-cj 15295  df-re 15296  df-im 15297  df-sqrt 15431  df-abs 15432  df-limsup 15667  df-clim 15684  df-rlim 15685  df-sum 15883  df-ef 16262  df-sin 16264  df-cos 16265  df-pi 16267  df-dvds 16452  df-gcd 16694  df-prm 16876  df-pc 17044  df-struct 17354  df-sets 17371  df-slot 17389  df-ndx 17401  df-base 17417  df-ress 17438  df-plusg 17470  df-mulr 17471  df-starv 17472  df-sca 17473  df-vsca 17474  df-ip 17475  df-tset 17476  df-ple 17477  df-ds 17479  df-unif 17480  df-hom 17481  df-cco 17482  df-rest 17622  df-topn 17623  df-0g 17641  df-gsum 17642  df-topgen 17643  df-pt 17644  df-prds 17647  df-xrs 17703  df-qtop 17708  df-imas 17709  df-xps 17711  df-mre 17785  df-mrc 17786  df-acs 17788  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-submnd 19008  df-mulg 19307  df-cntz 19561  df-cmn 20026  df-psmet 21700  df-xmet 21701  df-met 21702  df-bl 21703  df-mopn 21704  df-fbas 21705  df-fg 21706  df-cnfld 21709  df-top 23242  df-topon 23259  df-topsp 23281  df-bases 23294  df-cld 23367  df-ntr 23368  df-cls 23369  df-nei 23446  df-lp 23484  df-perf 23485  df-cn 23575  df-cnp 23576  df-haus 23663  df-tx 23911  df-hmeo 24104  df-fil 24195  df-fm 24287  df-flim 24288  df-flf 24289  df-xms 24669  df-ms 24670  df-tms 24671  df-cncf 25229  df-limc 26216  df-dv 26217  df-log 26914

This theorem is used by:  lighneal  48901