ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  logbgcd1irraplemap GIF version

Theorem logbgcd1irraplemap 13967
Description: Lemma for logbgcd1irrap 13968. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.)
Hypotheses
Ref Expression
logbgcd1irraplem.x (𝜑𝑋 ∈ (ℤ‘2))
logbgcd1irraplem.b (𝜑𝐵 ∈ (ℤ‘2))
logbgcd1irraplem.rp (𝜑 → (𝑋 gcd 𝐵) = 1)
logbgcd1irraplem.m (𝜑𝑀 ∈ ℤ)
logbgcd1irraplem.n (𝜑𝑁 ∈ ℕ)
Assertion
Ref Expression
logbgcd1irraplemap (𝜑 → (𝐵 logb 𝑋) # (𝑀 / 𝑁))

Proof of Theorem logbgcd1irraplemap
StepHypRef Expression
1 logbgcd1irraplem.x . . . . 5 (𝜑𝑋 ∈ (ℤ‘2))
2 logbgcd1irraplem.b . . . . 5 (𝜑𝐵 ∈ (ℤ‘2))
3 logbgcd1irraplem.rp . . . . 5 (𝜑 → (𝑋 gcd 𝐵) = 1)
4 logbgcd1irraplem.m . . . . 5 (𝜑𝑀 ∈ ℤ)
5 logbgcd1irraplem.n . . . . 5 (𝜑𝑁 ∈ ℕ)
61, 2, 3, 4, 5logbgcd1irraplemexp 13966 . . . 4 (𝜑 → (𝑋𝑁) # (𝐵𝑀))
7 eluz2nn 9539 . . . . . . . 8 (𝐵 ∈ (ℤ‘2) → 𝐵 ∈ ℕ)
82, 7syl 14 . . . . . . 7 (𝜑𝐵 ∈ ℕ)
98nnrpd 9665 . . . . . 6 (𝜑𝐵 ∈ ℝ+)
10 1red 7947 . . . . . . 7 (𝜑 → 1 ∈ ℝ)
118nnred 8905 . . . . . . 7 (𝜑𝐵 ∈ ℝ)
12 eluz2gt1 9575 . . . . . . . 8 (𝐵 ∈ (ℤ‘2) → 1 < 𝐵)
132, 12syl 14 . . . . . . 7 (𝜑 → 1 < 𝐵)
1410, 11, 13gtapd 8568 . . . . . 6 (𝜑𝐵 # 1)
15 eluz2nn 9539 . . . . . . . 8 (𝑋 ∈ (ℤ‘2) → 𝑋 ∈ ℕ)
161, 15syl 14 . . . . . . 7 (𝜑𝑋 ∈ ℕ)
1716nnrpd 9665 . . . . . 6 (𝜑𝑋 ∈ ℝ+)
18 rpcxplogb 13962 . . . . . 6 ((𝐵 ∈ ℝ+𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (𝐵𝑐(𝐵 logb 𝑋)) = 𝑋)
199, 14, 17, 18syl3anc 1238 . . . . 5 (𝜑 → (𝐵𝑐(𝐵 logb 𝑋)) = 𝑋)
2019oveq1d 5880 . . . 4 (𝜑 → ((𝐵𝑐(𝐵 logb 𝑋))↑𝑁) = (𝑋𝑁))
21 znq 9597 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℚ)
224, 5, 21syl2anc 411 . . . . . . 7 (𝜑 → (𝑀 / 𝑁) ∈ ℚ)
23 qre 9598 . . . . . . 7 ((𝑀 / 𝑁) ∈ ℚ → (𝑀 / 𝑁) ∈ ℝ)
2422, 23syl 14 . . . . . 6 (𝜑 → (𝑀 / 𝑁) ∈ ℝ)
255nncnd 8906 . . . . . 6 (𝜑𝑁 ∈ ℂ)
269, 24, 25cxpmuld 13936 . . . . 5 (𝜑 → (𝐵𝑐((𝑀 / 𝑁) · 𝑁)) = ((𝐵𝑐(𝑀 / 𝑁))↑𝑐𝑁))
274zcnd 9349 . . . . . . . 8 (𝜑𝑀 ∈ ℂ)
285nnap0d 8938 . . . . . . . 8 (𝜑𝑁 # 0)
2927, 25, 28divcanap1d 8721 . . . . . . 7 (𝜑 → ((𝑀 / 𝑁) · 𝑁) = 𝑀)
3029oveq2d 5881 . . . . . 6 (𝜑 → (𝐵𝑐((𝑀 / 𝑁) · 𝑁)) = (𝐵𝑐𝑀))
31 cxpexpnn 13897 . . . . . . 7 ((𝐵 ∈ ℕ ∧ 𝑀 ∈ ℤ) → (𝐵𝑐𝑀) = (𝐵𝑀))
328, 4, 31syl2anc 411 . . . . . 6 (𝜑 → (𝐵𝑐𝑀) = (𝐵𝑀))
3330, 32eqtrd 2208 . . . . 5 (𝜑 → (𝐵𝑐((𝑀 / 𝑁) · 𝑁)) = (𝐵𝑀))
349, 24rpcxpcld 13932 . . . . . 6 (𝜑 → (𝐵𝑐(𝑀 / 𝑁)) ∈ ℝ+)
355nnzd 9347 . . . . . 6 (𝜑𝑁 ∈ ℤ)
36 cxpexprp 13896 . . . . . 6 (((𝐵𝑐(𝑀 / 𝑁)) ∈ ℝ+𝑁 ∈ ℤ) → ((𝐵𝑐(𝑀 / 𝑁))↑𝑐𝑁) = ((𝐵𝑐(𝑀 / 𝑁))↑𝑁))
3734, 35, 36syl2anc 411 . . . . 5 (𝜑 → ((𝐵𝑐(𝑀 / 𝑁))↑𝑐𝑁) = ((𝐵𝑐(𝑀 / 𝑁))↑𝑁))
3826, 33, 373eqtr3rd 2217 . . . 4 (𝜑 → ((𝐵𝑐(𝑀 / 𝑁))↑𝑁) = (𝐵𝑀))
396, 20, 383brtr4d 4030 . . 3 (𝜑 → ((𝐵𝑐(𝐵 logb 𝑋))↑𝑁) # ((𝐵𝑐(𝑀 / 𝑁))↑𝑁))
40 relogbzcl 13950 . . . . . . 7 ((𝐵 ∈ (ℤ‘2) ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) ∈ ℝ)
412, 17, 40syl2anc 411 . . . . . 6 (𝜑 → (𝐵 logb 𝑋) ∈ ℝ)
4241recnd 7960 . . . . 5 (𝜑 → (𝐵 logb 𝑋) ∈ ℂ)
439, 42rpcncxpcld 13927 . . . 4 (𝜑 → (𝐵𝑐(𝐵 logb 𝑋)) ∈ ℂ)
44 qcn 9607 . . . . . 6 ((𝑀 / 𝑁) ∈ ℚ → (𝑀 / 𝑁) ∈ ℂ)
4522, 44syl 14 . . . . 5 (𝜑 → (𝑀 / 𝑁) ∈ ℂ)
469, 45rpcncxpcld 13927 . . . 4 (𝜑 → (𝐵𝑐(𝑀 / 𝑁)) ∈ ℂ)
47 apexp1 10666 . . . 4 (((𝐵𝑐(𝐵 logb 𝑋)) ∈ ℂ ∧ (𝐵𝑐(𝑀 / 𝑁)) ∈ ℂ ∧ 𝑁 ∈ ℕ) → (((𝐵𝑐(𝐵 logb 𝑋))↑𝑁) # ((𝐵𝑐(𝑀 / 𝑁))↑𝑁) → (𝐵𝑐(𝐵 logb 𝑋)) # (𝐵𝑐(𝑀 / 𝑁))))
4843, 46, 5, 47syl3anc 1238 . . 3 (𝜑 → (((𝐵𝑐(𝐵 logb 𝑋))↑𝑁) # ((𝐵𝑐(𝑀 / 𝑁))↑𝑁) → (𝐵𝑐(𝐵 logb 𝑋)) # (𝐵𝑐(𝑀 / 𝑁))))
4939, 48mpd 13 . 2 (𝜑 → (𝐵𝑐(𝐵 logb 𝑋)) # (𝐵𝑐(𝑀 / 𝑁)))
50 apcxp2 13938 . . 3 (((𝐵 ∈ ℝ+𝐵 # 1) ∧ ((𝐵 logb 𝑋) ∈ ℝ ∧ (𝑀 / 𝑁) ∈ ℝ)) → ((𝐵 logb 𝑋) # (𝑀 / 𝑁) ↔ (𝐵𝑐(𝐵 logb 𝑋)) # (𝐵𝑐(𝑀 / 𝑁))))
519, 14, 41, 24, 50syl22anc 1239 . 2 (𝜑 → ((𝐵 logb 𝑋) # (𝑀 / 𝑁) ↔ (𝐵𝑐(𝐵 logb 𝑋)) # (𝐵𝑐(𝑀 / 𝑁))))
5249, 51mpbird 167 1 (𝜑 → (𝐵 logb 𝑋) # (𝑀 / 𝑁))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105   = wceq 1353  wcel 2146   class class class wbr 3998  cfv 5208  (class class class)co 5865  cc 7784  cr 7785  1c1 7787   · cmul 7791   < clt 7966   # cap 8512   / cdiv 8602  cn 8892  2c2 8943  cz 9226  cuz 9501  cq 9592  +crp 9624  cexp 10489   gcd cgcd 11910  𝑐ccxp 13858   logb clogb 13941
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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-iinf 4581  ax-cnex 7877  ax-resscn 7878  ax-1cn 7879  ax-1re 7880  ax-icn 7881  ax-addcl 7882  ax-addrcl 7883  ax-mulcl 7884  ax-mulrcl 7885  ax-addcom 7886  ax-mulcom 7887  ax-addass 7888  ax-mulass 7889  ax-distr 7890  ax-i2m1 7891  ax-0lt1 7892  ax-1rid 7893  ax-0id 7894  ax-rnegex 7895  ax-precex 7896  ax-cnre 7897  ax-pre-ltirr 7898  ax-pre-ltwlin 7899  ax-pre-lttrn 7900  ax-pre-apti 7901  ax-pre-ltadd 7902  ax-pre-mulgt0 7903  ax-pre-mulext 7904  ax-arch 7905  ax-caucvg 7906  ax-pre-suploc 7907  ax-addf 7908  ax-mulf 7909
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-nel 2441  df-ral 2458  df-rex 2459  df-reu 2460  df-rmo 2461  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-if 3533  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-iun 3884  df-disj 3976  df-br 3999  df-opab 4060  df-mpt 4061  df-tr 4097  df-id 4287  df-po 4290  df-iso 4291  df-iord 4360  df-on 4362  df-ilim 4363  df-suc 4365  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-isom 5217  df-riota 5821  df-ov 5868  df-oprab 5869  df-mpo 5870  df-of 6073  df-1st 6131  df-2nd 6132  df-recs 6296  df-irdg 6361  df-frec 6382  df-1o 6407  df-2o 6408  df-oadd 6411  df-er 6525  df-map 6640  df-pm 6641  df-en 6731  df-dom 6732  df-fin 6733  df-sup 6973  df-inf 6974  df-pnf 7968  df-mnf 7969  df-xr 7970  df-ltxr 7971  df-le 7972  df-sub 8104  df-neg 8105  df-reap 8506  df-ap 8513  df-div 8603  df-inn 8893  df-2 8951  df-3 8952  df-4 8953  df-n0 9150  df-z 9227  df-uz 9502  df-q 9593  df-rp 9625  df-xneg 9743  df-xadd 9744  df-ioo 9863  df-ico 9865  df-icc 9866  df-fz 9980  df-fzo 10113  df-fl 10240  df-mod 10293  df-seqfrec 10416  df-exp 10490  df-fac 10674  df-bc 10696  df-ihash 10724  df-shft 10792  df-cj 10819  df-re 10820  df-im 10821  df-rsqrt 10975  df-abs 10976  df-clim 11255  df-sumdc 11330  df-ef 11624  df-e 11625  df-dvds 11763  df-gcd 11911  df-prm 12075  df-rest 12621  df-topgen 12640  df-psmet 13067  df-xmet 13068  df-met 13069  df-bl 13070  df-mopn 13071  df-top 13076  df-topon 13089  df-bases 13121  df-ntr 13176  df-cn 13268  df-cnp 13269  df-tx 13333  df-cncf 13638  df-limced 13705  df-dvap 13706  df-relog 13859  df-rpcxp 13860  df-logb 13942
This theorem is referenced by:  logbgcd1irrap  13968
  Copyright terms: Public domain W3C validator