Theorem logbgcd1irr 15483

Description: The logarithm of an integer greater than 1 to an integer base greater than 1 is not rational if the argument and the base are relatively prime. For example, (2 log_b 9) ∈ (ℝ ∖ ℚ). (Contributed by AV, 29-Dec-2022.)

Assertion

Ref	Expression
logbgcd1irr	⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → (𝐵 logb 𝑋) ∈ (ℝ ∖ ℚ))

Proof of Theorem logbgcd1irr

Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluz2nn 9694	. . . . 5 ⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 ∈ ℕ)
2	1	nnrpd 9823	. . . 4 ⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 ∈ ℝ+)
3	2	3ad2ant2 1022	. . 3 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → 𝐵 ∈ ℝ+)
4		1red 8094	. . . . 5 ⊢ (𝐵 ∈ (ℤ≥‘2) → 1 ∈ ℝ)
5		eluzelre 9665	. . . . 5 ⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 ∈ ℝ)
6		eluz2gt1 9730	. . . . 5 ⊢ (𝐵 ∈ (ℤ≥‘2) → 1 < 𝐵)
7	4, 5, 6	gtapd 8717	. . . 4 ⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 # 1)
8	7	3ad2ant2 1022	. . 3 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → 𝐵 # 1)
9		eluz2nn 9694	. . . . 5 ⊢ (𝑋 ∈ (ℤ≥‘2) → 𝑋 ∈ ℕ)
10	9	nnrpd 9823	. . . 4 ⊢ (𝑋 ∈ (ℤ≥‘2) → 𝑋 ∈ ℝ+)
11	10	3ad2ant1 1021	. . 3 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → 𝑋 ∈ ℝ+)
12		rplogbcl 15462	. . 3 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) ∈ ℝ)
13	3, 8, 11, 12	syl3anc 1250	. 2 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → (𝐵 logb 𝑋) ∈ ℝ)
14		eluz2gt1 9730	. . . . . . . . . 10 ⊢ (𝑋 ∈ (ℤ≥‘2) → 1 < 𝑋)
15	14	adantr 276	. . . . . . . . 9 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → 1 < 𝑋)
16	9	adantr 276	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → 𝑋 ∈ ℕ)
17	16	nnrpd 9823	. . . . . . . . . 10 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → 𝑋 ∈ ℝ+)
18	1	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → 𝐵 ∈ ℕ)
19	18	nnrpd 9823	. . . . . . . . . 10 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → 𝐵 ∈ ℝ+)
20	6	adantl 277	. . . . . . . . . 10 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → 1 < 𝐵)
21		logbgt0b 15482	. . . . . . . . . 10 ⊢ ((𝑋 ∈ ℝ+ ∧ (𝐵 ∈ ℝ+ ∧ 1 < 𝐵)) → (0 < (𝐵 logb 𝑋) ↔ 1 < 𝑋))
22	17, 19, 20, 21	syl12anc 1248	. . . . . . . . 9 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → (0 < (𝐵 logb 𝑋) ↔ 1 < 𝑋))
23	15, 22	mpbird 167	. . . . . . . 8 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → 0 < (𝐵 logb 𝑋))
24	23	anim1ci 341	. . . . . . 7 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝐵 logb 𝑋) ∈ ℚ) → ((𝐵 logb 𝑋) ∈ ℚ ∧ 0 < (𝐵 logb 𝑋)))
25		elpq 9777	. . . . . . 7 ⊢ (((𝐵 logb 𝑋) ∈ ℚ ∧ 0 < (𝐵 logb 𝑋)) → ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (𝐵 logb 𝑋) = (𝑚 / 𝑛))
26	24, 25	syl 14	. . . . . 6 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝐵 logb 𝑋) ∈ ℚ) → ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (𝐵 logb 𝑋) = (𝑚 / 𝑛))
27	26	ex 115	. . . . 5 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → ((𝐵 logb 𝑋) ∈ ℚ → ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (𝐵 logb 𝑋) = (𝑚 / 𝑛)))
28		oveq2 5959	. . . . . . . . . 10 ⊢ ((𝑚 / 𝑛) = (𝐵 logb 𝑋) → (𝐵↑𝑐(𝑚 / 𝑛)) = (𝐵↑𝑐(𝐵 logb 𝑋)))
29	28	eqcoms 2209	. . . . . . . . 9 ⊢ ((𝐵 logb 𝑋) = (𝑚 / 𝑛) → (𝐵↑𝑐(𝑚 / 𝑛)) = (𝐵↑𝑐(𝐵 logb 𝑋)))
30	7	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → 𝐵 # 1)
31		rpcxplogb 15480	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋)
32	19, 30, 17, 31	syl3anc 1250	. . . . . . . . . 10 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋)
33	32	adantr 276	. . . . . . . . 9 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋)
34	29, 33	sylan9eqr 2261	. . . . . . . 8 ⊢ ((((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝐵 logb 𝑋) = (𝑚 / 𝑛)) → (𝐵↑𝑐(𝑚 / 𝑛)) = 𝑋)
35	34	ex 115	. . . . . . 7 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐵 logb 𝑋) = (𝑚 / 𝑛) → (𝐵↑𝑐(𝑚 / 𝑛)) = 𝑋))
36		oveq1 5958	. . . . . . . 8 ⊢ ((𝐵↑𝑐(𝑚 / 𝑛)) = 𝑋 → ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛) = (𝑋↑𝑛))
37	19	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝐵 ∈ ℝ+)
38		nnrp 9792	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
39	38	ad2antrl 490	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑚 ∈ ℝ+)
40		nnrp 9792	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
41	40	ad2antll 491	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑛 ∈ ℝ+)
42	39, 41	rpdivcld 9843	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝑚 / 𝑛) ∈ ℝ+)
43	42	rpred 9825	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝑚 / 𝑛) ∈ ℝ)
44		nncn 9051	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
45	44	ad2antll 491	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑛 ∈ ℂ)
46	37, 43, 45	cxpmuld 15453	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝐵↑𝑐((𝑚 / 𝑛) · 𝑛)) = ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑐𝑛))
47	39	rpcnd 9827	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑚 ∈ ℂ)
48	41	rpap0d 9831	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑛 # 0)
49	47, 45, 48	divcanap1d 8871	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝑚 / 𝑛) · 𝑛) = 𝑚)
50	49	oveq2d 5967	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝐵↑𝑐((𝑚 / 𝑛) · 𝑛)) = (𝐵↑𝑐𝑚))
51	1	ad2antlr 489	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝐵 ∈ ℕ)
52		nnz 9398	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
53	52	ad2antrl 490	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑚 ∈ ℤ)
54		cxpexpnn 15412	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (𝐵↑𝑐𝑚) = (𝐵↑𝑚))
55	51, 53, 54	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝐵↑𝑐𝑚) = (𝐵↑𝑚))
56	50, 55	eqtrd 2239	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝐵↑𝑐((𝑚 / 𝑛) · 𝑛)) = (𝐵↑𝑚))
57	37, 43	rpcxpcld 15449	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝐵↑𝑐(𝑚 / 𝑛)) ∈ ℝ+)
58		nnz 9398	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
59	58	ad2antll 491	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑛 ∈ ℤ)
60		cxpexprp 15411	. . . . . . . . . . . 12 ⊢ (((𝐵↑𝑐(𝑚 / 𝑛)) ∈ ℝ+ ∧ 𝑛 ∈ ℤ) → ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑐𝑛) = ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛))
61	57, 59, 60	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑐𝑛) = ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛))
62	46, 56, 61	3eqtr3rd 2248	. . . . . . . . . 10 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛) = (𝐵↑𝑚))
63	62	eqeq1d 2215	. . . . . . . . 9 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛) = (𝑋↑𝑛) ↔ (𝐵↑𝑚) = (𝑋↑𝑛)))
64		simpr 110	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
65		rplpwr 12392	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → ((𝑋 gcd 𝐵) = 1 → ((𝑋↑𝑛) gcd 𝐵) = 1))
66	16, 18, 64, 65	syl2an3an 1311	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝑋 gcd 𝐵) = 1 → ((𝑋↑𝑛) gcd 𝐵) = 1))
67		oveq1 5958	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋↑𝑛) = (𝐵↑𝑚) → ((𝑋↑𝑛) gcd 𝐵) = ((𝐵↑𝑚) gcd 𝐵))
68	67	eqeq1d 2215	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋↑𝑛) = (𝐵↑𝑚) → (((𝑋↑𝑛) gcd 𝐵) = 1 ↔ ((𝐵↑𝑚) gcd 𝐵) = 1))
69	68	eqcoms 2209	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵↑𝑚) = (𝑋↑𝑛) → (((𝑋↑𝑛) gcd 𝐵) = 1 ↔ ((𝐵↑𝑚) gcd 𝐵) = 1))
70	69	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝐵↑𝑚) = (𝑋↑𝑛)) → (((𝑋↑𝑛) gcd 𝐵) = 1 ↔ ((𝐵↑𝑚) gcd 𝐵) = 1))
71		eluzelz 9664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 ∈ ℤ)
72	71	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → 𝐵 ∈ ℤ)
73		simpl 109	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) → 𝑚 ∈ ℕ)
74		rpexp 12519	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑚 ∈ ℕ) → (((𝐵↑𝑚) gcd 𝐵) = 1 ↔ (𝐵 gcd 𝐵) = 1))
75	72, 72, 73, 74	syl2an3an 1311	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝐵↑𝑚) gcd 𝐵) = 1 ↔ (𝐵 gcd 𝐵) = 1))
76		gcdid 12351	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ∈ ℤ → (𝐵 gcd 𝐵) = (abs‘𝐵))
77	71, 76	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ (ℤ≥‘2) → (𝐵 gcd 𝐵) = (abs‘𝐵))
78		nnnn0 9309	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℕ0)
79		nn0ge0 9327	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐵 ∈ ℕ0 → 0 ≤ 𝐵)
80	1, 78, 79	3syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ∈ (ℤ≥‘2) → 0 ≤ 𝐵)
81	5, 80	absidd 11522	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ (ℤ≥‘2) → (abs‘𝐵) = 𝐵)
82	77, 81	eqtrd 2239	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ (ℤ≥‘2) → (𝐵 gcd 𝐵) = 𝐵)
83	82	eqeq1d 2215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (ℤ≥‘2) → ((𝐵 gcd 𝐵) = 1 ↔ 𝐵 = 1))
84	83	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐵 gcd 𝐵) = 1 ↔ 𝐵 = 1))
85	4, 6	gtned 8192	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 ≠ 1)
86		eqneqall 2387	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 = 1 → (𝐵 ≠ 1 → ⊥))
87	85, 86	syl5com 29	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (ℤ≥‘2) → (𝐵 = 1 → ⊥))
88	87	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝐵 = 1 → ⊥))
89	84, 88	sylbid 150	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐵 gcd 𝐵) = 1 → ⊥))
90	75, 89	sylbid 150	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝐵↑𝑚) gcd 𝐵) = 1 → ⊥))
91	90	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝐵↑𝑚) = (𝑋↑𝑛)) → (((𝐵↑𝑚) gcd 𝐵) = 1 → ⊥))
92	70, 91	sylbid 150	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝐵↑𝑚) = (𝑋↑𝑛)) → (((𝑋↑𝑛) gcd 𝐵) = 1 → ⊥))
93	92	ex 115	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐵↑𝑚) = (𝑋↑𝑛) → (((𝑋↑𝑛) gcd 𝐵) = 1 → ⊥)))
94	93	com23 78	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑋↑𝑛) gcd 𝐵) = 1 → ((𝐵↑𝑚) = (𝑋↑𝑛) → ⊥)))
95	66, 94	syld 45	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝑋 gcd 𝐵) = 1 → ((𝐵↑𝑚) = (𝑋↑𝑛) → ⊥)))
96		dfnot 1391	. . . . . . . . . . 11 ⊢ (¬ (𝐵↑𝑚) = (𝑋↑𝑛) ↔ ((𝐵↑𝑚) = (𝑋↑𝑛) → ⊥))
97	95, 96	imbitrrdi 162	. . . . . . . . . 10 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝑋 gcd 𝐵) = 1 → ¬ (𝐵↑𝑚) = (𝑋↑𝑛)))
98	97	con2d 625	. . . . . . . . 9 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐵↑𝑚) = (𝑋↑𝑛) → ¬ (𝑋 gcd 𝐵) = 1))
99	63, 98	sylbid 150	. . . . . . . 8 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛) = (𝑋↑𝑛) → ¬ (𝑋 gcd 𝐵) = 1))
100	36, 99	syl5 32	. . . . . . 7 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐵↑𝑐(𝑚 / 𝑛)) = 𝑋 → ¬ (𝑋 gcd 𝐵) = 1))
101	35, 100	syld 45	. . . . . 6 ⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐵 logb 𝑋) = (𝑚 / 𝑛) → ¬ (𝑋 gcd 𝐵) = 1))
102	101	rexlimdvva 2632	. . . . 5 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (𝐵 logb 𝑋) = (𝑚 / 𝑛) → ¬ (𝑋 gcd 𝐵) = 1))
103	27, 102	syld 45	. . . 4 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → ((𝐵 logb 𝑋) ∈ ℚ → ¬ (𝑋 gcd 𝐵) = 1))
104	103	con2d 625	. . 3 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → ((𝑋 gcd 𝐵) = 1 → ¬ (𝐵 logb 𝑋) ∈ ℚ))
105	104	3impia 1203	. 2 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → ¬ (𝐵 logb 𝑋) ∈ ℚ)
106	13, 105	eldifd 3177	1 ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → (𝐵 logb 𝑋) ∈ (ℝ ∖ ℚ))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 981   = wceq 1373  ⊥wfal 1378   ∈ wcel 2177   ≠ wne 2377  ∃wrex 2486   ∖ cdif 3164   class class class wbr 4047  ‘cfv 5276  (class class class)co 5951  ℂcc 7930  ℝcr 7931  0cc0 7932  1c1 7933   · cmul 7937   < clt 8114   ≤ cle 8115   # cap 8661   / cdiv 8752  ℕcn 9043  2c2 9094  ℕ₀cn0 9302  ℤcz 9379  ℤ_≥cuz 9655  ℚcq 9747  ℝ⁺crp 9782  ↑cexp 10690  abscabs 11352   gcd cgcd 12318  ↑_𝑐ccxp 15373   log_b clogb 15459

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-coll 4163  ax-sep 4166  ax-nul 4174  ax-pow 4222  ax-pr 4257  ax-un 4484  ax-setind 4589  ax-iinf 4640  ax-cnex 8023  ax-resscn 8024  ax-1cn 8025  ax-1re 8026  ax-icn 8027  ax-addcl 8028  ax-addrcl 8029  ax-mulcl 8030  ax-mulrcl 8031  ax-addcom 8032  ax-mulcom 8033  ax-addass 8034  ax-mulass 8035  ax-distr 8036  ax-i2m1 8037  ax-0lt1 8038  ax-1rid 8039  ax-0id 8040  ax-rnegex 8041  ax-precex 8042  ax-cnre 8043  ax-pre-ltirr 8044  ax-pre-ltwlin 8045  ax-pre-lttrn 8046  ax-pre-apti 8047  ax-pre-ltadd 8048  ax-pre-mulgt0 8049  ax-pre-mulext 8050  ax-arch 8051  ax-caucvg 8052  ax-pre-suploc 8053  ax-addf 8054  ax-mulf 8055

