metakunt29 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > metakunt29		Structured version Visualization version GIF version

Theorem metakunt29 41332

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)

**Hypotheses**
Ref	Expression
metakunt29.1	⊢ (𝜑 → 𝑀 ∈ ℕ)
metakunt29.2	⊢ (𝜑 → 𝐼 ∈ ℕ)
metakunt29.3	⊢ (𝜑 → 𝐼 ≤ 𝑀)
metakunt29.4	⊢ (𝜑 → 𝑋 ∈ (1...𝑀))
metakunt29.5	⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))
metakunt29.6	⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))
metakunt29.7	⊢ (𝜑 → ¬ 𝑋 = 𝐼)
metakunt29.8	⊢ (𝜑 → 𝑋 < 𝐼)
metakunt29.9	⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))
metakunt29.10	⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)

**Assertion**
Ref	Expression
metakunt29	⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))

Distinct variable groups: 𝑦,𝐻 𝑦,𝐼 𝑧,𝐼 𝑥,𝑀 𝑦,𝑀 𝑧,𝑀 𝑥,𝑋 𝑦,𝑋 𝑧,𝑋 𝜑,𝑥 𝜑,𝑦 𝜑,𝑧 Allowed substitution hints: 𝐴(𝑥,𝑦,𝑧) 𝐵(𝑥,𝑦,𝑧) 𝐶(𝑥,𝑦,𝑧) 𝐻(𝑥,𝑧) 𝐼(𝑥)

