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

Theorem recidpipr 7687
 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 [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ ·P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑁, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1o⟩] ~Q ) <Q 𝑢}⟩) = 1P)
Distinct variable group:   𝑁,𝑙,𝑢

Proof of Theorem recidpipr
StepHypRef Expression
1 nnnq 7253 . . 3 (𝑁N → [⟨𝑁, 1o⟩] ~QQ)
2 recclnq 7223 . . . 4 ([⟨𝑁, 1o⟩] ~QQ → (*Q‘[⟨𝑁, 1o⟩] ~Q ) ∈ Q)
31, 2syl 14 . . 3 (𝑁N → (*Q‘[⟨𝑁, 1o⟩] ~Q ) ∈ Q)
4 mulnqpr 7408 . . 3 (([⟨𝑁, 1o⟩] ~QQ ∧ (*Q‘[⟨𝑁, 1o⟩] ~Q ) ∈ Q) → ⟨{𝑙𝑙 <Q ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q ))}, {𝑢 ∣ ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q )) <Q 𝑢}⟩ = (⟨{𝑙𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ ·P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑁, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1o⟩] ~Q ) <Q 𝑢}⟩))
51, 3, 4syl2anc 409 . 2 (𝑁N → ⟨{𝑙𝑙 <Q ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q ))}, {𝑢 ∣ ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q )) <Q 𝑢}⟩ = (⟨{𝑙𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ ·P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑁, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1o⟩] ~Q ) <Q 𝑢}⟩))
6 recidnq 7224 . . . . . . 7 ([⟨𝑁, 1o⟩] ~QQ → ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q )) = 1Q)
71, 6syl 14 . . . . . 6 (𝑁N → ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q )) = 1Q)
87breq2d 3948 . . . . 5 (𝑁N → (𝑙 <Q ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q )) ↔ 𝑙 <Q 1Q))
98abbidv 2258 . . . 4 (𝑁N → {𝑙𝑙 <Q ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q ))} = {𝑙𝑙 <Q 1Q})
107breq1d 3946 . . . . 5 (𝑁N → (([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q )) <Q 𝑢 ↔ 1Q <Q 𝑢))
1110abbidv 2258 . . . 4 (𝑁N → {𝑢 ∣ ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q )) <Q 𝑢} = {𝑢 ∣ 1Q <Q 𝑢})
129, 11opeq12d 3720 . . 3 (𝑁N → ⟨{𝑙𝑙 <Q ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q ))}, {𝑢 ∣ ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q )) <Q 𝑢}⟩ = ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩)
13 df-i1p 7298 . . 3 1P = ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
1412, 13eqtr4di 2191 . 2 (𝑁N → ⟨{𝑙𝑙 <Q ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q ))}, {𝑢 ∣ ([⟨𝑁, 1o⟩] ~Q ·Q (*Q‘[⟨𝑁, 1o⟩] ~Q )) <Q 𝑢}⟩ = 1P)
155, 14eqtr3d 2175 1 (𝑁N → (⟨{𝑙𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ ·P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑁, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1o⟩] ~Q ) <Q 𝑢}⟩) = 1P)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481  {cab 2126  ⟨cop 3534   class class class wbr 3936  ‘cfv 5130  (class class class)co 5781  1oc1o 6313  [cec 6434  Ncnpi 7103   ~Q ceq 7110  Qcnq 7111  1Qc1q 7112   ·Q cmq 7114  *Qcrq 7115
 Copyright terms: Public domain W3C validator