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	$⊢ (X \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2} \land X \gcd B = 1) \to \log_{B} X \in (ℝ ∖ ℚ)$

Proof

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

Metamath Proof Explorer

Theorem logbgcd1irr

Proof