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

Theorem map2psrprg 7620
Description: Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
Assertion
Ref Expression
map2psrprg (𝐶R → ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Proof of Theorem map2psrprg
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelsr 7553 . . . . . . 7 <R ⊆ (R × R)
21brel 4591 . . . . . 6 ((𝐶 +R -1R) <R 𝐴 → ((𝐶 +R -1R) ∈ R𝐴R))
32simprd 113 . . . . 5 ((𝐶 +R -1R) <R 𝐴𝐴R)
43anim2i 339 . . . 4 ((𝐶R ∧ (𝐶 +R -1R) <R 𝐴) → (𝐶R𝐴R))
5 simpr 109 . . . 4 ((𝐶R ∧ (𝐶 +R -1R) <R 𝐴) → (𝐶 +R -1R) <R 𝐴)
6 m1r 7567 . . . . . . . 8 -1RR
76a1i 9 . . . . . . 7 ((𝐶R𝐴R) → -1RR)
8 simpl 108 . . . . . . . . 9 ((𝐶R𝐴R) → 𝐶R)
9 mulclsr 7569 . . . . . . . . 9 ((𝐶R ∧ -1RR) → (𝐶 ·R -1R) ∈ R)
108, 7, 9syl2anc 408 . . . . . . . 8 ((𝐶R𝐴R) → (𝐶 ·R -1R) ∈ R)
11 simpr 109 . . . . . . . 8 ((𝐶R𝐴R) → 𝐴R)
12 addclsr 7568 . . . . . . . 8 (((𝐶 ·R -1R) ∈ R𝐴R) → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
1310, 11, 12syl2anc 408 . . . . . . 7 ((𝐶R𝐴R) → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
14 ltasrg 7585 . . . . . . 7 ((-1RR ∧ ((𝐶 ·R -1R) +R 𝐴) ∈ R𝐶R) → (-1R <R ((𝐶 ·R -1R) +R 𝐴) ↔ (𝐶 +R -1R) <R (𝐶 +R ((𝐶 ·R -1R) +R 𝐴))))
157, 13, 8, 14syl3anc 1216 . . . . . 6 ((𝐶R𝐴R) → (-1R <R ((𝐶 ·R -1R) +R 𝐴) ↔ (𝐶 +R -1R) <R (𝐶 +R ((𝐶 ·R -1R) +R 𝐴))))
16 pn0sr 7586 . . . . . . . . . . 11 (𝐶R → (𝐶 +R (𝐶 ·R -1R)) = 0R)
1716oveq1d 5789 . . . . . . . . . 10 (𝐶R → ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (0R +R 𝐴))
1817adantr 274 . . . . . . . . 9 ((𝐶R𝐴R) → ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (0R +R 𝐴))
19 addasssrg 7571 . . . . . . . . . 10 ((𝐶R ∧ (𝐶 ·R -1R) ∈ R𝐴R) → ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)))
208, 10, 11, 19syl3anc 1216 . . . . . . . . 9 ((𝐶R𝐴R) → ((𝐶 +R (𝐶 ·R -1R)) +R 𝐴) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)))
21 0r 7565 . . . . . . . . . . 11 0RR
2221a1i 9 . . . . . . . . . 10 ((𝐶R𝐴R) → 0RR)
23 addcomsrg 7570 . . . . . . . . . 10 ((0RR𝐴R) → (0R +R 𝐴) = (𝐴 +R 0R))
2422, 11, 23syl2anc 408 . . . . . . . . 9 ((𝐶R𝐴R) → (0R +R 𝐴) = (𝐴 +R 0R))
2518, 20, 243eqtr3d 2180 . . . . . . . 8 ((𝐶R𝐴R) → (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) = (𝐴 +R 0R))
26 0idsr 7582 . . . . . . . . 9 (𝐴R → (𝐴 +R 0R) = 𝐴)
2726adantl 275 . . . . . . . 8 ((𝐶R𝐴R) → (𝐴 +R 0R) = 𝐴)
2825, 27eqtrd 2172 . . . . . . 7 ((𝐶R𝐴R) → (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) = 𝐴)
2928breq2d 3941 . . . . . 6 ((𝐶R𝐴R) → ((𝐶 +R -1R) <R (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)) ↔ (𝐶 +R -1R) <R 𝐴))
3015, 29bitrd 187 . . . . 5 ((𝐶R𝐴R) → (-1R <R ((𝐶 ·R -1R) +R 𝐴) ↔ (𝐶 +R -1R) <R 𝐴))
316, 9mpan2 421 . . . . . . . 8 (𝐶R → (𝐶 ·R -1R) ∈ R)
3231, 12sylan 281 . . . . . . 7 ((𝐶R𝐴R) → ((𝐶 ·R -1R) +R 𝐴) ∈ R)
33 df-nr 7542 . . . . . . . 8 R = ((P × P) / ~R )
34 breq2 3933 . . . . . . . . 9 ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ -1R <R ((𝐶 ·R -1R) +R 𝐴)))
35 eqeq2 2149 . . . . . . . . . 10 ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
3635rexbidv 2438 . . . . . . . . 9 ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (∃𝑥P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ ∃𝑥P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
3734, 36imbi12d 233 . . . . . . . 8 ([⟨𝑦, 𝑧⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → ((-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ) ↔ (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴))))
38 df-m1r 7548 . . . . . . . . . . . 12 -1R = [⟨1P, (1P +P 1P)⟩] ~R
3938breq1i 3936 . . . . . . . . . . 11 (-1R <R [⟨𝑦, 𝑧⟩] ~R ↔ [⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R )
40 1pr 7369 . . . . . . . . . . . . . . 15 1PP
41 addassprg 7394 . . . . . . . . . . . . . . 15 ((1PP ∧ 1PP𝑦P) → ((1P +P 1P) +P 𝑦) = (1P +P (1P +P 𝑦)))
4240, 40, 41mp3an12 1305 . . . . . . . . . . . . . 14 (𝑦P → ((1P +P 1P) +P 𝑦) = (1P +P (1P +P 𝑦)))
4342breq2d 3941 . . . . . . . . . . . . 13 (𝑦P → ((1P +P 𝑧)<P ((1P +P 1P) +P 𝑦) ↔ (1P +P 𝑧)<P (1P +P (1P +P 𝑦))))
4443adantr 274 . . . . . . . . . . . 12 ((𝑦P𝑧P) → ((1P +P 𝑧)<P ((1P +P 1P) +P 𝑦) ↔ (1P +P 𝑧)<P (1P +P (1P +P 𝑦))))
45 addclpr 7352 . . . . . . . . . . . . . 14 ((1PP ∧ 1PP) → (1P +P 1P) ∈ P)
4640, 40, 45mp2an 422 . . . . . . . . . . . . 13 (1P +P 1P) ∈ P
47 ltsrprg 7562 . . . . . . . . . . . . 13 (((1PP ∧ (1P +P 1P) ∈ P) ∧ (𝑦P𝑧P)) → ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R ↔ (1P +P 𝑧)<P ((1P +P 1P) +P 𝑦)))
4840, 46, 47mpanl12 432 . . . . . . . . . . . 12 ((𝑦P𝑧P) → ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R ↔ (1P +P 𝑧)<P ((1P +P 1P) +P 𝑦)))
49 simpr 109 . . . . . . . . . . . . 13 ((𝑦P𝑧P) → 𝑧P)
5040a1i 9 . . . . . . . . . . . . . 14 ((𝑦P𝑧P) → 1PP)
51 simpl 108 . . . . . . . . . . . . . 14 ((𝑦P𝑧P) → 𝑦P)
52 addclpr 7352 . . . . . . . . . . . . . 14 ((1PP𝑦P) → (1P +P 𝑦) ∈ P)
5350, 51, 52syl2anc 408 . . . . . . . . . . . . 13 ((𝑦P𝑧P) → (1P +P 𝑦) ∈ P)
54 ltaprg 7434 . . . . . . . . . . . . 13 ((𝑧P ∧ (1P +P 𝑦) ∈ P ∧ 1PP) → (𝑧<P (1P +P 𝑦) ↔ (1P +P 𝑧)<P (1P +P (1P +P 𝑦))))
5549, 53, 50, 54syl3anc 1216 . . . . . . . . . . . 12 ((𝑦P𝑧P) → (𝑧<P (1P +P 𝑦) ↔ (1P +P 𝑧)<P (1P +P (1P +P 𝑦))))
5644, 48, 553bitr4d 219 . . . . . . . . . . 11 ((𝑦P𝑧P) → ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝑦, 𝑧⟩] ~R𝑧<P (1P +P 𝑦)))
5739, 56syl5bb 191 . . . . . . . . . 10 ((𝑦P𝑧P) → (-1R <R [⟨𝑦, 𝑧⟩] ~R𝑧<P (1P +P 𝑦)))
58 ltexpri 7428 . . . . . . . . . 10 (𝑧<P (1P +P 𝑦) → ∃𝑥P (𝑧 +P 𝑥) = (1P +P 𝑦))
5957, 58syl6bi 162 . . . . . . . . 9 ((𝑦P𝑧P) → (-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥P (𝑧 +P 𝑥) = (1P +P 𝑦)))
60 enreceq 7551 . . . . . . . . . . . . 13 (((𝑥P ∧ 1PP) ∧ (𝑦P𝑧P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑥 +P 𝑧) = (1P +P 𝑦)))
6140, 60mpanl2 431 . . . . . . . . . . . 12 ((𝑥P ∧ (𝑦P𝑧P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑥 +P 𝑧) = (1P +P 𝑦)))
6249adantl 275 . . . . . . . . . . . . . 14 ((𝑥P ∧ (𝑦P𝑧P)) → 𝑧P)
63 simpl 108 . . . . . . . . . . . . . 14 ((𝑥P ∧ (𝑦P𝑧P)) → 𝑥P)
64 addcomprg 7393 . . . . . . . . . . . . . 14 ((𝑧P𝑥P) → (𝑧 +P 𝑥) = (𝑥 +P 𝑧))
6562, 63, 64syl2anc 408 . . . . . . . . . . . . 13 ((𝑥P ∧ (𝑦P𝑧P)) → (𝑧 +P 𝑥) = (𝑥 +P 𝑧))
6665eqeq1d 2148 . . . . . . . . . . . 12 ((𝑥P ∧ (𝑦P𝑧P)) → ((𝑧 +P 𝑥) = (1P +P 𝑦) ↔ (𝑥 +P 𝑧) = (1P +P 𝑦)))
6761, 66bitr4d 190 . . . . . . . . . . 11 ((𝑥P ∧ (𝑦P𝑧P)) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑧 +P 𝑥) = (1P +P 𝑦)))
6867ancoms 266 . . . . . . . . . 10 (((𝑦P𝑧P) ∧ 𝑥P) → ([⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ (𝑧 +P 𝑥) = (1P +P 𝑦)))
6968rexbidva 2434 . . . . . . . . 9 ((𝑦P𝑧P) → (∃𝑥P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ↔ ∃𝑥P (𝑧 +P 𝑥) = (1P +P 𝑦)))
7059, 69sylibrd 168 . . . . . . . 8 ((𝑦P𝑧P) → (-1R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥P [⟨𝑥, 1P⟩] ~R = [⟨𝑦, 𝑧⟩] ~R ))
7133, 37, 70ecoptocl 6516 . . . . . . 7 (((𝐶 ·R -1R) +R 𝐴) ∈ R → (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
7232, 71syl 14 . . . . . 6 ((𝐶R𝐴R) → (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)))
73 oveq2 5782 . . . . . . . . 9 ([⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = (𝐶 +R ((𝐶 ·R -1R) +R 𝐴)))
7473, 28sylan9eqr 2194 . . . . . . . 8 (((𝐶R𝐴R) ∧ [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴)) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)
7574ex 114 . . . . . . 7 ((𝐶R𝐴R) → ([⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
7675reximdv 2533 . . . . . 6 ((𝐶R𝐴R) → (∃𝑥P [⟨𝑥, 1P⟩] ~R = ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
7772, 76syld 45 . . . . 5 ((𝐶R𝐴R) → (-1R <R ((𝐶 ·R -1R) +R 𝐴) → ∃𝑥P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
7830, 77sylbird 169 . . . 4 ((𝐶R𝐴R) → ((𝐶 +R -1R) <R 𝐴 → ∃𝑥P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
794, 5, 78sylc 62 . . 3 ((𝐶R ∧ (𝐶 +R -1R) <R 𝐴) → ∃𝑥P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)
8079ex 114 . 2 (𝐶R → ((𝐶 +R -1R) <R 𝐴 → ∃𝑥P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
81 mappsrprg 7619 . . . . 5 ((𝑥P𝐶R) → (𝐶 +R -1R) <R (𝐶 +R [⟨𝑥, 1P⟩] ~R ))
82 breq2 3933 . . . . 5 ((𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑥, 1P⟩] ~R ) ↔ (𝐶 +R -1R) <R 𝐴))
8381, 82syl5ibcom 154 . . . 4 ((𝑥P𝐶R) → ((𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → (𝐶 +R -1R) <R 𝐴))
8483ancoms 266 . . 3 ((𝐶R𝑥P) → ((𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → (𝐶 +R -1R) <R 𝐴))
8584rexlimdva 2549 . 2 (𝐶R → (∃𝑥P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴 → (𝐶 +R -1R) <R 𝐴))
8680, 85impbid 128 1 (𝐶R → ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1331  wcel 1480  wrex 2417  cop 3530   class class class wbr 3929  (class class class)co 5774  [cec 6427  Pcnp 7106  1Pc1p 7107   +P cpp 7108  <P cltp 7110   ~R cer 7111  Rcnr 7112  0Rc0r 7113  -1Rcm1r 7115   +R cplr 7116   ·R cmr 7117   <R cltr 7118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-eprel 4211  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-1o 6313  df-2o 6314  df-oadd 6317  df-omul 6318  df-er 6429  df-ec 6431  df-qs 6435  df-ni 7119  df-pli 7120  df-mi 7121  df-lti 7122  df-plpq 7159  df-mpq 7160  df-enq 7162  df-nqqs 7163  df-plqqs 7164  df-mqqs 7165  df-1nqqs 7166  df-rq 7167  df-ltnqqs 7168  df-enq0 7239  df-nq0 7240  df-0nq0 7241  df-plq0 7242  df-mq0 7243  df-inp 7281  df-i1p 7282  df-iplp 7283  df-imp 7284  df-iltp 7285  df-enr 7541  df-nr 7542  df-plr 7543  df-mr 7544  df-ltr 7545  df-0r 7546  df-1r 7547  df-m1r 7548
This theorem is referenced by:  suplocsrlemb  7621  suplocsrlempr  7622  suplocsrlem  7623
  Copyright terms: Public domain W3C validator