**Proof of Theorem metakunt29**
Step	Hyp	Ref	Expression
1		metakunt29.1	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
2		metakunt29.2	. . . 4 ⊢ (𝜑 → 𝐼 ∈ ℕ)
3		metakunt29.3	. . . 4 ⊢ (𝜑 → 𝐼 ≤ 𝑀)
4		metakunt29.4	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))
5		metakunt29.5	. . . 4 ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))
6		metakunt29.6	. . . 4 ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))
7		metakunt29.7	. . . 4 ⊢ (𝜑 → ¬ 𝑋 = 𝐼)
8		metakunt29.8	. . . 4 ⊢ (𝜑 → 𝑋 < 𝐼)
9	1, 2, 3, 4, 5, 6, 7, 8	metakunt27 41330	. . 3 ⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 + (𝑀 − 𝐼)))
10	9	fveq2d 6895	. 2 ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = (𝐶‘(𝑋 + (𝑀 − 𝐼))))
11		metakunt29.9	. . . 4 ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))
12	11	a1i 11	. . 3 ⊢ (𝜑 → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))))
13		elfznn 13537	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ)
14	4, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℕ)
15		nnre 12226	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℕ → 𝑋 ∈ ℝ)
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
17	1	nnred 12234	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
18	2	nnred 12234	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℝ)
19	17, 18	resubcld 11649	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℝ)
20	16, 19	readdcld 11250	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ)
21	16	recnd 11249	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℂ)
22	17	recnd 11249	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
23	18	recnd 11249	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℂ)
24	21, 22, 23	addsub12d 11601	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) = (𝑀 + (𝑋 − 𝐼)))
25	22, 23, 21	subsub2d 11607	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) = (𝑀 + (𝑋 − 𝐼)))
26	18, 16	resubcld 11649	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ)
27	16, 18	posdifd 11808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 < 𝐼 ↔ 0 < (𝐼 − 𝑋)))
28	8, 27	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (𝐼 − 𝑋))
29	26, 28	elrpd 13020	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ⁺)
30	17, 29	ltsubrpd 13055	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) < 𝑀)
31	25, 30	eqbrtrrd 5172	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 + (𝑋 − 𝐼)) < 𝑀)
32	24, 31	eqbrtrd 5170	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) < 𝑀)
33	20, 32	ltned 11357	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)
34	33	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)
35		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
36	35	neeq1d 2999	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑦 ≠ 𝑀 ↔ (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀))
37	34, 36	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 ≠ 𝑀)
38	37	neneqd 2944	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 = 𝑀)
39	38	iffalsed 4539	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))
40		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
41	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ∈ ℝ)
42	16	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑋 ∈ ℝ)
43	17	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑀 ∈ ℝ)
44	43, 41	resubcld 11649	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑀 − 𝐼) ∈ ℝ)
45	42, 44	readdcld 11250	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ)
46	41, 45	lenltd 11367	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
47	40, 46	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)
48	47	3adant2 1130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)
49		simp2 1136	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
50	49	breq1d 5158	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
51	50	notbid 318	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (¬ 𝑦 < 𝐼 ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
52	48, 51	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 < 𝐼)
53	52	iffalsed 4539	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = (𝑦 + 1))
54	49	oveq1d 7427	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 + 1) = ((𝑋 + (𝑀 − 𝐼)) + 1))
55	53, 54	eqtrd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 1))
56		simp3 1137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
57	56	iftrued 4536	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 1)
58	57	eqcomd 2737	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
59		metakunt29.10	. . . . . . . . 9 ⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)
60	58, 59	eqtr4di 2789	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = 𝐻)
61	60	oveq2d 7428	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ((𝑋 + (𝑀 − 𝐼)) + 1) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
62	55, 61	eqtrd 2771	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
63	62	3expa 1117	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
64	20, 18	ltnled 11368	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 ↔ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))))
65	64	biimprd 247	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) < 𝐼))
66	65	imp 406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)
67	66	3adant2 1130	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)
68		simp2 1136	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
69	68	breq1d 5158	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
70	67, 69	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 < 𝐼)
71	70	iftrued 4536	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = 𝑦)
72	21	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑋 ∈ ℂ)
73	22	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑀 ∈ ℂ)
74	23	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐼 ∈ ℂ)
75	73, 74	subcld 11578	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑀 − 𝐼) ∈ ℂ)
76	72, 75	addcld 11240	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) ∈ ℂ)
77	76	addridd 11421	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = (𝑋 + (𝑀 − 𝐼)))
78	77	eqcomd 2737	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 0))
79	64	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
80	79	iffalsed 4539	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 0)
81	80	eqcomd 2737	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
82	59	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
83	82	eqcomd 2737	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 𝐻)
84	81, 83	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = 𝐻)
85	84	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
86	78, 85	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
87	86	ex 412	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)))
88	65, 87	syld 47	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)))
89	88	imp 406	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
90	89	3adant2 1130	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
91	68, 90	eqtrd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
92	71, 91	eqtrd 2771	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
93	92	3expa 1117	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
94	63, 93	pm2.61dan 810	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
95	39, 94	eqtrd 2771	. . 3 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
96		1zzd 12600	. . . 4 ⊢ (𝜑 → 1 ∈ ℤ)
97	1	nnzd 12592	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98	14	nnzd 12592	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℤ)
99	2	nnzd 12592	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
100	97, 99	zsubcld 12678	. . . . 5 ⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ)
101	98, 100	zaddcld 12677	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ)
102		1p0e1 12343	. . . . 5 ⊢ (1 + 0) = 1
103		1red 11222	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
104		0red 11224	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
105	14	nnge1d 12267	. . . . . 6 ⊢ (𝜑 → 1 ≤ 𝑋)
106	17, 18	subge0d 11811	. . . . . . 7 ⊢ (𝜑 → (0 ≤ (𝑀 − 𝐼) ↔ 𝐼 ≤ 𝑀))
107	3, 106	mpbird 257	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝑀 − 𝐼))
108	103, 104, 16, 19, 105, 107	le2addd 11840	. . . . 5 ⊢ (𝜑 → (1 + 0) ≤ (𝑋 + (𝑀 − 𝐼)))
109	102, 108	eqbrtrrid 5184	. . . 4 ⊢ (𝜑 → 1 ≤ (𝑋 + (𝑀 − 𝐼)))
110	20, 17, 32	ltled 11369	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≤ 𝑀)
111	96, 97, 101, 109, 110	elfzd 13499	. . 3 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ (1...𝑀))
112	111	elfzelzd 13509	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ)
113		0zd 12577	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
114	96, 113	ifcld 4574	. . . . 5 ⊢ (𝜑 → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ)
115	59	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
116	115	eleq1d 2817	. . . . 5 ⊢ (𝜑 → (𝐻 ∈ ℤ ↔ if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ))
117	114, 116	mpbird 257	. . . 4 ⊢ (𝜑 → 𝐻 ∈ ℤ)
118	112, 117	zaddcld 12677	. . 3 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) + 𝐻) ∈ ℤ)
119	12, 95, 111, 118	fvmptd 7005	. 2 ⊢ (𝜑 → (𝐶‘(𝑋 + (𝑀 − 𝐼))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
120	10, 119	eqtrd 2771	1 ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ≠ wne 2939 ifcif 4528 class class class wbr 5148 ↦ cmpt 5231 ‘cfv 6543 (class class class)co 7412 ℂcc 11114 ℝcr 11115 0cc0 11116 1c1 11117 + caddc 11119 < clt 11255 ≤ cle 11256 − cmin 11451 ℕcn 12219 ℤcz 12565 ...cfz 13491

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-cnex 11172 ax-resscn 11173 ax-1cn 11174 ax-icn 11175 ax-addcl 11176 ax-addrcl 11177 ax-mulcl 11178 ax-mulrcl 11179 ax-mulcom 11180 ax-addass 11181 ax-mulass 11182 ax-distr 11183 ax-i2m1 11184 ax-1ne0 11185 ax-1rid 11186 ax-rnegex 11187 ax-rrecex 11188 ax-cnre 11189 ax-pre-lttri 11190 ax-pre-lttrn 11191 ax-pre-ltadd 11192 ax-pre-mulgt0 11193

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7860 df-1st 7979 df-2nd 7980 df-frecs 8272 df-wrecs 8303 df-recs 8377 df-rdg 8416 df-er 8709 df-en 8946 df-dom 8947 df-sdom 8948 df-pnf 11257 df-mnf 11258 df-xr 11259 df-ltxr 11260 df-le 11261 df-sub 11453 df-neg 11454 df-nn 12220 df-n0 12480 df-z 12566 df-uz 12830 df-rp 12982 df-fz 13492

This theorem is referenced by: metakunt31 41334

W3C validator