Theorem logbgcd1irr

Description: The logarithm of an integer greater than 1 to an integer base greater than 1 is an irrational number if the argument and the base are relatively prime. For example, ( 2 logb 9 ) e. ( RR \ QQ ) (see 2logb9irr ). (Contributed by AV, 29-Dec-2022)

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

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℕ )
2	1	nnrpd	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℝ+ )
3	2	3ad2ant2	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → 𝐵 ∈ ℝ+ )
4		eluz2nn	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) → 𝑋 ∈ ℕ )
5	4	nnrpd	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) → 𝑋 ∈ ℝ+ )
6	5	3ad2ant1	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → 𝑋 ∈ ℝ+ )
7		eluz2b3	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐵 ∈ ℕ ∧ 𝐵 ≠ 1 ) )
8	7	simprbi	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ≠ 1 )
9	8	3ad2ant2	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → 𝐵 ≠ 1 )
10	3 6 9	3jca	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → ( 𝐵 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) )
11		relogbcl	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 𝑋 ) ∈ ℝ )
12	10 11	syl	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → ( 𝐵 logb 𝑋 ) ∈ ℝ )
13		eluz2gt1	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑋 )
14	13	adantr	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 𝑋 )
15	4	adantr	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑋 ∈ ℕ )
16	15	nnrpd	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑋 ∈ ℝ+ )
17	1	adantl	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐵 ∈ ℕ )
18	17	nnrpd	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐵 ∈ ℝ+ )
19		eluz2gt1	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐵 )
20	19	adantl	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 𝐵 )
21		logbgt0b	⊢ ( ( 𝑋 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → ( 0 < ( 𝐵 logb 𝑋 ) ↔ 1 < 𝑋 ) )
22	16 18 20 21	syl12anc	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 0 < ( 𝐵 logb 𝑋 ) ↔ 1 < 𝑋 ) )
23	14 22	mpbird	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 0 < ( 𝐵 logb 𝑋 ) )
24	23	anim1ci	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐵 logb 𝑋 ) ∈ ℚ ) → ( ( 𝐵 logb 𝑋 ) ∈ ℚ ∧ 0 < ( 𝐵 logb 𝑋 ) ) )
25		elpq	⊢ ( ( ( 𝐵 logb 𝑋 ) ∈ ℚ ∧ 0 < ( 𝐵 logb 𝑋 ) ) → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) )
26	24 25	syl	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐵 logb 𝑋 ) ∈ ℚ ) → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) )
27	26	ex	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐵 logb 𝑋 ) ∈ ℚ → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) ) )
28		oveq2	⊢ ( ( 𝑚 / 𝑛 ) = ( 𝐵 logb 𝑋 ) → ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) = ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) )
29	28	eqcoms	⊢ ( ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) → ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) = ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) )
30		eluzelcn	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℂ )
31	30	adantl	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐵 ∈ ℂ )
32		nnne0	⊢ ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
33	1 32	syl	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ≠ 0 )
34	33 8	nelprd	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ¬ 𝐵 ∈ { 0 , 1 } )
35	34	adantl	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ 𝐵 ∈ { 0 , 1 } )
36	31 35	eldifd	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
37		eluzelcn	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) → 𝑋 ∈ ℂ )
38	37	adantr	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑋 ∈ ℂ )
39		nnne0	⊢ ( 𝑋 ∈ ℕ → 𝑋 ≠ 0 )
40		nelsn	⊢ ( 𝑋 ≠ 0 → ¬ 𝑋 ∈ { 0 } )
41	4 39 40	3syl	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) → ¬ 𝑋 ∈ { 0 } )
42	41	adantr	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ 𝑋 ∈ { 0 } )
43	38 42	eldifd	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑋 ∈ ( ℂ ∖ { 0 } ) )
44		cxplogb	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )
45	36 43 44	syl2anc	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )
46	45	adantr	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )
47	29 46	sylan9eqr	⊢ ( ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) ) → ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) = 𝑋 )
48	47	ex	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) → ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) = 𝑋 ) )
49		oveq1	⊢ ( ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) = 𝑋 → ( ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝑋 ↑ 𝑛 ) )
50	31	adantr	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝐵 ∈ ℂ )
51		nncn	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
52	51	adantr	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑚 ∈ ℂ )
53		nncn	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
54	53	adantl	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
55		nnne0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
56	55	adantl	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
57	52 54 56	3jca	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
58		divcl	⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) → ( 𝑚 / 𝑛 ) ∈ ℂ )
59	57 58	syl	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑚 / 𝑛 ) ∈ ℂ )
60	59	adantl	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝑚 / 𝑛 ) ∈ ℂ )
61		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
62	61	adantl	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
63	62	adantl	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝑛 ∈ ℕ0 )
64	50 60 63	3jca	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵 ∈ ℂ ∧ ( 𝑚 / 𝑛 ) ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) )
65		cxpmul2	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝑚 / 𝑛 ) ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝐵 ↑𝑐 ( ( 𝑚 / 𝑛 ) · 𝑛 ) ) = ( ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) )
66	65	eqcomd	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝑚 / 𝑛 ) ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝐵 ↑𝑐 ( ( 𝑚 / 𝑛 ) · 𝑛 ) ) )
67	64 66	syl	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝐵 ↑𝑐 ( ( 𝑚 / 𝑛 ) · 𝑛 ) ) )
68	57	adantl	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
69		divcan1	⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) → ( ( 𝑚 / 𝑛 ) · 𝑛 ) = 𝑚 )
70	68 69	syl	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝑚 / 𝑛 ) · 𝑛 ) = 𝑚 )
71	70	oveq2d	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵 ↑𝑐 ( ( 𝑚 / 𝑛 ) · 𝑛 ) ) = ( 𝐵 ↑𝑐 𝑚 ) )
72	33	adantl	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐵 ≠ 0 )
73	72	adantr	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝐵 ≠ 0 )
74		nnz	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
75	74	adantr	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑚 ∈ ℤ )
76	75	adantl	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝑚 ∈ ℤ )
77	50 73 76	cxpexpzd	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵 ↑𝑐 𝑚 ) = ( 𝐵 ↑ 𝑚 ) )
78	71 77	eqtrd	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵 ↑𝑐 ( ( 𝑚 / 𝑛 ) · 𝑛 ) ) = ( 𝐵 ↑ 𝑚 ) )
79	67 78	eqtrd	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝐵 ↑ 𝑚 ) )
80	79	eqeq1d	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝑋 ↑ 𝑛 ) ↔ ( 𝐵 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑛 ) ) )
81		simpr	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
82		rplpwr	⊢ ( ( 𝑋 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑋 gcd 𝐵 ) = 1 → ( ( 𝑋 ↑ 𝑛 ) gcd 𝐵 ) = 1 ) )
83	15 17 81 82	syl2an3an	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝑋 gcd 𝐵 ) = 1 → ( ( 𝑋 ↑ 𝑛 ) gcd 𝐵 ) = 1 ) )
84		oveq1	⊢ ( ( 𝑋 ↑ 𝑛 ) = ( 𝐵 ↑ 𝑚 ) → ( ( 𝑋 ↑ 𝑛 ) gcd 𝐵 ) = ( ( 𝐵 ↑ 𝑚 ) gcd 𝐵 ) )
85	84	eqeq1d	⊢ ( ( 𝑋 ↑ 𝑛 ) = ( 𝐵 ↑ 𝑚 ) → ( ( ( 𝑋 ↑ 𝑛 ) gcd 𝐵 ) = 1 ↔ ( ( 𝐵 ↑ 𝑚 ) gcd 𝐵 ) = 1 ) )
86	85	eqcoms	⊢ ( ( 𝐵 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑛 ) → ( ( ( 𝑋 ↑ 𝑛 ) gcd 𝐵 ) = 1 ↔ ( ( 𝐵 ↑ 𝑚 ) gcd 𝐵 ) = 1 ) )
87	86	adantl	⊢ ( ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝐵 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑛 ) ) → ( ( ( 𝑋 ↑ 𝑛 ) gcd 𝐵 ) = 1 ↔ ( ( 𝐵 ↑ 𝑚 ) gcd 𝐵 ) = 1 ) )
88		eluzelz	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℤ )
89	88	adantl	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐵 ∈ ℤ )
90		simpl	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑚 ∈ ℕ )
91		rpexp	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝐵 ↑ 𝑚 ) gcd 𝐵 ) = 1 ↔ ( 𝐵 gcd 𝐵 ) = 1 ) )
92	89 89 90 91	syl2an3an	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝐵 ↑ 𝑚 ) gcd 𝐵 ) = 1 ↔ ( 𝐵 gcd 𝐵 ) = 1 ) )
93		gcdid	⊢ ( 𝐵 ∈ ℤ → ( 𝐵 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
94	88 93	syl	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
95		eluzelre	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℝ )
96		nnnn0	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 )
97		nn0ge0	⊢ ( 𝐵 ∈ ℕ0 → 0 ≤ 𝐵 )
98	1 96 97	3syl	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 𝐵 )
99	95 98	absidd	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( abs ‘ 𝐵 ) = 𝐵 )
100	94 99	eqtrd	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 gcd 𝐵 ) = 𝐵 )
101	100	eqeq1d	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐵 gcd 𝐵 ) = 1 ↔ 𝐵 = 1 ) )
102	101	adantl	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐵 gcd 𝐵 ) = 1 ↔ 𝐵 = 1 ) )
103	102	adantr	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 gcd 𝐵 ) = 1 ↔ 𝐵 = 1 ) )
104		eqneqall	⊢ ( 𝐵 = 1 → ( 𝐵 ≠ 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
105	8 104	syl5com	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
106	105	adantl	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐵 = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
107	106	adantr	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵 = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
108	103 107	sylbid	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 gcd 𝐵 ) = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
109	92 108	sylbid	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝐵 ↑ 𝑚 ) gcd 𝐵 ) = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
110	109	adantr	⊢ ( ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝐵 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑛 ) ) → ( ( ( 𝐵 ↑ 𝑚 ) gcd 𝐵 ) = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
111	87 110	sylbid	⊢ ( ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝐵 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑛 ) ) → ( ( ( 𝑋 ↑ 𝑛 ) gcd 𝐵 ) = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
112	111	ex	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑛 ) → ( ( ( 𝑋 ↑ 𝑛 ) gcd 𝐵 ) = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) ) )
113	112	com23	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝑋 ↑ 𝑛 ) gcd 𝐵 ) = 1 → ( ( 𝐵 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) ) )
114	83 113	syld	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝑋 gcd 𝐵 ) = 1 → ( ( 𝐵 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) ) )
115		ax-1	⊢ ( ¬ ( 𝑋 gcd 𝐵 ) = 1 → ( ( 𝐵 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
116	114 115	pm2.61d1	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
117	80 116	sylbid	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝑋 ↑ 𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
118	49 117	syl5	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 ↑𝑐 ( 𝑚 / 𝑛 ) ) = 𝑋 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
119	48 118	syld	⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
120	119	rexlimdvva	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
121	27 120	syld	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐵 logb 𝑋 ) ∈ ℚ → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
122	121	con2d	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑋 gcd 𝐵 ) = 1 → ¬ ( 𝐵 logb 𝑋 ) ∈ ℚ ) )
123	122	3impia	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → ¬ ( 𝐵 logb 𝑋 ) ∈ ℚ )
124	12 123	eldifd	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → ( 𝐵 logb 𝑋 ) ∈ ( ℝ ∖ ℚ ) )