HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  stadd3i Structured version   Visualization version   GIF version

Theorem stadd3i 31232
Description: If the sum of 3 states is 3, then each state is 1. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.)
Hypotheses
Ref Expression
stle.1 𝐴C
stle.2 𝐵C
stm1add3.3 𝐶C
Assertion
Ref Expression
stadd3i (𝑆 ∈ States → ((((𝑆𝐴) + (𝑆𝐵)) + (𝑆𝐶)) = 3 → (𝑆𝐴) = 1))

Proof of Theorem stadd3i
StepHypRef Expression
1 stle.1 . . . . . 6 𝐴C
2 stcl 31200 . . . . . 6 (𝑆 ∈ States → (𝐴C → (𝑆𝐴) ∈ ℝ))
31, 2mpi 20 . . . . 5 (𝑆 ∈ States → (𝑆𝐴) ∈ ℝ)
43recnd 11190 . . . 4 (𝑆 ∈ States → (𝑆𝐴) ∈ ℂ)
5 stle.2 . . . . . 6 𝐵C
6 stcl 31200 . . . . . 6 (𝑆 ∈ States → (𝐵C → (𝑆𝐵) ∈ ℝ))
75, 6mpi 20 . . . . 5 (𝑆 ∈ States → (𝑆𝐵) ∈ ℝ)
87recnd 11190 . . . 4 (𝑆 ∈ States → (𝑆𝐵) ∈ ℂ)
9 stm1add3.3 . . . . . 6 𝐶C
10 stcl 31200 . . . . . 6 (𝑆 ∈ States → (𝐶C → (𝑆𝐶) ∈ ℝ))
119, 10mpi 20 . . . . 5 (𝑆 ∈ States → (𝑆𝐶) ∈ ℝ)
1211recnd 11190 . . . 4 (𝑆 ∈ States → (𝑆𝐶) ∈ ℂ)
134, 8, 12addassd 11184 . . 3 (𝑆 ∈ States → (((𝑆𝐴) + (𝑆𝐵)) + (𝑆𝐶)) = ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))))
1413eqeq1d 2739 . 2 (𝑆 ∈ States → ((((𝑆𝐴) + (𝑆𝐵)) + (𝑆𝐶)) = 3 ↔ ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) = 3))
15 eqcom 2744 . . . 4 (((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) = 3 ↔ 3 = ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))))
167, 11readdcld 11191 . . . . . . 7 (𝑆 ∈ States → ((𝑆𝐵) + (𝑆𝐶)) ∈ ℝ)
173, 16readdcld 11191 . . . . . 6 (𝑆 ∈ States → ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) ∈ ℝ)
18 ltne 11259 . . . . . . 7 ((((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) ∈ ℝ ∧ ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < 3) → 3 ≠ ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))))
1918ex 414 . . . . . 6 (((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) ∈ ℝ → (((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < 3 → 3 ≠ ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶)))))
2017, 19syl 17 . . . . 5 (𝑆 ∈ States → (((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < 3 → 3 ≠ ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶)))))
2120necon2bd 2960 . . . 4 (𝑆 ∈ States → (3 = ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) → ¬ ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < 3))
2215, 21biimtrid 241 . . 3 (𝑆 ∈ States → (((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) = 3 → ¬ ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < 3))
23 1re 11162 . . . . . . . . . . 11 1 ∈ ℝ
2423, 23readdcli 11177 . . . . . . . . . 10 (1 + 1) ∈ ℝ
2524a1i 11 . . . . . . . . 9 (𝑆 ∈ States → (1 + 1) ∈ ℝ)
26 1red 11163 . . . . . . . . . 10 (𝑆 ∈ States → 1 ∈ ℝ)
27 stle1 31209 . . . . . . . . . . 11 (𝑆 ∈ States → (𝐵C → (𝑆𝐵) ≤ 1))
285, 27mpi 20 . . . . . . . . . 10 (𝑆 ∈ States → (𝑆𝐵) ≤ 1)
29 stle1 31209 . . . . . . . . . . 11 (𝑆 ∈ States → (𝐶C → (𝑆𝐶) ≤ 1))
309, 29mpi 20 . . . . . . . . . 10 (𝑆 ∈ States → (𝑆𝐶) ≤ 1)
317, 11, 26, 26, 28, 30le2addd 11781 . . . . . . . . 9 (𝑆 ∈ States → ((𝑆𝐵) + (𝑆𝐶)) ≤ (1 + 1))
3216, 25, 3, 31leadd2dd 11777 . . . . . . . 8 (𝑆 ∈ States → ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) ≤ ((𝑆𝐴) + (1 + 1)))
3332adantr 482 . . . . . . 7 ((𝑆 ∈ States ∧ (𝑆𝐴) < 1) → ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) ≤ ((𝑆𝐴) + (1 + 1)))
34 ltadd1 11629 . . . . . . . . . 10 (((𝑆𝐴) ∈ ℝ ∧ 1 ∈ ℝ ∧ (1 + 1) ∈ ℝ) → ((𝑆𝐴) < 1 ↔ ((𝑆𝐴) + (1 + 1)) < (1 + (1 + 1))))
3534biimpd 228 . . . . . . . . 9 (((𝑆𝐴) ∈ ℝ ∧ 1 ∈ ℝ ∧ (1 + 1) ∈ ℝ) → ((𝑆𝐴) < 1 → ((𝑆𝐴) + (1 + 1)) < (1 + (1 + 1))))
363, 26, 25, 35syl3anc 1372 . . . . . . . 8 (𝑆 ∈ States → ((𝑆𝐴) < 1 → ((𝑆𝐴) + (1 + 1)) < (1 + (1 + 1))))
3736imp 408 . . . . . . 7 ((𝑆 ∈ States ∧ (𝑆𝐴) < 1) → ((𝑆𝐴) + (1 + 1)) < (1 + (1 + 1)))
38 readdcl 11141 . . . . . . . . . 10 (((𝑆𝐴) ∈ ℝ ∧ (1 + 1) ∈ ℝ) → ((𝑆𝐴) + (1 + 1)) ∈ ℝ)
393, 24, 38sylancl 587 . . . . . . . . 9 (𝑆 ∈ States → ((𝑆𝐴) + (1 + 1)) ∈ ℝ)
4023, 24readdcli 11177 . . . . . . . . . 10 (1 + (1 + 1)) ∈ ℝ
4140a1i 11 . . . . . . . . 9 (𝑆 ∈ States → (1 + (1 + 1)) ∈ ℝ)
42 lelttr 11252 . . . . . . . . 9 ((((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) ∈ ℝ ∧ ((𝑆𝐴) + (1 + 1)) ∈ ℝ ∧ (1 + (1 + 1)) ∈ ℝ) → ((((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) ≤ ((𝑆𝐴) + (1 + 1)) ∧ ((𝑆𝐴) + (1 + 1)) < (1 + (1 + 1))) → ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < (1 + (1 + 1))))
4317, 39, 41, 42syl3anc 1372 . . . . . . . 8 (𝑆 ∈ States → ((((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) ≤ ((𝑆𝐴) + (1 + 1)) ∧ ((𝑆𝐴) + (1 + 1)) < (1 + (1 + 1))) → ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < (1 + (1 + 1))))
4443adantr 482 . . . . . . 7 ((𝑆 ∈ States ∧ (𝑆𝐴) < 1) → ((((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) ≤ ((𝑆𝐴) + (1 + 1)) ∧ ((𝑆𝐴) + (1 + 1)) < (1 + (1 + 1))) → ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < (1 + (1 + 1))))
4533, 37, 44mp2and 698 . . . . . 6 ((𝑆 ∈ States ∧ (𝑆𝐴) < 1) → ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < (1 + (1 + 1)))
46 df-3 12224 . . . . . . 7 3 = (2 + 1)
47 df-2 12223 . . . . . . . 8 2 = (1 + 1)
4847oveq1i 7372 . . . . . . 7 (2 + 1) = ((1 + 1) + 1)
49 ax-1cn 11116 . . . . . . . 8 1 ∈ ℂ
5049, 49, 49addassi 11172 . . . . . . 7 ((1 + 1) + 1) = (1 + (1 + 1))
5146, 48, 503eqtrri 2770 . . . . . 6 (1 + (1 + 1)) = 3
5245, 51breqtrdi 5151 . . . . 5 ((𝑆 ∈ States ∧ (𝑆𝐴) < 1) → ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < 3)
5352ex 414 . . . 4 (𝑆 ∈ States → ((𝑆𝐴) < 1 → ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < 3))
5453con3d 152 . . 3 (𝑆 ∈ States → (¬ ((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) < 3 → ¬ (𝑆𝐴) < 1))
55 stle1 31209 . . . . . 6 (𝑆 ∈ States → (𝐴C → (𝑆𝐴) ≤ 1))
561, 55mpi 20 . . . . 5 (𝑆 ∈ States → (𝑆𝐴) ≤ 1)
57 leloe 11248 . . . . . 6 (((𝑆𝐴) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑆𝐴) ≤ 1 ↔ ((𝑆𝐴) < 1 ∨ (𝑆𝐴) = 1)))
583, 23, 57sylancl 587 . . . . 5 (𝑆 ∈ States → ((𝑆𝐴) ≤ 1 ↔ ((𝑆𝐴) < 1 ∨ (𝑆𝐴) = 1)))
5956, 58mpbid 231 . . . 4 (𝑆 ∈ States → ((𝑆𝐴) < 1 ∨ (𝑆𝐴) = 1))
6059ord 863 . . 3 (𝑆 ∈ States → (¬ (𝑆𝐴) < 1 → (𝑆𝐴) = 1))
6122, 54, 603syld 60 . 2 (𝑆 ∈ States → (((𝑆𝐴) + ((𝑆𝐵) + (𝑆𝐶))) = 3 → (𝑆𝐴) = 1))
6214, 61sylbid 239 1 (𝑆 ∈ States → ((((𝑆𝐴) + (𝑆𝐵)) + (𝑆𝐶)) = 3 → (𝑆𝐴) = 1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3a 1088   = wceq 1542  wcel 2107  wne 2944   class class class wbr 5110  cfv 6501  (class class class)co 7362  cr 11057  1c1 11059   + caddc 11061   < clt 11196  cle 11197  2c2 12215  3c3 12216   C cch 29913  Statescst 29946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-hilex 29983
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-2 12223  df-3 12224  df-icc 13278  df-sh 30191  df-ch 30205  df-st 31195
This theorem is referenced by:  golem2  31256
  Copyright terms: Public domain W3C validator