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

Theorem recidpipr 6932
 Description: Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.)
Assertion
Ref Expression
recidpipr (𝑁N → (⟨{𝑙𝑙 <Q [⟨𝑁, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1𝑜⟩] ~Q <Q 𝑢}⟩ ·P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = 1P)
Distinct variable group:   𝑁,𝑙,𝑢

Proof of Theorem recidpipr
StepHypRef Expression
1 nnnq 6520 . . 3 (𝑁N → [⟨𝑁, 1𝑜⟩] ~QQ)
2 recclnq 6490 . . . 4 ([⟨𝑁, 1𝑜⟩] ~QQ → (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ) ∈ Q)
31, 2syl 14 . . 3 (𝑁N → (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ) ∈ Q)
4 mulnqpr 6675 . . 3 (([⟨𝑁, 1𝑜⟩] ~QQ ∧ (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ) ∈ Q) → ⟨{𝑙𝑙 <Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ))}, {𝑢 ∣ ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )) <Q 𝑢}⟩ = (⟨{𝑙𝑙 <Q [⟨𝑁, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1𝑜⟩] ~Q <Q 𝑢}⟩ ·P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
51, 3, 4syl2anc 391 . 2 (𝑁N → ⟨{𝑙𝑙 <Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ))}, {𝑢 ∣ ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )) <Q 𝑢}⟩ = (⟨{𝑙𝑙 <Q [⟨𝑁, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1𝑜⟩] ~Q <Q 𝑢}⟩ ·P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
6 recidnq 6491 . . . . . . 7 ([⟨𝑁, 1𝑜⟩] ~QQ → ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )) = 1Q)
71, 6syl 14 . . . . . 6 (𝑁N → ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )) = 1Q)
87breq2d 3776 . . . . 5 (𝑁N → (𝑙 <Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )) ↔ 𝑙 <Q 1Q))
98abbidv 2155 . . . 4 (𝑁N → {𝑙𝑙 <Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ))} = {𝑙𝑙 <Q 1Q})
107breq1d 3774 . . . . 5 (𝑁N → (([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )) <Q 𝑢 ↔ 1Q <Q 𝑢))
1110abbidv 2155 . . . 4 (𝑁N → {𝑢 ∣ ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )) <Q 𝑢} = {𝑢 ∣ 1Q <Q 𝑢})
129, 11opeq12d 3557 . . 3 (𝑁N → ⟨{𝑙𝑙 <Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ))}, {𝑢 ∣ ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )) <Q 𝑢}⟩ = ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩)
13 df-i1p 6565 . . 3 1P = ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
1412, 13syl6eqr 2090 . 2 (𝑁N → ⟨{𝑙𝑙 <Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ))}, {𝑢 ∣ ([⟨𝑁, 1𝑜⟩] ~Q ·Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )) <Q 𝑢}⟩ = 1P)
155, 14eqtr3d 2074 1 (𝑁N → (⟨{𝑙𝑙 <Q [⟨𝑁, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1𝑜⟩] ~Q <Q 𝑢}⟩ ·P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑁, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = 1P)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1243   ∈ wcel 1393  {cab 2026  ⟨cop 3378   class class class wbr 3764  ‘cfv 4902  (class class class)co 5512  1𝑜c1o 5994  [cec 6104  Ncnpi 6370   ~Q ceq 6377  Qcnq 6378  1Qc1q 6379   ·Q cmq 6381  *Qcrq 6382
 Copyright terms: Public domain W3C validator