This theorem depends on definitions:  df-bi 117  df-stab 833  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-reu 2492  df-rmo 2493  df-rab 2494  df-v 2775  df-sbc 3000  df-csb 3095  df-dif 3169  df-un 3171  df-in 3173  df-ss 3180  df-nul 3462  df-if 3573  df-pw 3619  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-int 3888  df-iun 3931  df-disj 4024  df-br 4048  df-opab 4110  df-mpt 4111  df-tr 4147  df-id 4344  df-po 4347  df-iso 4348  df-iord 4417  df-on 4419  df-ilim 4420  df-suc 4422  df-iom 4643  df-xp 4685  df-rel 4686  df-cnv 4687  df-co 4688  df-dm 4689  df-rn 4690  df-res 4691  df-ima 4692  df-iota 5237  df-fun 5278  df-fn 5279  df-f 5280  df-f1 5281  df-fo 5282  df-f1o 5283  df-fv 5284  df-isom 5285  df-riota 5906  df-ov 5954  df-oprab 5955  df-mpo 5956  df-of 6165  df-1st 6233  df-2nd 6234  df-recs 6398  df-irdg 6463  df-frec 6484  df-1o 6509  df-2o 6510  df-oadd 6513  df-er 6627  df-map 6744  df-pm 6745  df-en 6835  df-dom 6836  df-fin 6837  df-sup 7093  df-inf 7094  df-pnf 8116  df-mnf 8117  df-xr 8118  df-ltxr 8119  df-le 8120  df-sub 8252  df-neg 8253  df-reap 8655  df-ap 8662  df-div 8753  df-inn 9044  df-2 9102  df-3 9103  df-4 9104  df-n0 9303  df-z 9380  df-uz 9656  df-q 9748  df-rp 9783  df-xneg 9901  df-xadd 9902  df-ioo 10021  df-ico 10023  df-icc 10024  df-fz 10138  df-fzo 10272  df-fl 10420  df-mod 10475  df-seqfrec 10600  df-exp 10691  df-fac 10878  df-bc 10900  df-ihash 10928  df-shft 11170  df-cj 11197  df-re 11198  df-im 11199  df-rsqrt 11353  df-abs 11354  df-clim 11634  df-sumdc 11709  df-ef 12003  df-e 12004  df-dvds 12143  df-gcd 12319  df-prm 12474  df-rest 13117  df-topgen 13136  df-psmet 14349  df-xmet 14350  df-met 14351  df-bl 14352  df-mopn 14353  df-top 14514  df-topon 14527  df-bases 14559  df-ntr 14612  df-cn 14704  df-cnp 14705  df-tx 14769  df-cncf 15087  df-limced 15172  df-dvap 15173  df-relog 15374  df-rpcxp 15375  df-logb 15460

This theorem is referenced by:  2logb9irr  15487  logbprmirr  15488