Theorem logbgcd1irraplemexp 15825

Description: Lemma for logbgcd1irrap 15827. Apartness of 𝑋↑𝑁 and 𝐵↑𝑀. (Contributed by Jim Kingdon, 11-Jul-2024.)

Hypotheses

Ref	Expression
logbgcd1irraplem.x	⊢ (𝜑 → 𝑋 ∈ (ℤ≥‘2))
logbgcd1irraplem.b	⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘2))
logbgcd1irraplem.rp	⊢ (𝜑 → (𝑋 gcd 𝐵) = 1)
logbgcd1irraplem.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
logbgcd1irraplem.n	⊢ (𝜑 → 𝑁 ∈ ℕ)

Assertion

Ref	Expression
logbgcd1irraplemexp	⊢ (𝜑 → (𝑋↑𝑁) # (𝐵↑𝑀))

Proof of Theorem logbgcd1irraplemexp

Step	Hyp	Ref	Expression
1		logbgcd1irraplem.rp	. . . . . . . 8 ⊢ (𝜑 → (𝑋 gcd 𝐵) = 1)
2		logbgcd1irraplem.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (ℤ≥‘2))
3		eluz2nn 9897	. . . . . . . . . 10 ⊢ (𝑋 ∈ (ℤ≥‘2) → 𝑋 ∈ ℕ)
4	2, 3	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ℕ)
5		logbgcd1irraplem.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘2))
6		eluz2nn 9897	. . . . . . . . . 10 ⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 ∈ ℕ)
7	5, 6	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℕ)
8		logbgcd1irraplem.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		rplpwr 12719	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑋 gcd 𝐵) = 1 → ((𝑋↑𝑁) gcd 𝐵) = 1))
10	4, 7, 8, 9	syl3anc 1274	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 gcd 𝐵) = 1 → ((𝑋↑𝑁) gcd 𝐵) = 1))
11	1, 10	mpd 13	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑𝑁) gcd 𝐵) = 1)
12	11	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ (𝐵↑𝑀) = (𝑋↑𝑁)) → ((𝑋↑𝑁) gcd 𝐵) = 1)
13		1red 8288	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ)
14		eluz2gt1 9933	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ (ℤ≥‘2) → 1 < 𝐵)
15	5, 14	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 < 𝐵)
16	13, 15	gtned 8385	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ≠ 1)
17	16	neneqd 2433	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝐵 = 1)
18	7	nnzd 9698	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℤ)
19		gcdid 12678	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℤ → (𝐵 gcd 𝐵) = (abs‘𝐵))
20	18, 19	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 gcd 𝐵) = (abs‘𝐵))
21	7	nnred 9249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ)
22	7	nnnn0d 9552	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℕ0)
23	22	nn0ge0d 9555	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ 𝐵)
24	21, 23	absidd 11848	. . . . . . . . . . . . 13 ⊢ (𝜑 → (abs‘𝐵) = 𝐵)
25	20, 24	eqtrd 2265	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 gcd 𝐵) = 𝐵)
26	25	eqeq1d 2241	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 gcd 𝐵) = 1 ↔ 𝐵 = 1))
27	17, 26	mtbird 680	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐵 gcd 𝐵) = 1)
28	27	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ¬ (𝐵 gcd 𝐵) = 1)
29	18	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝐵 ∈ ℤ)
30		simpr 110	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝑀 ∈ ℕ)
31		rpexp 12846	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((𝐵↑𝑀) gcd 𝐵) = 1 ↔ (𝐵 gcd 𝐵) = 1))
32	29, 29, 30, 31	syl3anc 1274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (((𝐵↑𝑀) gcd 𝐵) = 1 ↔ (𝐵 gcd 𝐵) = 1))
33	28, 32	mtbird 680	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ¬ ((𝐵↑𝑀) gcd 𝐵) = 1)
34	33	adantr 276	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ (𝐵↑𝑀) = (𝑋↑𝑁)) → ¬ ((𝐵↑𝑀) gcd 𝐵) = 1)
35		oveq1 6056	. . . . . . . . . 10 ⊢ ((𝑋↑𝑁) = (𝐵↑𝑀) → ((𝑋↑𝑁) gcd 𝐵) = ((𝐵↑𝑀) gcd 𝐵))
36	35	eqeq1d 2241	. . . . . . . . 9 ⊢ ((𝑋↑𝑁) = (𝐵↑𝑀) → (((𝑋↑𝑁) gcd 𝐵) = 1 ↔ ((𝐵↑𝑀) gcd 𝐵) = 1))
37	36	eqcoms 2235	. . . . . . . 8 ⊢ ((𝐵↑𝑀) = (𝑋↑𝑁) → (((𝑋↑𝑁) gcd 𝐵) = 1 ↔ ((𝐵↑𝑀) gcd 𝐵) = 1))
38	37	adantl 277	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ (𝐵↑𝑀) = (𝑋↑𝑁)) → (((𝑋↑𝑁) gcd 𝐵) = 1 ↔ ((𝐵↑𝑀) gcd 𝐵) = 1))
39	34, 38	mtbird 680	. . . . . 6 ⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ (𝐵↑𝑀) = (𝑋↑𝑁)) → ¬ ((𝑋↑𝑁) gcd 𝐵) = 1)
40	12, 39	pm2.65da 667	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ¬ (𝐵↑𝑀) = (𝑋↑𝑁))
41	40	neqcomd 2237	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ¬ (𝑋↑𝑁) = (𝐵↑𝑀))
42	41	neqned 2419	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑋↑𝑁) ≠ (𝐵↑𝑀))
43	4	nnzd 9698	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℤ)
44	43	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝑋 ∈ ℤ)
45	8	nnnn0d 9552	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
46	45	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝑁 ∈ ℕ0)
47		zexpcl 10915	. . . . 5 ⊢ ((𝑋 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑋↑𝑁) ∈ ℤ)
48	44, 46, 47	syl2anc 411	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑋↑𝑁) ∈ ℤ)
49	30	nnnn0d 9552	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝑀 ∈ ℕ0)
50		zexpcl 10915	. . . . 5 ⊢ ((𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝐵↑𝑀) ∈ ℤ)
51	29, 49, 50	syl2anc 411	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝐵↑𝑀) ∈ ℤ)
52		zapne 9651	. . . 4 ⊢ (((𝑋↑𝑁) ∈ ℤ ∧ (𝐵↑𝑀) ∈ ℤ) → ((𝑋↑𝑁) # (𝐵↑𝑀) ↔ (𝑋↑𝑁) ≠ (𝐵↑𝑀)))
53	48, 51, 52	syl2anc 411	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ((𝑋↑𝑁) # (𝐵↑𝑀) ↔ (𝑋↑𝑁) ≠ (𝐵↑𝑀)))
54	42, 53	mpbird 167	. 2 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑋↑𝑁) # (𝐵↑𝑀))
55	7	nnrpd 10026	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
56	55	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 𝐵 ∈ ℝ+)
57		logbgcd1irraplem.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
58	57	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 𝑀 ∈ ℤ)
59	56, 58	rpexpcld 11058	. . . 4 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑𝑀) ∈ ℝ+)
60	59	rpred 10028	. . 3 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑𝑀) ∈ ℝ)
61	4	nnred 9249	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℝ)
62	61, 45	reexpcld 11051	. . . 4 ⊢ (𝜑 → (𝑋↑𝑁) ∈ ℝ)
63	62	adantr 276	. . 3 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝑋↑𝑁) ∈ ℝ)
64		1red 8288	. . . 4 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 ∈ ℝ)
65		1rp 9989	. . . . . . 7 ⊢ 1 ∈ ℝ+
66	65	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 ∈ ℝ+)
67	21	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 𝐵 ∈ ℝ)
68		simpr 110	. . . . . . . 8 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → -𝑀 ∈ ℕ0)
69	7	nnge1d 9279	. . . . . . . . 9 ⊢ (𝜑 → 1 ≤ 𝐵)
70	69	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 ≤ 𝐵)
71	67, 68, 70	expge1d 11053	. . . . . . 7 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 ≤ (𝐵↑-𝑀))
72	67	recnd 8301	. . . . . . . 8 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 𝐵 ∈ ℂ)
73	7	nnap0d 9282	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 # 0)
74	73	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 𝐵 # 0)
75	72, 74, 58	expnegapd 11041	. . . . . . 7 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑-𝑀) = (1 / (𝐵↑𝑀)))
76	71, 75	breqtrd 4134	. . . . . 6 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 ≤ (1 / (𝐵↑𝑀)))
77	66, 59, 76	lerec2d 10050	. . . . 5 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑𝑀) ≤ (1 / 1))
78		1div1e1 8977	. . . . 5 ⊢ (1 / 1) = 1
79	77, 78	breqtrdi 4149	. . . 4 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑𝑀) ≤ 1)
80		eluz2gt1 9933	. . . . . . 7 ⊢ (𝑋 ∈ (ℤ≥‘2) → 1 < 𝑋)
81	2, 80	syl 14	. . . . . 6 ⊢ (𝜑 → 1 < 𝑋)
82		expgt1 10938	. . . . . 6 ⊢ ((𝑋 ∈ ℝ ∧ 𝑁 ∈ ℕ ∧ 1 < 𝑋) → 1 < (𝑋↑𝑁))
83	61, 8, 81, 82	syl3anc 1274	. . . . 5 ⊢ (𝜑 → 1 < (𝑋↑𝑁))
84	83	adantr 276	. . . 4 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 < (𝑋↑𝑁))
85	60, 64, 63, 79, 84	lelttrd 8397	. . 3 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑𝑀) < (𝑋↑𝑁))
86	60, 63, 85	gtapd 8910	. 2 ⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝑋↑𝑁) # (𝐵↑𝑀))
87		elznn 9592	. . . 4 ⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ0)))
88	57, 87	sylib 122	. . 3 ⊢ (𝜑 → (𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ0)))
89	88	simprd 114	. 2 ⊢ (𝜑 → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ0))
90	54, 86, 89	mpjaodan 806	1 ⊢ (𝜑 → (𝑋↑𝑁) # (𝐵↑𝑀))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 716   = wceq 1398   ∈ wcel 2203   ≠ wne 2412   class class class wbr 4108  ‘cfv 5351  (class class class)co 6049  ℝcr 8125  0cc0 8126  1c1 8127   < clt 8307   ≤ cle 8308  -cneg 8444   # cap 8854   / cdiv 8945  ℕcn 9236  2c2 9287  ℕ₀cn0 9495  ℤcz 9576  ℤ_≥cuz 9852  ℝ⁺crp 9985  ↑cexp 10899  abscabs 11678   gcd cgcd 12645

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4224  ax-sep 4227  ax-nul 4235  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-iinf 4709  ax-cnex 8217  ax-resscn 8218  ax-1cn 8219  ax-1re 8220  ax-icn 8221  ax-addcl 8222  ax-addrcl 8223  ax-mulcl 8224  ax-mulrcl 8225  ax-addcom 8226  ax-mulcom 8227  ax-addass 8228  ax-mulass 8229  ax-distr 8230  ax-i2m1 8231  ax-0lt1 8232  ax-1rid 8233  ax-0id 8234  ax-rnegex 8235  ax-precex 8236  ax-cnre 8237  ax-pre-ltirr 8238  ax-pre-ltwlin 8239  ax-pre-lttrn 8240  ax-pre-apti 8241  ax-pre-ltadd 8242  ax-pre-mulgt0 8243  ax-pre-mulext 8244  ax-arch 8245  ax-caucvg 8246

This theorem depends on definitions:  df-bi 117  df-stab 839  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rmo 2528  df-rab 2529  df-v 2814  df-sbc 3042  df-csb 3138  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-nul 3508  df-if 3620  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-int 3949  df-iun 3992  df-br 4109  df-opab 4171  df-mpt 4172  df-tr 4208  df-id 4413  df-po 4416  df-iso 4417  df-iord 4486  df-on 4488  df-ilim 4489  df-suc 4491  df-iom 4712  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-res 4760  df-ima 4761  df-iota 5311  df-fun 5353  df-fn 5354  df-f 5355  df-f1 5356  df-fo 5357  df-f1o 5358  df-fv 5359  df-riota 6002  df-ov 6052  df-oprab 6053  df-mpo 6054  df-1st 6333  df-2nd 6334  df-recs 6535  df-frec 6621  df-1o 6646  df-2o 6647  df-er 6766  df-en 6975  df-sup 7274  df-pnf 8309  df-mnf 8310  df-xr 8311  df-ltxr 8312  df-le 8313  df-sub 8445  df-neg 8446  df-reap 8848  df-ap 8855  df-div 8946  df-inn 9237  df-2 9295  df-3 9296  df-4 9297  df-n0 9496  df-z 9577  df-uz 9853  df-q 9951  df-rp 9986  df-fz 10342  df-fzo 10476  df-fl 10629  df-mod 10684  df-seqfrec 10809  df-exp 10900  df-cj 11523  df-re 11524  df-im 11525  df-rsqrt 11679  df-abs 11680  df-dvds 12470  df-gcd 12646  df-prm 12801

This theorem is referenced by:  logbgcd1irraplemap  15826