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

Theorem caucvgprlemk 7485
 Description: Lemma for caucvgpr 7502. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.)
Hypotheses
Ref Expression
caucvgprlemk.jk (𝜑𝐽 <N 𝐾)
caucvgprlemk.jkq (𝜑 → (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑄)
Assertion
Ref Expression
caucvgprlemk (𝜑 → (*Q‘[⟨𝐾, 1o⟩] ~Q ) <Q 𝑄)

Proof of Theorem caucvgprlemk
StepHypRef Expression
1 caucvgprlemk.jk . . . 4 (𝜑𝐽 <N 𝐾)
2 ltrelpi 7144 . . . . . . 7 <N ⊆ (N × N)
32brel 4591 . . . . . 6 (𝐽 <N 𝐾 → (𝐽N𝐾N))
41, 3syl 14 . . . . 5 (𝜑 → (𝐽N𝐾N))
5 ltnnnq 7243 . . . . 5 ((𝐽N𝐾N) → (𝐽 <N 𝐾 ↔ [⟨𝐽, 1o⟩] ~Q <Q [⟨𝐾, 1o⟩] ~Q ))
64, 5syl 14 . . . 4 (𝜑 → (𝐽 <N 𝐾 ↔ [⟨𝐽, 1o⟩] ~Q <Q [⟨𝐾, 1o⟩] ~Q ))
71, 6mpbid 146 . . 3 (𝜑 → [⟨𝐽, 1o⟩] ~Q <Q [⟨𝐾, 1o⟩] ~Q )
8 ltrnqi 7241 . . 3 ([⟨𝐽, 1o⟩] ~Q <Q [⟨𝐾, 1o⟩] ~Q → (*Q‘[⟨𝐾, 1o⟩] ~Q ) <Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))
97, 8syl 14 . 2 (𝜑 → (*Q‘[⟨𝐾, 1o⟩] ~Q ) <Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))
10 caucvgprlemk.jkq . 2 (𝜑 → (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑄)
11 ltsonq 7218 . . 3 <Q Or Q
12 ltrelnq 7185 . . 3 <Q ⊆ (Q × Q)
1311, 12sotri 4934 . 2 (((*Q‘[⟨𝐾, 1o⟩] ~Q ) <Q (*Q‘[⟨𝐽, 1o⟩] ~Q ) ∧ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑄) → (*Q‘[⟨𝐾, 1o⟩] ~Q ) <Q 𝑄)
149, 10, 13syl2anc 408 1 (𝜑 → (*Q‘[⟨𝐾, 1o⟩] ~Q ) <Q 𝑄)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 1480  ⟨cop 3530   class class class wbr 3929  ‘cfv 5123  1oc1o 6306  [cec 6427  Ncnpi 7092
 Copyright terms: Public domain W3C validator